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

Module GCSemantics (Sigma : State).
Module GCSyn := GCSyntax.GCSyntax Sigma.
Export GCSyn.

Implicit Types (P Q : Pred state) (x y z : state).
Implicit Types (a : action) (b : guard) (G : gc) (s t : cmd).

Definition gtest G : state → bool :=
  fun x ⇒ has (fun p : guard ⇒ p x) (unzip1 G).
Coercion gtest : gc >-> Funclass.

Inductive wps Q : cmd → Pred state :=
| wps_skip x :
    Q x →
    wps Q Skip x
| wps_assn a x :
    Q (a x) →
    wps Q (Assn a) x
| wps_seq s t x P :
    wps P s x →
    P <<= wps Q t →
    wps Q (Seq s t) x
| wps_case G x :
    G x →
    (∀ b s, (b,s) \in G → b x → wps Q s x) →
    wps Q (Case G) x
| wps_loop_true G x P :
    G x →
    (∀ b s, (b,s) \in G → b x → wps P s x) →
    P <<= wps Q (Do G) →
    wps Q (Do G) x
| wps_loop_false G x :
    ~~G x →
    Q x →
    wps Q (Do G) x.

Definition wpG´ (wp : Pred state → cmd → Pred state) Q : gc → Pred state :=
  fix rec G x := match G with
  | (b,s) :: G ⇒ (b x → wp Q s x) ∧ rec G x
  | [::] ⇒ True
  end.

Fixpoint wpg Q s : Pred state :=
  match s with
  | Skip ⇒ Q
  | Assn a ⇒ Q \o a
  | Seq s t ⇒ wpg (wpg Q t) s
  | Case G ⇒ fun x ⇒ gtest G x ∧ wpG´ wpg Q G x
  | Do G ⇒ Fix (fun P x ⇒ if gtest G x then wpG´ wpg P G x else Q x)
  end.

Notation wpG := (wpG´ wpg).

Lemma gtest_cons (G : gc) b s x :
  gtest ((b,s) :: G) x = b x || G x.
Proof. by []. Qed.

Lemma gtestP (G : gc) x :
  reflect (∃ (b:guard) (s:cmd), (b,s) \in G ∧ b x) (G x).
Proof.
  apply: (iffP hasP) ⇒ [[b/mapP[[b´ s]/=mem→bx]]|[b[s[mem bx]]]].
  by ∃ b´, s. ∃ b ⇒ //. apply/mapP. by ∃ (b,s).
Qed.

Lemma gtest_contra (G : gc) b s x :
  (b,s) \in G → ~~G x → ~~b x.
Proof.
  move⇒ mem. apply/contra ⇒ bx. apply/gtestP. by ∃ b, s.
Qed.

Lemma wpgG_mono :
  (∀ s, monotone (wpg^~ s)) ∧ (∀ G, monotone (wpG^~ G)).
Proof.
  apply: gc_ind ⇒ /=;
    try (move⇒ G ih P Q le; apply: fix_mono ⇒ I x; case: ifP); firstorder.
Qed.

Lemma wpg_mono s : monotone (wpg^~ s). by case: wpgG_mono. Qed.
Lemma wpG_mono G : monotone (wpG^~ G). by case: wpgG_mono. Qed.

Lemma wpgG_wps :
  (∀ s Q, wpg Q s <<= wps Q s) ∧
  (∀ G Q x,
      wpG Q G x → ∀ b s, (b,s) \in G → b x → wps Q s x).
Proof with eauto using wps.
  apply: gc_ind...
  - move⇒ G ih Q x /=[h1 h2]...
  - move⇒ G ih Q x /=. elim⇒ {x}x P h1 h2.
    case: ifPn ⇒ i gx. apply (wps_loop_true (P := P))...
    exact: wps_loop_false.
  - move⇒ Q b s x. by rewrite/wpG.
  - move⇒ b s G ihs ihG Q x/= [h1 h2] b´ t´.
    rewrite inE ⇒ /orP[/eqP[->->]|]...
Qed.

Lemma wpg_wps Q s : wpg Q s <<= wps Q s.
Proof. case: wpgG_wps; eauto. Qed.

Lemma wps_wpG Q (G:gc) x :
  (∀ b s, (b,s) \in G → b x → wpg Q s x) →
  wpG Q G x.
Proof.
  elim: G ⇒ //=-[b s]G ih h. split. apply: h. exact: mem_head.
  apply: ih ⇒ b´ t mem. apply: h. by rewrite inE mem orbT.
Qed.

Lemma wps_wpg Q (s : cmd) : wps Q s <<= wpg Q s.
Proof with eauto using wpg_mono, wpG_mono, wps_wpG.
  move⇒ x. elim⇒ {Q s x}/=...
  - move⇒ Q s t x P _ ih1 _ ih2. exact: wpg_mono ih1.
  - move⇒ Q G x P gt _ /wps_wpG ih1 _ ih2. apply: fix_fold.
    rewrite gt. exact: wpG_mono ih1.
  - move⇒ Q G x gt q. apply: fix_fold. by rewrite ifN.
Qed.

End GCSemantics.