Require Import Facts States.
Require Import GCSemantics.
Set Implicit Arguments.
Unset Strict Implicit.

Module GCContinuity (Sigma : State).
Module GCSem := GCSemantics.GCSemantics Sigma.
Export GCSem.

Implicit Types (G : gc) (P Q:Pred state) (x:state) (n:nat).

Lemma gc_continuous´ :
  (∀ s, continuous (wpg^~ s)) ∧
  (∀ G, continuous (fun Q x ⇒ G x → wpG Q G x)).
Proof with eauto using wpg_mono, wpG_mono.
  apply: gc_ind ⇒ //=[a|s t ihs iht|G ih|G ih||b s G ihs ihG] //=.
  - move⇒ M cM x /= h. apply: ihs ⇒ [n|]. exact/wpg_mono/cM.
    apply: wpg_mono x h. exact: iht.
  - move⇒ M cM x /=[h1 h2]. case: (ih M cM x). by rewrite h1.
    move⇒ n /=. rewrite h1 ⇒ h. ∃ n=>/=...
  - apply: fix_continuous.
    + move⇒ P1 P2 Q1 Q2 l1 l2 x. case: ifP... move⇒ _. exact: wpG_mono.
    + move⇒ P M cM x. rewrite/sup/=. case: ifP; last by ∃ 0.
      move⇒ h1 h2. case: (ih M cM x) ⇒ [_|]. apply: wpG_mono h2...
      move⇒ n /=. rewrite h1...
    + move⇒ Q M cM x. rewrite/sup/=. case: ifP ⇒ // gt h. by ∃ 0.
  - move⇒ M cM x _; by ∃ 0.
  - move⇒ M cM x. rewrite/sup//=.
    rewrite gtest_cons. case: (b x); case e2:(G x) ⇒ //=; last (by ∃ 0);
    case/(_ _)/Wrap=>//-[]; (move/(_ erefl) || move⇒_).
    + move⇒ w1 w2.
      case: (ihs M cM x w1) ⇒ /= m {w1} w1.
      case: (ihG M cM x) ⇒ [] //={w2}n. rewrite e2 ⇒ /(_ erefl) w2.
      ∃ (maxn m n) ⇒ _. split⇒ [_|]. apply: wpg_mono w1.
      exact: chain_maxl. apply: wpG_mono w2. exact: chain_maxr.
    + case/ihs=>// m /= ih _. ∃ m ⇒ _. split⇒ //.
      apply: wps_wpG ⇒ b´ s´ /gtest_contra cn bx. exfalso. apply/negP: bx.
      apply: cn. by rewrite e2.
    + move⇒ w. case: (ihG M cM x) ⇒ //=m{w}w. ∃ m ⇒ _. split=>//.
      exact: w.
Qed.

Theorem gc_continuous s : continuous (wpg^~ s).
Proof. by case: gc_continuous´. Qed.

Fixpoint dijkstra_wpg Q s : Pred state :=
  match s with
  | Skip ⇒ Q
  | Assn a ⇒ Q \o a
  | Seq s t ⇒ dijkstra_wpg (dijkstra_wpg Q t) s
  | Case G ⇒ fun x ⇒ gtest G x ∧ wpG´ dijkstra_wpg Q G x
  | Do G ⇒
    let F P x :=
        ((G:gc) x ∧ wpG´ dijkstra_wpg P G x) ∨ (~~(G:gc) x ∧ Q x)
    in fixk F
  end.

Lemma wpG_continuous G (Q : NPred state) x :
  G x → chain Q → wpG (sup Q) G x → ∃ m, wpG (Q m) G x.
Proof.
  case: gc_continuous´ ⇒ _ cont gx cQ qx. case: (cont G Q cQ x) ⇒ //=y. eauto.
Qed.

Theorem dijkstra_equiv :
  (∀ s Q x, wpg Q s x ↔ dijkstra_wpg Q s x) ∧
  (∀ G Q x, wpG Q G x ↔ wpG´ dijkstra_wpg Q G x).
Proof.
  apply: gc_ind ⇒ //= [s t ih1 ih2|G ih|G ih|b s G ih1 ih2] Q x.
  - rewrite -ih1. split; apply: wpg_mono x ⇒ x; by rewrite ih2.
  - by rewrite ih.
  - rewrite <- fix_fixk.
    + apply: fix_ext x ⇒ P x. rewrite -ih. case: ifP; by intuition.
    + move⇒ {x} M cM x/=. rewrite -ih ⇒ -[[gx mx]|[gx qx]].
      case: (wpG_continuous gx cM mx) ⇒ m w. ∃ m ⇒ //=.
      rewrite gx -ih; by eauto. by ∃ 0 ⇒ /=; tauto.
    + move⇒ P1 P2 /wpG_mono le {x} x /=. rewrite -!ih. by intuition.
  - by rewrite ih1 ih2.
Qed.

End GCContinuity.