Library GCContinuity

Continuity of the wp predicate for GC

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 xG xwpG 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] //=.
  - moveM cM x /= h. apply: ihs ⇒ [n|]. exact/wpg_mono/cM.
    apply: wpg_mono x h. exact: iht.
  - moveM cM x /=[h1 h2]. case: (ih M cM x). by rewrite h1.
    moven /=. rewrite h1h. n=>/=...
  - apply: fix_continuous.
    + moveP1 P2 Q1 Q2 l1 l2 x. case: ifP... move_. exact: wpG_mono.
    + moveP M cM x. rewrite/sup/=. case: ifP; last by 0.
      moveh1 h2. case: (ih M cM x) ⇒ [_|]. apply: wpG_mono h2...
      moven /=. rewrite h1...
    + moveQ M cM x. rewrite/sup/=. case: ifP ⇒ // gt h. by 0.
  - moveM cM x _; by 0.
  - moveM cM x. rewrite/sup//=.
    rewrite gtest_cons. case: (b x); case e2:(G x) ⇒ //=; last (by 0);
    case/(_ _)/Wrap=>//-[]; (move/(_ erefl) || move_).
    + movew1 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 /gtest_contra cn bx. exfalso. apply/negP: bx.
      apply: cn. by rewrite e2.
    + movew. case: (ihG M cM x) ⇒ //=m{w}w. m_. split=>//.
      exact: w.

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

Equivalence to Dijkstra's definition of WP

Fixpoint dijkstra_wpg Q s : Pred state :=
  match s with
  | SkipQ
  | Assn aQ \o a
  | Seq s tdijkstra_wpg (dijkstra_wpg Q t) s
  | Case Gfun xgtest 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

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

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).
  apply: gc_ind ⇒ //= [s t ih1 ih2|G ih|G ih|b s G ih1 ih2] Q x.
  - rewrite -ih1. split; apply: wpg_mono xx; by rewrite ih2.
  - by rewrite ih.
  - rewrite <- fix_fixk.
    + apply: fix_ext xP 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.
    + moveP1 P2 /wpG_mono le {x} x /=. rewrite -!ih. by intuition.
  - by rewrite ih1 ih2.

End GCContinuity.