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

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 <~ t → t <~ u → s <~ u.

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

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

Lemma refines_def s1 s2 t1 t2 :
  s1 <~ s2 → t1 <~ t2 → Def s1 t1 <~ Def s2 t2.

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_hole ⇒ s
  | ctx_act a c ⇒ Act a (fill c s)
  | ctx_if1 b c t ⇒ If b (fill c s) t
  | ctx_if2 b t c ⇒ If b t (fill c s)
  | ctx_def1 c t ⇒ Def (fill c s) t
  | ctx_def2 t c ⇒ Def t (fill c s)
  end.

Fixpoint appc (c c´ : ctx) : ctx :=
  match c with
  | ctx_hole ⇒ c´
  | ctx_act a c ⇒ ctx_act a (appc c c´)
  | ctx_if1 b c t ⇒ ctx_if1 b (appc c c´) t
  | ctx_if2 b t c ⇒ ctx_if2 b t (appc c c´)
  | ctx_def1 c t ⇒ ctx_def1 (appc c c´) t
  | ctx_def2 t c ⇒ ctx_def2 t (appc c c´)
  end.

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

Implicit Types (R : term → term → Prop).

Definition consistent R := ∀ s t, R s t → terminates s <<= terminates t.
Definition compatible R := ∀ c s t, R s t → R (fill c s) (fill c t).
Definition approximation R := consistent R ∧ compatible R.

Lemma fill_fill c c´ s : fill c (fill c´ s) = fill (appc c c´) s.

Lemma approximates_consistent : consistent approximates.

Lemma approximates_compatible : compatible approximates.

Lemma approximatesI R s t : approximation R → R s t → approximates s t.

Lemma refines_consistent : consistent refines.

Lemma refines_compatible : compatible refines.

Lemma refines_approximates s t : s <~ t → approximates s t.

Lemma wp_safe Q s t :
  approximates s t → wp Q s <<= terminates t.

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.+1 ⇒ skip_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.

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 = g → terminates 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) x → wp (point_pred f y) t x →
  terminates s y.

Lemma approximates_ss s t f x y :
  approximates s t → mstep (s,x) (Jump f,y) → mstep (t,x) (Jump f,y).

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

Fixpoint fix_n (n : nat) (s : term) : term :=
  match n with
  | 0 ⇒ Def (Jump 0) (Jump 0)
  | n.+1 ⇒ s.[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.

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.