rename InvOpener -> AccElim

theories/base_logic/lib/cancelable_invariants.v

@@ -93,10 +93,10 @@ Section proofs.
   Global Instance into_inv_cinv N γ P : IntoInv (cinv N γ P) N.
 
   Global Instance elim_inv_cinv E N γ P p Q Q' :
-    InvOpener E (E∖↑N) (▷ P ∗ cinv_own γ p) (▷ P) None Q Q' →
+    AccElim E (E∖↑N) (▷ P ∗ cinv_own γ p) (▷ P) None Q Q' →
     ElimInv (↑N ⊆ E) (cinv N γ P) (cinv_own γ p) (▷ P ∗ cinv_own γ p) Q Q'.
   Proof.
-    rewrite /ElimInv /InvOpener. iIntros (Helim ?) "(#Hinv & Hown & Hcont)".
+    rewrite /ElimInv /AccElim. iIntros (Helim ?) "(#Hinv & Hown & Hcont)".
     iApply (Helim with "Hcont"). clear Helim. rewrite -assoc.
     iApply (cinv_open with "Hinv"); done.
   Qed.

theories/base_logic/lib/invariants.v

@@ -110,10 +110,10 @@ Qed.
 Global Instance into_inv_inv N P : IntoInv (inv N P) N.
 
 Global Instance elim_inv_inv E N P Q Q' :
-  InvOpener E (E∖↑N) (▷ P) (▷ P) None Q Q' →
+  AccElim E (E∖↑N) (▷ P) (▷ P) None Q Q' →
   ElimInv (↑N ⊆ E) (inv N P) True (▷ P) Q Q'.
 Proof.
-  rewrite /ElimInv /InvOpener. iIntros (Hopener ?) "(#Hinv & _ & Hcont)".
+  rewrite /ElimInv /AccElim. iIntros (Hopener ?) "(#Hinv & _ & Hcont)".
   iApply (Hopener with "Hcont"). iApply inv_open; done.
 Qed.
 

theories/base_logic/lib/na_invariants.v

@@ -114,12 +114,12 @@ Section proofs.
   Global Instance into_inv_na p N P : IntoInv (na_inv p N P) N.
 
   Global Instance elim_inv_na p F E N P Q Q':
-    InvOpener E E (▷ P ∗ na_own p (F ∖ ↑ N)) (▷ P ∗ na_own p (F ∖ ↑ N))
+    AccElim E E (▷ P ∗ na_own p (F ∖ ↑ N)) (▷ P ∗ na_own p (F ∖ ↑ N))
               (Some (na_own p F)) Q Q' →
     ElimInv (↑N ⊆ E ∧ ↑N ⊆ F) (na_inv p N P) (na_own p F)
       (▷ P ∗ na_own p (F∖↑N)) Q Q'.
   Proof.
-    rewrite /ElimInv /InvOpener. iIntros (Helim (?&?)) "(#Hinv & Hown & Hcont)".
+    rewrite /ElimInv /AccElim. iIntros (Helim (?&?)) "(#Hinv & Hown & Hcont)".
     iApply (Helim with "Hcont"). clear Helim. rewrite -assoc /=.
     iApply (na_inv_open with "Hinv"); done.
   Qed.

theories/program_logic/weakestpre.v

@@ -405,22 +405,22 @@ Section proofmode_classes.
     AddModal (|={E}=> P) P (WP e @ s; E {{ Φ }}).
   Proof. by rewrite /AddModal fupd_frame_r wand_elim_r fupd_wp. Qed.
 
-  Global Instance inv_opener_wp E1 E2 P P' (P'' : option _) e s Φ :
+  Global Instance acc_elim_wp E1 E2 P P' (P'' : option _) e s Φ :
     Atomic (stuckness_to_atomicity s) e →
