From a8fe7b7fe0797894d2a5e6f29838a43afb710aa2 Mon Sep 17 00:00:00 2001
From: Ralf Jung <jung@mpi-sws.org>
Date: Tue, 11 Feb 2020 09:32:12 +0100
Subject: [PATCH] rename _access -> _acc

---
 tests/ipm_paper.v                             |  2 +-
 theories/base_logic/lib/auth.v                |  6 +++---
 .../base_logic/lib/cancelable_invariants.v    | 12 +++++------
 theories/base_logic/lib/invariants.v          | 20 +++++++++----------
 theories/base_logic/lib/na_invariants.v       |  4 ++--
 theories/base_logic/lib/sts.v                 |  8 ++++----
 theories/bi/lib/counterexamples.v             |  4 ++--
 7 files changed, 28 insertions(+), 28 deletions(-)

diff --git a/tests/ipm_paper.v b/tests/ipm_paper.v
index 19a59fa93..5dad15580 100644
--- a/tests/ipm_paper.v
+++ b/tests/ipm_paper.v
@@ -112,7 +112,7 @@ Lemma wp_inv_open `{!irisG Î› Î£} N E P e Î¦ :
   inv N P âˆ— (â–· P -âˆ— WP e @ E âˆ– â†‘N {{ v, â–· P âˆ— Î¦ v }}) âŠ¢ WP e @ E {{ Î¦ }}.
 Proof.
   iIntros (??) "[#Hinv Hwp]".
-  iMod (inv_access E N P with "Hinv") as "[HP Hclose]"=>//.
+  iMod (inv_acc E N P with "Hinv") as "[HP Hclose]"=>//.
   iApply wp_wand_r; iSplitL "HP Hwp"; [by iApply "Hwp"|].
   iIntros (v) "[HP $]". by iApply "Hclose".
 Qed.
diff --git a/theories/base_logic/lib/auth.v b/theories/base_logic/lib/auth.v
index 6bb76bced..9e14b4cb3 100644
--- a/theories/base_logic/lib/auth.v
+++ b/theories/base_logic/lib/auth.v
@@ -147,7 +147,7 @@ Section auth.
     iModIntro. iFrame. iExists u. iFrame.
   Qed.
 
-  Lemma auth_access E N Î³ a :
+  Lemma auth_acc E N Î³ a :
     â†‘N âŠ† E â†’
     auth_ctx Î³ N f Ï† âˆ— auth_own Î³ a ={E,Eâˆ–â†‘N}=âˆ— âˆƒ t,
       âŒœa â‰¼ f tâŒ âˆ— â–· Ï† t âˆ— âˆ€ u b,
@@ -155,7 +155,7 @@ Section auth.
   Proof using Type*.
     iIntros (?) "[#? HÎ³f]". rewrite /auth_ctx. iInv N as "Hinv" "Hclose".
     (* The following is essentially a very trivial composition of the accessors
-       [auth_inv_acc] and [inv_access] -- but since we don't have any good support
+       [auth_inv_acc] and [inv_acc] -- but since we don't have any good support
        for that currently, this gets more tedious than it should, with us having
        to unpack and repack various proofs.
        TODO: Make this mostly automatic, by supporting "opening accessors
@@ -166,4 +166,4 @@ Section auth.
   Qed.
 End auth.
 
-Arguments auth_access {_ _ _} [_] {_} [_] _ _ _ _ _ _ _.
+Arguments auth_acc {_ _ _} [_] {_} [_] _ _ _ _ _ _ _.
diff --git a/theories/base_logic/lib/cancelable_invariants.v b/theories/base_logic/lib/cancelable_invariants.v
index 03716dd2a..38f1a16b7 100644
--- a/theories/base_logic/lib/cancelable_invariants.v
+++ b/theories/base_logic/lib/cancelable_invariants.v
@@ -109,13 +109,13 @@ Section proofs.
   Qed.
 
   (*** Accessors *)
-  Lemma cinv_access_strong E N Î³ p P :
+  Lemma cinv_acc_strong E N Î³ p P :
     â†‘N âŠ† E â†’
     cinv N Î³ P -âˆ— (cinv_own Î³ p ={E,Eâˆ–â†‘N}=âˆ—
     â–· P âˆ— cinv_own Î³ p âˆ— (âˆ€ E' : coPset, â–· P âˆ¨ cinv_own Î³ 1 ={E',â†‘N âˆª E'}=âˆ— True)).
   Proof.
     iIntros (?) "Hinv Hown".
-    iPoseProof (inv_access (â†‘ N) N with "Hinv") as "H"; first done.
+    iPoseProof (inv_acc (â†‘ N) N with "Hinv") as "H"; first done.
     rewrite difference_diag_L.
     iPoseProof (fupd_mask_frame_r _ _ (E âˆ– â†‘ N) with "H") as "H"; first set_solver.
     rewrite left_id_L -union_difference_L //. iMod "H" as "[[$ | >Hown'] H]".
@@ -126,12 +126,12 @@ Section proofs.
     - iDestruct (cinv_own_1_l with "Hown' Hown") as %[].
   Qed.
 
-  Lemma cinv_access E N Î³ p P :
+  Lemma cinv_acc E N Î³ p P :
     â†‘N âŠ† E â†’
     cinv N Î³ P -âˆ— cinv_own Î³ p ={E,Eâˆ–â†‘N}=âˆ— â–· P âˆ— cinv_own Î³ p âˆ— (â–· P ={Eâˆ–â†‘N,E}=âˆ— True).
   Proof.
     iIntros (?) "#Hinv HÎ³".
-    iMod (cinv_access_strong with "Hinv HÎ³") as "($ & $ & H)"; first done.
+    iMod (cinv_acc_strong with "Hinv HÎ³") as "($ & $ & H)"; first done.
     iIntros "!> HP".
     rewrite {2}(union_difference_L (â†‘N) E)=> //.
     iApply "H". by iLeft.
@@ -141,7 +141,7 @@ Section proofs.
   Lemma cinv_cancel E N Î³ P : â†‘N âŠ† E â†’ cinv N Î³ P -âˆ— cinv_own Î³ 1 ={E}=âˆ— â–· P.
   Proof.
     iIntros (?) "#Hinv HÎ³".
-    iMod (cinv_access_strong with "Hinv HÎ³") as "($ & HÎ³ & H)"; first done.
+    iMod (cinv_acc_strong with "Hinv HÎ³") as "($ & HÎ³ & H)"; first done.
     rewrite {2}(union_difference_L (â†‘N) E)=> //.
     iApply "H". by iRight.
   Qed.
@@ -155,7 +155,7 @@ Section proofs.
   Proof.
     rewrite /IntoAcc /accessor. iIntros (?) "#Hinv Hown".
     rewrite exist_unit -assoc.
-    iApply (cinv_access with "Hinv"); done.
+    iApply (cinv_acc with "Hinv"); done.
   Qed.
 End proofs.
 
diff --git a/theories/base_logic/lib/invariants.v b/theories/base_logic/lib/invariants.v
index 0a5cf4aca..337e27bfd 100644
--- a/theories/base_logic/lib/invariants.v
+++ b/theories/base_logic/lib/invariants.v
@@ -27,7 +27,7 @@ Section inv.
   Definition own_inv (N : namespace) (P : iProp Î£) : iProp Î£ :=
     (âˆƒ i, âŒœi âˆˆ (â†‘N:coPset)âŒ âˆ§ ownI i P)%I.
 
-  Lemma own_inv_access E N P :
+  Lemma own_inv_acc E N P :
     â†‘N âŠ† E â†’ own_inv N P ={E,Eâˆ–â†‘N}=âˆ— â–· P âˆ— (â–· P ={Eâˆ–â†‘N,E}=âˆ— True).
   Proof.
     rewrite uPred_fupd_eq /uPred_fupd_def. iDestruct 1 as (i) "[Hi #HiP]".
@@ -81,7 +81,7 @@ Section inv.
   Lemma own_inv_to_inv M P: own_inv M P  -âˆ— inv M P.
   Proof.
     iIntros "#I". rewrite inv_eq. iIntros (E H).
-    iPoseProof (own_inv_access with "I") as "H"; eauto.
+    iPoseProof (own_inv_acc with "I") as "H"; eauto.
   Qed.
 
   (** ** Public API of invariants *)
@@ -97,7 +97,7 @@ Section inv.
   Global Instance inv_persistent N P : Persistent (inv N P).
   Proof. rewrite inv_eq. apply _. Qed.
 
-  Lemma inv_acc N P Q:
+  Lemma inv_alter N P Q:
     inv N P -âˆ— â–· â–¡ (P -âˆ— Q âˆ— (Q -âˆ— P)) -âˆ— inv N Q.
   Proof.
     rewrite inv_eq. iIntros "#HI #Acc !>" (E H).
@@ -108,7 +108,7 @@ Section inv.
 
   Lemma inv_iff N P Q : â–· â–¡ (P â†” Q) -âˆ— inv N P -âˆ— inv N Q.
   Proof.
-    iIntros "#HPQ #HI". iApply (inv_acc with "HI").
+    iIntros "#HPQ #HI". iApply (inv_alter with "HI").
     iIntros "!> !# HP". iSplitL "HP".
     - by iApply "HPQ".
     - iIntros "HQ". by iApply "HPQ".
@@ -127,7 +127,7 @@ Section inv.
     iApply own_inv_to_inv. done.
   Qed.
 
-  Lemma inv_access E N P :
+  Lemma inv_acc E N P :
     â†‘N âŠ† E â†’ inv N P ={E,Eâˆ–â†‘N}=âˆ— â–· P âˆ— (â–· P ={Eâˆ–â†‘N,E}=âˆ— True).
   Proof.
     rewrite inv_eq /inv_def; iIntros (?) "#HI". by iApply "HI".
@@ -146,11 +146,11 @@ Section inv.
   Qed.
 
   (** ** Derived properties *)
-  Lemma inv_access_strong E N P :
+  Lemma inv_acc_strong E N P :
     â†‘N âŠ† E â†’ inv N P ={E,Eâˆ–â†‘N}=âˆ— â–· P âˆ— âˆ€ E', â–· P ={E',â†‘N âˆª E'}=âˆ— True.
   Proof.
     iIntros (?) "Hinv".
-    iPoseProof (inv_access (â†‘ N) N with "Hinv") as "H"; first done.
+    iPoseProof (inv_acc (â†‘ N) N with "Hinv") as "H"; first done.
     rewrite difference_diag_L.
     iPoseProof (fupd_mask_frame_r _ _ (E âˆ– â†‘ N) with "H") as "H"; first set_solver.
     rewrite left_id_L -union_difference_L //. iMod "H" as "[$ H]"; iModIntro.
@@ -159,16 +159,16 @@ Section inv.
     by rewrite left_id_L.
   Qed.
 
-  Lemma inv_access_timeless E N P `{!Timeless P} :
+  Lemma inv_acc_timeless E N P `{!Timeless P} :
     â†‘N âŠ† E â†’ inv N P ={E,Eâˆ–â†‘N}=âˆ— P âˆ— (P ={Eâˆ–â†‘N,E}=âˆ— True).
   Proof.
-    iIntros (?) "Hinv". iMod (inv_access with "Hinv") as "[>HP Hclose]"; auto.
+    iIntros (?) "Hinv". iMod (inv_acc with "Hinv") as "[>HP Hclose]"; auto.
     iIntros "!> {$HP} HP". iApply "Hclose"; auto.
   Qed.
 
   Lemma inv_sep_l N P Q : inv N (P âˆ— Q) -âˆ— inv N P.
   Proof.
-    iIntros "#HI". iApply inv_acc; eauto.
+    iIntros "#HI". iApply inv_alter; eauto.
     iIntros "!> !# [$ $] $".
   Qed.
 
diff --git a/theories/base_logic/lib/na_invariants.v b/theories/base_logic/lib/na_invariants.v
index f291a9d10..40b9d0671 100644
--- a/theories/base_logic/lib/na_invariants.v
+++ b/theories/base_logic/lib/na_invariants.v
@@ -91,7 +91,7 @@ Section proofs.
     iNext. iLeft. by iFrame.
   Qed.
 
-  Lemma na_inv_access p E F N P :
+  Lemma na_inv_acc p E F N P :
     â†‘N âŠ† E â†’ â†‘N âŠ† F â†’
     na_inv p N P -âˆ— na_own p F ={E}=âˆ— â–· P âˆ— na_own p (Fâˆ–â†‘N) âˆ—
                        (â–· P âˆ— na_own p (Fâˆ–â†‘N) ={E}=âˆ— na_own p F).
@@ -121,6 +121,6 @@ Section proofs.
   Proof.
     rewrite /IntoAcc /accessor. iIntros ((?&?)) "#Hinv Hown".
     rewrite exist_unit -assoc /=.
-    iApply (na_inv_access with "Hinv"); done.
+    iApply (na_inv_acc with "Hinv"); done.
   Qed.
 End proofs.
diff --git a/theories/base_logic/lib/sts.v b/theories/base_logic/lib/sts.v
index 24964273b..6b6b748e4 100644
--- a/theories/base_logic/lib/sts.v
+++ b/theories/base_logic/lib/sts.v
@@ -150,7 +150,7 @@ Section sts.
       âŒœsts.steps (s, T) (s', T')âŒ âˆ— â–· Ï† s' ={E}=âˆ— â–· sts_inv Î³ Ï† âˆ— sts_own Î³ s' T'.
   Proof. by apply sts_inv_accS. Qed.
 
-  Lemma sts_accessS Ï† E N Î³ S T :
+  Lemma sts_accS Ï† E N Î³ S T :
     â†‘N âŠ† E â†’
     sts_ctx Î³ N Ï† âˆ— sts_ownS Î³ S T ={E,Eâˆ–â†‘N}=âˆ— âˆƒ s,
       âŒœs âˆˆ SâŒ âˆ— â–· Ï† s âˆ— âˆ€ s' T',
@@ -158,7 +158,7 @@ Section sts.
   Proof.
     iIntros (?) "[#? HÎ³f]". rewrite /sts_ctx. iInv N as "Hinv" "Hclose".
     (* The following is essentially a very trivial composition of the accessors
-       [sts_inv_acc] and [inv_access] -- but since we don't have any good support
+       [sts_inv_acc] and [inv_acc] -- but since we don't have any good support
        for that currently, this gets more tedious than it should, with us having
        to unpack and repack various proofs.
        TODO: Make this mostly automatic, by supporting "opening accessors
@@ -168,12 +168,12 @@ Section sts.
     iMod ("HclSts" $! s' T' with "H") as "(Hinv & ?)". by iMod ("Hclose" with "Hinv").
   Qed.
 
-  Lemma sts_access Ï† E N Î³ s0 T :
+  Lemma sts_acc Ï† E N Î³ s0 T :
     â†‘N âŠ† E â†’
     sts_ctx Î³ N Ï† âˆ— sts_own Î³ s0 T ={E,Eâˆ–â†‘N}=âˆ— âˆƒ s,
       âŒœsts.frame_steps T s0 sâŒ âˆ— â–· Ï† s âˆ— âˆ€ s' T',
       âŒœsts.steps (s, T) (s', T')âŒ âˆ— â–· Ï† s' ={Eâˆ–â†‘N,E}=âˆ— sts_own Î³ s' T'.
-  Proof. by apply sts_accessS. Qed.
+  Proof. by apply sts_accS. Qed.
 End sts.
 
 Typeclasses Opaque sts_own sts_ownS sts_inv sts_ctx.
diff --git a/theories/bi/lib/counterexamples.v b/theories/bi/lib/counterexamples.v
index d268871d0..594799bf0 100644
--- a/theories/bi/lib/counterexamples.v
+++ b/theories/bi/lib/counterexamples.v
@@ -308,7 +308,7 @@ Module linear2. Section linear2.
   Context (gname : Type) (cinv : gname â†’ PROP â†’ PROP) (cinv_own : gname â†’ PROP).
   Hypothesis cinv_alloc : âˆ€ E,
     fupd E E (âˆƒ Î³, âˆ€ P, â–· P -âˆ— fupd E E (cinv Î³ P âˆ— cinv_own Î³))%I.
-  Hypothesis cinv_access : âˆ€ P Î³,
+  Hypothesis cinv_acc : âˆ€ P Î³,
     cinv Î³ P -âˆ— cinv_own Î³ -âˆ— fupd M1 M0 (â–· P âˆ— cinv_own Î³ âˆ— (â–· P -âˆ— fupd M0 M1 emp)).
 
   (** Some general lemmas and proof mode compatibility. *)
@@ -335,7 +335,7 @@ Module linear2. Section linear2.
     iIntros "HP".
     iMod cinv_alloc as (Î³) "Hmkinv".
     iMod ("Hmkinv" $! True%I with "[//]") as "[Hinv Htok]".
-    iMod (cinv_access with "Hinv Htok") as "(Htrue & Htok & Hclose)".
+    iMod (cinv_acc with "Hinv Htok") as "(Htrue & Htok & Hclose)".
     iApply "Hclose". done.
   Qed.
 End linear2. End linear2.
-- 
GitLab