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

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

Lemma refines_act a s t : s <~ t → Act a s <~ Act a t.
Proof. move⇒ h Q x /=. exact: h. Qed.

Lemma refines_if b s1 s2 t1 t2 :
  s1 <~ s2 → t1 <~ t2 → If b s1 t1 <~ If b s2 t2.
Proof.
  move⇒ h1 h2 Q x /=. case: ifP ⇒ _; by [exact: h1|exact: h2].
Qed.

Lemma refines_def s1 s2 t1 t2 :
  s1 <~ s2 → t1 <~ t2 → Def s1 t1 <~ Def s2 t2.
Proof.
  move⇒ h1 h2 Q x /=/h2. apply: wp_cons_mono x.
  apply: wp_fix ⇒ x /h1. exact: fix_fold.
Qed.

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.
Proof. elim: c ⇒ //=[a c->|b c->|b t c->|c->|t c->]//. Qed.

Lemma approximates_consistent : consistent approximates.
Proof. by move⇒ s t /(_ ctx_hole). Qed.

Lemma approximates_compatible : compatible approximates.
Proof. move⇒ c s t cap c´. rewrite !fill_fill. exact: cap. Qed.

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

Lemma refines_consistent : consistent refines.
Proof. move⇒ s 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 <~ t → approximates s t.
Proof.
  apply: approximatesI. split; by
    [exact: refines_consistent|exact: refines_compatible].
Qed.

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

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).
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 x ⇒ x.
  - move⇒ fx. apply fix_unfold in fx. by rewrite wp_ren in fx.
    exact: wp_cons_mono.
  - move⇒ sx. 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 = g → terminates s y) →
  terminates (fill (point_ctx f s) t) x.
Proof.
  rewrite -!wp_terminates point_wp ⇒ w1 w2. apply: wp_mono x w1.
  move⇒ f´ tau´ [<-<-] {f´ tau´}.
  elim: f g w2 ⇒ [|f ih] [|g h]//=. exact.
  apply: ih ⇒ e. apply: h. by rewrite e.
Qed.

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.
Proof.
  rewrite-wp_terminates point_wp-/Top-/top -wp_step_equiv ⇒ w1 w2.
  move: w1. rewrite (mstep_admissible _ w2). elim: f {w2} ⇒ //=.
  by rewrite wp_terminates.
Qed.

Lemma approximates_ss s t f x y :
  approximates s t → mstep (s,x) (Jump f,y) → mstep (t,x) (Jump f,y).
Proof.
  move⇒ cap. rewrite !wp_step_equiv ⇒ sx.
  have[f´[y´/wp_step_equiv tx]]: terminates t x by exact: wp_safe sx.
  suff: f == f´ ∧ y´ == y by case=>/eqP->/eqP<-.
  have cn: ¬terminates (fill (test_ctx f´ y´) 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 f´. case: h ⇒ [/eqP//|h].
  by rewrite -wp_terminates/=ifN.
Qed.

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

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.
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.
  move⇒ Q x. rewrite/=wp_subst. apply: wp_mono ⇒ -[]//=.
  elim: n ⇒ {x}[|n ih] x /=. by elim;eauto.
  rewrite wp_subst. move⇒ sx. 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.
  - move⇒ h 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.
  - move⇒ h n. apply: refines_trans h. exact: fix_n_fix.
Qed.

End ICEquivalence.