IC Program Preorder

We show that the preorder given by specification preservation is always precongruence. If there are enough guards in the language it coincides with contextual approximation. Together with the continuity result we obtain additional proof rules for showing specification preservation.
Require Import Facts States ICContinuity.
Set Implicit Arguments.
Unset Strict Implicit.

Module ICEquivalence (Sigma : State) (SigmaEq : EqState Sigma).
Module ICCont := ICContinuity.ICContinuity Sigma.
Export SigmaEq.
Export ICCont.

Implicit Types (Q : NPred state) (a : action) (b : guard) (s t u : term).

Preservation of specifications / Refinement

Definition refines s t := Q, wp Q s <<= wp Q t.
Local Notation "s <~ t" := (refines s t) (at level 55).

Lemma refines_refl s : s <~ s. firstorder. Qed.
Lemma refines_trans s t u : s <~ tt <~ us <~ u. firstorder. Qed.

Lemma refines_act a s t : s <~ tAct a s <~ Act a t.
Proof. moveh Q x /=. exact: h. Qed.

Lemma refines_if b s1 s2 t1 t2 :
s1 <~ s2t1 <~ t2If b s1 t1 <~ If b s2 t2.
Proof.
moveh1 h2 Q x /=. case: ifP_; by [exact: h1|exact: h2].
Qed.

Lemma refines_def s1 s2 t1 t2 :
s1 <~ s2t1 <~ t2Def s1 t1 <~ Def s2 t2.
Proof.
moveh1 h2 Q x /=/h2. apply: wp_cons_mono x.
apply: wp_fixx /h1. exact: fix_fold.
Qed.

Contextual approximation

Inductive ctx :=
| ctx_hole
| ctx_act (a : action) (c : ctx)
| ctx_if1 (b : guard) (c : ctx) (t : term)
| ctx_if2 (b : guard) (s : term) (c : ctx)
| ctx_def1 (c : ctx) (s : term)
| ctx_def2 (s : term) (c : ctx).

Fixpoint fill (c : ctx) (s : term) : term :=
match c with
| ctx_holes
| ctx_act a cAct a (fill c s)
| ctx_if1 b c tIf b (fill c s) t
| ctx_if2 b t cIf b t (fill c s)
| ctx_def1 c tDef (fill c s) t
| ctx_def2 t cDef t (fill c s)
end.

Fixpoint appc (c : ctx) : ctx :=
match c with
| ctx_hole
| ctx_act a cctx_act a (appc c )
| ctx_if1 b c tctx_if1 b (appc c ) t
| ctx_if2 b t cctx_if2 b t (appc c )
| ctx_def1 c tctx_def1 (appc c ) t
| ctx_def2 t cctx_def2 t (appc c )
end.

Definition approximates s t :=
c, terminates (fill c s) <<= terminates (fill c t).

Contextual approximation is the coarsest consistent precongruence.

Implicit Types (R : termtermProp).

Definition consistent R := s t, R s tterminates s <<= terminates t.
Definition compatible R := c s t, R s tR (fill c s) (fill c t).
Definition approximation R := consistent R compatible R.

Lemma fill_fill c s : fill c (fill s) = fill (appc c ) s.
Proof. elim: c ⇒ //=[a c->|b c->|b t c->|c->|t c->]//. Qed.

Lemma approximates_consistent : consistent approximates.
Proof. by moves t /(_ ctx_hole). Qed.

Lemma approximates_compatible : compatible approximates.
Proof. movec s t cap . rewrite !fill_fill. exact: cap. Qed.

Lemma approximatesI R s t : approximation RR s tapproximates s t.
Proof. move⇒ [h1 h2] rst c. exact/h1/h2. Qed.

Refinement -> Approximation

Lemma refines_consistent : consistent refines.
Proof. moves t rst x. rewrite -!wp_terminates. exact: rst. Qed.

Lemma refines_compatible : compatible refines.
Proof.
elim⇒ /=; eauto using refines_refl, refines_act, refines_if, refines_def.
Qed.

Lemma refines_approximates s t : s <~ tapproximates s t.
Proof.
apply: approximatesI. split; by
[exact: refines_consistent|exact: refines_compatible].
Qed.

Approximation -> Refinement

Lemma wp_safe Q s t :
approximates s twp Q s <<= terminates t.
Proof.
movecap x sx. apply: approximates_consistent cap _ _.
rewrite -wp_terminates. exact: wp_mono x sx.
Qed.

Building distinguishing contexts

Definition Omega := Def (Jump 0) (Jump 0).

Definition ctx_let (s : term) (c : ctx) : ctx :=
ctx_def2 s.[ren (+1)] c.

Fixpoint skip_ctx (f : nat) (c : ctx) : ctx :=
match f with
| 0 ⇒ c
| g.+1skip_ctx g (ctx_let (Jump f) c)
end.

Definition point_ctx (f : nat) (s : term) : ctx :=
ctx_let s (skip_ctx f ctx_hole).

