Library ICEquivalence

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.

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.
Lemma refines_trans s t u : s <~ tt <~ us <~ u.

Lemma refines_act a s t : s <~ tAct a s <~ Act a t.

Lemma refines_if b s1 s2 t1 t2 :
  s1 <~ s2t1 <~ t2If b s1 t1 <~ If b s2 t2.

Lemma refines_def s1 s2 t1 t2 :
  s1 <~ s2t1 <~ t2Def s1 t1 <~ Def s2 t2.

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)

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 )

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.

Lemma approximates_consistent : consistent approximates.

Lemma approximates_compatible : compatible approximates.

Lemma approximatesI R s t : approximation RR s tapproximates s t.

Refinement -> Approximation

Approximation -> Refinement

Lemma wp_safe Q s t :
  approximates s twp Q s <<= terminates t.

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)

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).

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.

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.

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.

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.

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.

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).

Theorem approximates_refines s t :
  approximates s ts <~ t.

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/]

Lemma fix_nP (n : nat) Q s x :
  wp Q (fix_n n s) x fix_step n Q s x.

Lemma fix_n_fix (n : nat) s t :
  t.[fix_n n s/] <~ Def s t.

Theorem least_upper_bound s t u :
  ( n, t.[fix_n n s/] <~ u) (Def s t <~ u).

End ICEquivalence.