Merge branch 'master' of gitlab.mpi-sws.org:FP/iris-coq

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&?&?)].

barrier/barrier.v

@@ -42,7 +42,7 @@ Module barrier_proto.
   Proof.
     split.
     - move=>[p I]. rewrite /= /tok !mkSet_elem_of /= =>HI.
-      destruct p; set_solver eauto.
+      destruct p; set_solver by eauto.
     - (* If we do the destruct of the states early, and then inversion
          on the proof of a transition, it doesn't work - we do not obtain
          the equalities we need. So we destruct the states late, because this
@@ -90,7 +90,7 @@ Module barrier_proto.
     i ∈ I → sts.steps (State High I, {[ Change i ]}) (State High (I ∖ {[ i ]}), ∅).
   Proof.
     intros. apply rtc_once.
-    constructor; first constructor; rewrite /= /tok /=; [set_solver eauto..|].
+    constructor; first constructor; rewrite /= /tok /=; [set_solver by eauto..|].
     (* TODO this proof is rather annoying. *)
     apply elem_of_equiv=>t. rewrite !elem_of_union.
     rewrite !mkSet_elem_of /change_tokens /=.

prelude/collections.v

@@ -253,19 +253,18 @@ Ltac set_unfold :=
 (** Since [firstorder] fails or loops on very small goals generated by
 [set_solver] already. We use the [naive_solver] tactic as a substitute.
 This tactic either fails or proves the goal. *)
-Tactic Notation "set_solver" tactic3(tac) :=
+Tactic Notation "set_solver" "by" tactic3(tac) :=
   setoid_subst;
   decompose_empty;
   set_unfold;
   naive_solver tac.
-Tactic Notation "set_solver" "-" hyp_list(Hs) "/" tactic3(tac) :=
-  clear Hs; set_solver tac.
-Tactic Notation "set_solver" "+" hyp_list(Hs) "/" tactic3(tac) :=
-  revert Hs; clear; set_solver tac.
-Tactic Notation "set_solver" := set_solver idtac.
+Tactic Notation "set_solver" "-" hyp_list(Hs) "by" tactic3(tac) :=
+  clear Hs; set_solver by tac.
+Tactic Notation "set_solver" "+" hyp_list(Hs) "by" tactic3(tac) :=
+  clear -Hs; set_solver by tac.
+Tactic Notation "set_solver" := set_solver by idtac.
 Tactic Notation "set_solver" "-" hyp_list(Hs) := clear Hs; set_solver.
-Tactic Notation "set_solver" "+" hyp_list(Hs) :=
-  revert Hs; clear; set_solver.
+Tactic Notation "set_solver" "+" hyp_list(Hs) := clear -Hs; set_solver.
 
 (** * More theorems *)
 Section collection.
@@ -537,10 +536,10 @@ Section collection_monad.
 
   Global Instance collection_fmap_mono {A B} :
     Proper (pointwise_relation _ (=) ==> (⊆) ==> (⊆)) (@fmap M _ A B).
-  Proof. intros f g ? X Y ?; set_solver eauto. Qed.
+  Proof. intros f g ? X Y ?; set_solver by eauto. Qed.
   Global Instance collection_fmap_proper {A B} :
     Proper (pointwise_relation _ (=) ==> (≡) ==> (≡)) (@fmap M _ A B).
-  Proof. intros f g ? X Y [??]; split; set_solver eauto. Qed.
+  Proof. intros f g ? X Y [??]; split; set_solver by eauto. Qed.
   Global Instance collection_bind_mono {A B} :
     Proper (((=) ==> (⊆)) ==> (⊆) ==> (⊆)) (@mbind M _ A B).
   Proof. unfold respectful; intros f g Hfg X Y ?; set_solver. Qed.
@@ -575,12 +574,12 @@ Section collection_monad.
     l ∈ mapM f k ↔ Forall2 (λ x y, x ∈ f y) l k.
   Proof.
     split.
-    - revert l. induction k; set_solver eauto.
+    - revert l. induction k; set_solver by eauto.
     - induction 1; set_solver.
   Qed.
   Lemma collection_mapM_length {A B} (f : A → M B) l k :
     l ∈ mapM f k → length l = length k.
-  Proof. revert l; induction k; set_solver eauto. Qed.
+  Proof. revert l; induction k; set_solver by eauto. Qed.
   Lemma elem_of_mapM_fmap {A B} (f : A → B) (g : B → M A) l k :
     Forall (λ x, ∀ y, y ∈ g x → f y = x) l → k ∈ mapM g l → fmap f k = l.
   Proof.

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.