From de990a190b0da91847c7e3152d1644edb3e40209 Mon Sep 17 00:00:00 2001
From: Robbert Krebbers <mail@robbertkrebbers.nl>
Date: Wed, 21 Oct 2020 11:58:45 +0200
Subject: [PATCH 1/3] =?UTF-8?q?Add=20lemmas=20for=20validity=20of=20`?=
 =?UTF-8?q?=E2=97=8F{=5F}=20=5F=20=E2=8B=85=20=E2=97=8F{=5F}=20=5F`=20for?=
 =?UTF-8?q?=20both=20view=20and=20auth.?=
MIME-Version: 1.0
Content-Type: text/plain; charset=UTF-8
Content-Transfer-Encoding: 8bit

The diff might be hard to read, because I had to change the order. The following
lemmas have been added:

```coq
Lemma view_auth_frac_op_validN n q1 q2 a1 a2 :
  ✓{n} (●V{q1} a1 ⋅ ●V{q2} a2) ↔ ✓ (q1 + q2)%Qp ∧ a1 ≡{n}≡ a2 ∧ rel n a1 ε.
Lemma view_auth_op_validN n a1 a2 : ✓{n} (●V a1 ⋅ ●V a2) ↔ False.

Lemma view_auth_frac_op_valid q1 q2 a1 a2 :
  ✓ (●V{q1} a1 ⋅ ●V{q2} a2) ↔ ✓ (q1 + q2)%Qp ∧ a1 ≡ a2 ∧ ∀ n, rel n a1 ε.
Lemma view_auth_op_valid a1 a2 : ✓ (●V a1 ⋅ ●V a2) ↔ False.

Lemma auth_auth_frac_op_validN n q1 q2 a1 a2 :
  ✓{n} (●{q1} a1 ⋅ ●{q2} a2) ↔ ✓ (q1 + q2)%Qp ∧ a1 ≡{n}≡ a2 ∧ ✓{n} a1.
Lemma auth_auth_op_validN n a1 a2 : ✓{n} (● a1 ⋅ ● a2) ↔ False.

Lemma auth_auth_frac_op_valid q1 q2 a1 a2 :
  ✓ (●{q1} a1 ⋅ ●{q2} a2) ↔ ✓ (q1 + q2)%Qp ∧ a1 ≡ a2 ∧ ✓ a1.
Lemma auth_auth_op_valid a1 a2 : ✓ (● a1 ⋅ ● a2) ↔ False.
```
---
 theories/algebra/auth.v | 120 ++++++++++++++++++++---------------
 theories/algebra/view.v | 137 ++++++++++++++++++++++++----------------
 2 files changed, 151 insertions(+), 106 deletions(-)

diff --git a/theories/algebra/auth.v b/theories/algebra/auth.v
index fc6f1806f..6ad65d62f 100644
--- a/theories/algebra/auth.v
+++ b/theories/algebra/auth.v
@@ -100,11 +100,71 @@ Section auth.
   Global Instance auth_frag_inj : Inj (≡) (≡) (@auth_frag A).
   Proof. rewrite /auth_frag. apply _. Qed.
 
