Change cmra_extend to have an exist instead of a sig.

This is more consistent with the definition of the extension order, which
is also defined in terms of an existential.

algebra/agree.v

@@ -108,7 +108,7 @@ Proof.
     symmetry; apply dist_le with n; try apply Hx; auto.
   - intros x. apply agree_idemp.
   - by intros n x y [(?&?&?) ?].
-  - intros n x y1 y2 Hval Hx; exists (x,x); simpl; split.
+  - 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.

algebra/auth.v

@@ -134,10 +134,10 @@ Proof.
      naive_solver eauto using cmra_validN_op_l, cmra_validN_includedN.
   - intros n x y1 y2 ? [??]; simpl in *.
     destruct (cmra_extend n (authoritative x) (authoritative y1)
-      (authoritative y2)) as (ea&?&?&?); auto using authoritative_validN.
+      (authoritative y2)) as (ea1&ea2&?&?&?); auto using authoritative_validN.
     destruct (cmra_extend n (auth_own x) (auth_own y1) (auth_own y2))
-      as (b&?&?&?); auto using auth_own_validN.
-    by exists (Auth (ea.1) (b.1), Auth (ea.2) (b.2)).
+      as (b1&b2&?&?&?); auto using auth_own_validN.
+    by exists (Auth ea1 b1), (Auth ea2 b2).
 Qed.
 Canonical Structure authR := CMRAT (auth A) auth_cofe_mixin auth_cmra_mixin.
 

algebra/cmra.v

