From 6ae49bd9d3d5a750c864bc982084cdcb9d10f603 Mon Sep 17 00:00:00 2001
From: Ralf Jung <jung@mpi-sws.org>
Date: Tue, 24 Apr 2018 19:46:15 +0200
Subject: [PATCH] rename InvOpener -> AccElim
---
.../base_logic/lib/cancelable_invariants.v | 4 +--
theories/base_logic/lib/invariants.v | 4 +--
theories/base_logic/lib/na_invariants.v | 4 +--
theories/program_logic/weakestpre.v | 14 ++++-----
theories/proofmode/class_instances_sbi.v | 12 ++++----
theories/proofmode/classes.v | 30 +++++++++----------
6 files changed, 34 insertions(+), 34 deletions(-)
diff --git a/theories/base_logic/lib/cancelable_invariants.v b/theories/base_logic/lib/cancelable_invariants.v
index 2ce16d7f6..f3fff6412 100644
--- a/theories/base_logic/lib/cancelable_invariants.v
+++ b/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.
diff --git a/theories/base_logic/lib/invariants.v b/theories/base_logic/lib/invariants.v
index 81def8c6a..785558bfc 100644
--- a/theories/base_logic/lib/invariants.v
+++ b/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.
diff --git a/theories/base_logic/lib/na_invariants.v b/theories/base_logic/lib/na_invariants.v
index a1c6d8950..810fe5cb3 100644
--- a/theories/base_logic/lib/na_invariants.v
+++ b/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.
diff --git a/theories/program_logic/weakestpre.v b/theories/program_logic/weakestpre.v
index e671a953f..c847355b1 100644
--- a/theories/program_logic/weakestpre.v
+++ b/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".
diff --git a/theories/proofmode/class_instances_sbi.v b/theories/proofmode/class_instances_sbi.v
index fdfdb69a8..79b177e77 100644
--- a/theories/proofmode/class_instances_sbi.v
+++ b/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".
diff --git a/theories/proofmode/classes.v b/theories/proofmode/classes.v
index ed0e4d354..2ab4f51e9 100644
--- a/theories/proofmode/classes.v
+++ b/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:
--
GitLab