Make valid a primitive instead of derived notion.

This way it behaves better for discrete CMRAs.

algebra/agree.v

@@ -16,9 +16,12 @@ Context {A : cofeT}.
 
 Instance agree_validN : ValidN (agree A) := λ n x,
   agree_is_valid x n ∧ ∀ n', n' ≤ n → x n' ≡{n'}≡ x n.
+Instance agree_valid : Valid (agree A) := λ x, ∀ n, ✓{n} x.
+
 Lemma agree_valid_le n n' (x : agree A) :
   agree_is_valid x n → n' ≤ n → agree_is_valid x n'.
 Proof. induction 2; eauto using agree_valid_S. Qed.
+
 Instance agree_equiv : Equiv (agree A) := λ x y,
   (∀ n, agree_is_valid x n ↔ agree_is_valid y n) ∧
   (∀ n, agree_is_valid x n → x n ≡{n}≡ y n).

algebra/auth.v

 From algebra Require Export excl.
 From algebra Require Import functor upred.
+Local Arguments valid _ _ !_ /.
 Local Arguments validN _ _ _ !_ /.
 
 Record auth (A : Type) : Type := Auth { authoritative : excl A ; own : A }.
@@ -66,6 +67,13 @@ Implicit Types a b : A.
 Implicit Types x y : auth A.
 
 Global Instance auth_empty `{Empty A} : Empty (auth A) := Auth ∅ ∅.
+Instance auth_valid : Valid (auth A) := λ x,
+  match authoritative x with
+  | Excl a => own x ≼ a ∧ ✓ a
+  | ExclUnit => ✓ own x
+  | ExclBot => False
+  end.
+Global Arguments auth_valid !_ /.
 Instance auth_validN : ValidN (auth A) := λ n x,
   match authoritative x with
   | Excl a => own x ≼{n} a ∧ ✓{n} a
@@ -105,6 +113,8 @@ Proof.
       destruct Hx; intros ?; cofe_subst; auto.
   - by intros n x1 x2 [Hx Hx'] y1 y2 [Hy Hy'];
       split; simpl; rewrite ?Hy ?Hy' ?Hx ?Hx'.
+  - intros [[] ?]; rewrite /= ?cmra_included_includedN ?cmra_valid_validN;
+      naive_solver eauto using O.
   - intros n [[] ?] ?; naive_solver eauto using cmra_includedN_S, cmra_validN_S.
   - by split; simpl; rewrite assoc.
   - by split; simpl; rewrite comm.
@@ -169,7 +179,7 @@ Lemma auth_local_update L `{!LocalUpdate Lv L} a a' :
   Lv a → ✓ L a' →
   ● a' ⋅ ◯ a ~~> ● L a' ⋅ ◯ L a.
 Proof.
-  intros. apply auth_update=>n af ? EQ; split; last done.
+  intros. apply auth_update=>n af ? EQ; split; last by apply cmra_valid_validN.
   by rewrite EQ (local_updateN L) // -EQ.
 Qed.
 
