Make CMRAExtend part of CMRAMixin.

algebra/agree.v

@@ -59,6 +59,7 @@ Program Instance agree_op : Op (agree A) := λ x y,
 Next Obligation. naive_solver eauto using agree_valid_S, dist_S. Qed.
 Instance agree_unit : Unit (agree A) := id.
 Instance agree_minus : Minus (agree A) := λ x y, x.
+
 Instance: Comm (≡) (@op (agree A) _).
 Proof. intros x y; split; [naive_solver|by intros n (?&?&Hxy); apply Hxy]. Qed.
 Lemma agree_idemp (x : agree A) : x ⋅ x ≡ x.
@@ -87,11 +88,20 @@ Proof.
     repeat match goal with H : agree_is_valid _ _ |- _ => clear H end;
     by cofe_subst; rewrite !agree_idemp.
 Qed.
+
 Lemma agree_includedN n (x y : agree A) : x ≼{n} y ↔ y ≡{n}≡ x ⋅ y.
 Proof.
   split; [|by intros ?; exists y].
   by intros [z Hz]; rewrite Hz assoc agree_idemp.
 Qed.
+Lemma agree_op_inv n (x1 x2 : agree A) : ✓{n} (x1 ⋅ x2) → x1 ≡{n}≡ x2.
+Proof. intros Hxy; apply Hxy. Qed.
+Lemma agree_valid_includedN n (x y : agree A) : ✓{n} y → x ≼{n} y → x ≡{n}≡ y.
+Proof.
+  move=> Hval [z Hy]; move: Hval; rewrite Hy.
+  by move=> /agree_op_inv->; rewrite agree_idemp.
+Qed.
+
 Definition agree_cmra_mixin : CMRAMixin (agree A).
 Proof.
   split; try (apply _ || done).
@@ -102,22 +112,11 @@ Proof.
   - intros x; apply agree_idemp.
   - by intros n x y [(?&?&?) ?].
   - by intros n x y; rewrite agree_includedN.
+  - intros n x y1 y2 Hval Hx; exists (x,x); simpl; split.
+    + by rewrite agree_idemp.
+    + by move: Hval; rewrite Hx; move=> /agree_op_inv->; rewrite agree_idemp.
 Qed.
-Lemma agree_op_inv n (x1 x2 : agree A) : ✓{n} (x1 ⋅ x2) → x1 ≡{n}≡ x2.
-Proof. intros Hxy; apply Hxy. Qed.
-Lemma agree_valid_includedN n (x y : agree A) : ✓{n} y → x ≼{n} y → x ≡{n}≡ y.
-Proof.
-  move=> Hval [z Hy]; move: Hval; rewrite Hy.
-  by move=> /agree_op_inv->; rewrite agree_idemp.
-Qed.
-Definition agree_cmra_extend_mixin : CMRAExtendMixin (agree A).
-Proof.
-  intros n x y1 y2 Hval Hx; exists (x,x); simpl; split.
-  - by rewrite agree_idemp.
-  - by move: Hval; rewrite Hx; move=> /agree_op_inv->; rewrite agree_idemp.
-Qed.
-Canonical Structure agreeRA : cmraT :=
-  CMRAT agree_cofe_mixin agree_cmra_mixin agree_cmra_extend_mixin.
+Canonical Structure agreeRA : cmraT := CMRAT agree_cofe_mixin agree_cmra_mixin.
 
 Program Definition to_agree (x : A) : agree A :=
   {| agree_car n := x; agree_is_valid n := True |}.

algebra/auth.v

@@ -118,18 +118,14 @@ Proof.
      naive_solver eauto using cmra_validN_op_l, cmra_validN_includedN.
   - by intros n ??; rewrite auth_includedN;
       intros [??]; split; simpl; apply cmra_op_minus.
