Merge branch 'robbert/fupd_new_axioms' into 'master'

More principled set of axioms for fancy updates and plainly

Closes #164

See merge request FP/iris-coq!184

theories/base_logic/lib/fancy_updates.v

@@ -41,17 +41,26 @@ Proof. rewrite /BiBUpdFUpd uPred_fupd_eq. by iIntros (E P) ">? [$ $] !> !>". Qed
 Instance uPred_bi_fupd_plainly `{invG Σ} : BiFUpdPlainly (uPredSI (iResUR Σ)).
 Proof.
   split.
-  - rewrite uPred_fupd_eq /uPred_fupd_def. iIntros (E P Q) "HQP HQ [Hw HE]".
-    iAssert (◇ ■ P)%I as "#>HP'".
-    { by iMod ("HQP" with "HQ [$]") as "(_ & _ & HP)". }
+  - rewrite uPred_fupd_eq /uPred_fupd_def. iIntros (E P) "H [Hw HE]".
+    iAssert (◇ ■ P)%I as "#>HP".
+    { by iMod ("H" with "[$]") as "(_ & _ & HP)". }
+    by iFrame.
+  - rewrite uPred_fupd_eq /uPred_fupd_def. iIntros (E P Q) "[H HQ] [Hw HE]".
+    iAssert (◇ ■ P)%I as "#>HP".
+    { by iMod ("H" with "HQ [$]") as "(_ & _ & HP)". }
+    by iFrame.
+  - rewrite uPred_fupd_eq /uPred_fupd_def. iIntros (E P) "H [Hw HE]".
+    iAssert (▷ ◇ ■ P)%I as "#HP".
+    { iNext. by iMod ("H" with "[$]") as "(_ & _ & HP)". }
+    iFrame. iIntros "!> !> !>". by iMod "HP".
+  - rewrite uPred_fupd_eq /uPred_fupd_def. iIntros (E A Φ) "HΦ [Hw HE]".
+    iAssert (◇ ■ ∀ x : A, Φ x)%I as "#>HP".
+    { iIntros (x). by iMod ("HΦ" with "[$Hw $HE]") as "(_&_&?)". }
     by iFrame.
-  - rewrite uPred_fupd_eq /uPred_fupd_def. iIntros (p E1 E2 P) "HP [Hw HE]".
-    iAssert (▷?p ◇ ■ P)%I with "[-]" as "#HP'"; last by (rewrite plainly_elim; iFrame).
-    iNext. by iMod ("HP" with "[$]") as "(_ & _ & HP)".
 Qed.
 
 Lemma fupd_plain_soundness `{invPreG Σ} E (P: iProp Σ) `{!Plain P}:
-  (∀ `{Hinv: invG Σ}, (|={⊤, E}=> P)%I) → (▷ P)%I.
+  (∀ `{Hinv: invG Σ}, (|={⊤,E}=> P)%I) → (▷ P)%I.
 Proof.
   iIntros (Hfupd). iMod wsat_alloc as (Hinv) "[Hw HE]".
   iPoseProof (Hfupd Hinv) as "H".
@@ -60,30 +69,28 @@ Proof.
 Qed.
 
 Lemma step_fupdN_soundness `{invPreG Σ} φ n :
-  (∀ `{Hinv: invG Σ}, (|={⊤, ∅}▷=>^n |={⊤, ∅}=> ⌜ φ ⌝ : iProp Σ)%I) →
+  (∀ `{Hinv: invG Σ}, (|={⊤,∅}▷=>^n |={⊤,∅}=> ⌜ φ ⌝ : iProp Σ)%I) →
   φ.
 Proof.
   intros Hiter.
   apply (soundness (M:=iResUR Σ) _  (S (S n))); simpl.
-  apply (fupd_plain_soundness ⊤ _).
-  intros Hinv. iPoseProof (Hiter Hinv) as "H".
+  apply (fupd_plain_soundness ⊤ _)=> Hinv.
+  iPoseProof (Hiter Hinv) as "H". clear Hiter.
   destruct n as [|n].
-  - rewrite //=. iPoseProof (fupd_plain_strong with "H") as "H'".
-    do 2 iMod "H'"; iModIntro; auto.
-  - iPoseProof (step_fupdN_mono _ _ _ _ (|={⊤}=> ◇ ⌜φ⌝)%I with "H") as "H'".
-    { iIntros "H". iMod (fupd_plain_strong with "H"); auto. }
+  - iApply fupd_plainly_mask_empty. iMod "H" as %?; auto.
+  - iDestruct (step_fupdN_wand _ _ _ _ (|={⊤}=> ⌜φ⌝)%I with "H []") as "H'".
+    { by iApply fupd_plain_mask_empty. }
     rewrite -step_fupdN_S_fupd.
     iMod (step_fupdN_plain with "H'") as "Hφ". iModIntro. iNext.
     rewrite -later_laterN laterN_later.
-    iNext. by do 2 iMod "Hφ".
+    iNext. by iMod "Hφ".
 Qed.
 
 Lemma step_fupdN_soundness' `{invPreG Σ} φ n :
-  (∀ `{Hinv: invG Σ}, (|={⊤, ∅}▷=>^n ⌜ φ ⌝ : iProp Σ)%I)  →
+  (∀ `{Hinv: invG Σ}, (|={⊤,∅}▷=>^n ⌜ φ ⌝ : iProp Σ)%I)  →
   φ.
 Proof.
   iIntros (Hiter). eapply (step_fupdN_soundness _ n).
   iIntros (Hinv). iPoseProof (Hiter Hinv) as "Hiter".
-  iApply (step_fupdN_mono with "Hiter").
-  iIntros (?). iMod (fupd_intro_mask' _ ∅) as "_"; auto.
+  iApply (step_fupdN_wand with "Hiter"). by iApply (fupd_mask_weaken _ _ _).
 Qed.

theories/bi/monpred.v

@@ -956,11 +956,17 @@ Proof. move => [] /(_ i). rewrite /Plain monPred_at_plainly bi.forall_elim //. Q
 
 Global Instance monPred_bi_fupd_plainly `{BiFUpdPlainly PROP} : BiFUpdPlainly monPredSI.
 Proof.
-  split; rewrite monPred_fupd_eq; unseal.
-  - intros E P Q. split=>/= i. do 3 f_equiv.
-    rewrite monPred_at_plainly (bi.forall_elim _) fupd_plainly_weak //=.
-  - intros p E1 E2 P; split=>/= i; specialize (later_fupd_plainly p) => HFP.
-    destruct p; simpl; [ unseal | ]; rewrite monPred_at_plainly (bi.forall_elim _); apply HFP.
+  split; rewrite !monPred_fupd_eq; try unseal.
+  - intros E P. split=>/= i.
+    by rewrite monPred_at_plainly (bi.forall_elim i) fupd_plainly_mask_empty.
+  - intros E P R. split=>/= i.
+    rewrite (bi.forall_elim i) bi.pure_True // bi.True_impl.
+    by rewrite monPred_at_plainly (bi.forall_elim i) fupd_plainly_keep_l.
+  - intros E P. split=>/= i.
+    by rewrite monPred_at_plainly (bi.forall_elim i) fupd_plainly_later.
+  - intros E A Φ. split=>/= i.
+    rewrite -fupd_plainly_forall_2. apply bi.forall_mono=> x.
+    by rewrite monPred_at_plainly (bi.forall_elim i).
 Qed.
 
 Global Instance plainly_objective `{BiPlainly PROP} P : Objective (■ P).

theories/bi/updates.v

@@ -54,7 +54,7 @@ Record BiFUpdMixin (PROP : sbi) `(FUpd PROP) := {
   bi_fupd_mixin_fupd_trans E1 E2 E3 (P : PROP) : (|={E1,E2}=> |={E2,E3}=> P) ⊢ |={E1,E3}=> P;
   bi_fupd_mixin_fupd_mask_frame_r' E1 E2 Ef (P : PROP) :
     E1 ## Ef → (|={E1,E2}=> ⌜E2 ## Ef⌝ → P) ={E1 ∪ Ef,E2 ∪ Ef}=∗ P;
-  bi_fupd_mixin_fupd_frame_r E1 E2 (P Q : PROP) : (|={E1,E2}=> P) ∗ Q ={E1,E2}=∗ P ∗ Q;
+  bi_fupd_mixin_fupd_frame_r E1 E2 (P R : PROP) : (|={E1,E2}=> P) ∗ R ={E1,E2}=∗ P ∗ R;
 }.
 
 Class BiBUpd (PROP : bi) := {
@@ -79,11 +79,28 @@ Class BiBUpdPlainly (PROP : sbi) `{!BiBUpd PROP, !BiPlainly PROP} :=
   bupd_plainly (P : PROP) : (|==> ■ P) -∗ P.
 Hint Mode BiBUpdPlainly ! - - : typeclass_instances.
 
+(** These rules for the interaction between the [■] and [|={E1,E2=>] modalities
+only make sense for affine logics. From the axioms below, one could derive
+[■ P ={E}=∗ P] (see the lemma [fupd_plainly_elim]), which in turn gives
+[True ={E}=∗ emp]. *)
 Class BiFUpdPlainly (PROP : sbi) `{!BiFUpd PROP, !BiPlainly PROP} := {
-  fupd_plainly_weak E (P Q : PROP) :
-    (Q ={E}=∗ ■ P) -∗ Q ={E}=∗ Q ∗ P;
-  later_fupd_plainly p E1 E2 (P : PROP) :
-    (▷?p |={E1, E2}=> ■ P) ={E1}=∗ ▷?p ◇ P;
+  (** When proving a fancy update of a plain proposition, you can also prove it
+  while being allowed to open all invariants. *)
+  fupd_plainly_mask_empty E (P : PROP) :
+    (|={E,∅}=> ■ P) ⊢ |={E}=> P;
+  (** A strong eliminator (a la modus ponens) for the wand-fancy-update with a
+  plain conclusion: We eliminate [R ={E}=∗ ■ P] by supplying an [R], but we get
+  to keep the [R]. *)
+  fupd_plainly_keep_l E (P R : PROP) :
+    (R ={E}=∗ ■ P) ∗ R ⊢ |={E}=> P ∗ R;
+  (** Later "almost" commutes with fancy updates over plain propositions. It
+  commutes "almost" because of the ◇ modality, which is needed in the definition
+  of fancy updates so one can remove laters of timeless propositions. *)
+  fupd_plainly_later E (P : PROP) :
+    (▷ |={E}=> ■ P) ⊢ |={E}=> ▷ ◇ P;
+  (** Forall quantifiers commute with fancy updates over plain propositions. *)
+  fupd_plainly_forall_2 E {A} (Φ : A → PROP) :
+    (∀ x, |={E}=> ■ Φ x) ⊢ |={E}=> ∀ x, Φ x
 }.
 Hint Mode BiBUpdFUpd ! - - : typeclass_instances.
 
@@ -120,7 +137,7 @@ Section fupd_laws.
   Lemma fupd_mask_frame_r' E1 E2 Ef (P : PROP) :
     E1 ## Ef → (|={E1,E2}=> ⌜E2 ## Ef⌝ → P) ={E1 ∪ Ef,E2 ∪ Ef}=∗ P.
   Proof. eapply bi_fupd_mixin_fupd_mask_frame_r', bi_fupd_mixin. Qed.
-  Lemma fupd_frame_r E1 E2 (P Q : PROP) : (|={E1,E2}=> P) ∗ Q ={E1,E2}=∗ P ∗ Q.
+  Lemma fupd_frame_r E1 E2 (P R : PROP) : (|={E1,E2}=> P) ∗ R ={E1,E2}=∗ P ∗ R.
   Proof. eapply bi_fupd_mixin_fupd_frame_r, bi_fupd_mixin. Qed.
 End fupd_laws.
 
@@ -196,8 +213,8 @@ Section fupd_derived.
   Lemma fupd_except_0 E1 E2 P : (|={E1,E2}=> ◇ P) ={E1,E2}=∗ P.
   Proof. by rewrite {1}(fupd_intro E2 P) except_0_fupd fupd_trans. Qed.
 
-  Lemma fupd_frame_l E1 E2 P Q : (P ∗ |={E1,E2}=> Q) ={E1,E2}=∗ P ∗ Q.
-  Proof. rewrite !(comm _ P); apply fupd_frame_r. Qed.
+  Lemma fupd_frame_l E1 E2 R Q : (R ∗ |={E1,E2}=> Q) ={E1,E2}=∗ R ∗ Q.
+  Proof. rewrite !(comm _ R); apply fupd_frame_r. Qed.
   Lemma fupd_wand_l E1 E2 P Q : (P -∗ Q) ∗ (|={E1,E2}=> P) ={E1,E2}=∗ Q.
   Proof. by rewrite fupd_frame_l wand_elim_l. Qed.
   Lemma fupd_wand_r E1 E2 P Q : (|={E1,E2}=> P) ∗ (P -∗ Q) ={E1,E2}=∗ Q.
@@ -239,8 +256,7 @@ Section fupd_derived.
   Proof.
     intros ?. rewrite (fupd_mask_frame_r _ _ (E ∖ E1)); last set_solver.
     rewrite fupd_trans.
-    assert (E = E1 ∪ E ∖ E1) as <-; last done.
-    apply union_difference_L. done.
+    by replace (E1 ∪ E ∖ E1) with E by (by apply union_difference_L).
   Qed.
   (* A variant of [fupd_mask_frame] that works well for accessors: Tailored to
      elliminate updates of the form [|={E1,E1∖E2}=> Q] and provides a way to
@@ -335,8 +351,7 @@ Section fupd_derived.
     by apply later_mono, fupd_mono.
   Qed.
 
-  Lemma step_fupd_fupd E P:
-    (|={E, ∅}▷=> P) ⊣⊢ (|={E, ∅}▷=> |={E}=> P).
+  Lemma step_fupd_fupd E E' P : (|={E,E'}▷=> P) ⊣⊢ (|={E,E'}▷=> |={E}=> P).
   Proof.
     apply (anti_symm (⊢)).
     - by rewrite -fupd_intro.
@@ -344,11 +359,20 @@ Section fupd_derived.
   Qed.
 
   Lemma step_fupdN_mono E1 E2 n P Q :
-    (P ⊢ Q) → (|={E1, E2}▷=>^n P) ⊢ (|={E1, E2}▷=>^n Q).
+    (P ⊢ Q) → (|={E1,E2}▷=>^n P) ⊢ (|={E1,E2}▷=>^n Q).
   Proof.
     intros HPQ. induction n as [|n IH]=> //=. rewrite IH //.
   Qed.
 
+  Lemma step_fupdN_wand E1 E2 n P Q :
+    (|={E1,E2}▷=>^n P) -∗ (P -∗ Q) -∗ (|={E1,E2}▷=>^n Q).
+  Proof.
+    apply wand_intro_l. induction n as [|n IH]=> /=.
+    { by rewrite wand_elim_l. }
+    rewrite -IH -fupd_frame_l later_sep -fupd_frame_l.
+    by apply sep_mono; first apply later_intro.
+  Qed.
+
   Lemma step_fupdN_S_fupd n E P:
     (|={E, ∅}▷=>^(S n) P) ⊣⊢ (|={E, ∅}▷=>^(S n) |={E}=> P).
   Proof.
@@ -366,55 +390,89 @@ Section fupd_derived.
   Section fupd_plainly_derived.
     Context `{BiPlainly PROP, !BiFUpdPlainly PROP}.
 
-    Lemma fupd_plain_weak E P Q `{!Plain P}:
-      (Q ={E}=∗ P) -∗ Q ={E}=∗ Q ∗ P.
-    Proof. by rewrite {1}(plain P) fupd_plainly_weak. Qed.
+    Lemma fupd_plainly_mask E E' P : (|={E,E'}=> ■ P) ⊢ |={E}=> P.
+    Proof.
+      rewrite -(fupd_plainly_mask_empty).
+      apply fupd_elim, (fupd_mask_weaken _ _ _). set_solver.
+    Qed.
+
+    Lemma fupd_plainly_elim E P : ■ P ={E}=∗ P.
+    Proof. by rewrite (fupd_intro E (■ P)%I) fupd_plainly_mask. Qed.
+
+    Lemma fupd_plainly_keep_r E P R : R ∗ (R ={E}=∗ ■ P) ⊢ |={E}=> R ∗ P.
+    Proof. by rewrite !(comm _ R) fupd_plainly_keep_l. Qed.
 
-    Lemma later_fupd_plain p E1 E2 P `{!Plain P} :
-      (▷?p |={E1, E2}=> P) ={E1}=∗ ▷?p ◇ P.
-    Proof. by rewrite {1}(plain P) later_fupd_plainly. Qed.
+    Lemma fupd_plain_mask_empty E P `{!Plain P} : (|={E,∅}=> P) ⊢ |={E}=> P.
+    Proof. by rewrite {1}(plain P) fupd_plainly_mask_empty. Qed.
+    Lemma fupd_plain_mask E E' P `{!Plain P} : (|={E,E'}=> P) ⊢ |={E}=> P.
+    Proof. by rewrite {1}(plain P) fupd_plainly_mask. Qed.
 
-    Lemma fupd_plain_strong E1 E2 P `{!Plain P} :
-      (|={E1, E2}=> P) ={E1}=∗ ◇ P.
-    Proof. by apply (later_fupd_plain false). Qed.
+    Lemma fupd_plain_keep_l E P R `{!Plain P} : (R ={E}=∗ P) ∗ R ⊢ |={E}=> P ∗ R.
+    Proof. by rewrite {1}(plain P) fupd_plainly_keep_l. Qed.
+    Lemma fupd_plain_keep_r E P R `{!Plain P} : R ∗ (R ={E}=∗ P) ⊢ |={E}=> R ∗ P.
+    Proof. by rewrite {1}(plain P) fupd_plainly_keep_r. Qed.
 
-    Lemma fupd_plain' E1 E2 E2' P Q `{!Plain P} :
-      E1 ⊆ E2 →
-      (Q ={E1, E2'}=∗ P) -∗ (|={E1, E2}=> Q) ={E1}=∗ (|={E1, E2}=> Q) ∗ P.
+    Lemma fupd_plain_later E P `{!Plain P} : (▷ |={E}=> P) ⊢ |={E}=> ▷ ◇ P.
+    Proof. by rewrite {1}(plain P) fupd_plainly_later. Qed.
+    Lemma fupd_plain_forall_2 E {A} (Φ : A → PROP) `{!∀ x, Plain (Φ x)} :
+      (∀ x, |={E}=> Φ x) ⊢ |={E}=> ∀ x, Φ x.
     Proof.
-      intros (E3&->&HE)%subseteq_disjoint_union_L.
-      apply wand_intro_l. rewrite fupd_frame_r.
-      rewrite fupd_plain_strong fupd_except_0 fupd_plain_weak wand_elim_r.
-      rewrite (fupd_mask_mono E1 (E1 ∪ E3)); last by set_solver+.
-      rewrite fupd_trans -(fupd_trans E1 (E1 ∪ E3) E1).
-      apply fupd_mono. rewrite -fupd_frame_r.
-      apply sep_mono; auto. apply fupd_intro_mask; set_solver+.
+      rewrite -fupd_plainly_forall_2. apply forall_mono=> x.
+      by rewrite {1}(plain (Φ _)).
     Qed.
 
-    Lemma fupd_plain E1 E2 P Q `{!Plain P} :
-      E1 ⊆ E2 → (Q -∗ P) -∗ (|={E1, E2}=> Q) ={E1}=∗ (|={E1, E2}=> Q) ∗ P.
+    Lemma fupd_plainly_laterN E n P `{HP : !Plain P} :
+      (▷^n |={E}=> P) ⊢ |={E}=> ▷^n ◇ P.
     Proof.
-      intros HE. rewrite -(fupd_plain' _ _ E1) //. apply wand_intro_l.
-        by rewrite wand_elim_r -fupd_intro.
+      revert P HP. induction n as [|n IH]=> P ? /=.
+      - by rewrite -except_0_intro.
+      - rewrite -!later_laterN !laterN_later.
+        rewrite fupd_plain_later. by rewrite IH except_0_later.
     Qed.
 
-    Lemma step_fupd_plain E P `{!Plain P} :
-      (|={E, ∅}▷=> P) ={E}=∗ ▷ ◇ P.
+    Lemma fupd_plain_forall E1 E2 {A} (Φ : A → PROP) `{!∀ x, Plain (Φ x)} :
+      E2 ⊆ E1 →
+      (|={E1,E2}=> ∀ x, Φ x) ⊣⊢ (∀ x, |={E1,E2}=> Φ x).
     Proof.
-      specialize (later_fupd_plain true ∅ E P) => //= ->.
-      rewrite fupd_trans fupd_plain_strong. apply fupd_mono, except_0_later.
+      intros. apply (anti_symm _).
+      { apply forall_intro=> x. by rewrite (forall_elim x). }
+      trans (∀ x, |={E1}=> Φ x)%I.
+      { apply forall_mono=> x. by rewrite fupd_plain_mask. }
+      rewrite fupd_plain_forall_2. apply fupd_elim.
+      rewrite {1}(plain (∀ x, Φ x)) (fupd_mask_weaken E1 E2 (■ _)%I) //.
+      apply fupd_elim. by rewrite fupd_plainly_elim.
     Qed.
+    Lemma fupd_plain_forall' E {A} (Φ : A → PROP) `{!∀ x, Plain (Φ x)} :
+      (|={E}=> ∀ x, Φ x) ⊣⊢ (∀ x, |={E}=> Φ x).
+    Proof. by apply fupd_plain_forall. Qed.
 
-    Lemma step_fupdN_plain E n P `{!Plain P}:
-      (|={E, ∅}▷=>^n P) ={E}=∗ ▷^n ◇ P.
+    Lemma step_fupd_plain E E' P `{!Plain P} : (|={E,E'}▷=> P) ={E}=∗ ▷ ◇ P.
+    Proof.
+      rewrite -(fupd_plain_mask _ E' (▷ ◇ P)%I).
+      apply fupd_elim. by rewrite fupd_plain_mask -fupd_plain_later.
+    Qed.
+
+    Lemma step_fupdN_plain E E' n P `{!Plain P} : (|={E,E'}▷=>^n P) ={E}=∗ ▷^n ◇ P.
     Proof.
       induction n as [|n IH].
-      - rewrite -fupd_intro. apply except_0_intro.
-      - rewrite Nat_iter_S step_fupd_fupd IH ?fupd_trans step_fupd_plain.
-        apply fupd_mono. destruct n; simpl.
+      - by rewrite -fupd_intro -except_0_intro.
+      - rewrite Nat_iter_S step_fupd_fupd IH !fupd_trans step_fupd_plain.
+        apply fupd_mono. destruct n as [|n]; simpl.
         * by rewrite except_0_idemp.
         * by rewrite except_0_later.
     Qed.
-  End fupd_plainly_derived.
 
+    Lemma step_fupd_plain_forall E1 E2 {A} (Φ : A → PROP) `{!∀ x, Plain (Φ x)} :
+      E2 ⊆ E1 →
+      (|={E1,E2}▷=> ∀ x, Φ x) ⊣⊢ (∀ x, |={E1,E2}▷=> Φ x).
+    Proof.
+      intros. apply (anti_symm _).
+      { apply forall_intro=> x. by rewrite (forall_elim x). }
+      trans (∀ x, |={E1}=> ▷ ◇ Φ x)%I.
+      { apply forall_mono=> x. by rewrite step_fupd_plain. }
+      rewrite -fupd_plain_forall'. apply fupd_elim.
+      rewrite -(fupd_except_0 E2 E1) -step_fupd_intro //.
+      by rewrite -later_forall -except_0_forall.
+    Qed.
+  End fupd_plainly_derived.
 End fupd_derived.

theories/program_logic/adequacy.v

@@ -44,7 +44,7 @@ Notation wptp s t := ([∗ list] ef ∈ t, WP ef @ s; ⊤ {{ _, True }})%I.
 Lemma wp_step s E e1 σ1 κ κs e2 σ2 efs Φ :
   prim_step e1 σ1 κ e2 σ2 efs →
   state_interp σ1 (κ ++ κs) ∗ WP e1 @ s; E {{ Φ }}
-  ={E, ∅}▷=∗ (state_interp σ2 κs ∗ WP e2 @ s; E {{ Φ }} ∗ wptp s efs).
+  ={E,∅}▷=∗ (state_interp σ2 κs ∗ WP e2 @ s; E {{ Φ }} ∗ wptp s efs).
 Proof.
   rewrite {1}wp_unfold /wp_pre. iIntros (?) "[Hσ H]".
   rewrite (val_stuck e1 σ1 κ e2 σ2 efs) //.
@@ -57,7 +57,7 @@ Lemma wptp_step s e1 t1 t2 κ κs σ1 σ2 Φ :
   step (e1 :: t1,σ1) κ (t2, σ2) →
   state_interp σ1 (κ ++ κs) ∗ WP e1 @ s; ⊤ {{ Φ }} ∗ wptp s t1
   ==∗ ∃ e2 t2',
-    ⌜t2 = e2 :: t2'⌝ ∗ |={⊤, ∅}▷=> (state_interp σ2 κs ∗ WP e2 @ s; ⊤ {{ Φ }} ∗ wptp s t2').
+    ⌜t2 = e2 :: t2'⌝ ∗ |={⊤,∅}▷=> (state_interp σ2 κs ∗ WP e2 @ s; ⊤ {{ Φ }} ∗ wptp s t2').
 Proof.
   iIntros (Hstep) "(HW & He & Ht)".
   destruct Hstep as [e1' σ1' e2' σ2' efs [|? t1'] t2' ?? Hstep]; simplify_eq/=.
@@ -71,7 +71,7 @@ Qed.
 Lemma wptp_steps s n e1 t1 κs κs' t2 σ1 σ2 Φ :
   nsteps n (e1 :: t1, σ1) κs (t2, σ2) →
   state_interp σ1 (κs ++ κs') ∗ WP e1 @ s; ⊤ {{ Φ }} ∗ wptp s t1 ⊢
-  |={⊤, ∅}▷=>^n (∃ e2 t2',
+  |={⊤,∅}▷=>^n (∃ e2 t2',
     ⌜t2 = e2 :: t2'⌝ ∗ state_interp σ2 κs' ∗ WP e2 @ s; ⊤ {{ Φ }} ∗ wptp s t2').
 Proof.
   revert e1 t1 κs κs' t2 σ1 σ2; simpl; induction n as [|n IH]=> e1 t1 κs κs' t2 σ1 σ2 /=.
@@ -88,15 +88,15 @@ Lemma wptp_result s n e1 t1 κs κs' v2 t2 σ1 σ2 φ :
   state_interp σ1 (κs ++ κs') ∗
   WP e1 @ s; ⊤ {{ v, ∀ σ, state_interp σ κs' ={⊤,∅}=∗ ⌜φ v σ⌝ }} ∗
   wptp s t1 ⊢
-  |={⊤, ∅}▷=>^(S n) ⌜φ v2 σ2⌝.
+  |={⊤,∅}▷=>^(S n) ⌜φ v2 σ2⌝.
 Proof.
   intros. rewrite Nat_iter_S_r wptp_steps //.
   apply step_fupdN_mono.
   iDestruct 1 as (e2 t2' ?) "(Hσ & H & _)"; simplify_eq.
   iMod (wp_value_inv' with "H") as "H".
-  iMod (later_fupd_plain false ⊤ ∅ (⌜φ v2 σ2⌝)%I with "[H Hσ]") as ">#%".
-  { rewrite //=. by iMod ("H" with "Hσ") as "$". }
-  iApply (step_fupd_mask_mono ∅ _ _ ∅); auto.
+  iMod (fupd_plain_mask_empty _ ⌜φ v2 σ2⌝%I with "[H Hσ]") as %?.
+  { by iMod ("H" with "Hσ") as "$". }
+  by iApply step_fupd_intro.
 Qed.
 
 Lemma wp_safe E e σ κs Φ :
@@ -105,8 +105,8 @@ Proof.
   rewrite wp_unfold /wp_pre. iIntros "Hσ H".
   destruct (to_val e) as [v|] eqn:?.
   { iApply (step_fupd_mask_mono ∅ _ _ ∅); eauto. set_solver. }
-  iMod (later_fupd_plain false E ∅ (⌜reducible e σ⌝)%I with "[H Hσ]") as ">#%".
-  { rewrite //=. by iMod ("H" $! σ [] κs with "Hσ") as "($&H)". }
+  iMod (fupd_plain_mask_empty _ ⌜reducible e σ⌝%I with "[H Hσ]") as %?.
+  { by iMod ("H" $! σ [] κs with "Hσ") as "($&H)". }
   iApply step_fupd_intro; first by set_solver+. 
   iIntros "!> !%". by right.
 Qed.
@@ -114,7 +114,7 @@ Qed.
 Lemma wptp_safe n e1 κs κs' e2 t1 t2 σ1 σ2 Φ :
   nsteps n (e1 :: t1, σ1) κs (t2, σ2) → e2 ∈ t2 →
   state_interp σ1 (κs ++ κs') ∗ WP e1 {{ Φ }} ∗ wptp NotStuck t1
-  ⊢ |={⊤, ∅}▷=>^(S n) ⌜is_Some (to_val e2) ∨ reducible e2 σ2⌝.
+  ⊢ |={⊤,∅}▷=>^(S n) ⌜is_Some (to_val e2) ∨ reducible e2 σ2⌝.
 Proof.
   intros ? He2. rewrite Nat_iter_S_r wptp_steps //.
   apply step_fupdN_mono.
@@ -126,14 +126,14 @@ Qed.
 
 Lemma wptp_invariance s n e1 κs κs' e2 t1 t2 σ1 σ2 φ Φ :
   nsteps n (e1 :: t1, σ1) κs (t2, σ2) →
-  (state_interp σ2 κs' ={⊤,∅}=∗ ⌜φ⌝) ∗ state_interp σ1 (κs ++ κs') ∗ WP e1 @ s; ⊤ {{ Φ }} ∗ wptp s t1
-  ⊢ |={⊤, ∅}▷=>^(S n) |={⊤,∅}=> ⌜φ⌝.
+  (state_interp σ2 κs' ={⊤,∅}=∗ ⌜φ⌝) ∗
+  state_interp σ1 (κs ++ κs') ∗ WP e1 @ s; ⊤ {{ Φ }} ∗ wptp s t1
+  ⊢ |={⊤,∅}▷=>^(S n) |={⊤,∅}=> ⌜φ⌝.
 Proof.
   intros ?. rewrite Nat_iter_S_r wptp_steps // step_fupdN_frame_l.
   apply step_fupdN_mono.
   iIntros "[Hback H]"; iDestruct "H" as (e2' t2' ->) "[Hσ _]".
-  iSpecialize ("Hback" with "Hσ").
-  iApply (step_fupd_mask_mono ∅ _ _ ∅); auto.
+  iSpecialize ("Hback" with "Hσ"). by iApply step_fupd_intro.
 Qed.
 End adequacy.
 
@@ -146,15 +146,13 @@ Theorem wp_strong_adequacy Σ Λ `{invPreG Σ} s e σ φ :
 Proof.
   intros Hwp; split.
   - intros t2 σ2 v2 [n [κs ?]]%erased_steps_nsteps.
-    eapply (step_fupdN_soundness' _ (S (S n))).
-    iIntros (Hinv).
+    eapply (step_fupdN_soundness' _ (S (S n)))=> Hinv.
     rewrite Nat_iter_S.
     iMod Hwp as (Istate) "[HI Hwp]".
     iApply (step_fupd_mask_mono ∅ _ _ ∅); auto. iModIntro. iNext; iModIntro.
     iApply (@wptp_result _ _ (IrisG _ _ _ Hinv Istate) _ _ _ _ _ []); eauto with iFrame.
   - destruct s; last done. intros t2 σ2 e2 _ [n [κs ?]]%erased_steps_nsteps ?.
-    eapply (step_fupdN_soundness' _ (S (S n))).
-    iIntros (Hinv).
+    eapply (step_fupdN_soundness' _ (S (S n)))=> Hinv.
     rewrite Nat_iter_S.
     iMod Hwp as (Istate) "[HI Hwp]".
     iApply (step_fupd_mask_mono ∅ _ _ ∅); auto.
@@ -184,11 +182,10 @@ Theorem wp_invariance Σ Λ `{invPreG Σ} s e σ1 t2 σ2 φ :
   φ.
 Proof.
   intros Hwp [n [κs ?]]%erased_steps_nsteps.
-  eapply (step_fupdN_soundness _ (S (S n))).
-  iIntros (Hinv).
+  eapply (step_fupdN_soundness _ (S (S n)))=> Hinv.
   rewrite Nat_iter_S.
   iMod (Hwp Hinv κs []) as (Istate) "(HIstate & Hwp & Hclose)".
-  iApply (step_fupd_mask_mono ∅ _ _ ∅); auto.
+  iApply step_fupd_intro; first done.
   iApply (@wptp_invariance _ _ (IrisG _ _ _ Hinv Istate)); eauto with iFrame.
 Qed.
 

theories/program_logic/total_adequacy.v

 From iris.program_logic Require Export total_weakestpre adequacy.
 From iris.algebra Require Import gmap auth agree gset coPset list.
 From iris.bi Require Import big_op fixpoint.
-From iris.base_logic.lib Require Import wsat.
 From iris.proofmode Require Import tactics.
 Set Default Proof Using "Type".
 Import uPred.
@@ -99,18 +98,15 @@ Proof.
   iApply (twptp_app [_] with "[IH']"); [by iApply "IH'"|by iApply "IH"].
 Qed.
 
-Notation world σ := (wsat ∗ ownE ⊤ ∗ state_interp σ [])%I.
-
-Lemma twptp_total σ t : world σ -∗ twptp t -∗ ▷ ⌜sn erased_step (t, σ)⌝.
+Lemma twptp_total σ t :
+  state_interp σ [] -∗ twptp t ={⊤}=∗ ▷ ⌜sn erased_step (t, σ)⌝.
 Proof.
   iIntros "Hw Ht". iRevert (σ) "Hw". iRevert (t) "Ht".
-  iApply twptp_ind; iIntros "!#" (t) "IH"; iIntros (σ) "(Hw&HE&Hσ)".
+  iApply twptp_ind; iIntros "!#" (t) "IH"; iIntros (σ) "Hσ".
   iApply (pure_mono _ _ (Acc_intro _)). iIntros ([t' σ'] [κ Hstep]).
-  rewrite /twptp_pre uPred_fupd_eq /uPred_fupd_def.
-  iMod ("IH" with "[% //] Hσ [$Hw $HE]") as ">(Hw & HE & % & Hσ & [IH _])".
-  iApply "IH". by iFrame.
+  iMod ("IH" with "[% //] Hσ") as (->) "[Hσ [H _]]".
+  by iApply "H".
 Qed.
-
 End adequacy.
 
 Theorem twp_total Σ Λ `{invPreG Σ} s e σ Φ :
@@ -120,11 +116,9 @@ Theorem twp_total Σ Λ `{invPreG Σ} s e σ Φ :
        stateI σ [] ∗ WP e @ s; ⊤ [{ Φ }])%I) →
   sn erased_step ([e], σ). (* i.e. ([e], σ) is strongly normalizing *)
 Proof.
-  intros Hwp.
-  eapply (soundness (M:=iResUR Σ) _ 1); iIntros "/=".
-  iMod wsat_alloc as (Hinv) "[Hw HE]". specialize (Hwp Hinv).
-  rewrite uPred_fupd_eq in Hwp; iMod (Hwp with "[$Hw $HE]") as ">(Hw & HE & Hwp)".
-  iDestruct "Hwp" as (Istate) "[HI Hwp]".
-  iApply (@twptp_total _ _ (IrisG _ _ _ Hinv Istate) with "[$Hw $HE $HI]").
-  by iApply (@twp_twptp _ _ (IrisG _ _ _ Hinv Istate)).
+  intros Hwp. apply (soundness (M:=iResUR Σ) _  2); simpl.
+  apply (fupd_plain_soundness ⊤ _)=> Hinv.
+  iMod (Hwp) as (stateI) "[Hσ H]".
+  iApply (@twptp_total _ _ (IrisG _ _ _ Hinv stateI) with "Hσ").
+  by iApply (@twp_twptp _ _ (IrisG _ _ _ Hinv stateI)).
 Qed.

theories/proofmode/class_instances_sbi.v

@@ -321,6 +321,24 @@ Global Instance from_forall_plainly `{BiPlainly PROP} {A} P (Φ : A → PROP) :
   FromForall P Φ → FromForall (■ P)%I (λ a, ■ (Φ a))%I.
 Proof. rewrite /FromForall=> <-. by rewrite plainly_forall. Qed.
 
+Global Instance from_forall_fupd `{BiFUpdPlainly PROP} E1 E2 {A} P (Φ : A → PROP) :
+  (* Some cases in which [E2 ⊆ E1] holds *)
+  TCOr (TCEq E1 E2) (TCOr (TCEq E1 ⊤) (TCEq E2 ∅)) →
+  FromForall P Φ → (∀ x, Plain (Φ x)) →
+  FromForall (|={E1,E2}=> P)%I (λ a, |={E1,E2}=> (Φ a))%I.
+Proof.
+  rewrite /FromForall=> -[->|[->|->]] <- ?; rewrite fupd_plain_forall; set_solver.
+Qed.
+
+Global Instance from_forall_step_fupd `{BiFUpdPlainly PROP} E1 E2 {A} P (Φ : A → PROP) :
+  (* Some cases in which [E2 ⊆ E1] holds *)
+  TCOr (TCEq E1 E2) (TCOr (TCEq E1 ⊤) (TCEq E2 ∅)) →
+  FromForall P Φ → (∀ x, Plain (Φ x)) →
+  FromForall (|={E1,E2}▷=> P)%I (λ a, |={E1,E2}▷=> (Φ a))%I.
+Proof.
+  rewrite /FromForall=> -[->|[->|->]] <- ?; rewrite step_fupd_plain_forall; set_solver.
+Qed.
+
 (** IsExcept0 *)
 Global Instance is_except_0_except_0 P : IsExcept0 (◇ P).
 Proof. by rewrite /IsExcept0 except_0_idemp. Qed.