@@ -188,7 +198,7 @@ Lemma auth_local_update_l L `{!LocalUpdate Lv L} a a' :
   Lv a → ✓ (L a ⋅ a') →
   ● (a ⋅ a') ⋅ ◯ a ~~> ● (L a ⋅ a') ⋅ ◯ L a.
 Proof.
-  intros. apply auth_update=>n af ? EQ; split; last done.
+  intros. apply auth_update=>n af ? EQ; split; last by apply cmra_valid_validN.
   by rewrite -(local_updateN L) // EQ -(local_updateN L) // -EQ.
 Qed.
 

algebra/cmra.v

@@ -26,7 +26,6 @@ Notation "✓{ n } x" := (validN n x)
 Class Valid (A : Type) := valid : A → Prop.
 Instance: Params (@valid) 2.
 Notation "✓ x" := (valid x) (at level 20) : C_scope.
-Instance validN_valid `{ValidN A} : Valid A := λ x, ∀ n, ✓{n} x.
 
 Definition includedN `{Dist A, Op A} (n : nat) (x y : A) := ∃ z, y ≡{n}≡ x ⋅ z.
 Notation "x ≼{ n } y" := (includedN n x y)
@@ -34,13 +33,15 @@ Notation "x ≼{ n } y" := (includedN n x y)
 Instance: Params (@includedN) 4.
 Hint Extern 0 (_ ≼{_} _) => reflexivity.
 
-Record CMRAMixin A `{Dist A, Equiv A, Unit A, Op A, ValidN A, Minus A} := {
+Record CMRAMixin A
+    `{Dist A, Equiv A, Unit A, Op A, Valid A, ValidN A, Minus A} := {
   (* setoids *)
   mixin_cmra_op_ne n (x : A) : Proper (dist n ==> dist n) (op x);
   mixin_cmra_unit_ne n : Proper (dist n ==> dist n) unit;
   mixin_cmra_validN_ne n : Proper (dist n ==> impl) (validN n);
   mixin_cmra_minus_ne n : Proper (dist n ==> dist n ==> dist n) minus;
   (* valid *)
+  mixin_cmra_valid_validN x : ✓ x ↔ ∀ n, ✓{n} x;
   mixin_cmra_validN_S n x : ✓{S n} x → ✓{n} x;
   (* monoid *)
   mixin_cmra_assoc : Assoc (≡) (⋅);
@@ -63,24 +64,26 @@ Structure cmraT := CMRAT {
   cmra_compl : Compl cmra_car;
   cmra_unit : Unit cmra_car;
   cmra_op : Op cmra_car;
+  cmra_valid : Valid cmra_car;
   cmra_validN : ValidN cmra_car;
   cmra_minus : Minus cmra_car;
   cmra_cofe_mixin : CofeMixin cmra_car;
   cmra_mixin : CMRAMixin cmra_car
 }.
-Arguments CMRAT {_ _ _ _ _ _ _ _} _ _.
+Arguments CMRAT {_ _ _ _ _ _ _ _ _} _ _.
 Arguments cmra_car : simpl never.
 Arguments cmra_equiv : simpl never.
 Arguments cmra_dist : simpl never.
 Arguments cmra_compl : simpl never.
 Arguments cmra_unit : simpl never.
 Arguments cmra_op : simpl never.
+Arguments cmra_valid : simpl never.
 Arguments cmra_validN : simpl never.
 Arguments cmra_minus : simpl never.
 Arguments cmra_cofe_mixin : simpl never.
 Arguments cmra_mixin : simpl never.
 Add Printing Constructor cmraT.
-Existing Instances cmra_unit cmra_op cmra_validN cmra_minus.
+Existing Instances cmra_unit cmra_op cmra_valid cmra_validN cmra_minus.
 Coercion cmra_cofeC (A : cmraT) : cofeT := CofeT (cmra_cofe_mixin A).
 Canonical Structure cmra_cofeC.
 
@@ -97,6 +100,8 @@ Section cmra_mixin.
   Global Instance cmra_minus_ne n :
     Proper (dist n ==> dist n ==> dist n) (@minus A _).
   Proof. apply (mixin_cmra_minus_ne _ (cmra_mixin A)). Qed.
+  Lemma cmra_valid_validN x : ✓ x ↔ ∀ n, ✓{n} x.
+  Proof. apply (mixin_cmra_valid_validN _ (cmra_mixin A)). Qed.
   Lemma cmra_validN_S n x : ✓{S n} x → ✓{n} x.
   Proof. apply (mixin_cmra_validN_S _ (cmra_mixin A)). Qed.
   Global Instance cmra_assoc : Assoc (≡) (@op A _).
@@ -178,7 +183,10 @@ Global Instance cmra_minus_proper : Proper ((≡) ==> (≡) ==> (≡)) (@minus A
 Proof. apply (ne_proper_2 _). Qed.
 
 Global Instance cmra_valid_proper : Proper ((≡) ==> iff) (@valid A _).
-Proof. by intros x y Hxy; split; intros ? n; [rewrite -Hxy|rewrite Hxy]. Qed.
+Proof.
+  intros x y Hxy; rewrite !cmra_valid_validN.
+  by split=> ? n; [rewrite -Hxy|rewrite Hxy].
+Qed.
 Global Instance cmra_includedN_ne n :
   Proper (dist n ==> dist n ==> iff) (@includedN A _ _ n) | 1.
 Proof.
@@ -210,8 +218,6 @@ Proof.
 Qed.
 
 (** ** Validity *)
-Lemma cmra_valid_validN x : ✓ x ↔ ∀ n, ✓{n} x.
-Proof. done. Qed.
 Lemma cmra_validN_le n n' x : ✓{n} x → n' ≤ n → ✓{n'} x.
 Proof. induction 2; eauto using cmra_validN_S. Qed.
 Lemma cmra_valid_op_l x y : ✓ (x ⋅ y) → ✓ x.
@@ -309,13 +315,15 @@ Lemma cmra_op_timeless x1 x2 :
 Proof.
   intros ??? z Hz.
   destruct (cmra_extend 0 z x1 x2) as ([y1 y2]&Hz'&?&?); auto; simpl in *.
-  { by rewrite -?Hz. }
+  { rewrite -?Hz. by apply cmra_valid_validN. }
   by rewrite Hz' (timeless x1 y1) // (timeless x2 y2).
 Qed.
 
 (** ** RAs with an empty element *)
 Section identity.
   Context `{Empty A, !CMRAIdentity A}.
+  Lemma cmra_empty_validN n : ✓{n} ∅.
+  Proof. apply cmra_valid_validN, cmra_empty_valid. Qed.
   Lemma cmra_empty_leastN n x : ∅ ≼{n} x.
   Proof. by exists x; rewrite left_id. Qed.
   Lemma cmra_empty_least x : ∅ ≼ x.
@@ -333,7 +341,9 @@ Proof. intros; apply (ne_proper _). Qed.
 
 Lemma local_update L `{!LocalUpdate Lv L} x y :
   Lv x → ✓ (x ⋅ y) → L (x ⋅ y) ≡ L x ⋅ y.
-Proof. by rewrite equiv_dist=>?? n; apply (local_updateN L). Qed.
+Proof.
+  by rewrite cmra_valid_validN equiv_dist=>?? n; apply (local_updateN L).
+Qed.
 
 Global Instance local_update_op x : LocalUpdate (λ _, True) (op x).
 Proof. split. apply _. by intros n y1 y2 _ _; rewrite assoc. Qed.
@@ -464,15 +474,16 @@ Class RA A `{Equiv A, Unit A, Op A, Valid A, Minus A} := {
 
 Section discrete.
   Context {A : cofeT} `{∀ x : A, Timeless x}.
-  Context {v : Valid A} `{Unit A, Op A, Minus A} (ra : RA A).
+  Context `{Unit A, Op A, Valid A, Minus A} (ra : RA A).
 
   Instance discrete_validN : ValidN A := λ n x, ✓ x.
   Definition discrete_cmra_mixin : CMRAMixin A.
   Proof.
     destruct ra; split; unfold Proper, respectful, includedN;
       try setoid_rewrite <-(timeless_iff _ _); try done.
-    intros n x y1 y2 ??; exists (y1,y2); split_and?; auto.
-    apply (timeless _), dist_le with n; auto with lia.
+    - intros x; split; first done. by move=> /(_ 0).
+    - intros n x y1 y2 ??; exists (y1,y2); split_and?; auto.
+      apply (timeless _), dist_le with n; auto with lia.
   Qed.
   Definition discreteRA : cmraT := CMRAT (cofe_mixin A) discrete_cmra_mixin.
   Lemma discrete_updateP (x : discreteRA) (P : A → Prop) :
@@ -481,8 +492,6 @@ Section discrete.
   Lemma discrete_update (x y : discreteRA) :
     (∀ z, ✓ (x ⋅ z) → ✓ (y ⋅ z)) → x ~~> y.
   Proof. intros Hvalid n z; apply Hvalid. Qed.
-  Lemma discrete_valid (x : discreteRA) : v x → validN_valid x.
-  Proof. move=>Hx n. exact Hx. Qed.
 End discrete.
 
 (** ** CMRA for the unit type *)
@@ -497,7 +506,7 @@ Section unit.
   Canonical Structure unitRA : cmraT :=
     Eval cbv [unitC discreteRA cofe_car] in discreteRA unit_ra.
   Global Instance unit_cmra_identity : CMRAIdentity unitRA.
-  Proof. by split; intros []. Qed.
+  Proof. by split. Qed.
 End unit.
 
 (** ** Product *)
@@ -506,6 +515,7 @@ Section prod.
   Instance prod_op : Op (A * B) := λ x y, (x.1 ⋅ y.1, x.2 ⋅ y.2).
   Global Instance prod_empty `{Empty A, Empty B} : Empty (A * B) := (∅, ∅).
   Instance prod_unit : Unit (A * B) := λ x, (unit (x.1), unit (x.2)).
+  Instance prod_valid : Valid (A * B) := λ x, ✓ x.1 ∧ ✓ x.2.
   Instance prod_validN : ValidN (A * B) := λ n x, ✓{n} x.1 ∧ ✓{n} x.2.
   Instance prod_minus : Minus (A * B) := λ x y, (x.1 ⩪ y.1, x.2 ⩪ y.2).
   Lemma prod_included (x y : A * B) : x ≼ y ↔ x.1 ≼ y.1 ∧ x.2 ≼ y.2.
@@ -526,6 +536,9 @@ Section prod.
     - by intros n y1 y2 [Hy1 Hy2] [??]; split; rewrite /= -?Hy1 -?Hy2.
     - by intros n x1 x2 [Hx1 Hx2] y1 y2 [Hy1 Hy2];
         split; rewrite /= ?Hx1 ?Hx2 ?Hy1 ?Hy2.
+    - intros x; split.
+      + intros [??] n; split; by apply cmra_valid_validN.
+      + intros Hxy; split; apply cmra_valid_validN=> n; apply Hxy.
     - by intros n x [??]; split; apply cmra_validN_S.
     - by split; rewrite /= assoc.
     - by split; rewrite /= comm.

algebra/excl.v

@@ -83,6 +83,8 @@ Global Instance excl_leibniz : LeibnizEquiv A → LeibnizEquiv (excl A).
 Proof. by destruct 2; f_equal; apply leibniz_equiv. Qed.
 
 (* CMRA *)
+Instance excl_valid : Valid (excl A) := λ x,
+  match x with Excl _ | ExclUnit => True | ExclBot => False end.
 Instance excl_validN : ValidN (excl A) := λ n x,
   match x with Excl _ | ExclUnit => True | ExclBot => False end.
 Global Instance excl_empty : Empty (excl A) := ExclUnit.
@@ -106,6 +108,7 @@ Proof.
   - constructor.
   - by destruct 1; intros ?.
   - by destruct 1; inversion_clear 1; constructor.
+  - intros x; split. done. by move=> /(_ 0).
   - intros n [?| |]; simpl; auto with lia.
   - by intros [?| |] [?| |] [?| |]; constructor.
   - by intros [?| |] [?| |]; constructor.

algebra/fin_maps.v

@@ -96,6 +96,7 @@ Implicit Types m : gmap K A.
 
 Instance map_op : Op (gmap K A) := merge op.
 Instance map_unit : Unit (gmap K A) := fmap unit.
+Instance map_valid : Valid (gmap K A) := λ m, ∀ i, ✓ (m !! i).
 Instance map_validN : ValidN (gmap K A) := λ n m, ∀ i, ✓{n} (m !! i).
 Instance map_minus : Minus (gmap K A) := merge minus.
 
@@ -106,8 +107,6 @@ Proof. by apply lookup_merge. Qed.
 Lemma lookup_unit m i : unit m !! i = unit (m !! i).
 Proof. by apply lookup_fmap. Qed.
 
-Lemma map_valid_spec m : ✓ m ↔ ∀ i, ✓ (m !! i).
-Proof. split; intros Hm ??; apply Hm. Qed.
 Lemma map_included_spec (m1 m2 : gmap K A) : m1 ≼ m2 ↔ ∀ i, m1 !! i ≼ m2 !! i.
 Proof.
   split.
@@ -131,6 +130,9 @@ Proof.
   - by intros n m1 m2 Hm i; rewrite !lookup_unit (Hm i).
   - by intros n m1 m2 Hm ? i; rewrite -(Hm i).
   - by intros n m1 m1' Hm1 m2 m2' Hm2 i; rewrite !lookup_minus (Hm1 i) (Hm2 i).
+  - intros m; split.
+    + by intros ? n i; apply cmra_valid_validN.
+    + intros Hm i; apply cmra_valid_validN=> n; apply Hm.
   - intros n m Hm i; apply cmra_validN_S, Hm.
   - by intros m1 m2 m3 i; rewrite !lookup_op assoc.
   - by intros m1 m2 i; rewrite !lookup_op comm.
@@ -162,7 +164,7 @@ Canonical Structure mapRA : cmraT := CMRAT map_cofe_mixin map_cmra_mixin.
 Global Instance map_cmra_identity : CMRAIdentity mapRA.
 Proof.
   split.
-  - by intros ? n; rewrite lookup_empty.
+  - by intros i; rewrite lookup_empty.
   - by intros m i; rewrite /= lookup_op lookup_empty (left_id_L None _).
   - apply map_empty_timeless.
 Qed.
@@ -187,18 +189,18 @@ Implicit Types a : A.
 Lemma map_lookup_validN n m i x : ✓{n} m → m !! i ≡{n}≡ Some x → ✓{n} x.
 Proof. by move=> /(_ i) Hm Hi; move:Hm; rewrite Hi. Qed.
 Lemma map_lookup_valid m i x : ✓ m → m !! i ≡ Some x → ✓ x.
-Proof. move=>Hm Hi n. move:(Hm n i). by rewrite Hi. Qed.
+Proof. move=> Hm Hi. move:(Hm i). by rewrite Hi. Qed.
 Lemma map_insert_validN n m i x : ✓{n} x → ✓{n} m → ✓{n} <[i:=x]>m.
 Proof. by intros ?? j; destruct (decide (i = j)); simplify_map_eq. Qed.
 Lemma map_insert_valid m i x : ✓ x → ✓ m → ✓ <[i:=x]>m.
-Proof. intros ?? n j; apply map_insert_validN; auto. Qed.
+Proof. by intros ?? j; destruct (decide (i = j)); simplify_map_eq. Qed.
 Lemma map_singleton_validN n i x : ✓{n} ({[ i := x ]} : gmap K A) ↔ ✓{n} x.
 Proof.
-  split; [|by intros; apply map_insert_validN, cmra_empty_valid].
+  split; [|by intros; apply map_insert_validN, cmra_empty_validN].
   by move=>/(_ i); simplify_map_eq.
 Qed.
 Lemma map_singleton_valid i x : ✓ ({[ i := x ]} : gmap K A) ↔ ✓ x.
-Proof. split; intros ? n; eapply map_singleton_validN; eauto. Qed.
+Proof. rewrite !cmra_valid_validN. by setoid_rewrite map_singleton_validN. Qed.
 
 Lemma map_insert_singleton_opN n m i x :
   m !! i = None ∨ m !! i ≡{n}≡ Some (unit x) → <[i:=x]> m ≡{n}≡ {[ i := x ]} ⋅ m.
@@ -275,7 +277,7 @@ Proof.
   intros Hx HQ n gf Hg.
   destruct (Hx n (from_option ∅ (gf !! i))) as (y&?&Hy).
   { move:(Hg i). rewrite !left_id.
-    case _: (gf !! i); simpl; auto using cmra_empty_valid. }
+    case _: (gf !! i); simpl; auto using cmra_empty_validN. }
   exists {[ i := y ]}; split; first by auto.
   intros i'; destruct (decide (i' = i)) as [->|].
   - rewrite lookup_op lookup_singleton.