+  - intros n x y1 y2 ? [??]; simpl in *.
+    destruct (cmra_extend n (authoritative x) (authoritative y1)
+      (authoritative y2)) as (ea&?&?&?); auto using authoritative_validN.
+    destruct (cmra_extend n (own x) (own y1) (own y2))
+      as (b&?&?&?); auto using own_validN.
+    by exists (Auth (ea.1) (b.1), Auth (ea.2) (b.2)).
 Qed.
-Definition auth_cmra_extend_mixin : CMRAExtendMixin (auth A).
-Proof.
-  intros n x y1 y2 ? [??]; simpl in *.
-  destruct (cmra_extend_op n (authoritative x) (authoritative y1)
-    (authoritative y2)) as (ea&?&?&?); auto using authoritative_validN.
-  destruct (cmra_extend_op n (own x) (own y1) (own y2))
-    as (b&?&?&?); auto using own_validN.
-  by exists (Auth (ea.1) (b.1), Auth (ea.2) (b.2)).
-Qed.
-Canonical Structure authRA : cmraT :=
-  CMRAT auth_cofe_mixin auth_cmra_mixin auth_cmra_extend_mixin.
+Canonical Structure authRA : cmraT := CMRAT auth_cofe_mixin auth_cmra_mixin.
 
 (** Internalized properties *)
 Lemma auth_equivI {M} (x y : auth A) :

algebra/cmra.v

