Consistent naming for auth/view lemmas.

Use infix `_frac` for the `●{q}` variants. This was already done for the
external validity lemmas, but not for those for inclusion and internal validity.

theories/algebra/auth.v

@@ -201,11 +201,17 @@ Section auth.
   Proof. apply (big_opMS_commute _). Qed.
 
   (** Inclusion *)
-  Lemma auth_auth_includedN n p1 p2 a1 a2 b :
+  Lemma auth_auth_frac_includedN n p1 p2 a1 a2 b :
     ●{p1} a1 ≼{n} ●{p2} a2 ⋅ ◯ b ↔ (p1 ≤ p2)%Qc ∧ a1 ≡{n}≡ a2.
-  Proof. apply view_auth_includedN. Qed.
-  Lemma auth_auth_included p1 p2 a1 a2 b :
+  Proof. apply view_auth_frac_includedN. Qed.
+  Lemma auth_auth_frac_included p1 p2 a1 a2 b :
     ●{p1} a1 ≼ ●{p2} a2 ⋅ ◯ b ↔ (p1 ≤ p2)%Qc ∧ a1 ≡ a2.
+  Proof. apply view_auth_frac_included. Qed.
+  Lemma auth_auth_includedN n a1 a2 b :
+    ● a1 ≼{n} ● a2 ⋅ ◯ b ↔ a1 ≡{n}≡ a2.
+  Proof. apply view_auth_includedN. Qed.
+  Lemma auth_auth_included a1 a2 b :
+    ● a1 ≼ ● a2 ⋅ ◯ b ↔ a1 ≡ a2.
   Proof. apply view_auth_included. Qed.
 
   Lemma auth_frag_includedN n p a b1 b2 :
@@ -217,26 +223,41 @@ Section auth.
 
   (** The weaker [auth_both_included] lemmas below are a consequence of the
   [auth_auth_included] and [auth_frag_included] lemmas above. *)
-  Lemma auth_both_includedN n p1 p2 a1 a2 b1 b2 :
+  Lemma auth_both_frac_includedN n p1 p2 a1 a2 b1 b2 :
     ●{p1} a1 ⋅ ◯ b1 ≼{n} ●{p2} a2 ⋅ ◯ b2 ↔ (p1 ≤ p2)%Qc ∧ a1 ≡{n}≡ a2 ∧ b1 ≼{n} b2.
-  Proof. apply view_both_includedN. Qed.
-  Lemma auth_both_included p1 p2 a1 a2 b1 b2 :
+  Proof. apply view_both_frac_includedN. Qed.
+  Lemma auth_both_frac_included p1 p2 a1 a2 b1 b2 :
     ●{p1} a1 ⋅ ◯ b1 ≼ ●{p2} a2 ⋅ ◯ b2 ↔ (p1 ≤ p2)%Qc ∧ a1 ≡ a2 ∧ b1 ≼ b2.
+  Proof. apply view_both_frac_included. Qed.
+  Lemma auth_both_includedN n a1 a2 b1 b2 :
+    ● a1 ⋅ ◯ b1 ≼{n} ● a2 ⋅ ◯ b2 ↔ a1 ≡{n}≡ a2 ∧ b1 ≼{n} b2.
+  Proof. apply view_both_includedN. Qed.
+  Lemma auth_both_included a1 a2 b1 b2 :
+    ● a1 ⋅ ◯ b1 ≼ ● a2 ⋅ ◯ b2 ↔ a1 ≡ a2 ∧ b1 ≼ b2.
   Proof. apply view_both_included. Qed.
 
   (** Internalized properties *)
-  Lemma auth_auth_validI {M} q (a b: A) :
-    ✓ (●{q} a) ⊣⊢@{uPredI M} ✓ q ∧ ✓ a.
+  Lemma auth_auth_frac_validI {M} q a : ✓ (●{q} a) ⊣⊢@{uPredI M} ✓ q ∧ ✓ a.
   Proof.