algebra/iprod.v

@@ -118,6 +118,7 @@ Section iprod_cmra.
 
   Instance iprod_op : Op (iprod B) := λ f g x, f x ⋅ g x.
   Instance iprod_unit : Unit (iprod B) := λ f x, unit (f x).
+  Instance iprod_valid : Valid (iprod B) := λ f, ∀ x, ✓ f x.
   Instance iprod_validN : ValidN (iprod B) := λ n f, ∀ x, ✓{n} f x.
   Instance iprod_minus : Minus (iprod B) := λ f g x, f x ⩪ g x.
 
@@ -140,6 +141,9 @@ Section iprod_cmra.
     - by intros n f1 f2 Hf x; rewrite iprod_lookup_unit (Hf x).
     - by intros n f1 f2 Hf ? x; rewrite -(Hf x).
     - by intros n f f' Hf g g' Hg i; rewrite iprod_lookup_minus (Hf i) (Hg i).
+    - intros g; split.
+      + intros Hg n i; apply cmra_valid_validN, Hg.
+      + intros Hg i; apply cmra_valid_validN=> n; apply Hg.
     - intros n f Hf x; apply cmra_validN_S, Hf.
     - by intros f1 f2 f3 x; rewrite iprod_lookup_op assoc.
     - by intros f1 f2 x; rewrite iprod_lookup_op comm.
@@ -160,7 +164,7 @@ Section iprod_cmra.
     (∀ x, CMRAIdentity (B x)) → CMRAIdentity iprodRA.
   Proof.
     intros ?; split.
-    - intros n x; apply cmra_empty_valid.
+    - intros x; apply cmra_empty_valid.
     - by intros f x; rewrite iprod_lookup_op left_id.
     - by apply _.
   Qed.
@@ -204,7 +208,7 @@ Section iprod_cmra.
     split; [by move=>/(_ x); rewrite iprod_lookup_singleton|].
     move=>Hx x'; destruct (decide (x = x')) as [->|];
       rewrite ?iprod_lookup_singleton ?iprod_lookup_singleton_ne //.
-    by apply cmra_empty_valid.
+    by apply cmra_empty_validN.
   Qed.
 
   Lemma iprod_unit_singleton x (y : B x) :

algebra/option.v

@@ -61,6 +61,8 @@ Arguments optionC : clear implicits.
 Section cmra.
 Context {A : cmraT}.
 
+Instance option_valid : Valid (option A) := λ mx,
+  match mx with Some x => ✓ x | None => True end.
 Instance option_validN : </