From 9120035b4faa08910c10522f4785c657df81159b Mon Sep 17 00:00:00 2001
From: Ralf Jung <jung@mpi-sws.org>
Date: Thu, 26 Nov 2020 12:13:30 +0100
Subject: [PATCH] wp_fupd is now unnecessary in these proofs

---
 iris_heap_lang/lib/counter.v     | 4 ++--
 iris_heap_lang/lib/spin_lock.v   | 2 +-
 iris_heap_lang/lib/ticket_lock.v | 2 +-
 tests/ipm_paper.v                | 2 +-
 tests/one_shot.v                 | 2 +-
 tests/one_shot_once.v            | 2 +-
 6 files changed, 7 insertions(+), 7 deletions(-)

diff --git a/iris_heap_lang/lib/counter.v b/iris_heap_lang/lib/counter.v
index a40c90c2b..6efb2e241 100644
--- a/iris_heap_lang/lib/counter.v
+++ b/iris_heap_lang/lib/counter.v
@@ -35,7 +35,7 @@ Section mono_proof.
   Lemma newcounter_mono_spec :
     {{{ True }}} newcounter #() {{{ l, RET #l; mcounter l 0 }}}.
   Proof.
-    iIntros (Φ) "_ HΦ". rewrite -wp_fupd /newcounter /=. wp_lam. wp_alloc l as "Hl".
+    iIntros (Φ) "_ HΦ". rewrite /newcounter /=. wp_lam. wp_alloc l as "Hl".
     iMod (own_alloc (● (MaxNat O) ⋅ ◯ (MaxNat O))) as (γ) "[Hγ Hγ']";
       first by apply auth_both_valid_discrete.
     iMod (inv_alloc N _ (mcounter_inv γ l) with "[Hl Hγ]").
@@ -114,7 +114,7 @@ Section contrib_spec.
     {{{ True }}} newcounter #()
     {{{ γ l, RET #l; ccounter_ctx γ l ∗ ccounter γ 1 0 }}}.
   Proof.
-    iIntros (Φ) "_ HΦ". rewrite -wp_fupd /newcounter /=. wp_lam. wp_alloc l as "Hl".
+    iIntros (Φ) "_ HΦ". rewrite /newcounter /=. wp_lam. wp_alloc l as "Hl".
     iMod (own_alloc (●F O ⋅ ◯F 0)) as (γ) "[Hγ Hγ']";
       first by apply auth_both_valid_discrete.
     iMod (inv_alloc N _ (ccounter_inv γ l) with "[Hl Hγ]").
diff --git a/iris_heap_lang/lib/spin_lock.v b/iris_heap_lang/lib/spin_lock.v
index 5fcfeed61..61afd495a 100644
--- a/iris_heap_lang/lib/spin_lock.v
+++ b/iris_heap_lang/lib/spin_lock.v
@@ -59,7 +59,7 @@ Section proof.
   Lemma newlock_spec (R : iProp Σ):
     {{{ R }}} newlock #() {{{ lk γ, RET lk; is_lock γ lk R }}}.
   Proof.
-    iIntros (Φ) "HR HΦ". rewrite -wp_fupd /newlock /=.
+    iIntros (Φ) "HR HΦ". rewrite /newlock /=.
     wp_lam. wp_alloc l as "Hl".
     iMod (own_alloc (Excl ())) as (γ) "Hγ"; first done.
     iMod (inv_alloc N _ (lock_inv γ l R) with "[-HΦ]") as "#?".
diff --git a/iris_heap_lang/lib/ticket_lock.v b/iris_heap_lang/lib/ticket_lock.v
index 55856b304..a464b44a5 100644
--- a/iris_heap_lang/lib/ticket_lock.v
+++ b/iris_heap_lang/lib/ticket_lock.v
@@ -82,7 +82,7 @@ Section proof.
   Lemma newlock_spec (R : iProp Σ) :
     {{{ R }}} newlock #() {{{ lk γ, RET lk; is_lock γ lk R }}}.
   Proof.
-    iIntros (Φ) "HR HΦ". rewrite -wp_fupd. wp_lam.
+    iIntros (Φ) "HR HΦ". wp_lam.
     wp_alloc ln as "Hln". wp_alloc lo as "Hlo".
     iMod (own_alloc (● (Excl' 0, GSet ∅) ⋅ ◯ (Excl' 0, GSet ∅))) as (γ) "[Hγ Hγ']".
     { by apply auth_both_valid_discrete. }
diff --git a/tests/ipm_paper.v b/tests/ipm_paper.v
index 5895fe954..c5b7ed824 100644
--- a/tests/ipm_paper.v
+++ b/tests/ipm_paper.v
@@ -204,7 +204,7 @@ Section counter_proof.
   Lemma newcounter_spec :
     ⊢ {{ True }} newcounter #() {{ v, ∃ l, ⌜v = #l⌝ ∧ C l 0 }}.
   Proof.
-    iIntros "!> _ /=". rewrite -wp_fupd /newcounter /=. wp_lam. wp_alloc l as "Hl".
+    iIntros "!> _ /=". rewrite /newcounter /=. wp_lam. wp_alloc l as "Hl".
     iMod (own_alloc (Auth 0)) as (γ) "Hγ"; first done.
     rewrite (auth_frag_op 0 0) //; iDestruct "Hγ" as "[Hγ Hγf]".
     set (N:= nroot .@ "counter").
diff --git a/tests/one_shot.v b/tests/one_shot.v
index cec2f71d4..b859132b9 100644
--- a/tests/one_shot.v
+++ b/tests/one_shot.v
@@ -47,7 +47,7 @@ Lemma wp_one_shot (Φ : val → iProp Σ) :
   ⊢ WP one_shot_example #() {{ Φ }}.
 Proof.
   iIntros "Hf /=". pose proof (nroot .@ "N") as N.
-  rewrite -wp_fupd. wp_lam. wp_alloc l as "Hl".
+  wp_lam. wp_alloc l as "Hl".
   iMod (own_alloc Pending) as (γ) "Hγ"; first done.
   iMod (inv_alloc N _ (one_shot_inv γ l) with "[Hl Hγ]") as "#HN".
   { iNext. iLeft. by iSplitL "Hl". }
diff --git a/tests/one_shot_once.v b/tests/one_shot_once.v
index e2fb69892..5ce48658c 100644
--- a/tests/one_shot_once.v
+++ b/tests/one_shot_once.v
@@ -61,7 +61,7 @@ Lemma wp_one_shot (Φ : val → iProp Σ) :
   ⊢ WP one_shot_example #() {{ Φ }}.
 Proof.
   iIntros "Hf /=". pose proof (nroot .@ "N") as N.
-  rewrite -wp_fupd. wp_lam. wp_alloc l as "Hl".
+  wp_lam. wp_alloc l as "Hl".
   iMod (own_alloc (Pending 1%Qp)) as (γ) "Hγ"; first done.
   iDestruct (pending_split with "Hγ") as "[Hγ1 Hγ2]".
   iMod (inv_alloc N _ (one_shot_inv γ l) with "[Hl Hγ2]") as "#HN".
-- 
GitLab