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

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

Theorem gc_continuous s : continuous (wpg^~ s).

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.

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

End GCContinuity.