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] =?UTF-8?q?Add=20lemmas=20for=20validity=20of=20`=E2=97=8F?=
 =?UTF-8?q?{=5F}=20=5F=20=E2=8B=85=20=E2=97=8F{=5F}=20=5F`=20for=20both=20?=
 =?UTF-8?q?view=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