+  Global Instance auth_ofe_discrete : OfeDiscrete A → OfeDiscrete (authO A).
+  Proof. apply _. Qed.
+  Global Instance auth_auth_discrete q a :
+    Discrete a → Discrete (ε : A) → Discrete (●{q} a).
+  Proof. rewrite /auth_auth. apply _. Qed.
+  Global Instance auth_frag_discrete a : Discrete a → Discrete (◯ a).
+  Proof. rewrite /auth_frag. apply _. Qed.
+  Global Instance auth_cmra_discrete : CmraDiscrete A → CmraDiscrete (authR A).
+  Proof. apply _. Qed.
+
+  (** Operation *)
+  Lemma auth_auth_frac_op p q a : ●{p + q} a ≡ ●{p} a ⋅ ●{q} a.
+  Proof. apply view_auth_frac_op. Qed.
+  Global Instance auth_auth_frac_is_op q q1 q2 a :
+    IsOp q q1 q2 → IsOp' (●{q} a) (●{q1} a) (●{q2} a).
+  Proof. rewrite /auth_auth. apply _. Qed.
+
+  Lemma auth_frag_op a b : ◯ (a ⋅ b) = ◯ a ⋅ ◯ b.
+  Proof. apply view_frag_op. Qed.
+  Lemma auth_frag_mono a b : a ≼ b → ◯ a ≼ ◯ b.
+  Proof. apply view_frag_mono. Qed.
+  Lemma auth_frag_core a : core (◯ a) = ◯ (core a).
+  Proof. apply view_frag_core. Qed.
+  Global Instance auth_frag_core_id a : CoreId a → CoreId (◯ a).
+  Proof. rewrite /auth_frag. apply _. Qed.
+  Global Instance auth_frag_is_op a b1 b2 :
+    IsOp a b1 b2 → IsOp' (◯ a) (◯ b1) (◯ b2).
+  Proof. rewrite /auth_frag. apply _. Qed.
+  Global Instance auth_frag_sep_homomorphism :
+    MonoidHomomorphism op op (≡) (@auth_frag A).
+  Proof. rewrite /auth_frag. apply _. Qed.
+
+  Lemma big_opL_auth_frag {B} (g : nat → B → A) (l : list B) :
+    (◯ [^op list] k↦x ∈ l, g k x) ≡ [^op list] k↦x ∈ l, ◯ (g k x).
+  Proof. apply (big_opL_commute _). Qed.
+  Lemma big_opM_auth_frag `{Countable K} {B} (g : K → B → A) (m : gmap K B) :
+    (◯ [^op map] k↦x ∈ m, g k x) ≡ [^op map] k↦x ∈ m, ◯ (g k x).
+  Proof. apply (big_opM_commute _). Qed.
+  Lemma big_opS_auth_frag `{Countable B} (g : B → A) (X : gset B) :
+    (◯ [^op set] x ∈ X, g x) ≡ [^op set] x ∈ X, ◯ (g x).
+  Proof. apply (big_opS_commute _). Qed.
+  Lemma big_opMS_auth_frag `{Countable B} (g : B → A) (X : gmultiset B) :
+    (◯ [^op mset] x ∈ X, g x) ≡ [^op mset] x ∈ X, ◯ (g x).
+  Proof. apply (big_opMS_commute _). Qed.
+
+  (** Validity *)
+  Lemma auth_auth_frac_op_invN n p a q b : ✓{n} (●{p} a ⋅ ●{q} b) → a ≡{n}≡ b.
+  Proof. apply view_auth_frac_op_invN. Qed.
+  Lemma auth_auth_frac_op_inv p a q b : ✓ (●{p} a ⋅ ●{q} b) → a ≡ b.
+  Proof. apply view_auth_frac_op_inv. Qed.
+  Lemma auth_auth_frac_op_inv_L `{!LeibnizEquiv A} q a p b :
+    ✓ (●{p} a ⋅ ●{q} b) → a = b.
+  Proof. by apply view_auth_frac_op_inv_L. Qed.
+
   Lemma auth_auth_frac_validN n q a : ✓{n} (●{q} a) ↔ ✓{n} q ∧ ✓{n} a.
   Proof. by rewrite view_auth_frac_validN auth_view_rel_unit. Qed.
   Lemma auth_auth_validN n a : ✓{n} (● a) ↔ ✓{n} a.
   Proof. by rewrite view_auth_validN auth_view_rel_unit. Qed.
 
+  Lemma auth_auth_frac_op_validN n q1 q2 a1 a2 :
+    ✓{n} (●{q1} a1 ⋅ ●{q2} a2) ↔ ✓ (q1 + q2)%Qp ∧ a1 ≡{n}≡ a2 ∧ ✓{n} a1.
+  Proof. by rewrite view_auth_frac_op_validN auth_view_rel_unit. Qed.
+  Lemma auth_auth_op_validN n a1 a2 : ✓{n} (● a1 ⋅ ● a2) ↔ False.
+  Proof. rewrite view_auth_frac_op_validN. naive_solver. Qed.
+
   (** The following lemmas are also stated as implications, which can be used
   to force [apply] to use the lemma in the right direction. *)
   Lemma auth_frag_validN n b : ✓{n} (◯ b) ↔ ✓{n} b.
@@ -137,6 +197,15 @@ Section auth.
     by setoid_rewrite auth_view_rel_unit.
   Qed.
 
