From 597ec42e28ec6a7eb4f235272bbcb3f3465cf069 Mon Sep 17 00:00:00 2001
From: Robbert Krebbers <mail@robbertkrebbers.nl>
Date: Fri, 24 May 2019 07:46:56 +0200
Subject: [PATCH] More consistent naming for `auth`.
MIME-Version: 1.0
Content-Type: text/plain; charset=UTF-8
Content-Transfer-Encoding: 8bit

This MR is a follow up on the renamings performed (implicitly) as part of
!215. This MR makes the following changes:

- `auth_both_frac_valid` and `auth_both_valid` are now of the same shape
  as `auth_both_frac_validN` and `auth_both_validN`. That is, both are
  now biimplications.
- The left-to-right  direction of `auth_both_frac_valid` and
  `auth_both_valid` only holds in case the camera is discrete. The
  right-to-left versions for non-discrete cameras are prefixed `_2`, the
  convention that we use throughout the development.
- Change the direction of lemmas like `auth_frag_valid` and
  `auth_auth_valid` so that it's consistent with the other lemmas. I.e.
  make sure that the ◯ and ● are always on the LHS of the biimplication.
---
 theories/algebra/auth.v              | 31 +++++++++++++++-------------
 theories/algebra/frac_auth.v         |  4 ++--
 theories/base_logic/lib/auth.v       |  4 ++--
 theories/base_logic/lib/boxes.v      |  4 ++--
 theories/base_logic/lib/gen_heap.v   |  8 +++----
 theories/base_logic/lib/proph_map.v  |  4 ++--
 theories/base_logic/lib/wsat.v       |  2 +-
 theories/heap_lang/lib/counter.v     |  8 +++----
 theories/heap_lang/lib/ticket_lock.v |  6 +++---
 theories/program_logic/ownp.v        |  8 +++----
 10 files changed, 41 insertions(+), 38 deletions(-)

diff --git a/theories/algebra/auth.v b/theories/algebra/auth.v
index ec5d2b9bf..3a1bcc81c 100644
--- a/theories/algebra/auth.v
+++ b/theories/algebra/auth.v
@@ -150,7 +150,7 @@ Proof.
   naive_solver eauto using cmra_validN_includedN.
 Qed.
 
-Lemma auth_frag_validN n a : ✓{n} a ↔ ✓{n} (◯ a).
+Lemma auth_frag_validN n a : ✓{n} (◯ a) ↔ ✓{n} a.
 Proof. done. Qed.
 Lemma auth_auth_frac_validN n q a :
   ✓{n} (●{q} a) ↔ ✓{n} q ∧ ✓{n} a.
@@ -176,26 +176,29 @@ Proof.
   rewrite auth_both_frac_validN -cmra_discrete_valid_iff frac_valid'. naive_solver.
 Qed.
 
-Lemma auth_frag_valid a : ✓ a ↔ ✓ (◯ a).
+Lemma auth_frag_valid a : ✓ (◯ a) ↔ ✓ a.
 Proof. done. Qed.
-Lemma auth_auth_frac_valid q a : ✓ q ∧ ✓ a ↔ ✓ (●{q} a).
+Lemma auth_auth_frac_valid q a : ✓ (●{q} a) ↔ ✓ q ∧ ✓ a.
 Proof.
   rewrite auth_valid_eq /=. apply and_iff_compat_l. split.
