algebra: use Qp inequality instead of frac validity for lemma statements

CHANGELOG.md

@@ -53,6 +53,8 @@ With this release, we dropped support for Coq 8.9.
   equal to `✓ b`.
 * Add `mnat_auth`, a wrapper for `auth max_nat`. The result is an authoritative
   `nat` where a fragment is a lower bound whose ownership is persistent.
+* Change `*_valid` lemma statements involving fractions to use `Qp` addition and
+  inequality instead of RA composition and validity.
 
 **Changes in `bi`:**
 

theories/algebra/auth.v

@@ -154,13 +154,13 @@ Section auth.
     ✓ (●{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.
+  Lemma auth_auth_frac_validN n q a : ✓{n} (●{q} a) ↔ (q ≤ 1)%Qp ∧ ✓{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.
+    ✓{n} (●{q1} a1 ⋅ ●{q2} a2) ↔ (q1 + q2 ≤ 1)%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. apply view_auth_op_validN. Qed.
@@ -181,12 +181,12 @@ Section auth.
   Proof. apply auth_frag_op_validN. Qed.
 
   Lemma auth_both_frac_validN n q a b :
-    ✓{n} (●{q} a ⋅ ◯ b) ↔ ✓{n} q ∧ b ≼{n} a ∧ ✓{n} a.
+    ✓{n} (●{q} a ⋅ ◯ b) ↔ (q ≤ 1)%Qp ∧ b ≼{n} a ∧ ✓{n} a.
   Proof. apply view_both_frac_validN. Qed.
   Lemma auth_both_validN n a b : ✓{n} (● a ⋅ ◯ b) ↔ b ≼{n} a ∧ ✓{n} a.
   Proof. apply view_both_validN. Qed.
 
-  Lemma auth_auth_frac_valid q a : ✓ (●{q} a) ↔ ✓ q ∧ ✓ a.
+  Lemma auth_auth_frac_valid q a : ✓ (●{q} a) ↔ (q ≤ 1)%Qp ∧ ✓ a.
   Proof.
     rewrite view_auth_frac_valid !cmra_valid_validN.
     by setoid_rewrite auth_view_rel_unit.
@@ -198,10 +198,10 @@ Section auth.
   Qed.
 
   Lemma auth_auth_frac_op_valid q1 q2 a1 a2 :
-    ✓ (●{q1} a1 ⋅ ●{q2} a2) ↔ ✓ (q1 + q2)%Qp ∧ a1 ≡ a2 ∧ ✓ a1.
+    ✓ (●{q1} a1 ⋅ ●{q2} a2) ↔ (q1 + q2 ≤ 1)%Qp ∧ a1 ≡ a2 ∧ ✓ a1.
   Proof.
     rewrite view_auth_frac_op_valid !cmra_valid_validN.
-    by setoid_rewrite auth_view_rel_unit.
+    setoid_rewrite auth_view_rel_unit. done.
   Qed.
   Lemma auth_auth_op_valid a1 a2 : ✓ (● a1 ⋅ ● a2) ↔ False.
   Proof. apply view_auth_op_valid. Qed.
@@ -228,7 +228,7 @@ Section auth.
   single witness for [b ≼ a] from validity, we have to make do with one witness
   per step-index, i.e., [∀ n, b ≼{n} a]. *)
   Lemma auth_both_frac_valid q a b :
-    ✓ (●{q} a ⋅ ◯ b) ↔ ✓ q ∧ (∀ n, b ≼{n} a) ∧ ✓ a.
+    ✓ (●{q} a ⋅ ◯ b) ↔ (q ≤ 1)%Qp ∧ (∀ n, b ≼{n} a) ∧ ✓ a.
   Proof.
     rewrite view_both_frac_valid. apply and_iff_compat_l. split.
     - intros Hrel. split.
@@ -238,11 +238,11 @@ Section auth.
   Qed.
   Lemma auth_both_valid a b :
     ✓ (● a ⋅ ◯ b) ↔ (∀ n, b ≼{n} a) ∧ ✓ a.
-  Proof. rewrite auth_both_frac_valid frac_valid'. naive_solver. Qed.
+  Proof. rewrite auth_both_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).
+  Lemma auth_both_frac_valid_2 q a b : (q ≤ 1)%Qp → ✓ a → b ≼ a → ✓ (●{q} a ⋅ ◯ b).
   Proof.
     intros. apply auth_both_frac_valid.
     naive_solver eauto using cmra_included_includedN.
@@ -251,14 +251,14 @@ Section auth.
   Proof. intros ??. by apply auth_both_frac_valid_2. Qed.
 
   Lemma auth_both_frac_valid_discrete `{!CmraDiscrete A} q a b :
-    ✓ (●{q} a ⋅ ◯ b) ↔ ✓ q ∧ b ≼ a ∧ ✓ a.
+    ✓ (●{q} a ⋅ ◯ b) ↔ (q ≤ 1)%Qp ∧ b ≼ a ∧ ✓ a.
   Proof.
     rewrite auth_both_frac_valid. setoid_rewrite <-cmra_discrete_included_iff.
     naive_solver eauto using O.
   Qed.
   Lemma auth_both_valid_discrete `{!CmraDiscrete A} a b :
     ✓ (● a ⋅ ◯ b) ↔ b ≼ a ∧ ✓ a.
-  Proof. rewrite auth_both_frac_valid_discrete frac_valid'. naive_solver. Qed.
+  Proof. rewrite auth_both_frac_valid_discrete. naive_solver. Qed.
 
   (** Inclusion *)
   Lemma auth_auth_frac_includedN n p1 p2 a1 a2 b :

theories/algebra/lib/frac_agree.v

@@ -31,18 +31,18 @@ Section lemmas.
 
   Lemma frac_agree_op_valid q1 a1 q2 a2 :
     ✓ (to_frac_agree q1 a1 ⋅ to_frac_agree q2 a2) →
-    ✓ (q1 + q2)%Qp ∧ a1 ≡ a2.
+    (q1 + q2 ≤ 1)%Qp ∧ a1 ≡ a2.
   Proof.
     intros [Hq Ha]%pair_valid. simpl in *. split; first done.
     apply to_agree_op_inv. done.
   Qed.
   Lemma frac_agree_op_valid_L `{!LeibnizEquiv A} q1 a1 q2 a2 :
     ✓ (to_frac_agree q1 a1 ⋅ to_frac_agree q2 a2) →
-    ✓ (q1 + q2)%Qp ∧ a1 = a2.
+    (q1 + q2 ≤ 1)%Qp ∧ a1 = a2.
   Proof. unfold_leibniz. apply frac_agree_op_valid. Qed.
   Lemma frac_agree_op_validN q1 a1 q2 a2 n :
     ✓{n} (to_frac_agree q1 a1 ⋅ to_frac_agree q2 a2) →
-    ✓ (q1 + q2)%Qp ∧ a1 ≡{n}≡ a2.
+    (q1 + q2 ≤ 1)%Qp ∧ a1 ≡{n}≡ a2.
   Proof.
     intros [Hq Ha]%pair_validN. simpl in *. split; first done.
     apply to_agree_op_invN. done.

theories/algebra/lib/frac_auth.v

@@ -83,9 +83,9 @@ Section frac_auth.
   Lemma frac_auth_auth_valid a : ✓ (●F a) ↔ ✓ a.
   Proof. rewrite !cmra_valid_validN. by setoid_rewrite frac_auth_auth_validN. Qed.
 
-  Lemma frac_auth_frag_validN n q a : ✓{n} (◯F{q} a) ↔ ✓{n} q ∧ ✓{n} a.
+  Lemma frac_auth_frag_validN n q a : ✓{n} (◯F{q} a) ↔ (q ≤ 1)%Qp ∧ ✓{n} a.
   Proof. by rewrite /frac_auth_frag auth_frag_validN. Qed.
-  Lemma frac_auth_frag_valid q a : ✓ (◯F{q} a) ↔ ✓ q ∧ ✓ a.
+  Lemma frac_auth_frag_valid q a : ✓ (◯F{q} a) ↔ (q ≤ 1)%Qp ∧ ✓ a.
   Proof. by rewrite /frac_auth_frag auth_frag_valid. Qed.
 
   Lemma frac_auth_frag_op q1 q2 a1 a2 : ◯F{q1+q2} (a1 ⋅ a2) ≡ ◯F{q1} a1 ⋅ ◯F{q2} a2.

theories/algebra/lib/gmap_view.v

@@ -194,7 +194,7 @@ Section lemmas.
     ✓ (gmap_view_auth p m1 ⋅ gmap_view_auth q m2) → m1 = m2.
   Proof. apply view_auth_frac_op_inv_L, _. Qed.
 
-  Lemma gmap_view_auth_frac_valid m q : ✓ gmap_view_auth q m ↔ ✓ q.
+  Lemma gmap_view_auth_frac_valid m q : ✓ gmap_view_auth q m ↔ (q ≤ 1)%Qp.
   Proof.
     rewrite view_auth_frac_valid. intuition eauto using gmap_view_rel_unit.
   Qed.
@@ -202,7 +202,7 @@ Section lemmas.
   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.
+    ✓ (gmap_view_auth q1 m1 ⋅ gmap_view_auth q2 m2) ↔ (q1 + q2 ≤ 1)%Qp ∧ m1 ≡ m2.
   Proof.
     rewrite view_auth_frac_op_valid. intuition eauto using gmap_view_rel_unit.
   Qed.
@@ -251,7 +251,7 @@ Section lemmas.
 
   Lemma gmap_view_both_frac_validN n q m k dq v :
     ✓{n} (gmap_view_auth q m ⋅ gmap_view_frag k dq v) ↔
-      ✓ q ∧ ✓ dq ∧ m !! k ≡{n}≡ Some v.
+      (q ≤ 1)%Qp ∧ ✓ dq ∧ m !! k ≡{n}≡ Some v.
   Proof.
     rewrite /gmap_view_auth /gmap_view_frag.
     rewrite view_both_frac_validN gmap_view_rel_lookup.
@@ -263,7 +263,7 @@ Section lemmas.
   Proof. rewrite gmap_view_both_frac_validN. naive_solver done. Qed.
   Lemma gmap_view_both_frac_valid q m k dq v :
     ✓ (gmap_view_auth q m ⋅ gmap_view_frag k dq v) ↔
-    ✓ q ∧ ✓ dq ∧ m !! k ≡ Some v.
+    (q ≤ 1)%Qp ∧ ✓ dq ∧ m !! k ≡ Some v.
   Proof.
     rewrite /gmap_view_auth /gmap_view_frag.
     rewrite view_both_frac_valid. setoid_rewrite gmap_view_rel_lookup.

theories/algebra/lib/mnat_auth.v

@@ -43,7 +43,7 @@ Section mnat_auth.
   Proof. intros. rewrite mnat_auth_frag_op Nat.max_r //. Qed.
 
   Lemma mnat_auth_frac_op_valid q1 q2 n1 n2 :
-    ✓ (mnat_auth_auth q1 n1 ⋅ mnat_auth_auth q2 n2) ↔ ✓ (q1 + q2)%Qp ∧ n1 = n2.
+    ✓ (mnat_auth_auth q1 n1 ⋅ mnat_auth_auth q2 n2) ↔ (q1 + q2 ≤ 1)%Qp ∧ n1 = n2.
   Proof.
     rewrite /mnat_auth_auth (comm _ (●{q2} _)) -!assoc (assoc _ (◯ _)).
     rewrite -auth_frag_op (comm _ (◯ _)) assoc. split.
@@ -57,7 +57,7 @@ Section mnat_auth.
   Proof. rewrite mnat_auth_frac_op_valid. naive_solver. Qed.
 
   Lemma mnat_auth_both_frac_valid q n m :
-    ✓ (mnat_auth_auth q n ⋅ mnat_auth_frag m) ↔ ✓ q ∧ m ≤ n.
+    ✓ (mnat_auth_auth q n ⋅ mnat_auth_frag m) ↔ (q ≤ 1)%Qp ∧ m ≤ n.
   Proof.
     rewrite /mnat_auth_auth /mnat_auth_frag -assoc -auth_frag_op.
     rewrite auth_both_frac_valid_discrete max_nat_included /=.
@@ -66,7 +66,7 @@ Section mnat_auth.
 
   Lemma mnat_auth_both_valid n m :
     ✓ (mnat_auth_auth 1 n ⋅ mnat_auth_frag m) ↔ m ≤ n.
-  Proof. rewrite mnat_auth_both_frac_valid frac_valid'. naive_solver. Qed.
+  Proof. rewrite mnat_auth_both_frac_valid. naive_solver. Qed.
 
   Lemma mnat_auth_frag_mono n1 n2 : n1 ≤ n2 → mnat_auth_frag n1 ≼ mnat_auth_frag n2.
   Proof. intros. by apply auth_frag_mono, max_nat_included. Qed.

theories/algebra/lib/ufrac_auth.v

@@ -29,7 +29,7 @@ Definition ufrac_authUR (A : cmraT) : ucmraT :=
 [q : Qp] instead of [q : ufrac]. This way, the API does not expose that [ufrac]
 is used internally. This is quite important, as there are two canonical camera
 instances with carrier [Qp], namely [fracR] and [ufracR]. When writing things
-like [ufrac_auth_auth q a ∧ ✓{q}] we want Coq to infer the type of [q] as [Qp]
+like [ufrac_auth_auth q a ∧ ✓ q] we want Coq to infer the type of [q] as [Qp]
 such that the [✓] of the default [fracR] camera is used, and not the [✓] of
 the [ufracR] camera. *)
 Definition ufrac_auth_auth {A : cmraT} (q : Qp) (x : A) : ufrac_authR A :=

theories/algebra/view.v

@@ -317,18 +317,16 @@ Section cmra.
     ✓ (●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 ε.
+  Lemma view_auth_frac_validN n q a : ✓{n} (●V{q} a) ↔ (q ≤ 1)%Qp ∧ 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.
+  Proof. rewrite view_auth_frac_validN. 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 ε.
+    ✓{n} (●V{q1} a1 ⋅ ●V{q2} a2) ↔ (q1 + q2 ≤ 1)%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.
@@ -342,30 +340,29 @@ Section cmra.
   Proof. done. Qed.
 
   Lemma view_both_frac_validN n q a b :
-    ✓{n} (●V{q} a ⋅ ◯V b) ↔ ✓{n} q ∧ rel n a b.
+    ✓{n} (●V{q} a ⋅ ◯V b) ↔ (q ≤ 1)%Qp ∧ 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.
+  Proof. rewrite view_both_frac_validN. naive_solver. Qed.
 
-  Lemma view_auth_frac_valid q a : ✓ (●V{q} a) ↔ ✓ q ∧ ∀ n, rel n a ε.
+  Lemma view_auth_frac_valid q a : ✓ (●V{q} a) ↔ (q ≤ 1)%Qp ∧ ∀ 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.
+  Proof. rewrite view_auth_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 ε.
+    ✓ (●V{q1} a1 ⋅ ●V{q2} a2) ↔ (q1 + q2 ≤ 1)%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.
+    split; last naive_solver. intros Hv.
+    split; last naive_solver. apply (Hv 0).
   Qed.
   Lemma view_auth_op_valid a1 a2 : ✓ (●V a1 ⋅ ●V a2) ↔ False.
   Proof. rewrite view_auth_frac_op_valid. naive_solver. Qed.
@@ -373,14 +370,14 @@ Section cmra.
   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.
+  Lemma view_both_frac_valid q a b : ✓ (●V{q} a ⋅ ◯V b) ↔ (q ≤ 1)%Qp ∧ ∀ 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.
+  Proof. rewrite view_both_frac_valid. naive_solver. Qed.
 
   (** Inclusion *)
   Lemma view_auth_frac_includedN n p1 p2 a1 a2 b :