+  Lemma auth_auth_frac_op_valid q1 q2 a1 a2 :
+    ✓ (●{q1} a1 ⋅ ●{q2} a2) ↔ ✓ (q1 + q2)%Qp ∧ a1 ≡ a2 ∧ ✓ a1.
+  Proof.
+    rewrite view_auth_frac_op_valid !cmra_valid_validN.
+    by setoid_rewrite auth_view_rel_unit.
+  Qed.
+  Lemma auth_auth_op_valid a1 a2 : ✓ (● a1 ⋅ ● a2) ↔ False.
+  Proof. rewrite auth_auth_frac_op_valid. naive_solver. Qed.
+
   (** The following lemmas are also stated as implications, which can be used
   to force [apply] to use the lemma in the right direction. *)
   Lemma auth_frag_valid b : ✓ (◯ b) ↔ ✓ b.
@@ -191,57 +260,6 @@ Section auth.
     ✓ (● a ⋅ ◯ b) ↔ b ≼ a ∧ ✓ a.
   Proof. rewrite auth_both_frac_valid_discrete frac_valid'. naive_solver. Qed.
 
-  Global Instance auth_ofe_discrete : OfeDiscrete A → OfeDiscrete (authO A).
-  Proof. apply _. Qed.
-  Global Instance auth_auth_discrete q a :
-    Discrete a → Discrete (ε : A) → Discrete (●{q} a).
-  Proof. rewrite /auth_auth. apply _. Qed.
-  Global Instance auth_frag_discrete a : Discrete a → Discrete (◯ a).
-  Proof. rewrite /auth_frag. apply _. Qed.
-  Global Instance auth_cmra_discrete : CmraDiscrete A → CmraDiscrete (authR A).
-  Proof. apply _. Qed.
-
-  Lemma auth_auth_frac_op p q a : ●{p + q} a ≡ ●{p} a ⋅ ●{q} a.
-  Proof. apply view_auth_frac_op. Qed.
-  Lemma auth_auth_frac_op_invN n p a q b : ✓{n} (●{p} a ⋅ ●{q} b) → a ≡{n}≡ b.
-  Proof. apply view_auth_frac_op_invN. Qed.
-  Lemma auth_auth_frac_op_inv p a q b : ✓ (●{p} a ⋅ ●{q} b) → a ≡ b.
-  Proof. apply view_auth_frac_op_inv. Qed.
-  Lemma auth_auth_frac_op_inv_L `{!LeibnizEquiv A} q a p b :
-    ✓ (●{p} a ⋅ ●{q} b) → a = b.
-  Proof. by apply view_auth_frac_op_inv_L. Qed.
-  Global Instance auth_auth_frac_is_op q q1 q2 a :
-    IsOp q q1 q2 → IsOp' (●{q} a) (●{q1} a) (●{q2} a).
-  Proof. rewrite /auth_auth. apply _. Qed.
-
-  Lemma auth_frag_op a b : ◯ (a ⋅ b) = ◯ a ⋅ ◯ b.
-  Proof. apply view_frag_op. Qed.
-  Lemma auth_frag_mono a b : a ≼ b → ◯ a ≼ ◯ b.
-  Proof. apply view_frag_mono. Qed.
-  Lemma auth_frag_core a : core (◯ a) = ◯ (core a).
-  Proof. apply view_frag_core. Qed.
-  Global Instance auth_frag_core_id a : CoreId a → CoreId (◯ a).
-  Proof. rewrite /auth_frag. apply _. Qed.
-  Global Instance auth_frag_is_op a b1 b2 :
-    IsOp a b1 b2 → IsOp' (◯ a) (◯ b1) (◯ b2).
-  Proof. rewrite /auth_frag. apply _. Qed.
-  Global Instance auth_frag_sep_homomorphism :
-    MonoidHomomorphism op op (≡) (@auth_frag A).
-  Proof. rewrite /auth_frag. apply _. Qed.
-
-  Lemma big_opL_auth_frag {B} (g : nat → B → A) (l : list B) :
-    (◯ [^op list] k↦x ∈ l, g k x) ≡ [^op list] k↦x ∈ l, ◯ (g k x).
-  Proof. apply (big_opL_commute _). Qed.
-  Lemma big_opM_auth_frag `{Countable K} {B} (g : K → B → A) (m : gmap K B) :
-    (◯ [^op map] k↦x ∈ m, g k x) ≡ [^op map] k↦x ∈ m, ◯ (g k x).
-  Proof. apply (big_opM_commute _). Qed.
-  Lemma big_opS_auth_frag `{Countable B} (g : B → A) (X : gset B) :
-    (◯ [^op set] x ∈ X, g x) ≡ [^op set] x ∈ X, ◯ (g x).
-  Proof. apply (big_opS_commute _). Qed.
-  Lemma big_opMS_auth_frag `{Countable B} (g : B → A) (X : gmultiset B) :
-    (◯ [^op mset] x ∈ X, g x) ≡ [^op mset] x ∈ X, ◯ (g x).
-  Proof. apply (big_opMS_commute _). Qed.
-
   (** Inclusion *)
   Lemma auth_auth_frac_includedN n p1 p2 a1 a2 b :
     ●{p1} a1 ≼{n} ●{p2} a2 ⋅ ◯ b ↔ (p1 ≤ p2)%Qc ∧ a1 ≡{n}≡ a2.