-  - intros. exists a. split; [done|].
-    split; by [apply ucmra_unit_leastN|apply cmra_valid_validN].
   - intros H'. apply cmra_valid_validN. intros n.
     by destruct (H' n) as [? [->%to_agree_injN [??]]].
+  - intros. exists a. split; [done|].
+    split; by [apply ucmra_unit_leastN|apply cmra_valid_validN].
 Qed.
-Lemma auth_auth_valid a : ✓ a ↔ ✓ (● a).
-Proof. rewrite -auth_auth_frac_valid frac_valid'. naive_solver. Qed.
-Lemma auth_both_frac_valid q a b : ✓ q → ✓ a → b ≼ a → ✓ (●{q} a ⋅ ◯ b).
+Lemma auth_auth_valid a : ✓ (● a) ↔ ✓ a.
+Proof. rewrite auth_auth_frac_valid frac_valid'. naive_solver. Qed.
+
+(* The reverse direction of the two lemmas below only holds if the camera is
+discrete. *)
+Lemma auth_both_frac_valid_2 q a b : ✓ q → ✓ a → b ≼ a → ✓ (●{q} a ⋅ ◯ b).
 Proof.
   intros Val1 Val2 Incl. rewrite auth_valid_eq /=. split; [done|].
   intros n. exists a. split; [done|]. rewrite left_id.
   split; by [apply cmra_included_includedN|apply cmra_valid_validN].
 Qed.
-Lemma auth_both_valid a b : ✓ a → b ≼ a → ✓ (● a ⋅ ◯ b).
-Proof. intros ??. by apply auth_both_frac_valid. Qed.
+Lemma auth_both_valid_2 a b : ✓ a → b ≼ a → ✓ (● a ⋅ ◯ b).
+Proof. intros ??. by apply auth_both_frac_valid_2. Qed.
 
 Lemma auth_valid_discrete `{!CmraDiscrete A} x :
   ✓ x ↔ match auth_auth_proj x with
@@ -208,7 +211,7 @@ Proof.
   setoid_rewrite <-(discrete_iff _ a).
   setoid_rewrite <-cmra_discrete_valid_iff. naive_solver eauto using O.
 Qed.
-Lemma auth_frac_valid_discrete_2 `{!CmraDiscrete A} q a b :
+Lemma auth_both_frac_valid `{!CmraDiscrete A} q a b :
   ✓ (●{q} a ⋅ ◯ b) ↔ ✓ q ∧ b ≼ a ∧ ✓ a.
 Proof.
   rewrite auth_valid_discrete /=. apply and_iff_compat_l.
@@ -216,8 +219,8 @@ Proof.
   - by intros [?[->%to_agree_inj]].
   - naive_solver.
 Qed.
-Lemma auth_valid_discrete_2 `{!CmraDiscrete A} a b : ✓ (● a ⋅ ◯ b) ↔ b ≼ a ∧ ✓ a.
-Proof. rewrite auth_frac_valid_discrete_2 frac_valid'. naive_solver. Qed.
+Lemma auth_both_valid `{!CmraDiscrete A} a b : ✓ (● a ⋅ ◯ b) ↔ b ≼ a ∧ ✓ a.
+Proof. rewrite auth_both_frac_valid frac_valid'. naive_solver. Qed.
 
 Lemma auth_cmra_mixin : CmraMixin (auth A).
 Proof.
@@ -293,7 +296,7 @@ Proof. by rewrite /op /auth_op /= left_id. Qed.
 Lemma auth_both_op a b : Auth (Some (1%Qp,to_agree a)) b ≡ ● a ⋅ ◯ b.
 Proof. by rewrite auth_both_frac_op. Qed.
 
-Lemma auth_auth_frac_op p q a: ●{p} a ⋅ ●{q} a ≡ ●{p + q} a.
+Lemma auth_auth_frac_op p q a : ●{p + q} a ≡ ●{p} a ⋅ ●{q} a.
 Proof.
   intros; split; simpl; last by rewrite left_id.
   by rewrite -Some_op pair_op agree_idemp.
diff --git a/theories/algebra/frac_auth.v b/theories/algebra/frac_auth.v
index 0706fe627..3124b4769 100644
--- a/theories/algebra/frac_auth.v
+++ b/theories/algebra/frac_auth.v
@@ -49,7 +49,7 @@ Section frac_auth.
   Lemma frac_auth_validN n a : ✓{n} a → ✓{n} (●! a ⋅ ◯! a).
   Proof. by rewrite auth_both_validN. Qed.
   Lemma frac_auth_valid a : ✓ a → ✓ (●! a ⋅ ◯! a).
-  Proof. intros. by apply auth_both_valid. Qed.
+  Proof. intros. by apply auth_both_valid_2. Qed.
 
   Lemma frac_auth_agreeN n a b : ✓{n} (●! a ⋅ ◯! b) → a ≡{n}≡ b.
   Proof.
@@ -67,7 +67,7 @@ Section frac_auth.
   Proof. by rewrite auth_both_validN /= => -[/Some_pair_includedN [_ ?] _]. Qed.
   Lemma frac_auth_included `{CmraDiscrete A} q a b :
     ✓ (●! a ⋅ ◯!{q} b) → Some b ≼ Some a.
-  Proof. by rewrite auth_valid_discrete_2 /= => -[/Some_pair_included [_ ?] _]. Qed.
+  Proof. by rewrite auth_both_valid /= => -[/Some_pair_included [_ ?] _]. Qed.
   Lemma frac_auth_includedN_total `{CmraTotal A} n q a b :
     ✓{n} (●! a ⋅ ◯!{q} b) → b ≼{n} a.
   Proof. intros. by eapply Some_includedN_total, frac_auth_includedN. Qed.
diff --git a/theories/base_logic/lib/auth.v b/theories/base_logic/lib/auth.v
index 2a6974c29..c5a8b494a 100644
--- a/theories/base_logic/lib/auth.v
+++ b/theories/base_logic/lib/auth.v
@@ -108,7 +108,7 @@ Section auth.
   Proof.
     iIntros (??) "Hφ". rewrite /auth_own /auth_ctx.
     iMod (own_alloc_strong (● f t ⋅ ◯ f t) I) as (γ) "[% [Hγ Hγ']]";
-      [done|by apply auth_valid_discrete_2|].
+      [done|by apply auth_both_valid|].
     iMod (inv_alloc N _ (auth_inv γ f φ) with "[-Hγ']") as "#?".
     { iNext. rewrite /auth_inv. iExists t. by iFrame. }
     eauto.
@@ -140,7 +140,7 @@ Section auth.
     iIntros "[Hinv Hγf]". rewrite /auth_inv /auth_own.
     iDestruct "Hinv" as (t) "[>Hγa Hφ]".
     iModIntro. iExists t.
-    iDestruct (own_valid_2 with "Hγa Hγf") as % [? ?]%auth_valid_discrete_2.
+    iDestruct (own_valid_2 with "Hγa Hγf") as % [? ?]%auth_both_valid.
     iSplit; first done. iFrame. iIntros (u b) "[% Hφ]".
     iMod (own_update_2 with "Hγa Hγf") as "[Hγa Hγf]".
     { eapply auth_update; eassumption. }
diff --git a/theories/base_logic/lib/boxes.v b/theories/base_logic/lib/boxes.v
index 597c05835..600b2ad19 100644
--- a/theories/base_logic/lib/boxes.v
+++ b/theories/base_logic/lib/boxes.v
@@ -78,7 +78,7 @@ Lemma box_own_auth_agree γ b1 b2 :
   box_own_auth γ (● Excl' b1) ∗ box_own_auth γ (◯ Excl' b2) ⊢ ⌜b1 = b2⌝.
 Proof.
   rewrite /box_own_prop -own_op own_valid prod_validI /= and_elim_l.
-  by iDestruct 1 as % [[[] [=]%leibniz_equiv] ?]%auth_valid_discrete_2.
+  by iDestruct 1 as % [[[] [=]%leibniz_equiv] ?]%auth_both_valid.
 Qed.
 
 Lemma box_own_auth_update γ b1 b2 b3 :
@@ -110,7 +110,7 @@ Proof.
   iDestruct 1 as (Φ) "[#HeqP Hf]".
   iMod (own_alloc_cofinite (● Excl' false ⋅ ◯ Excl' false,
     Some (to_agree (Next (iProp_unfold Q)))) (dom _ f))
-    as (γ) "[Hdom Hγ]"; first by (split; [apply auth_valid_discrete_2|]).
+    as (γ) "[Hdom Hγ]"; first by (split; [apply auth_both_valid|]).
   rewrite pair_split. iDestruct "Hγ" as "[[Hγ Hγ'] #HγQ]".
   iDestruct "Hdom" as % ?%not_elem_of_dom.
   iMod (inv_alloc N _ (slice_inv γ Q) with "[Hγ]") as "#Hinv".
diff --git a/theories/base_logic/lib/gen_heap.v b/theories/base_logic/lib/gen_heap.v
index cb0b414a2..13502ff5e 100644
--- a/theories/base_logic/lib/gen_heap.v
+++ b/theories/base_logic/lib/gen_heap.v
@@ -76,7 +76,7 @@ Lemma gen_heap_init `{Countable L, !gen_heapPreG L V Σ} σ :
   (|==> ∃ _ : gen_heapG L V Σ, gen_heap_ctx σ)%I.
 Proof.
   iMod (own_alloc (● to_gen_heap σ)) as (γ) "Hh".
-  { rewrite -auth_auth_valid. exact: to_gen_heap_valid. }
+  { rewrite auth_auth_valid. exact: to_gen_heap_valid. }
   iModIntro. by iExists (GenHeapG L V Σ _ _ _ γ).
 Qed.
 
@@ -105,7 +105,7 @@ Section gen_heap.
   Proof.
     apply wand_intro_r.
     rewrite mapsto_eq /mapsto_def -own_op -auth_frag_op own_valid discrete_valid.
-    f_equiv. rewrite -auth_frag_valid op_singleton singleton_valid pair_op.
+    f_equiv. rewrite auth_frag_valid op_singleton singleton_valid pair_op.
     by intros [_ ?%agree_op_invL'].
   Qed.
 
@@ -154,7 +154,7 @@ Section gen_heap.
   Proof.
     iIntros "Hσ Hl". rewrite /gen_heap_ctx mapsto_eq /mapsto_def.
     iDestruct (own_valid_2 with "Hσ Hl")
-      as %[Hl%gen_heap_singleton_included _]%auth_valid_discrete_2; auto.
+      as %[Hl%gen_heap_singleton_included _]%auth_both_valid; auto.
   Qed.
 
   Lemma gen_heap_update σ l v1 v2 :
@@ -162,7 +162,7 @@ Section gen_heap.
   Proof.
     iIntros "Hσ Hl". rewrite /gen_heap_ctx mapsto_eq /mapsto_def.
     iDestruct (own_valid_2 with "Hσ Hl")
-      as %[Hl%gen_heap_singleton_included _]%auth_valid_discrete_2.
+      as %[Hl%gen_heap_singleton_included _]%auth_both_valid.
     iMod (own_update_2 with "Hσ Hl") as "[Hσ Hl]".
     { eapply auth_update, singleton_local_update,
         (exclusive_local_update _ (1%Qp, to_agree (v2:leibnizC _)))=> //.
diff --git a/theories/base_logic/lib/proph_map.v b/theories/base_logic/lib/proph_map.v
index 939ee3059..c1a990384 100644
--- a/theories/base_logic/lib/proph_map.v
+++ b/theories/base_logic/lib/proph_map.v
@@ -111,7 +111,7 @@ Lemma proph_map_init `{Countable P, !proph_mapPreG P V PVS} pvs ps :
   (|==> ∃ _ : proph_mapG P V PVS, proph_map_ctx pvs ps)%I.
 Proof.
   iMod (own_alloc (● to_proph_map ∅)) as (γ) "Hh".
-  { rewrite -auth_auth_valid. exact: to_proph_map_valid. }
+  { rewrite auth_auth_valid. exact: to_proph_map_valid. }
   iModIntro. iExists (ProphMapG P V PVS _ _ _ γ), ∅. iSplit; last by iFrame.
   iPureIntro. split =>//.
 Qed.
@@ -153,7 +153,7 @@ Section proph_map.
   Proof.
     iIntros "[HR Hp]". iDestruct "HR" as (R) "[HP H●]". iDestruct "HP" as %[Hres Hdom].
     rewrite /proph_map_ctx proph_eq /proph_def.
-    iDestruct (own_valid_2 with "H● Hp") as %[HR%proph_map_singleton_included _]%auth_valid_discrete_2.
+    iDestruct (own_valid_2 with "H● Hp") as %[HR%proph_map_singleton_included _]%auth_both_valid.
     assert (vs = v :: proph_list_resolves pvs p) as ->.
     { rewrite (Hres p vs HR). simpl. by rewrite decide_True. }
     iMod (own_update_2 with "H● Hp") as "[H● H◯]".
diff --git a/theories/base_logic/lib/wsat.v b/theories/base_logic/lib/wsat.v
index e09b59f9d..d6538bff8 100644
--- a/theories/base_logic/lib/wsat.v
+++ b/theories/base_logic/lib/wsat.v
@@ -198,7 +198,7 @@ Lemma wsat_alloc `{!invPreG Σ} : (|==> ∃ _ : invG Σ, wsat ∗ ownE ⊤)%I.
 Proof.
   iIntros.
   iMod (own_alloc (● (∅ : gmap positive _))) as (γI) "HI";
-    first by rewrite -auth_auth_valid.
+    first by rewrite auth_auth_valid.
   iMod (own_alloc (CoPset ⊤)) as (γE) "HE"; first done.
   iMod (own_alloc (GSet ∅)) as (γD) "HD"; first done.
   iModIntro; iExists (WsatG _ _ _ _ γI γE γD).
diff --git a/theories/heap_lang/lib/counter.v b/theories/heap_lang/lib/counter.v
index cb65f706b..cde2c0b41 100644
--- a/theories/heap_lang/lib/counter.v
+++ b/theories/heap_lang/lib/counter.v
@@ -37,7 +37,7 @@ Section mono_proof.
   Proof.
     iIntros (Φ) "_ HΦ". rewrite -wp_fupd /newcounter /=. wp_lam. wp_alloc l as "Hl".
     iMod (own_alloc (● (O:mnat) ⋅ ◯ (O:mnat))) as (γ) "[Hγ Hγ']";
-      first by apply auth_valid_discrete_2.
+      first by apply auth_both_valid.
     iMod (inv_alloc N _ (mcounter_inv γ l) with "[Hl Hγ]").
     { iNext. iExists 0%nat. by iFrame. }
     iModIntro. iApply "HΦ". rewrite /mcounter; eauto 10.
@@ -54,7 +54,7 @@ Section mono_proof.
     wp_bind (CAS _ _ _). iInv N as (c') ">[Hγ Hl]".
     destruct (decide (c' = c)) as [->|].
     - iDestruct (own_valid_2 with "Hγ Hγf")
-        as %[?%mnat_included _]%auth_valid_discrete_2.
+        as %[?%mnat_included _]%auth_both_valid.
       iMod (own_update_2 with "Hγ Hγf") as "[Hγ Hγf]".
       { apply auth_update, (mnat_local_update _ _ (S c)); auto. }
       wp_cas_suc. iModIntro. iSplitL "Hl Hγ".
@@ -75,7 +75,7 @@ Section mono_proof.
     rewrite /read /=. wp_lam. iInv N as (c) ">[Hγ Hl]".
     wp_load.
     iDestruct (own_valid_2 with "Hγ Hγf")
-      as %[?%mnat_included _]%auth_valid_discrete_2.
+      as %[?%mnat_included _]%auth_both_valid.
     iMod (own_update_2 with "Hγ Hγf") as "[Hγ Hγf]".
     { apply auth_update, (mnat_local_update _ _ c); auto. }
     iModIntro. iSplitL "Hl Hγ"; [iNext; iExists c; by iFrame|].
@@ -115,7 +115,7 @@ Section contrib_spec.
   Proof.
     iIntros (Φ) "_ HΦ". rewrite -wp_fupd /newcounter /=. wp_lam. wp_alloc l as "Hl".
     iMod (own_alloc (●! O%nat ⋅ ◯! 0%nat)) as (γ) "[Hγ Hγ']";
-      first by apply auth_valid_discrete_2.
+      first by apply auth_both_valid.
     iMod (inv_alloc N _ (ccounter_inv γ l) with "[Hl Hγ]").
     { iNext. iExists 0%nat. by iFrame. }
     iModIntro. iApply "HΦ". rewrite /ccounter_ctx /ccounter; eauto 10.
diff --git a/theories/heap_lang/lib/ticket_lock.v b/theories/heap_lang/lib/ticket_lock.v
index 681b7a22b..a3c601070 100644
--- a/theories/heap_lang/lib/ticket_lock.v
+++ b/theories/heap_lang/lib/ticket_lock.v
@@ -76,7 +76,7 @@ Section proof.
     iIntros (Φ) "HR HΦ". rewrite -wp_fupd. wp_lam.
     wp_alloc ln as "Hln". wp_alloc lo as "Hlo".
     iMod (own_alloc (● (Excl' 0%nat, GSet ∅) ⋅ ◯ (Excl' 0%nat, GSet ∅))) as (γ) "[Hγ Hγ']".
-    { by apply auth_valid_discrete_2. }
+    { by apply auth_both_valid. }
     iMod (inv_alloc _ _ (lock_inv γ lo ln R) with "[-HΦ]").
     { iNext. rewrite /lock_inv.
       iExists 0%nat, 0%nat. iFrame. iLeft. by iFrame. }
@@ -141,14 +141,14 @@ Section proof.
     iInv N as (o' n) "(>Hlo & >Hln & >Hauth & Haown)".
     wp_load.
     iDestruct (own_valid_2 with "Hauth Hγo") as
-      %[[<-%Excl_included%leibniz_equiv _]%prod_included _]%auth_valid_discrete_2.
+      %[[<-%Excl_included%leibniz_equiv _]%prod_included _]%auth_both_valid.
     iModIntro. iSplitL "Hlo Hln Hauth Haown".
     { iNext. iExists o, n. by iFrame. }
     wp_pures.
     iInv N as (o' n') "(>Hlo & >Hln & >Hauth & Haown)".
     iApply wp_fupd. wp_store.
     iDestruct (own_valid_2 with "Hauth Hγo") as
-      %[[<-%Excl_included%leibniz_equiv _]%prod_included _]%auth_valid_discrete_2.
+      %[[<-%Excl_included%leibniz_equiv _]%prod_included _]%auth_both_valid.
     iDestruct "Haown" as "[[Hγo' _]|Haown]".
     { iDestruct (own_valid_2 with "Hγo Hγo'") as %[[] ?]. }
     iMod (own_update_2 with "Hauth Hγo") as "[Hauth Hγo]".
diff --git a/theories/program_logic/ownp.v b/theories/program_logic/ownp.v
index 0bbe407ee..4b4b4a9a2 100644
--- a/theories/program_logic/ownp.v
+++ b/theories/program_logic/ownp.v
@@ -54,7 +54,7 @@ Proof.
   intros Hwp. apply (wp_adequacy Σ _).
   iIntros (? κs).
   iMod (own_alloc (● (Excl' σ) ⋅ ◯ (Excl' σ))) as (γσ) "[Hσ Hσf]";
-    first by apply auth_valid_discrete_2.
+    first by apply auth_both_valid.
   iModIntro. iExists (λ σ κs, own γσ (● (Excl' σ)))%I.
   iFrame "Hσ".
   iApply (Hwp (OwnPG _ _ _ _ γσ)). rewrite /ownP. iFrame.
@@ -70,14 +70,14 @@ Proof.
   intros Hwp Hsteps. eapply (wp_invariance Σ Λ s e σ1 t2 σ2 _)=> //.
   iIntros (? κs κs').
   iMod (own_alloc (● (Excl' σ1) ⋅ ◯ (Excl' σ1))) as (γσ) "[Hσ Hσf]";
-    first by apply auth_valid_discrete_2.
+    first by apply auth_both_valid.
   iExists (λ σ κs' _, own γσ (● (Excl' σ)))%I, (λ _, True%I).
   iFrame "Hσ".
   iMod (Hwp (OwnPG _ _ _ _ γσ) with "[Hσf]") as "[$ H]";
     first by rewrite /ownP; iFrame.
   iIntros "!> Hσ". iMod "H" as (σ2') "[Hσf %]". rewrite /ownP.
   iDestruct (own_valid_2 with "Hσ Hσf")
-    as %[Hp%Excl_included _]%auth_valid_discrete_2; simplify_eq; auto.
+    as %[Hp%Excl_included _]%auth_both_valid; simplify_eq; auto.
 Qed.
 
 
@@ -91,7 +91,7 @@ Section lifting.
   Lemma ownP_eq σ1 σ2 κs n : state_interp σ1 κs n -∗ ownP σ2 -∗ ⌜σ1 = σ2⌝.
   Proof.
     iIntros "Hσ● Hσ◯". rewrite /ownP.
-    iDestruct (own_valid_2 with "Hσ● Hσ◯") as %[Hps _]%auth_valid_discrete_2.
+    iDestruct (own_valid_2 with "Hσ● Hσ◯") as %[Hps _]%auth_both_valid.
     by pose proof (leibniz_equiv _ _ (Excl_included _ _ Hps)) as ->.
   Qed.
   Lemma ownP_state_twice σ1 σ2 : ownP σ1 ∗ ownP σ2 ⊢ False.
-- 
GitLab