@@ -53,7 +53,7 @@ Record CMRAMixin A `{Dist A, Equiv A, PCore A, Op A, Valid A, ValidN A} := {
   mixin_cmra_validN_op_l n x y : ✓{n} (x ⋅ y) → ✓{n} x;
   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 }
+    ∃ z1 z2, x ≡ z1 ⋅ z2 ∧ z1 ≡{n}≡ y1 ∧ z2 ≡{n}≡ y2
 }.
 
 (** Bundeled version *)
@@ -120,7 +120,7 @@ Section cmra_mixin.
   Proof. apply (mixin_cmra_validN_op_l _ (cmra_mixin A)). Qed.
   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 }.
+    ∃ z1 z2, x ≡ z1 ⋅ z2 ∧ z1 ≡{n}≡ y1 ∧ z2 ≡{n}≡ y2.
   Proof. apply (mixin_cmra_extend _ (cmra_mixin A)). Qed.
 End cmra_mixin.
 
@@ -472,7 +472,7 @@ End total_core.
 Lemma cmra_timeless_included_l x y : Timeless x → ✓{0} y → x ≼{0} y → x ≼ y.
 Proof.
   intros ?? [x' ?].
-  destruct (cmra_extend 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.
@@ -481,7 +481,7 @@ Lemma cmra_op_timeless x1 x2 :
   ✓ (x1 ⋅ x2) → Timeless x1 → Timeless x2 → Timeless (x1 ⋅ x2).
 Proof.
   intros ??? z Hz.
-  destruct (cmra_extend 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 *.
   { rewrite -?Hz. by apply cmra_valid_validN. }
   by rewrite Hz' (timeless x1 y1) // (timeless x2 y2).
 Qed.
@@ -540,7 +540,7 @@ Section cmra_total.
   Context (validN_op_l : ∀ n (x y : A), ✓{n} (x ⋅ y) → ✓{n} x).
   Context (extend : ∀ n (x y1 y2 : A),
     ✓{n} x → x ≡{n}≡ y1 ⋅ y2 →
-    { z | x ≡ z.1 ⋅ z.2 ∧ z.1 ≡{n}≡ y1 ∧ z.2 ≡{n}≡ y2 }).
+    ∃ z1 z2, x ≡ z1 ⋅ z2 ∧ z1 ≡{n}≡ y1 ∧ z2 ≡{n}≡ y2).
   Lemma cmra_total_mixin : CMRAMixin A.
   Proof.
     split; auto.
@@ -690,7 +690,7 @@ Section discrete.
   Proof.
     destruct ra_mix; split; try done.
     - intros x; split; first done. by move=> /(_ 0).
-    - intros n x y1 y2 ??; by exists (y1,y2).
+    - intros n x y1 y2 ??; by exists y1, y2.
   Qed.
 End discrete.
 
@@ -881,9 +881,9 @@ Section prod.
       exists (z1,z2). by rewrite prod_included prod_pcore_Some.
     - intros n x y [??]; split; simpl in *; eauto using cmra_validN_op_l.
     - 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)).
+      destruct (cmra_extend n (x.1) (y1.1) (y2.1)) as (z11&z12&?&?&?); auto.
+      destruct (cmra_extend n (x.2) (y1.2) (y2.2)) as (z21&z22&?&?&?); auto.
+      by exists (z11,z21), (z12,z22).
   Qed.
   Canonical Structure prodR :=
     CMRAT (A * B) prod_cofe_mixin prod_cmra_mixin.
@@ -1048,13 +1048,12 @@ Section option.
         eauto using cmra_validN_op_l.
     - 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.
+        inversion_clear Hx'; auto.
+      + destruct (cmra_extend n x y1 y2) as (z1&z2&?&?&?); auto.
+        by exists (Some z1), (Some z2); repeat constructor.
+      + by exists (Some x), None; repeat constructor.
+      + by exists None, (Some x); repeat constructor.
+      + exists None, None; repeat constructor.
   Qed.
   Canonical Structure optionR :=
     CMRAT (option A) option_cofe_mixin option_cmra_mixin.

algebra/csum.v

@@ -209,15 +209,13 @@ Proof.
       exists (Cinr cb'). rewrite csum_included; eauto 10.
   - intros n [a1|b1|] [a2|b2|]; simpl; eauto using cmra_validN_op_l; done.
   - intros n [a|b|] y1 y2 Hx Hx'.
-    + destruct y1 as [a1|b1|], y2 as [a2|b2|]; try (exfalso; by inversion_clear Hx').
-      apply (inj Cinl) in Hx'.
-      destruct (cmra_extend n a a1 a2) as ([z1 z2]&?&?&?); auto.
-      exists (Cinl z1, Cinl z2). by repeat constructor.
-    + destruct y1 as [a1|b1|], y2 as [a2|b2|]; try (exfalso; by inversion_clear Hx').
-      apply (inj Cinr) in Hx'.
-      destruct (cmra_extend n b b1 b2) as ([z1 z2]&?&?&?); auto.
-      exists (Cinr z1, Cinr z2). by repeat constructor.
-    + by exists (CsumBot, CsumBot); destruct y1, y2; inversion_clear Hx'.
+    + destruct y1 as [a1|b1|], y2 as [a2|b2|]; inversion_clear Hx'.
+      destruct (cmra_extend n a a1 a2) as (z1&z2&?&?&?); auto.
+      exists (Cinl z1), (Cinl z2). by repeat constructor.
+    + destruct y1 as [a1|b1|], y2 as [a2|b2|]; inversion_clear Hx'.
+      destruct (cmra_extend n b b1 b2) as (z1&z2&?&?&?); auto.
+      exists (Cinr z1), (Cinr z2). by repeat constructor.
+    + by exists CsumBot, CsumBot; destruct y1, y2; inversion_clear Hx'.
 Qed.
 Canonical Structure csumR :=
   CMRAT (csum A B) csum_cofe_mixin csum_cmra_mixin.

algebra/excl.v

@@ -88,11 +88,7 @@ Proof.
   - by intros [?|] [?|] [?|]; constructor.
   - by intros [?|] [?|]; constructor.
   - by intros n [?|] [?|].
-  - 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)
-      end; destruct y1, y2; inversion_clear Hx; repeat constructor.
+  - intros n x [?|] [?|] ?; inversion_clear 1; eauto.
 Qed.
 Canonical Structure exclR :=
   CMRAT (excl A) excl_cofe_mixin excl_cmra_mixin.

algebra/gmap.v

@@ -137,21 +137,30 @@ Proof.
     rewrite !lookup_core. by apply cmra_core_mono.
   - intros n m1 m2 Hm i; apply cmra_validN_op_l with (m2 !! i).
     by rewrite -lookup_op.
-  - 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))|].
-      move: (Hm12' i). rewrite Hx -!timeless_iff.
-      rewrite !(symmetry_iff _ None) !equiv_None op_None; tauto.
-    + destruct (m !! i) as [x|] eqn:Hx; simpl; [apply (proj2_sig (f i))|].
-      move: (Hm12' i). rewrite Hx -!timeless_iff.
-      rewrite !(symmetry_iff _ None) !equiv_None op_None; tauto.
+  - intros n m. induction m as [|i x m Hi IH] using map_ind=> m1 m2 Hmv Hm.
+    { exists ∅, ∅; split_and!=> -i; symmetry; symmetry in Hm; move: Hm=> /(_ i);
+        rewrite !lookup_op !lookup_empty ?dist_None op_None; intuition. }
+    destruct (IH (delete i m1) (delete i m2)) as (m1'&m2'&Hm'&Hm1'&Hm2').
+    { intros j; move: Hmv=> /(_ j). destruct (decide (i = j)) as [->|].
+      + intros _. by rewrite Hi.
+      + by rewrite lookup_insert_ne. }
+    { intros j; move: Hm=> /(_ j); destruct (decide (i = j)) as [->|].
+      + intros _. by rewrite lookup_op !lookup_delete Hi.
+      + by rewrite !lookup_op lookup_insert_ne // !lookup_delete_ne. }
+    destruct (cmra_extend n (Some x) (m1 !! i) (m2 !! i)) as (y1&y2&?&?&?).
+    { move: Hmv=> /(_ i). by rewrite lookup_insert. } 
+    { move: Hm=> /(_ i). by rewrite lookup_insert lookup_op. }
+    exists (partial_alter (λ _, y1) i m1'), (partial_alter (λ _, y2) i m2').
+    split_and!.
+    + intros j. destruct (decide (i = j)) as [->|].
+      * by rewrite lookup_insert lookup_op !lookup_partial_alter.
+      * by rewrite lookup_insert_ne // Hm' !lookup_op !lookup_partial_alter_ne.
+    + intros j. destruct (decide (i = j)) as [->|].
+      * by rewrite lookup_partial_alter.
+      * by rewrite lookup_partial_alter_ne // Hm1' lookup_delete_ne.
+    + intros j. destruct (decide (i = j)) as [->|].
+      * by rewrite lookup_partial_alter.
+      * by rewrite lookup_partial_alter_ne // Hm2' lookup_delete_ne.
 Qed.
 Canonical Structure gmapR :=
   CMRAT (gmap K A) gmap_cofe_mixin gmap_cmra_mixin.

algebra/iprod.v

@@ -117,9 +117,12 @@ Section iprod_cmra.
       by rewrite iprod_lookup_core; apply cmra_core_mono, Hf.
     - intros n f1 f2 Hf x; apply cmra_validN_op_l with (f2 x), 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)).
+      destruct (finite_choice (λ x (yy : B x * B x),
+        f x ≡ yy.1 ⋅ yy.2 ∧ yy.1 ≡{n}≡ f1 x ∧ yy.2 ≡{n}≡ f2 x)) as [gg Hgg].
+      { intros x. specialize (Hf12 x).
+        destruct (cmra_extend n (f x) (f1 x) (f2 x)) as (y1&y2&?&?&?); eauto.
+        exists (y1,y2); eauto. }
+      exists (λ x, gg x.1), (λ x, gg x.2). split_and!=> -?; naive_solver.
   Qed.
   Canonical Structure iprodR :=
     CMRAT (iprod B) iprod_cofe_mixin iprod_cmra_mixin.

algebra/list.v

@@ -193,15 +193,14 @@ Section cmra.
       rewrite !list_lookup_core. by apply cmra_core_mono.
     - intros n l1 l2. rewrite !list_lookup_validN.
       setoid_rewrite list_lookup_op. eauto using cmra_validN_op_l.
-    - intros n l. induction l as [|x l IH]=> -[|y1 l1] [|y2 l2] Hl Hl';
-        try (by exfalso; inversion_clear Hl').
-      + by exists ([], []).
-      + by exists ([], x :: l).
-      + by exists (x :: l, []).
-      + destruct (IH l1 l2) as ([l1' l2']&?&?&?),
-          (cmra_extend n x y1 y2) as ([y1' y2']&?&?&?);
-          [inversion_clear Hl; inversion_clear Hl'; auto ..|]; simplify_eq/=.
-        exists (y1' :: l1', y2' :: l2'); repeat constructor; auto.
+    - intros n l.
+      induction l as [|x l IH]=> -[|y1 l1] [|y2 l2] Hl; inversion_clear 1.
+      + by exists [], [].
+      + exists [], (x :: l); by repeat constructor.
+      + exists (x :: l), []; by repeat constructor.
+      + inversion_clear Hl. destruct (IH l1 l2) as (l1'&l2'&?&?&?),
+          (cmra_extend n x y1 y2) as (y1'&y2'&?&?&?); simplify_eq/=; auto.
+        exists (y1' :: l1'), (y2' :: l2'); repeat constructor; auto.
   Qed.
   Canonical Structure listR := CMRAT (list A) list_cofe_mixin list_cmra_mixin.
 

algebra/upred.v

@@ -1035,7 +1035,7 @@ Proof.
   - destruct n as [|n]; simpl.
     { by exists x, (core x); rewrite cmra_core_r. }
     intros (x1&x2&Hx&?&?); destruct (cmra_extend n x x1 x2)
-      as ([y1 y2]&Hx'&Hy1&Hy2); eauto using cmra_validN_S; simpl in *.
+      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&?&?)].
     exists x1, x2; eauto using dist_S.