generalize proofmode accessors to work with all modalities, and not depend on SBI or FUpd any more

theories/base_logic/lib/cancelable_invariants.v

@@ -94,7 +94,7 @@ Section proofs.
 
   Global Instance into_acc_cinv E N γ P p :
     IntoAcc (X:=unit) (cinv N γ P)
-            (↑N ⊆ E) (cinv_own γ p) E (E∖↑N)
+            (↑N ⊆ E) (cinv_own γ p) (fupd E (E∖↑N)) (fupd (E∖↑N) E)
             (λ _, ▷ P ∗ cinv_own γ p)%I (λ _, ▷ P)%I (λ _, None)%I.
   Proof.
     rewrite /IntoAcc /accessor. iIntros (?) "#Hinv Hown".

theories/base_logic/lib/invariants.v

@@ -111,7 +111,8 @@ Global Instance into_inv_inv N P : IntoInv (inv N P) N.
 
 Global Instance into_acc_inv E N P :
   IntoAcc (X:=unit) (inv N P) 
-          (↑N ⊆ E) True E (E∖↑N) (λ _, ▷ P)%I (λ _, ▷ P)%I (λ _, None)%I.
+          (↑N ⊆ E) True (fupd E (E∖↑N)) (fupd (E∖↑N) E)
+          (λ _, ▷ P)%I (λ _, ▷ P)%I (λ _, None)%I.
 Proof.
   rewrite /IntoAcc /accessor exist_unit.
   iIntros (?) "#Hinv _". iApply inv_open; done.

theories/base_logic/lib/na_invariants.v

@@ -115,7 +115,7 @@ Section proofs.
 
   Global Instance into_acc_na p F E N P :
     IntoAcc (X:=unit) (na_inv p N P)
-            (↑N ⊆ E ∧ ↑N ⊆ F) (na_own p F) E E
+            (↑N ⊆ E ∧ ↑N ⊆ F) (na_own p F) (fupd E E) (fupd E E)
             (λ _, ▷ P ∗ na_own p (F∖↑N))%I (λ _, ▷ P ∗ na_own p (F∖↑N))%I
               (λ _, Some (na_own p F))%I.
   Proof.

theories/program_logic/weakestpre.v

@@ -407,7 +407,8 @@ Section proofmode_classes.
 
   Global Instance elim_acc_wp {X} E1 E2 α β γ e s Φ :
     Atomic (stuckness_to_atomicity s) e →
-    ElimAcc (X:=X) E1 E2 α β γ (WP e @ s; E1 {{ Φ }})
+    ElimAcc (X:=X) (fupd E1 E2) (fupd E2 E1)
+            α β γ (WP e @ s; E1 {{ Φ }})
             (λ x, WP e @ s; E2 {{ v, |={E2}=> β x ∗ coq_tactics.maybe_wand (γ x) (Φ v) }})%I.
   Proof.
     intros ?. rewrite /ElimAcc. setoid_rewrite coq_tactics.maybe_wand_sound.
@@ -417,7 +418,8 @@ Section proofmode_classes.
   Qed.
 
   Global Instance elim_acc_wp_nonatomic {X} E α β γ e s Φ :
-    ElimAcc (X:=X) E E α β γ (WP e @ s; E {{ Φ }})
+    ElimAcc (X:=X) (fupd E E) (fupd E E)
+            α β γ (WP e @ s; E {{ Φ }})
             (λ x, WP e @ s; E {{ v, |={E}=> β x ∗ coq_tactics.maybe_wand (γ x) (Φ v) }})%I.
   Proof.
     rewrite /ElimAcc. setoid_rewrite coq_tactics.maybe_wand_sound.

theories/proofmode/class_instances_bi.v

 From stdpp Require Import nat_cancel.
 From iris.bi Require Import bi tactics.
-From iris.proofmode Require Import modality_instances classes.
+From iris.proofmode Require Import modality_instances classes ltac_tactics.
 Set Default Proof Using "Type".
 Import bi.
 
@@ -8,6 +8,33 @@ Section bi_instances.
 Context {PROP : bi}.
 Implicit Types P Q R : PROP.
 
