Add lemmas for validity of `●{_} _ ⋅ ●{_} _` for both view and auth.

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

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

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.