-    apply view_auth_validI=> n. uPred.unseal; split; [|by intros [??]].
+    apply view_auth_frac_validI=> n. uPred.unseal; split; [|by intros [??]].
     split; [|done]. apply ucmra_unit_leastN.
   Qed.
-  Lemma auth_frag_validI {M} (a : A):
-    ✓ (◯ a) ⊣⊢@{uPredI M} ✓ a.
+  Lemma auth_auth_validI {M} a : ✓ (● a) ⊣⊢@{uPredI M} ✓ a.
+  Proof.
+    by rewrite auth_auth_frac_validI uPred.discrete_valid bi.pure_True // left_id.
+  Qed.
+
+  Lemma auth_frag_validI {M} a : ✓ (◯ a) ⊣⊢@{uPredI M} ✓ a.
   Proof. apply view_frag_validI. Qed.
-  Lemma auth_both_validI {M} q (a b: A) :
+
+  Lemma auth_both_frac_validI {M} q a b :
     ✓ (●{q} a ⋅ ◯ b) ⊣⊢@{uPredI M} ✓ q ∧ (∃ c, a ≡ b ⋅ c) ∧ ✓ a.
-  Proof. apply view_both_validI=> n. by uPred.unseal. Qed.
+  Proof. apply view_both_frac_validI=> n. by uPred.unseal. Qed.
+  Lemma auth_both_validI {M} a b :
+    ✓ (● a ⋅ ◯ b) ⊣⊢@{uPredI M} (∃ c, a ≡ b ⋅ c) ∧ ✓ a.
+  Proof.
+    by rewrite auth_both_frac_validI uPred.discrete_valid bi.pure_True // left_id.
+  Qed.
 
   (** Updates *)
   Lemma auth_update a b a' b' :

theories/algebra/lib/excl_auth.v

@@ -62,7 +62,7 @@ Section excl_auth.
 
   Lemma excl_auth_agreeI {M} a b : ✓ (●E a ⋅ ◯E b) ⊢@{uPredI M} (a ≡ b).
   Proof.
-    rewrite auth_both_validI bi.and_elim_r bi.and_elim_l.
+    rewrite auth_both_validI bi.and_elim_l.
     apply bi.exist_elim=> -[[c|]|];
       by rewrite option_equivI /= excl_equivI //= bi.False_elim.
   Qed.

theories/algebra/view.v

@@ -351,7 +351,7 @@ Section cmra.
   Proof. apply (big_opMS_commute _). Qed.
 
   (** Inclusion *)
-  Lemma view_auth_includedN n p1 p2 a1 a2 b :
+  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.
   Proof.
     split.
@@ -363,17 +363,24 @@ Section cmra.
       + rewrite view_auth_frac_op -assoc. apply cmra_includedN_l.
       + apply cmra_includedN_l.
   Qed.
-  Lemma view_auth_included p1 p2 a1 a2 b :
+  Lemma view_auth_frac_included p1 p2 a1 a2 b :
     ●V{p1} a1 ≼ ●V{p2} a2 ⋅ ◯V b ↔ (p1 ≤ p2)%Qc ∧ a1 ≡ a2.
   Proof.
     intros. split.
     - split.
-      + by eapply (view_auth_includedN 0), cmra_included_includedN.
-      + apply equiv_dist=> n. by eapply view_auth_includedN, cmra_included_includedN.
+      + by eapply (view_auth_frac_includedN 0), cmra_included_includedN.
+      + apply equiv_dist=> n.
+        by eapply view_auth_frac_includedN, cmra_included_includedN.
     - intros [[[q ->]%frac_included| ->%Qp_eq]%Qcanon.Qcle_lt_or_eq ->].
       + rewrite view_auth_frac_op -assoc. apply cmra_included_l.
       + apply cmra_included_l.
   Qed.