-    InvOpener E1 E2 P P' P'' (WP e @ s; E1 {{ Φ }})
+    AccElim E1 E2 P P' P'' (WP e @ s; E1 {{ Φ }})
               (WP e @ s; E2 {{ v, P' ∗ coq_tactics.maybe_wand P'' (Φ v) }})%I.
   Proof.
-    intros ?. rewrite /InvOpener. setoid_rewrite coq_tactics.maybe_wand_sound.
+    intros ?. rewrite /AccElim. setoid_rewrite coq_tactics.maybe_wand_sound.
     iIntros "Hinner >[HP Hclose]".
     iApply (wp_wand with "[Hinner HP]"); first by iApply "Hinner".
     iIntros (v) "[HP HΦ]". iApply "HΦ". by iApply "Hclose".
   Qed.
 
-  Global Instance inv_opener_wp_nonatomic E P P' (P'' : option _) e s Φ :
-    InvOpener E E P P' P'' (WP e @ s; E {{ Φ }})
-              (WP e @ s; E {{ v, P' ∗ coq_tactics.maybe_wand P'' (Φ v) }})%I.
+  Global Instance acc_elim_wp_nonatomic E P P' (P'' : option _) e s Φ :
+    AccElim E E P P' P'' (WP e @ s; E {{ Φ }})
+            (WP e @ s; E {{ v, P' ∗ coq_tactics.maybe_wand P'' (Φ v) }})%I.
   Proof.
-    rewrite /InvOpener. setoid_rewrite coq_tactics.maybe_wand_sound.
+    rewrite /AccElim. setoid_rewrite coq_tactics.maybe_wand_sound.
     iIntros "Hinner >[HP Hclose]". iApply wp_fupd.
     iApply (wp_wand with "[Hinner HP]"); first by iApply "Hinner".
     iIntros (v) "[HP HΦ]". iApply "HΦ". by iApply "Hclose".

theories/proofmode/class_instances_sbi.v

@@ -551,13 +551,13 @@ Global Instance add_modal_embed_fupd_goal `{BiEmbedFUpd PROP PROP'}
   AddModal P P' (|={E1,E2}=> ⎡Q⎤)%I → AddModal P P' ⎡|={E1,E2}=> Q⎤.
 Proof. by rewrite /AddModal !embed_fupd. Qed.
 
-(* InvOpener *)
-Global Instance inv_opener_vs `{BiFUpd PROP} E1 E2 E P P' (P'' : option PROP) Q :
-  (* FIXME: Why %I? ElimInv should set the right scopes! *)
-  InvOpener E1 E2 P P' P''
-            (|={E1,E}=> Q) (|={E2}=> (P' ∗ (coq_tactics.maybe_wand P'' (|={E1,E}=> Q))))%I.
+(* AccElim *)
+Global Instance acc_elim_vs `{BiFUpd PROP} E1 E2 E P P' (P'' : option PROP) Q :
+  (* FIXME: Why %I? AccElim sets the right scopes! *)
+  AccElim E1 E2 P P' P''
+          (|={E1,E}=> Q) (|={E2}=> (P' ∗ (coq_tactics.maybe_wand P'' (|={E1,E}=> Q))))%I.
 Proof.
-  rewrite /InvOpener coq_tactics.maybe_wand_sound.
+  rewrite /AccElim coq_tactics.maybe_wand_sound.
   iIntros "Hinner >[HP Hclose]".
   iMod ("Hinner" with "HP") as "[HP Hfin]".
   iMod ("Hclose" with "HP") as "HP''". by iApply "Hfin".

theories/proofmode/classes.v

@@ -513,21 +513,21 @@ Class IntoInv {PROP : bi} (P: PROP) (N: namespace).
 Arguments IntoInv {_} _%I _.
 Hint Mode IntoInv + ! - : typeclass_instances.
 
-(** Typeclass for assertions around which invariants can be opened.
-    Inputs: [Q]
-    Outputs: [E1], [E2], [P], [P'], [Q']
-
-    Transforms the goal [Q] into the goal [Q'] where additional assumptions [P]
-    are available, obtaining may require accessing invariants. Later, [P'] has
-    to be given up again to close these invariants again, which will
-    produce [P''].  If [P''] is None, that signifies [emp] and will be used to
-    make the goal shown to the user nicer (i.e., no unnecessary hypothesis is
-    added) *)
-Class InvOpener `{BiFUpd PROP} E1 E2 (P P' : PROP) (P'' : option PROP) (Q Q' : PROP) :=
-  inv_opener : ((P -∗ Q') -∗ (|={E1,E2}=> P ∗ (P' ={E2,E1}=∗ default emp P'' id)) -∗ Q).
-Arguments InvOpener {_} {_} _ _ _%I _%I _%I _%I : simpl never.
-Arguments inv_opener {_} {_} _ _ _%I _%I _%I _%I {_}.
-Hint Mode InvOpener + + - - - - - ! - : typeclass_instances.
+(** Typeclass for assertions around which accessors can be elliminated.
+    Inputs: [Q], [P], [P'], [P'']
+    Outputs: [Q']
+    In/Out (can be an evar and will not usually be instantiated): [E1], [E2]
+
+    Elliminates an accessor [|={E1,E2}=> P ∗ (P' ={E2,E1}=∗ P'')] in goal [Q'],
+    turning the goal into [Q'] with a new assumption [P].  If [P''] is None,
+    that signifies [emp] and will be used to make the goal shown to the user
+    nicer (i.e., no unnecessary hypothesis is added). [φ] is a Coq-level
+    side-condition that will be attempted to be discharged by solve_ndisj. *)
+Class AccElim `{BiFUpd PROP} E1 E2 (P P' : PROP) (P'' : option PROP) (Q Q' : PROP) :=
+  acc_elim : ((P -∗ Q') -∗ (|={E1,E2}=> P ∗ (P' ={E2,E1}=∗ default emp P'' id)) -∗ Q).
+Arguments AccElim {_} {_} _ _ _%I _%I _%I _%I : simpl never.
+Arguments acc_elim {_} {_} _ _ _%I _%I _%I _%I {_}.
+Hint Mode AccElim + + - - ! ! ! ! - : typeclass_instances.
 
 (* Input: [Pinv]
    Arguments: