Library ICContinuity

Continuity of the WP semantics for IC

This is a consequence of determinism. Continuity enables a different characterization of the WP predicate in terms of omega-iteration.
Require Import Facts States ICSemantics.
Set Implicit Arguments.
Unset Strict Implicit.

Module ICContinuity (Sigma : State).
Module ICSem := ICSemantics.ICSemantics Sigma.
Import Sigma.
Export ICSem.

Lemma wp_continuous (D : natNPred state) s :
  wp (sup \o D) s <<= sup (fun mwp (D^~ m) s).
Proof.
  movex /wp_det[f[y[sx/=[m dm]]]]. m. apply: wp_mono x sx.
    by moveg x [<-<-].
Qed.

Lemma wp_cons_continuous (D Q : NPred state) s :
  wp (sup D .: Q) s <<= sup (fun mwp (D m .: Q) s).
Proof.
  movex sx. apply: wp_continuous. by apply: wp_mono x sx ⇒ -[].
Qed.

Definition fix_step n Q s :=
  iter n (fun Pwp (P .: Q) s) bot.

Lemma wp_fix_kleene Q s x :
  Fix (fun Pwp (P .: Q) s) x sup (fun nfix_step n Q s) x.
Proof.
  apply: fix_fixk. moveD _. exact: wp_cons_continuous. exact: wp_cons_mono.
Qed.

Corollary wp_defn Q s t x :
  wp Q (Def s t) x wp (sup (fun ifix_step i Q s) .: Q) t x.
Proof.
  split=>/=; apply: wp_mono x ⇒ -[]//= x; by rewrite wp_fix_kleene.
Qed.

End ICContinuity.