+  Lemma view_auth_includedN n a1 a2 b :
+    ●V a1 ≼{n} ●V a2 ⋅ ◯V b ↔ a1 ≡{n}≡ a2.
+  Proof. rewrite view_auth_frac_includedN. naive_solver. Qed.
+  Lemma view_auth_included a1 a2 b :
+    ●V a1 ≼ ●V a2 ⋅ ◯V b ↔ a1 ≡ a2.
+  Proof. rewrite view_auth_frac_included. naive_solver. Qed.
 
   Lemma view_frag_includedN n p a b1 b2 :
     ◯V b1 ≼{n} ●V{p} a ⋅ ◯V b2 ↔ b1 ≼{n} b2.
@@ -394,41 +401,86 @@ Section cmra.
 
   (** The weaker [view_both_included] lemmas below are a consequence of the
   [view_auth_included] and [view_frag_included] lemmas above. *)
-  Lemma view_both_includedN n p1 p2 a1 a2 b1 b2 :
+  Lemma view_both_frac_includedN n p1 p2 a1 a2 b1 b2 :
     ●V{p1} a1 ⋅ ◯V b1 ≼{n} ●V{p2} a2 ⋅ ◯V b2 ↔ (p1 ≤ p2)%Qc ∧ a1 ≡{n}≡ a2 ∧ b1 ≼{n} b2.
   Proof.
     split.
     - intros. rewrite assoc. split.
-      + rewrite -view_auth_includedN. by etrans; [apply cmra_includedN_l|].
+      + rewrite -view_auth_frac_includedN. by etrans; [apply cmra_includedN_l|].
       + rewrite -view_frag_includedN. by etrans; [apply cmra_includedN_r|].
     - intros (?&->&?bf&->). rewrite (comm _ b1) view_frag_op assoc.
-      by apply cmra_monoN_r, view_auth_includedN.
+      by apply cmra_monoN_r, view_auth_frac_includedN.
   Qed.
-  Lemma view_both_included p1 p2 a1 a2 b1 b2 :
+  Lemma view_both_frac_included p1 p2 a1 a2 b1 b2 :
     ●V{p1} a1 ⋅ ◯V b1 ≼ ●V{p2} a2 ⋅ ◯V b2 ↔ (p1 ≤ p2)%Qc ∧ a1 ≡ a2 ∧ b1 ≼ b2.
   Proof.
     split.
     - intros. rewrite assoc. split.
-      + rewrite -view_auth_included. by etrans; [apply cmra_included_l|].
+      + rewrite -view_auth_frac_included. by etrans; [apply cmra_included_l|].
       + rewrite -view_frag_included. by etrans; [apply cmra_included_r|].
     - intros (?&->&?bf&->). rewrite (comm _ b1) view_frag_op assoc.
-      by apply cmra_mono_r, view_auth_included.
+      by apply cmra_mono_r, view_auth_frac_included.
   Qed.
+  Lemma view_both_includedN n a1 a2 b1 b2 :
+    ●V a1 ⋅ ◯V b1 ≼{n} ●V a2 ⋅ ◯V b2 ↔ a1 ≡{n}≡ a2 ∧ b1 ≼{n} b2.
+  Proof. rewrite view_both_frac_includedN. naive_solver. Qed.
+  Lemma view_both_included a1 a2 b1 b2 :
+    ●V a1 ⋅ ◯V b1 ≼ ●V a2 ⋅ ◯V b2 ↔ a1 ≡ a2 ∧ b1 ≼ b2.
+  Proof. rewrite view_both_frac_included. naive_solver. Qed.
 
   (** Internalized properties *)
-  Lemma view_both_validI {M} (relI : uPred M) q a b :
-    (∀ n (x : M), relI n x ↔ rel n a b) →
-    ✓ (●V{q} a ⋅ ◯V b) ⊣⊢ ✓ q ∧ relI.
+  Lemma view_both_frac_validI_1 {M} (relI : uPred M) q a b :
+    (∀ n (x : M), rel n a b → relI n x) →
+    ✓ (●V{q} a ⋅ ◯V b) ⊢ ✓ q ∧ relI.
+  Proof.
+    intros Hrel. uPred.unseal. split=> n x _ /=.
+    rewrite /uPred_holds /= view_both_frac_validN. by move=> [? /Hrel].
+  Qed.
+  Lemma view_both_frac_validI_2 {M} (relI : uPred M) q a b :
+    (∀ n (x : M), relI n x → rel n a b) →
+    ✓ q ∧ relI ⊢ ✓ (●V{q} a ⋅ ◯V b).
   Proof.
     intros Hrel. uPred.unseal. split=> n x _ /=.