Definition test_ctx (f : nat) (sigma : state) : ctx :=
point_ctx f (If (to_test sigma) Omega (Jump 0)).

Definition pushn n P Q : NPred state := iter n (scons P) Q.

Properties of contexts

Lemma skip_ctxP f c s :
fill (skip_ctx f c) s = fill (skip_ctx f ctx_hole) (fill c s).
Proof.
elim: f c s ⇒ //=n ih c s. by rewrite ih (ih (ctx_def2 _ _)).
Qed.

Lemma let_ctxP Q s t c x :
wp Q (fill (ctx_let s c) t) x wp (wp Q s .: Q) (fill c t) x.
Proof.
split=>/=; apply: wp_cons_mono xx.
- movefx. apply fix_unfold in fx. by rewrite wp_ren in fx.
exact: wp_cons_mono.
- movesx. apply: fix_fold. by rewrite wp_ren.
Qed.

Lemma skip_wp Q f c s x :
wp Q (fill (skip_ctx f c) s) x wp (pushn f (Q 1) Q) (fill c s) x.
Proof.
elim: f Q x c s ⇒ //= n ih Q x c s.
rewrite skip_ctxP ih let_ctxP. apply: wp_equiv ⇒ -[]//=y.
by elim: n {ih}.
Qed.

Lemma point_wp Q f s t x :
wp Q (fill (point_ctx f s) t) x wp (pushn f (Q 0) (wp Q s .: Q)) t x.
Proof. by rewrite let_ctxP skip_wp. Qed.

Lemma point_terminatesI f g s t x y :
wp (point_pred g y) t x → (f = gterminates s y) →
terminates (fill (point_ctx f s) t) x.
Proof.
rewrite -!wp_terminates point_wpw1 w2. apply: wp_mono x w1.
move tau´ [<-<-] { tau´}.
elim: f g w2 ⇒ [|f ih] [|g h]//=. exact.
apply: ihe. apply: h. by rewrite e.
Qed.

Lemma point_terminatesD f s t x y :
terminates (fill (point_ctx f s) t) xwp (point_pred f y) t x
terminates s y.
Proof.
rewrite-wp_terminates point_wp-/Top-/top -wp_step_equivw1 w2.
move: w1. rewrite (mstep_admissible _ w2). elim: f {w2} ⇒ //=.
by rewrite wp_terminates.
Qed.

Contextual approximation -> small-step equivalence

Lemma approximates_ss s t f x y :
approximates s tmstep (s,x) (Jump f,y)mstep (t,x) (Jump f,y).
Proof.
movecap. rewrite !wp_step_equivsx.
have[[/wp_step_equiv tx]]: terminates t x by exact: wp_safe sx.
suff: f == == y by case=>/eqP->/eqP<-.
have cn: ¬terminates (fill (test_ctx ) s) x.
move/cap/point_terminatesD ⇒ /(_ _ tx).
rewrite -wp_terminates/=to_testT. elim; by eauto.
apply/andP/negbNE/negP =>/nandP h; apply: cn.
apply: point_terminatesI sx _e. subst . case: h ⇒ [/eqP//|h].
by rewrite -wp_terminates/=ifN.
Qed.

Theorem approximates_refines s t :
approximates s ts <~ t.
Proof.
movecap Q x /correspondence[f [y[h1 h2]]].
apply/correspondence. f, y. split=>//.
exact: approximates_ss h1.
Qed.

Least upper bound property

Fixpoint fix_n (n : nat) (s : term) : term :=
match n with
| 0 ⇒ Def (Jump 0) (Jump 0)
| n.+1s.[fix_n n s/]
end.

Lemma fix_nP (n : nat) Q s x :
wp Q (fix_n n s) x fix_step n Q s x.
Proof.
elim: n Q s x ⇒ [|n ih] Q s x /=.
- split⇒ //=. by elim;eauto.
- by rewrite wp_subst; split; apply: wp_mono x ⇒ -[|f]//=x;
rewrite ih.
Qed.

Lemma fix_n_fix (n : nat) s t :
t.[fix_n n s/] <~ Def s t.
Proof.
moveQ x. rewrite/=wp_subst. apply: wp_mono ⇒ -[]//=.
elim: n ⇒ {x}[|n ih] x /=. by elim;eauto.
rewrite wp_subst. movesx. apply: fix_fold. by apply: wp_mono x sx ⇒ -[].
Qed.

Theorem least_upper_bound s t u :
( n, t.[fix_n n s/] <~ u) (Def s t <~ u).
Proof.
split.
- moveh Q x. rewrite wp_defn ⇒ /wp_cons_continuous[n tx].
apply: (h n). rewrite wp_subst. apply: wp_mono x tx ⇒ -[]//=x.
by rewrite -fix_nP.
- moveh n. apply: refines_trans h. exact: fix_n_fix.
Qed.

End ICEquivalence.