More consistent naming for `auth`.

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.

More consistent naming for `auth`.
597ec42e · Robbert Krebbers · 03f24a19 · 597ec42e · 597ec42e · 597ec42e
Commit 597ec42e authored 5 years ago by Robbert Krebbers
--- 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.

--- 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.

--- 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. }

--- 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".

--- 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 _)))=> //.

--- 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◯]".

--- 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).

--- 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.

--- 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]".

--- 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.