-    by rewrite {1}/uPred_holds /= view_both_frac_validN -(Hrel _ x).
+    rewrite /uPred_holds /= view_both_frac_validN. by move=> [? /Hrel].
   Qed.
-  Lemma view_auth_validI {M} (relI : uPred M) q a :
+  Lemma view_both_frac_validI {M} (relI : uPred M) q a b :
+    (∀ n (x : M), rel n a b ↔ relI n x) →
+    ✓ (●V{q} a ⋅ ◯V b) ⊣⊢ ✓ q ∧ relI.
+  Proof.
+    intros. apply (anti_symm _);
+      [apply view_both_frac_validI_1|apply view_both_frac_validI_2]; naive_solver.
+  Qed.
+
+  Lemma view_both_validI_1 {M} (relI : uPred M) a b :
+    (∀ n (x : M), rel n a b → relI n x) →
+    ✓ (●V a ⋅ ◯V b) ⊢ relI.
+  Proof. intros. by rewrite view_both_frac_validI_1 // bi.and_elim_r. Qed.
+  Lemma view_both_validI_2 {M} (relI : uPred M) a b :
+    (∀ n (x : M), relI n x → rel n a b) →
+    relI ⊢ ✓ (●V a ⋅ ◯V b).
+  Proof.
+    intros. rewrite -view_both_frac_validI_2 // uPred.discrete_valid.
+    apply bi.and_intro; [|done]. by apply bi.pure_intro.
+  Qed.
+  Lemma view_both_validI {M} (relI : uPred M) a b :
+    (∀ n (x : M), rel n a b ↔ relI n x) →
+    ✓ (●V a ⋅ ◯V b) ⊣⊢ relI.
+  Proof.
+    intros. apply (anti_symm _);
+      [apply view_both_validI_1|apply view_both_validI_2]; naive_solver.
+  Qed.
+
+  Lemma view_auth_frac_validI {M} (relI : uPred M) q a :
     (∀ n (x : M), relI n x ↔ rel n a ε) →
     ✓ (●V{q} a) ⊣⊢ ✓ q ∧ relI.
   Proof.
-    intros. rewrite -(right_id ε op (●V{q} a)). by apply view_both_validI.
+    intros. rewrite -(right_id ε op (●V{q} a)). by apply view_both_frac_validI.
   Qed.
+  Lemma view_auth_validI {M} (relI : uPred M) a :
+    (∀ n (x : M), relI n x ↔ rel n a ε) →
+    ✓ (●V a) ⊣⊢ relI.
+  Proof. intros. rewrite -(right_id ε op (●V a)). by apply view_both_validI. Qed.
+
   Lemma view_frag_validI {M} b : ✓ (◯V b) ⊣⊢@{uPredI M} ✓ b.
   Proof. by uPred.unseal. Qed.
 

theories/base_logic/lib/wsat.v

@@ -110,7 +110,7 @@ Lemma invariant_lookup (I : gmap positive (iProp Σ)) i P :
   own invariant_name (◯ {[i := invariant_unfold P]}) ⊢
   ∃ Q, ⌜I !! i = Some Q⌝ ∗ ▷ (Q ≡ P).
 Proof.
-  rewrite -own_op own_valid auth_both_validI /=. iIntros "[_ [#HI #HvI]]".
+  rewrite -own_op own_valid auth_both_validI /=. iIntros "[#HI #HvI]".
   iDestruct "HI" as (I') "HI". rewrite gmap_equivI gmap_validI.
   iSpecialize ("HI" $! i). iSpecialize ("HvI" $! i).
   rewrite lookup_fmap lookup_op lookup_singleton option_equivI.