+(* AsEmpValid *)
+Global Instance as_emp_valid_emp_valid {PROP : bi} (P : PROP) : AsEmpValid0 (bi_emp_valid P) P | 0.
+Proof. by rewrite /AsEmpValid. Qed.
+Global Instance as_emp_valid_entails {PROP : bi} (P Q : PROP) : AsEmpValid0 (P ⊢ Q) (P -∗ Q).
+Proof. split. apply bi.entails_wand. apply bi.wand_entails. Qed.
+Global Instance as_emp_valid_equiv {PROP : bi} (P Q : PROP) : AsEmpValid0 (P ≡ Q) (P ∗-∗ Q).
+Proof. split. apply bi.equiv_wand_iff. apply bi.wand_iff_equiv. Qed.
+
+Global Instance as_emp_valid_forall {A : Type} (φ : A → Prop) (P : A → PROP) :
+  (∀ x, AsEmpValid (φ x) (P x)) → AsEmpValid (∀ x, φ x) (∀ x, P x).
+Proof.
+  rewrite /AsEmpValid=>H1. split=>H2.
+  - apply bi.forall_intro=>?. apply H1, H2.
+  - intros x. apply H1. revert H2. by rewrite (bi.forall_elim x).
+Qed.
+
+(* We add a useless hypothesis [BiEmbed PROP PROP'] in order to make
+   sure this instance is not used when there is no embedding between
+   PROP and PROP'.
+   The first [`{BiEmbed PROP PROP'}] is not considered as a premise by
+   Coq TC search mechanism because the rest of the hypothesis is dependent
+   on it. *)
+Global Instance as_emp_valid_embed `{BiEmbed PROP PROP'} (φ : Prop) (P : PROP) :
+  BiEmbed PROP PROP' →
+  AsEmpValid0 φ P → AsEmpValid φ ⎡P⎤.
+Proof. rewrite /AsEmpValid0 /AsEmpValid=> _ ->. rewrite embed_emp_valid //. Qed.
+
 (* FromAffinely *)
 Global Instance from_affinely_affine P : Affine P → FromAffinely P P.
 Proof. intros. by rewrite /FromAffinely affinely_elim. Qed.
@@ -813,35 +840,37 @@ Global Instance add_modal_embed_bupd_goal `{BiEmbedBUpd PROP PROP'}
   AddModal P P' (|==> ⎡Q⎤)%I → AddModal P P' ⎡|==> Q⎤.
 Proof. by rewrite /AddModal !embed_bupd. Qed.
 
-(* IntoEmbed *)
-Global Instance into_embed_embed {PROP' : bi} `{BiEmbed PROP PROP'} P :
-  IntoEmbed ⎡P⎤ P.
-Proof. by rewrite /IntoEmbed. Qed.
-
-(* AsEmpValid *)
-Global Instance as_emp_valid_emp_valid {PROP : bi} (P : PROP) : AsEmpValid0 (bi_emp_valid P) P | 0.
-Proof. by rewrite /AsEmpValid. Qed.
-Global Instance as_emp_valid_entails {PROP : bi} (P Q : PROP) : AsEmpValid0 (P ⊢ Q) (P -∗ Q).
-Proof. split. apply bi.entails_wand. apply bi.wand_entails. Qed.
-Global Instance as_emp_valid_equiv {PROP : bi} (P Q : PROP) : AsEmpValid0 (P ≡ Q) (P ∗-∗ Q).
-Proof. split. apply bi.equiv_wand_iff. apply bi.wand_iff_equiv. Qed.
+(* ElimInv *)
+Global Instance elim_inv_acc_without_close {X : Type}
+       φ Pinv Pin
+       M1 M2 α β γ Q (Q' : X → PROP) :
+  IntoAcc (X:=X) Pinv φ Pin M1 M2 α β γ →
+  ElimAcc (X:=X) M1 M2 α β γ Q Q' →
+  ElimInv φ Pinv Pin α None Q Q'.
+Proof.
+  rewrite /ElimAcc /IntoAcc /ElimInv.
+  iIntros (Hacc Helim Hφ) "(Hinv & Hin & Hcont)".
+  iApply (Helim with "[Hcont]").
+  - iIntros (x) "Hα". iApply "Hcont". iSplitL; done.
+  - iApply (Hacc with "Hinv Hin"). done.
+Qed.
 
-Global Instance as_emp_valid_forall {A : Type} (φ : A → Prop) (P : A → PROP) :
-  (∀ x, AsEmpValid (φ x) (P x)) → AsEmpValid (∀ x, φ x) (∀ x, P x).
+Global Instance elim_inv_acc_with_close {X : Type}
+       φ Pinv Pin
+       M1 M2 α β γ Q Q' :
+  IntoAcc Pinv φ Pin M1 M2 α β γ →
+  (∀ R, ElimModal True false false (M1 R) R Q Q') →
+  ElimInv (X:=X) φ Pinv Pin α (Some (λ x, β x -∗ M2 (default emp (γ x) id)))%I
+          Q (λ _, Q').
 Proof.
-  rewrite /AsEmpValid=>H1. split=>H2.
-  - apply bi.forall_intro=>?. apply H1, H2.
-  - intros x. apply H1. revert H2. by rewrite (bi.forall_elim x).
+  rewrite /ElimAcc /IntoAcc /ElimInv.
+  iIntros (Hacc Helim Hφ) "(Hinv & Hin & Hcont)".
+  iMod (Hacc with "Hinv Hin") as (x) "[Hα Hclose]"; first done.
+  iApply "Hcont". simpl. iSplitL "Hα"; done.
 Qed.
 
-(* We add a useless hypothesis [BiEmbed PROP PROP'] in order to make
-   sure this instance is not used when there is no embedding between
-   PROP and PROP'.
-   The first [`{BiEmbed PROP PROP'}] is not considered as a premise by
-   Coq TC search mechanism because the rest of the hypothesis is dependent
-   on it. *)
-Global Instance as_emp_valid_embed `{BiEmbed PROP PROP'} (φ : Prop) (P : PROP) :
-  BiEmbed PROP PROP' →
-  AsEmpValid0 φ P → AsEmpValid φ ⎡P⎤.
-Proof. rewrite /AsEmpValid0 /AsEmpValid=> _ ->. rewrite embed_emp_valid //. Qed.
+(* IntoEmbed *)
+Global Instance into_embed_embed {PROP' : bi} `{BiEmbed PROP PROP'} P :
+  IntoEmbed ⎡P⎤ P.
+Proof. by rewrite /IntoEmbed. Qed.
 End bi_instances.

theories/proofmode/class_instances_sbi.v

@@ -554,7 +554,7 @@ Proof. by rewrite /AddModal !embed_fupd. Qed.
 (* ElimAcc *)
 Global Instance elim_acc_vs `{BiFUpd PROP} {X} E1 E2 E α β γ Q :
   (* FIXME: Why %I? ElimAcc sets the right scopes! *)
-  ElimAcc (X:=X) E1 E2 α β γ
+  ElimAcc (X:=X) (fupd E1 E2) (fupd E2 E1) α β γ
           (|={E1,E}=> Q)
           (λ x, |={E2}=> (β x ∗ (coq_tactics.maybe_wand (γ x) (|={E1,E}=> Q))))%I.
 Proof.
@@ -568,35 +568,6 @@ Qed.
 (* TODO: We could have instances from "unfolded" accessors with or without
    the first binder. *)
 
-(* ElimInv *)
-Global Instance elim_inv_acc_without_close `{BiFUpd PROP} {X : Type}
-       φ Pinv Pin
-       E1 E2 α β γ Q (Q' : X → PROP) :
-  IntoAcc (X:=X) Pinv φ Pin E1 E2 α β γ →
-  ElimAcc (X:=X) E1 E2 α β γ Q Q' →
-  ElimInv φ Pinv Pin α None Q Q'.
-Proof.
-  rewrite /ElimAcc /IntoAcc /ElimInv.
-  iIntros (Hacc Helim Hφ) "(Hinv & Hin & Hcont)".
-  iApply (Helim with "[Hcont]").
-  - iIntros (x) "Hα". iApply "Hcont". iSplitL; done.
-  - iApply (Hacc with "Hinv Hin"). done.
-Qed.
-
-Global Instance elim_inv_acc_with_close `{BiFUpd PROP} {X : Type}
-       φ Pinv Pin
-       E1 E2 α β γ Q Q' :
-  IntoAcc Pinv φ Pin E1 E2 α β γ →
-  (∀ R, ElimModal True false false (|={E1,E2}=> R) R Q Q') →
-  ElimInv (X:=X) φ Pinv Pin α (Some (λ x, β x ={E2,E1}=∗ default emp (γ x) id))%I
-          Q (λ _, Q').
-Proof.
-  rewrite /ElimAcc /IntoAcc /ElimInv.
-  iIntros (Hacc Helim Hφ) "(Hinv & Hin & Hcont)".
-  iMod (Hacc with "Hinv Hin") as (x) "[Hα Hclose]"; first done.
-  iApply "Hcont". simpl. iSplitL "Hα"; done.
-Qed.
-
 (* IntoLater *)
 Global Instance into_laterN_0 only_head P : IntoLaterN only_head 0 P P.
 Proof. by rewrite /IntoLaterN /MaybeIntoLaterN. Qed.

theories/proofmode/classes.v

@@ -518,23 +518,23 @@ Hint Mode IntoInv + ! - : typeclass_instances.
     usable and general form would use telescopes and also allow binders for the
     closing view shift.  [γ] is an [option] to make it easy for ElimAcc
     instances to recognize the [emp] case and make it look nicer. *)
-Definition accessor `{BiFUpd PROP} {X : Type} (E1 E2 : coPset)
+Definition accessor {PROP : bi} {X : Type} (M1 M2 : PROP → PROP)
            (α β : X → PROP) (γ : X → option PROP) : PROP :=
-  (|={E1,E2}=> ∃ x, α x ∗ (β x ={E2,E1}=∗ default emp (γ x) id))%I.
+  M1 (∃ x, α x ∗ (β x -∗ M2 (default emp (γ x) id)))%I.
 
 (* Typeclass for assertions around which accessors can be elliminated.
-   Inputs: [Q], [α], [β], [γ]
+   Inputs: [Q], [E1], [E2], [α], [β], [γ]
    Outputs: [Q']
-   In/Out (can be an evar and will not usually be instantiated): [E1], [E2]
 
    Elliminates an accessor [accessor E1 E2 α β γ] in goal [Q'], turning the goal
    into [Q'] with a new assumption [α x]. *)
-Class ElimAcc `{BiFUpd PROP} {X : Type} E1 E2 (α β : X → PROP) (γ : X → option PROP)
+Class ElimAcc {PROP : bi} {X : Type} (M1 M2 : PROP → PROP)
+      (α β : X → PROP) (γ : X → option PROP)
       (Q : PROP) (Q' : X → PROP) :=
-  elim_acc : ((∀ x, α x -∗ Q' x) -∗ accessor E1 E2 α β γ -∗ Q).
-Arguments ElimAcc {_} {_} {_} _ _ _%I _%I _%I _%I : simpl never.
-Arguments elim_acc {_} {_} {_} _ _ _%I _%I _%I _%I {_}.
-Hint Mode ElimAcc + + ! - - ! ! ! ! - : typeclass_instances.
+  elim_acc : ((∀ x, α x -∗ Q' x) -∗ accessor M1 M2 α β γ -∗ Q).
+Arguments ElimAcc {_} {_} _%I _%I _%I _%I _%I _%I : simpl never.
+Arguments elim_acc {_} {_} _%I _%I _%I _%I _%I _%I {_}.
+Hint Mode ElimAcc + ! ! ! ! ! ! ! - : typeclass_instances.
 
 (* Turn [P] into an accessor.
    Inputs:
@@ -543,14 +543,15 @@ Hint Mode ElimAcc + + ! - - ! ! ! ! - : typeclass_instances.
    - [Pin]: additional logic assertion needed for starting the accessor.
    - [φ]: additional Coq assertion needed for starting the accessor.
    - [X] [α], [β], [γ]: the accessor parameters.
-   In/Out (can be an evar and will not usually be instantiated): [E1], [E2]
+   - [M1], [M2]: the two accessor modalities (they will typically still have
+     some evars though, e.g. for the masks)
 *)
-Class IntoAcc `{BiFUpd PROP} (Pacc : PROP) (φ : Prop) (Pin : PROP)
-      {X : Type} E1 E2 (α β : X → PROP) (γ : X → option PROP) :=
-  into_acc : φ → Pacc -∗ Pin -∗ accessor E1 E2 α β γ.
-Arguments IntoAcc {_} {_} _%I _ _%I {_} _ _ _%I _%I _%I : simpl never.
-Arguments into_acc {_} {_} _%I _ _%I {_} _ _ _%I _%I _%I {_} : simpl never.
-Hint Mode IntoAcc + - ! - - - - - - - - : typeclass_instances.
+Class IntoAcc {PROP : bi} {X : Type} (Pacc : PROP) (φ : Prop) (Pin : PROP)
+      (M1 M2 : PROP → PROP) (α β : X → PROP) (γ : X → option PROP) :=
+  into_acc : φ → Pacc -∗ Pin -∗ accessor M1 M2 α β γ.
+Arguments IntoAcc {_} {_} _%I _ _%I _%I _%I _%I _%I _%I : simpl never.
+Arguments into_acc {_} {_} _%I _ _%I _%I _%I _%I _%I _%I {_} : simpl never.
+Hint Mode IntoAcc + - ! - - - - - - - : typeclass_instances.
 
 (* The typeclass used for the [iInv] tactic.
    Input: [Pinv]