From 3803dc19caacfbd139a2aee19189a054b1ec1f5b Mon Sep 17 00:00:00 2001
From: David Swasey <swasey@mpi-sws.org>
Date: Sun, 18 Dec 2016 19:04:13 +0100
Subject: [PATCH] Incorporate minor feedback from Ralf.

Pull progress bit out of the WP fixpoint,
make (most) wp adequacy notation only parsing, and
generalize forget_progress.
---
 theories/program_logic/adequacy.v   |  8 ++++----
 theories/program_logic/hoare.v      |  4 ++--
 theories/program_logic/weakestpre.v | 25 +++++++++++++------------
 3 files changed, 19 insertions(+), 18 deletions(-)

diff --git a/theories/program_logic/adequacy.v b/theories/program_logic/adequacy.v
index f1ca93587..f1e00507f 100644
--- a/theories/program_logic/adequacy.v
+++ b/theories/program_logic/adequacy.v
@@ -65,11 +65,11 @@ Implicit Types P Q : iProp Σ.
 Implicit Types Φ : val Λ → iProp Σ.
 Implicit Types Φs : list (val Λ → iProp Σ).
 
-Notation world' E σ := (wsat ∗ ownE E ∗ state_interp σ)%I.
-Notation world σ := (world' ⊤ σ).
+Notation world' E σ := (wsat ∗ ownE E ∗ state_interp σ)%I (only parsing).
+Notation world σ := (world' ⊤ σ) (only parsing).
 
-Notation wp' E e Φ := (WP e @ p; E {{ Φ }})%I.
-Notation wp e Φ := (wp' ⊤ e Φ).
+Notation wp' E e Φ := (WP e @ p; E {{ Φ }})%I (only parsing).
+Notation wp e Φ := (wp' ⊤ e Φ) (only parsing).
 Notation wptp t := ([∗ list] ef ∈ t, WP ef @ p; ⊤ {{ _, True }})%I.
 
 Lemma wp_step E e1 σ1 e2 σ2 efs Φ :
diff --git a/theories/program_logic/hoare.v b/theories/program_logic/hoare.v
index 953c05f6f..a94c60934 100644
--- a/theories/program_logic/hoare.v
+++ b/theories/program_logic/hoare.v
@@ -108,8 +108,8 @@ Proof.
   iIntros (v) "Hv". by iApply "HwpK".
 Qed.
 
-Lemma ht_forget_progress E P Φ e :
-  {{ P }} e @ E {{ Φ }} ⊢ {{ P }} e @ E ?{{ Φ }}.
+Lemma ht_forget_progress p E P Φ e :
+  {{ P }} e @ p; E {{ Φ }} ⊢ {{ P }} e @ E ?{{ Φ }}.
 Proof.
   by iIntros "#Hwp !# ?"; iApply wp_forget_progress; iApply "Hwp".
 Qed.
diff --git a/theories/program_logic/weakestpre.v b/theories/program_logic/weakestpre.v
index 12c77165c..d428af54d 100644
--- a/theories/program_logic/weakestpre.v
+++ b/theories/program_logic/weakestpre.v
@@ -11,26 +11,26 @@ Class irisG' (Λstate : Type) (Σ : gFunctors) := IrisG {
 }.
 Notation irisG Λ Σ := (irisG' (state Λ) Σ).
 
-Definition wp_pre `{irisG Λ Σ}
-    (wp : bool -c> coPset -c> expr Λ -c> (val Λ -c> iProp Σ) -c> iProp Σ) :
-    bool -c> coPset -c> expr Λ -c> (val Λ -c> iProp Σ) -c> iProp Σ := λ p E e1 Φ,
+Definition wp_pre `{irisG Λ Σ} (p : bool)
+    (wp : coPset -c> expr Λ -c> (val Λ -c> iProp Σ) -c> iProp Σ) :
+    coPset -c> expr Λ -c> (val Λ -c> iProp Σ) -c> iProp Σ := λ E e1 Φ,
   match to_val e1 with
   | Some v => |={E}=> Φ v
   | None => ∀ σ1,
      state_interp σ1 ={E,∅}=∗ ⌜if p then reducible e1 σ1 else True⌝ ∗
      ▷ ∀ e2 σ2 efs, ⌜prim_step e1 σ1 e2 σ2 efs⌝ ={∅,E}=∗
-       state_interp σ2 ∗ wp p E e2 Φ ∗
-       [∗ list] ef ∈ efs, wp p ⊤ ef (λ _, True)
+       state_interp σ2 ∗ wp E e2 Φ ∗
+       [∗ list] ef ∈ efs, wp ⊤ ef (λ _, True)
   end%I.
 
-Local Instance wp_pre_contractive `{irisG Λ Σ} : Contractive wp_pre.
+Local Instance wp_pre_contractive `{irisG Λ Σ} p : Contractive (wp_pre p).
 Proof.
-  rewrite /wp_pre=> n wp wp' Hwp p E e1 Φ.
+  rewrite /wp_pre=> n wp wp' Hwp E e1 Φ.
   repeat (f_contractive || f_equiv); apply Hwp.
 Qed.
 
-Definition wp_def `{irisG Λ Σ} :
-  bool → coPset → expr Λ → (val Λ → iProp Σ) → iProp Σ := fixpoint wp_pre.
+Definition wp_def `{irisG Λ Σ} p :
+  coPset → expr Λ → (val Λ → iProp Σ) → iProp Σ := fixpoint (wp_pre p).
 Definition wp_aux : seal (@wp_def). by eexists. Qed.
 Definition wp := unseal wp_aux.
 Definition wp_eq : @wp = @wp_def := seal_eq wp_aux.
@@ -172,8 +172,8 @@ Implicit Types v : val Λ.
 Implicit Types e : expr Λ.
 
 (* Weakest pre *)
-Lemma wp_unfold p E e Φ : WP e @ p; E {{ Φ }} ⊣⊢ wp_pre wp p E e Φ.
-Proof. rewrite wp_eq. apply (fixpoint_unfold wp_pre). Qed.
+Lemma wp_unfold p E e Φ : WP e @ p; E {{ Φ }} ⊣⊢ wp_pre p (wp p) E e Φ.
+Proof. rewrite wp_eq. apply (fixpoint_unfold (wp_pre p)). Qed.
 
 Global Instance wp_ne p E e n :
   Proper (pointwise_relation _ (dist n) ==> dist n) (@wp Λ Σ _ p E e).
@@ -210,7 +210,8 @@ Proof.
   iMod "Hclose" as "_". by iApply ("IH" with "HΦ").
 Qed.
 
-Lemma wp_forget_progress E e Φ : WP e @ E {{ Φ }} ⊢ WP e @ E ?{{ Φ }}.
+Lemma wp_forget_progress p E e Φ :
+  WP e @ p; E {{ Φ }} ⊢ WP e @ E ?{{ Φ }}.
 Proof.
   iIntros "H". iLöb as "IH" forall (E e Φ). rewrite !wp_unfold /wp_pre.
   destruct (to_val e) as [v|]; first iExact "H".
-- 
GitLab