From b7a767a75353956862473ca5408a1b84017634bf Mon Sep 17 00:00:00 2001
From: Ralf Jung <jung@mpi-sws.org>
Date: Fri, 29 Mar 2019 15:36:39 +0100
Subject: [PATCH] make fupd_plain_soundness more like soundness_bupd_plain

---
 theories/base_logic/lib/fancy_updates.v | 6 +++---
 theories/program_logic/total_adequacy.v | 2 +-
 2 files changed, 4 insertions(+), 4 deletions(-)

diff --git a/theories/base_logic/lib/fancy_updates.v b/theories/base_logic/lib/fancy_updates.v
index e72d196f4..eed3e7016 100644
--- a/theories/base_logic/lib/fancy_updates.v
+++ b/theories/base_logic/lib/fancy_updates.v
@@ -60,9 +60,9 @@ Proof.
 Qed.
 
 Lemma fupd_plain_soundness `{!invPreG Σ} E1 E2 (P: iProp Σ) `{!Plain P}:
-  (∀ `{Hinv: !invG Σ}, (|={E1,E2}=> P)%I) → (▷ P)%I.
+  (∀ `{Hinv: !invG Σ}, bi_emp_valid (|={E1,E2}=> P)) → bi_emp_valid P.
 Proof.
-  iIntros (Hfupd). iMod wsat_alloc as (Hinv) "[Hw HE]".
+  iIntros (Hfupd). apply soundness_later. iMod wsat_alloc as (Hinv) "[Hw HE]".
   iAssert (|={⊤,E2}=> P)%I as "H".
   { iMod fupd_intro_mask'; last iApply Hfupd. done. }
   rewrite uPred_fupd_eq /uPred_fupd_def.
@@ -74,7 +74,7 @@ Lemma step_fupdN_soundness `{!invPreG Σ} φ n :
   φ.
 Proof.
   intros Hiter.
-  apply (soundness (M:=iResUR Σ) _  (S (S n))); simpl.
+  apply (soundness (M:=iResUR Σ) _  (S n)); simpl.
   apply (fupd_plain_soundness ⊤ ⊤ _)=> Hinv.
   iPoseProof (Hiter Hinv) as "H". clear Hiter.
   destruct n as [|n].
diff --git a/theories/program_logic/total_adequacy.v b/theories/program_logic/total_adequacy.v
index 170602811..7d5512c4c 100644
--- a/theories/program_logic/total_adequacy.v
+++ b/theories/program_logic/total_adequacy.v
@@ -123,7 +123,7 @@ Theorem twp_total Σ Λ `{!invPreG Σ} s e σ Φ :
        stateI σ [] 0 ∗ WP e @ s; ⊤ [{ Φ }])%I) →
   sn erased_step ([e], σ). (* i.e. ([e], σ) is strongly normalizing *)
 Proof.
-  intros Hwp. apply (soundness (M:=iResUR Σ) _  2); simpl.
+  intros Hwp. apply (soundness (M:=iResUR Σ) _  1); simpl.
   apply (fupd_plain_soundness ⊤ ⊤ _)=> Hinv.
   iMod (Hwp) as (stateI fork_post) "[Hσ H]".
   iApply (@twptp_total _ _ (IrisG _ _ Hinv stateI fork_post) with "Hσ").
-- 
GitLab