@@ -49,11 +49,11 @@ Record CMRAMixin A `{Dist A, Equiv A, Unit A, Op A, ValidN A, Minus A} := {
   mixin_cmra_unit_idemp x : unit (unit x) ≡ unit x;
   mixin_cmra_unit_preservingN n x y : x ≼{n} y → unit x ≼{n} unit y;
   mixin_cmra_validN_op_l n x y : ✓{n} (x ⋅ y) → ✓{n} x;
-  mixin_cmra_op_minus n x y : x ≼{n} y → x ⋅ y ⩪ x ≡{n}≡ y
+  mixin_cmra_op_minus n x y : x ≼{n} y → x ⋅ y ⩪ x ≡{n}≡ y;
+  mixin_cmra_extend n x y1 y2 :
+    ✓{n} x → x ≡{n}≡ y1 ⋅ y2 →
+    { z | x ≡ z.1 ⋅ z.2 ∧ z.1 ≡{n}≡ y1 ∧ z.2 ≡{n}≡ y2 }
 }.
-Definition CMRAExtendMixin A `{Equiv A, Dist A, Op A, ValidN A} := ∀ n x y1 y2,
-  ✓{n} x → x ≡{n}≡ y1 ⋅ y2 →
-  { z | x ≡ z.1 ⋅ z.2 ∧ z.1 ≡{n}≡ y1 ∧ z.2 ≡{n}≡ y2 }.
 
 (** Bundeled version *)
 Structure cmraT := CMRAT {
@@ -66,10 +66,9 @@ Structure cmraT := CMRAT {
   cmra_validN : ValidN cmra_car;
   cmra_minus : Minus cmra_car;
   cmra_cofe_mixin : CofeMixin cmra_car;
-  cmra_mixin : CMRAMixin cmra_car;
-  cmra_extend_mixin : CMRAExtendMixin 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.
@@ -80,7 +79,6 @@ Arguments cmra_validN : simpl never.
 Arguments cmra_minus : simpl never.
 Arguments cmra_cofe_mixin : simpl never.
 Arguments cmra_mixin : simpl never.
-Arguments cmra_extend_mixin : simpl never.
 Add Printing Constructor cmraT.
 Existing Instances cmra_unit cmra_op cmra_validN cmra_minus.
 Coercion cmra_cofeC (A : cmraT) : cofeT := CofeT (cmra_cofe_mixin A).
@@ -115,10 +113,10 @@ Section cmra_mixin.
   Proof. apply (mixin_cmra_validN_op_l _ (cmra_mixin A)). Qed.
   Lemma cmra_op_minus n x y : x ≼{n} y → x ⋅ y ⩪ x ≡{n}≡ y.
   Proof. apply (mixin_cmra_op_minus _ (cmra_mixin A)). Qed.
-  Lemma cmra_extend_op n x y1 y2 :
+  Lemma cmra_extend n x y1 y2 :
     ✓{n} x → x ≡{n}≡ y1 ⋅ y2 →
     { z | x ≡ z.1 ⋅ z.2 ∧ z.1 ≡{n}≡ y1 ∧ z.2 ≡{n}≡ y2 }.
-  Proof. apply (cmra_extend_mixin A). Qed.
+  Proof. apply (mixin_cmra_extend _ (cmra_mixin A)). Qed.
 End cmra_mixin.
 
 (** * CMRAs with a global identity element *)
@@ -301,7 +299,7 @@ Qed.
 Lemma cmra_timeless_included_l x y : Timeless x → ✓{0} y → x ≼{0} y → x ≼ y.
 Proof.
   intros ?? [x' ?].
-  destruct (cmra_extend_op 0 y x x') as ([z z']&Hy&Hz&Hz'); auto; simpl in *.
+  destruct (cmra_extend 0 y x x') as ([z z']&Hy&Hz&Hz'); auto; simpl in *.
   by exists z'; rewrite Hy (timeless x z).
 Qed.
 Lemma cmra_timeless_included_r n x y : Timeless y → x ≼{0} y → x ≼{n} y.
@@ -310,7 +308,7 @@ Lemma cmra_op_timeless x1 x2 :
   ✓ (x1 ⋅ x2) → Timeless x1 → Timeless x2 → Timeless (x1 ⋅ x2).
 Proof.
   intros ??? z Hz.
-  destruct (cmra_extend_op 0 z x1 x2) as ([y1 y2]&Hz'&?&?); auto; simpl in *.
+  destruct (cmra_extend 0 z x1 x2) as ([y1 y2]&Hz'&?&?); auto; simpl in *.
   { by rewrite -?Hz. }
   by rewrite Hz' (timeless x1 y1) // (timeless x2 y2).
 Qed.
@@ -471,16 +469,12 @@ Section discrete.
   Instance discrete_validN : ValidN A := λ n x, ✓ x.
   Definition discrete_cmra_mixin : CMRAMixin A.
   Proof.
-    by destruct ra; split; unfold Proper, respectful, includedN;
-      try setoid_rewrite <-(timeless_iff _ _).
-  Qed.
-  Definition discrete_extend_mixin : CMRAExtendMixin 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.
   Qed.
-  Definition discreteRA : cmraT :=
-    CMRAT (cofe_mixin A) discrete_cmra_mixin discrete_extend_mixin.
+  Definition discreteRA : cmraT := CMRAT (cofe_mixin A) discrete_cmra_mixin.
   Lemma discrete_updateP (x : discreteRA) (P : A → Prop) :
     (∀ z, ✓ (x ⋅ z) → ∃ y, P y ∧ ✓ (y ⋅ z)) → x ~~>: P.
   Proof. intros Hvalid n z; apply Hvalid. Qed.
@@ -542,16 +536,12 @@ Section prod.
     - intros n x y [??]; split; simpl in *; eauto using cmra_validN_op_l.
     - intros n x y; rewrite prod_includedN; intros [??].
       by split; apply cmra_op_minus.
+    - intros n x y1 y2 [??] [??]; simpl in *.
+      destruct (cmra_extend n (x.1) (y1.1) (y2.1)) as (z1&?&?&?); auto.
+      destruct (cmra_extend n (x.2) (y1.2) (y2.2)) as (z2&?&?&?); auto.
+      by exists ((z1.1,z2.1),(z1.2,z2.2)).
   Qed.
-  Definition prod_cmra_extend_mixin : CMRAExtendMixin (A * B).
-  Proof.
-    intros n x y1 y2 [??] [??]; simpl in *.
-    destruct (cmra_extend_op n (x.1) (y1.1) (y2.1)) as (z1&?&?&?); auto.
-    destruct (cmra_extend_op n (x.2) (y1.2) (y2.2)) as (z2&?&?&?); auto.
-    by exists ((z1.1,z2.1),(z1.2,z2.2)).
-  Qed.
-  Canonical Structure prodRA : cmraT :=
-    CMRAT prod_cofe_mixin prod_cmra_mixin prod_cmra_extend_mixin.
+  Canonical Structure prodRA : cmraT := CMRAT prod_cofe_mixin prod_cmra_mixin.
   Global Instance prod_cmra_identity `{Empty A, Empty B} :
     CMRAIdentity A → CMRAIdentity B → CMRAIdentity prodRA.
   Proof.

algebra/excl.v

@@ -114,18 +114,14 @@ Proof.
   - by intros n [?| |] [?| |]; exists ∅.
   - by intros n [?| |] [?| |].
   - by intros n [?| |] [?| |] [[?| |] Hz]; inversion_clear Hz; constructor.
+  - intros n x y1 y2 ? Hx.
+    by exists match y1, y2 with
+      | Excl a1, Excl a2 => (Excl a1, Excl a2)
+      | ExclBot, _ => (ExclBot, y2) | _, ExclBot => (y1, ExclBot)
+      | ExclUnit, _ => (ExclUnit, x) | _, ExclUnit => (x, ExclUnit)
+      end; destruct y1, y2; inversion_clear Hx; repeat constructor.
 Qed.
-Definition excl_cmra_extend_mixin : CMRAExtendMixin (excl A).
-Proof.
-  intros n x y1 y2 ? Hx.
-  by exists match y1, y2 with
-    | Excl a1, Excl a2 => (Excl a1, Excl a2)
-    | ExclBot, _ => (ExclBot, y2) | _, ExclBot => (y1, ExclBot)
-    | ExclUnit, _ => (ExclUnit, x) | _, ExclUnit => (x, ExclUnit)
-    end; destruct y1, y2; inversion_clear Hx; repeat constructor.
-Qed.
-Canonical Structure exclRA : cmraT :=
-  CMRAT excl_cofe_mixin excl_cmra_mixin excl_cmra_extend_mixin.
+Canonical Structure exclRA : cmraT := CMRAT excl_cofe_mixin excl_cmra_mixin.
 Global Instance excl_cmra_identity : CMRAIdentity exclRA.
 Proof. split. done. by intros []. apply _. Qed.
 Lemma excl_validN_inv_l n x y : ✓{n} (Excl x ⋅ y) → y = ∅.

algebra/fin_maps.v

@@ -142,27 +142,23 @@ Proof.
     by rewrite -lookup_op.
   - intros n x y; rewrite map_includedN_spec=> ? i.
     by rewrite lookup_op lookup_minus cmra_op_minus.
+  - intros n m m1 m2 Hm Hm12.
+    assert (∀ i, m !! i ≡{n}≡ m1 !! i ⋅ m2 !! i) as Hm12'
+      by (by intros i; rewrite -lookup_op).
+    set (f i := cmra_extend n (m !! i) (m1 !! i) (m2 !! i) (Hm i) (Hm12' i)).
+    set (f_proj i := proj1_sig (f i)).
+    exists (map_imap (λ i _, (f_proj i).1) m, map_imap (λ i _, (f_proj i).2) m);
+      repeat split; intros i; rewrite /= ?lookup_op !lookup_imap.
+    + destruct (m !! i) as [x|] eqn:Hx; rewrite !Hx /=; [|constructor].
+      rewrite -Hx; apply (proj2_sig (f i)).
+    + destruct (m !! i) as [x|] eqn:Hx; rewrite /=; [apply (proj2_sig (f i))|].
+      pose proof (Hm12' i) as Hm12''; rewrite Hx in Hm12''.
+      by symmetry; apply option_op_positive_dist_l with (m2 !! i).
+    + destruct (m !! i) as [x|] eqn:Hx; simpl; [apply (proj2_sig (f i))|].
+      pose proof (Hm12' i) as Hm12''; rewrite Hx in Hm12''.
+      by symmetry; apply option_op_positive_dist_r with (m1 !! i).
 Qed.
-Definition map_cmra_extend_mixin : CMRAExtendMixin (gmap K A).
-Proof.
-  intros n m m1 m2 Hm Hm12.
-  assert (∀ i, m !! i ≡{n}≡ m1 !! i ⋅ m2 !! i) as Hm12'
-    by (by intros i; rewrite -lookup_op).
-  set (f i := cmra_extend_op n (m !! i) (m1 !! i) (m2 !! i) (Hm i) (Hm12' i)).
-  set (f_proj i := proj1_sig (f i)).
-  exists (map_imap (λ i _, (f_proj i).1) m, map_imap (λ i _, (f_proj i).2) m);
-    repeat split; intros i; rewrite /= ?lookup_op !lookup_imap.
-  - destruct (m !! i) as [x|] eqn:Hx; rewrite !Hx /=; [|constructor].
-    rewrite -Hx; apply (proj2_sig (f i)).
-  - destruct (m !! i) as [x|] eqn:Hx; rewrite /=; [apply (proj2_sig (f i))|].
-    pose proof (Hm12' i) as Hm12''; rewrite Hx in Hm12''.
-    by symmetry; apply option_op_positive_dist_l with (m2 !! i).
-  - destruct (m !! i) as [x|] eqn:Hx; simpl; [apply (proj2_sig (f i))|].
-    pose proof (Hm12' i) as Hm12''; rewrite Hx in Hm12''.
-    by symmetry; apply option_op_positive_dist_r with (m1 !! i).
-Qed.
-Canonical Structure mapRA : cmraT :=
-  CMRAT map_cofe_mixin map_cmra_mixin map_cmra_extend_mixin.
+Canonical Structure mapRA : cmraT := CMRAT map_cofe_mixin map_cmra_mixin.
 Global Instance map_cmra_identity : CMRAIdentity mapRA.
 Proof.
   split.

algebra/iprod.v

@@ -150,16 +150,12 @@ Section iprod_cmra.
     - intros n f1 f2 Hf x; apply cmra_validN_op_l with (f2 x), Hf.
     - intros n f1 f2; rewrite iprod_includedN_spec=> Hf x.
       by rewrite iprod_lookup_op iprod_lookup_minus cmra_op_minus; try apply Hf.
+    - intros n f f1 f2 Hf Hf12.
+      set (g x := cmra_extend n (f x) (f1 x) (f2 x) (Hf x) (Hf12 x)).
+      exists ((λ x, (proj1_sig (g x)).1), (λ x, (proj1_sig (g x)).2)).
+      split_and?; intros x; apply (proj2_sig (g x)).
   Qed.
-  Definition iprod_cmra_extend_mixin : CMRAExtendMixin (iprod B).
-  Proof.
-    intros n f f1 f2 Hf Hf12.
-    set (g x := cmra_extend_op n (f x) (f1 x) (f2 x) (Hf x) (Hf12 x)).
-    exists ((λ x, (proj1_sig (g x)).1), (λ x, (proj1_sig (g x)).2)).
-    split_and?; intros x; apply (proj2_sig (g x)).
-  Qed.
-  Canonical Structure iprodRA : cmraT :=
-    CMRAT iprod_cofe_mixin iprod_cmra_mixin iprod_cmra_extend_mixin.
+  Canonical Structure iprodRA : cmraT := CMRAT iprod_cofe_mixin iprod_cmra_mixin.
   Global Instance iprod_cmra_identity `{∀ x, Empty (B x)} :
     (∀ x, CMRAIdentity (B x)) → CMRAIdentity iprodRA.
   Proof.

algebra/option.v

@@ -105,21 +105,17 @@ Proof.
   - intros n mx my; rewrite option_includedN.
     intros [->|(x&y&->&->&?)]; [by destruct my|].
     by constructor; apply cmra_op_minus.
+  - intros n mx my1 my2.
+    destruct mx as [x|], my1 as [y1|], my2 as [y2|]; intros Hx Hx';
+      try (by exfalso; inversion Hx'; auto).
+    + destruct (cmra_extend n x y1 y2) as ([z1 z2]&?&?&?); auto.
+      { by inversion_clear Hx'. }
+      by exists (Some z1, Some z2); repeat constructor.
+    + by exists (Some x,None); inversion Hx'; repeat constructor.
+    + by exists (None,Some x); inversion Hx'; repeat constructor.
+    + exists (None,None); repeat constructor.
 Qed.
-Definition option_cmra_extend_mixin : CMRAExtendMixin (option A).
-Proof.
-  intros n mx my1 my2.
-  destruct mx as [x|], my1 as [y1|], my2 as [y2|]; intros Hx Hx';
-    try (by exfalso; inversion Hx'; auto).
-  - destruct (cmra_extend_op n x y1 y2) as ([z1 z2]&?&?&?); auto.
-    { by inversion_clear Hx'. }
-    by exists (Some z1, Some z2); repeat constructor.
-  - by exists (Some x,None); inversion Hx'; repeat constructor.
-  - by exists (None,Some x); inversion Hx'; repeat constructor.
-  - exists (None,None); repeat constructor.
-Qed.
-Canonical Structure optionRA :=
-  CMRAT option_cofe_mixin option_cmra_mixin option_cmra_extend_mixin.
+Canonical Structure optionRA := CMRAT option_cofe_mixin option_cmra_mixin.
 Global Instance option_cmra_identity : CMRAIdentity optionRA.
 Proof. split. done. by intros []. by inversion_clear 1. Qed.
 

algebra/upred.v

@@ -818,7 +818,7 @@ Proof.
   split=> n x ?; split.
   - destruct n as [|n]; simpl.
     { by exists x, (unit x); rewrite cmra_unit_r. }
-    intros (x1&x2&Hx&?&?); destruct (cmra_extend_op n x x1 x2)
+    intros (x1&x2&Hx&?&?); destruct (cmra_extend n x x1 x2)
       as ([y1 y2]&Hx'&Hy1&Hy2); eauto using cmra_validN_S; simpl in *.
     exists y1, y2; split; [by rewrite Hx'|by rewrite Hy1 Hy2].
   - destruct n as [|n]; simpl; [done|intros (x1&x2&Hx&?&?)].

program_logic/resources.v

@@ -113,17 +113,13 @@ Proof.
       split_and!; simpl in *; eapply cmra_validN_op_l; eauto.
   - intros n r1 r2; rewrite res_includedN; intros (?&?&?).
     by constructor; apply cmra_op_minus.
+  - intros n r r1 r2 (?&?&?) [???]; simpl in *.
+    destruct (cmra_extend n (wld r) (wld r1) (wld r2)) as ([w w']&?&?&?),
+      (cmra_extend n (pst r) (pst r1) (pst r2)) as ([σ σ']&?&?&?),
+      (cmra_extend n (gst r) (gst r1) (gst r2)) as ([m m']&?&?&?); auto.
+    by exists (Res w σ m, Res w' σ' m').
 Qed.
-Definition res_cmra_extend_mixin : CMRAExtendMixin (res Λ Σ A).
-Proof.
-  intros n r r1 r2 (?&?&?) [???]; simpl in *.
-  destruct (cmra_extend_op n (wld r) (wld r1) (wld r2)) as ([w w']&?&?&?),
-    (cmra_extend_op n (pst r) (pst r1) (pst r2)) as ([σ σ']&?&?&?),
-    (cmra_extend_op n (gst r) (gst r1) (gst r2)) as ([m m']&?&?&?); auto.
-  by exists (Res w σ m, Res w' σ' m').
-Qed.
-Canonical Structure resRA : cmraT :=
-  CMRAT res_cofe_mixin res_cmra_mixin res_cmra_extend_mixin.
+Canonical Structure resRA : cmraT := CMRAT res_cofe_mixin res_cmra_mixin.
 Global Instance res_cmra_identity : CMRAIdentity resRA.
 Proof.
   split.