diff --git a/theories/algebra/view.v b/theories/algebra/view.v
index 89954f77e..ab718ce3b 100644
--- a/theories/algebra/view.v
+++ b/theories/algebra/view.v
@@ -204,47 +204,6 @@ Section cmra.
       | None => ∃ a, rel n a (view_frag_proj x)
       end := eq_refl _.
 
-  Lemma view_auth_frac_validN n q a : ✓{n} (●V{q} a) ↔ ✓{n} q ∧ rel n a ε.
-  Proof.
-    rewrite view_validN_eq /=. apply and_iff_compat_l. split; [|by eauto].
-    by intros [? [->%(inj to_agree) ?]].
-  Qed.
-  Lemma view_auth_validN n a : ✓{n} (●V a) ↔ rel n a ε.
-  Proof.
-    rewrite view_auth_frac_validN -cmra_discrete_valid_iff frac_valid'. naive_solver.
-  Qed.
-  Lemma view_frag_validN n b : ✓{n} (◯V b) ↔ ∃ a, rel n a b.
-  Proof. done. Qed.
-  Lemma view_both_frac_validN n q a b :
-    ✓{n} (●V{q} a ⋅ ◯V b) ↔ ✓{n} q ∧ rel n a b.
-  Proof.
-    rewrite view_validN_eq /=. apply and_iff_compat_l.
-    setoid_rewrite (left_id _ _ b). split; [|by eauto].
-    by intros [?[->%(inj to_agree)]].
-  Qed.
-  Lemma view_both_validN n a b : ✓{n} (●V a ⋅ ◯V b) ↔ rel n a b.
-  Proof.
-    rewrite view_both_frac_validN -cmra_discrete_valid_iff frac_valid'. naive_solver.
-  Qed.
-
-  Lemma view_auth_frac_valid q a : ✓ (●V{q} a) ↔ ✓ q ∧ ∀ n, rel n a ε.
-  Proof.
-    rewrite view_valid_eq /=. apply and_iff_compat_l. split; [|by eauto].
-    intros H n. by destruct (H n) as [? [->%(inj to_agree) ?]].
-  Qed.
-  Lemma view_auth_valid a : ✓ (●V a) ↔ ∀ n, rel n a ε.
-  Proof. rewrite view_auth_frac_valid frac_valid'. naive_solver. Qed.
-  Lemma view_frag_valid b : ✓ (◯V b) ↔ ∀ n, ∃ a, rel n a b.
-  Proof. done. Qed.
-  Lemma view_both_frac_valid q a b : ✓ (●V{q} a ⋅ ◯V b) ↔ ✓ q ∧ ∀ n, rel n a b.
-  Proof.
-    rewrite view_valid_eq /=. apply and_iff_compat_l.
-    setoid_rewrite (left_id _ _ b). split; [|by eauto].
-    intros H n. by destruct (H n) as [?[->%(inj to_agree)]].
-  Qed.
-  Lemma view_both_valid a b : ✓ (●V a ⋅ ◯V b) ↔ ∀ n, rel n a b.
-  Proof. rewrite view_both_frac_valid frac_valid'. naive_solver. Qed.
-
   Lemma view_cmra_mixin : CmraMixin (view rel).
   Proof.
     apply (iso_cmra_mixin_restrict
@@ -304,25 +263,12 @@ Section cmra.
   Qed.
   Canonical Structure viewUR := UcmraT (view rel) view_ucmra_mixin.
 
+  (** Operation *)
   Lemma view_auth_frac_op p1 p2 a : ●V{p1 + p2} a ≡ ●V{p1} a ⋅ ●V{p2} a.
   Proof.
     intros; split; simpl; last by rewrite left_id.
     by rewrite -Some_op -pair_op agree_idemp.
   Qed.
-  Lemma view_auth_frac_op_invN n p1 a1 p2 a2 :
-    ✓{n} (●V{p1} a1 ⋅ ●V{p2} a2) → a1 ≡{n}≡ a2.
-  Proof.
-    rewrite /op /view_op /= left_id -Some_op -pair_op view_validN_eq /=.
-    intros (?&?& Eq &?). apply (inj to_agree), agree_op_invN. by rewrite Eq.
-  Qed.
-  Lemma view_auth_frac_op_inv p1 a1 p2 a2 : ✓ (●V{p1} a1 ⋅ ●V{p2} a2) → a1 ≡ a2.
-  Proof.
-    intros ?. apply equiv_dist. intros n.
-    by eapply view_auth_frac_op_invN, cmra_valid_validN.
-  Qed.
-  Lemma view_auth_frac_op_inv_L `{!LeibnizEquiv A} p1 a1 p2 a2 :
-    ✓ (●V{p1} a1 ⋅ ●V{p2} a2) → a1 = a2.
-  Proof. by intros ?%view_auth_frac_op_inv%leibniz_equiv. Qed.
   Global Instance view_auth_frac_is_op q q1 q2 a :
     IsOp q q1 q2 → IsOp' (●V{q} a) (●V{q1} a) (●V{q2} a).
   Proof. rewrite /IsOp' /IsOp => ->. by rewrite -view_auth_frac_op. Qed.
@@ -355,6 +301,87 @@ Section cmra.
     (◯V [^op mset] x ∈ X, g x) ≡ [^op mset] x ∈ X, ◯V (g x).
   Proof. apply (big_opMS_commute _). Qed.
 
+  (** Validity *)
+  Lemma view_auth_frac_op_invN n p1 a1 p2 a2 :
+    ✓{n} (●V{p1} a1 ⋅ ●V{p2} a2) → a1 ≡{n}≡ a2.
+  Proof.
+    rewrite /op /view_op /= left_id -Some_op -pair_op view_validN_eq /=.
+    intros (?&?& Eq &?). apply (inj to_agree), agree_op_invN. by rewrite Eq.
+  Qed.
+  Lemma view_auth_frac_op_inv p1 a1 p2 a2 : ✓ (●V{p1} a1 ⋅ ●V{p2} a2) → a1 ≡ a2.
+  Proof.
+    intros ?. apply equiv_dist. intros n.
+    by eapply view_auth_frac_op_invN, cmra_valid_validN.
+  Qed.
+  Lemma view_auth_frac_op_inv_L `{!LeibnizEquiv A} p1 a1 p2 a2 :
+    ✓ (●V{p1} a1 ⋅ ●V{p2} a2) → a1 = a2.
+  Proof. by intros ?%view_auth_frac_op_inv%leibniz_equiv. Qed.
+
+  Lemma view_auth_frac_validN n q a : ✓{n} (●V{q} a) ↔ ✓{n} q ∧ rel n a ε.
+  Proof.
+    rewrite view_validN_eq /=. apply and_iff_compat_l. split; [|by eauto].
+    by intros [? [->%(inj to_agree) ?]].
+  Qed.
+  Lemma view_auth_validN n a : ✓{n} (●V a) ↔ rel n a ε.
+  Proof.
+    rewrite view_auth_frac_validN -cmra_discrete_valid_iff frac_valid'. naive_solver.
+  Qed.
+
+  Lemma view_auth_frac_op_validN n q1 q2 a1 a2 :
+    ✓{n} (●V{q1} a1 ⋅ ●V{q2} a2) ↔ ✓ (q1 + q2)%Qp ∧ a1 ≡{n}≡ a2 ∧ rel n a1 ε.
+  Proof.
+    split.
+    - intros Hval. assert (a1 ≡{n}≡ a2) as Ha by eauto using view_auth_frac_op_invN.
+      revert Hval. rewrite Ha -view_auth_frac_op view_auth_frac_validN. naive_solver.
+    - intros (?&->&?). by rewrite -view_auth_frac_op view_auth_frac_validN.
+  Qed.
+  Lemma view_auth_op_validN n a1 a2 : ✓{n} (●V a1 ⋅ ●V a2) ↔ False.
+  Proof. rewrite view_auth_frac_op_validN. naive_solver. Qed.
+
+  Lemma view_frag_validN n b : ✓{n} (◯V b) ↔ ∃ a, rel n a b.
+  Proof. done. Qed.
+
+  Lemma view_both_frac_validN n q a b :
+    ✓{n} (●V{q} a ⋅ ◯V b) ↔ ✓{n} q ∧ rel n a b.
+  Proof.
+    rewrite view_validN_eq /=. apply and_iff_compat_l.
+    setoid_rewrite (left_id _ _ b). split; [|by eauto].
+    by intros [?[->%(inj to_agree)]].
+  Qed.
+  Lemma view_both_validN n a b : ✓{n} (●V a ⋅ ◯V b) ↔ rel n a b.
+  Proof.
+    rewrite view_both_frac_validN -cmra_discrete_valid_iff frac_valid'. naive_solver.
+  Qed.
+
+  Lemma view_auth_frac_valid q a : ✓ (●V{q} a) ↔ ✓ q ∧ ∀ n, rel n a ε.
+  Proof.
+    rewrite view_valid_eq /=. apply and_iff_compat_l. split; [|by eauto].
+    intros H n. by destruct (H n) as [? [->%(inj to_agree) ?]].
+  Qed.
+  Lemma view_auth_valid a : ✓ (●V a) ↔ ∀ n, rel n a ε.
+  Proof. rewrite view_auth_frac_valid frac_valid'. naive_solver. Qed.
+
+  Lemma view_auth_frac_op_valid q1 q2 a1 a2 :
+    ✓ (●V{q1} a1 ⋅ ●V{q2} a2) ↔ ✓ (q1 + q2)%Qp ∧ a1 ≡ a2 ∧ ∀ n, rel n a1 ε.
+  Proof.
+    rewrite !cmra_valid_validN equiv_dist. setoid_rewrite view_auth_frac_op_validN.
+    setoid_rewrite <-cmra_discrete_valid_iff. naive_solver.
+  Qed.
+  Lemma view_auth_op_valid a1 a2 : ✓ (●V a1 ⋅ ●V a2) ↔ False.
+  Proof. rewrite view_auth_frac_op_valid. naive_solver. Qed.
+
+  Lemma view_frag_valid b : ✓ (◯V b) ↔ ∀ n, ∃ a, rel n a b.
+  Proof. done. Qed.
+
+  Lemma view_both_frac_valid q a b : ✓ (●V{q} a ⋅ ◯V b) ↔ ✓ q ∧ ∀ n, rel n a b.
+  Proof.
+    rewrite view_valid_eq /=. apply and_iff_compat_l.
+    setoid_rewrite (left_id _ _ b). split; [|by eauto].
+    intros H n. by destruct (H n) as [?[->%(inj to_agree)]].
+  Qed.
+  Lemma view_both_valid a b : ✓ (●V a ⋅ ◯V b) ↔ ∀ n, rel n a b.
+  Proof. rewrite view_both_frac_valid frac_valid'. naive_solver. Qed.
+
   (** Inclusion *)
   Lemma view_auth_frac_includedN n p1 p2 a1 a2 b :
     ●V{p1} a1 ≼{n} ●V{p2} a2 ⋅ ◯V b ↔ (p1 ≤ p2)%Qc ∧ a1 ≡{n}≡ a2.
-- 
GitLab


From 034d1d23fc28246eff9e2555d77a62234f3ef8da Mon Sep 17 00:00:00 2001
From: Robbert Krebbers <mail@robbertkrebbers.nl>
Date: Wed, 21 Oct 2020 12:22:35 +0200
Subject: [PATCH 2/3] Add similar lemmas for `gmap_view`.
MIME-Version: 1.0
Content-Type: text/plain; charset=UTF-8
Content-Transfer-Encoding: 8bit

This also required changing the order a bit.

```coq
Lemma gmap_view_auth_frac_op_valid q1 q2 m1 m2 :
  ✓ (gmap_view_auth q1 m1 ⋅ gmap_view_auth q2 m2) ↔ ✓ (q1 + q2)%Qp ∧ m1 ≡ m2.
Lemma gmap_view_auth_op_valid m1 m2 :
  ✓ (gmap_view_auth 1 m1 ⋅ gmap_view_auth 1 m2) ↔ False.
```
---
 theories/algebra/lib/gmap_view.v | 39 ++++++++++++++++++++------------
 1 file changed, 25 insertions(+), 14 deletions(-)

diff --git a/theories/algebra/lib/gmap_view.v b/theories/algebra/lib/gmap_view.v
index 879c029e9..3a94b25a8 100644
--- a/theories/algebra/lib/gmap_view.v
+++ b/theories/algebra/lib/gmap_view.v
@@ -108,6 +108,9 @@ Section rel.
     - intros k'. rewrite !lookup_insert_None. naive_solver.
   Qed.
 
+  Local Lemma gmap_view_rel_unit n m : gmap_view_rel n m ε.
+  Proof. apply: map_Forall_empty. Qed.
+
   Local Lemma gmap_view_rel_discrete :
     OfeDiscrete V → ViewRelDiscrete gmap_view_rel.
   Proof.
@@ -174,18 +177,13 @@ Section lemmas.
   Qed.
 
   (** Composition and validity *)
-  Lemma gmap_view_auth_frac_valid m q : ✓ gmap_view_auth q m ↔ ✓ q.
-  Proof.
-    rewrite view_auth_frac_valid. split; first by naive_solver.
-    intros. split; first done.
-    intros n l ? Hl. rewrite lookup_empty in Hl. done.
-  Qed.
-  Lemma gmap_view_auth_valid m : ✓ gmap_view_auth 1 m.
-  Proof. rewrite gmap_view_auth_frac_valid. done. Qed.
-
   Lemma gmap_view_auth_frac_op p q m :
     gmap_view_auth (p + q) m ≡ gmap_view_auth p m ⋅ gmap_view_auth q m.
   Proof. apply view_auth_frac_op. Qed.
+  Global Instance gmap_view_auth_frac_is_op q q1 q2 m :
+    IsOp q q1 q2 → IsOp' (gmap_view_auth q m) (gmap_view_auth q1 m) (gmap_view_auth q2 m).
+  Proof. rewrite /gmap_view_auth. apply _. Qed.
+
   Lemma gmap_view_auth_frac_op_invN n p m1 q m2 :
     ✓{n} (gmap_view_auth p m1 ⋅ gmap_view_auth q m2) → m1 ≡{n}≡ m2.
   Proof. apply view_auth_frac_op_invN. Qed.
@@ -195,9 +193,22 @@ Section lemmas.
   Lemma gmap_view_auth_frac_op_inv_L `{!LeibnizEquiv V} q m1 p m2 :
     ✓ (gmap_view_auth p m1 ⋅ gmap_view_auth q m2) → m1 = m2.
   Proof. apply view_auth_frac_op_inv_L, _. Qed.
-  Global Instance gmap_view_auth_frac_is_op q q1 q2 m :
-    IsOp q q1 q2 → IsOp' (gmap_view_auth q m) (gmap_view_auth q1 m) (gmap_view_auth q2 m).
-  Proof. rewrite /gmap_view_auth. apply _. Qed.
+
+  Lemma gmap_view_auth_frac_valid m q : ✓ gmap_view_auth q m ↔ ✓ q.
+  Proof.
+    rewrite view_auth_frac_valid. intuition eauto using gmap_view_rel_unit.
+  Qed.
+  Lemma gmap_view_auth_valid m : ✓ gmap_view_auth 1 m.
+  Proof. rewrite gmap_view_auth_frac_valid. done. Qed.
+
+  Lemma gmap_view_auth_frac_op_valid q1 q2 m1 m2 :
+    ✓ (gmap_view_auth q1 m1 ⋅ gmap_view_auth q2 m2) ↔ ✓ (q1 + q2)%Qp ∧ m1 ≡ m2.
+  Proof.
+    rewrite view_auth_frac_op_valid. intuition eauto using gmap_view_rel_unit.
+  Qed.
+  Lemma gmap_view_auth_op_valid m1 m2 :
+    ✓ (gmap_view_auth 1 m1 ⋅ gmap_view_auth 1 m2) ↔ False.
+  Proof. rewrite gmap_view_auth_frac_op_valid. naive_solver. Qed.
 
   Lemma gmap_view_frag_validN n k dq v : ✓{n} gmap_view_frag k dq v ↔ ✓ dq.
   Proof.
@@ -256,8 +267,8 @@ Section lemmas.
     rewrite view_both_frac_valid. setoid_rewrite gmap_view_rel_lookup.
     split=>[[Hq Hm]|[Hq Hm]].
     - split; first done. split.
-      +  apply (Hm 0%nat).
-      +  apply equiv_dist=>n. apply Hm.
+      + apply (Hm 0%nat).
+      + apply equiv_dist=>n. apply Hm.
     - split; first done. split.
       + apply Hm.
       + revert n. apply equiv_dist. apply Hm.
-- 
GitLab


From 53d1f7f13d8e39ecd8017d74a259e94807b3466e Mon Sep 17 00:00:00 2001
From: Robbert Krebbers <mail@robbertkrebbers.nl>
Date: Wed, 21 Oct 2020 13:09:44 +0200
Subject: [PATCH 3/3] Make better use of `view` lemmas.

---
 theories/algebra/auth.v          | 4 ++--
 theories/algebra/lib/gmap_view.v | 2 +-
 2 files changed, 3 insertions(+), 3 deletions(-)

diff --git a/theories/algebra/auth.v b/theories/algebra/auth.v
index 6ad65d62f..449882765 100644
--- a/theories/algebra/auth.v
+++ b/theories/algebra/auth.v
@@ -163,7 +163,7 @@ Section auth.
     ✓{n} (●{q1} a1 ⋅ ●{q2} a2) ↔ ✓ (q1 + q2)%Qp ∧ a1 ≡{n}≡ a2 ∧ ✓{n} a1.
   Proof. by rewrite view_auth_frac_op_validN auth_view_rel_unit. Qed.
   Lemma auth_auth_op_validN n a1 a2 : ✓{n} (● a1 ⋅ ● a2) ↔ False.
-  Proof. rewrite view_auth_frac_op_validN. naive_solver. Qed.
+  Proof. apply view_auth_op_validN. Qed.
 
   (** The following lemmas are also stated as implications, which can be used
   to force [apply] to use the lemma in the right direction. *)
@@ -204,7 +204,7 @@ Section auth.
     by setoid_rewrite auth_view_rel_unit.
   Qed.
   Lemma auth_auth_op_valid a1 a2 : ✓ (● a1 ⋅ ● a2) ↔ False.
-  Proof. rewrite auth_auth_frac_op_valid. naive_solver. Qed.
+  Proof. apply view_auth_op_valid. Qed.
 
   (** The following lemmas are also stated as implications, which can be used
   to force [apply] to use the lemma in the right direction. *)
diff --git a/theories/algebra/lib/gmap_view.v b/theories/algebra/lib/gmap_view.v
index 3a94b25a8..7cc89e990 100644
--- a/theories/algebra/lib/gmap_view.v
+++ b/theories/algebra/lib/gmap_view.v
@@ -208,7 +208,7 @@ Section lemmas.
   Qed.
   Lemma gmap_view_auth_op_valid m1 m2 :
     ✓ (gmap_view_auth 1 m1 ⋅ gmap_view_auth 1 m2) ↔ False.
-  Proof. rewrite gmap_view_auth_frac_op_valid. naive_solver. Qed.
+  Proof. apply view_auth_op_valid. Qed.
 
   Lemma gmap_view_frag_validN n k dq v : ✓{n} gmap_view_frag k dq v ↔ ✓ dq.
   Proof.
-- 
GitLab