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

algebra/cmra.v

@@ -1208,8 +1208,14 @@ Section option.
 
   Lemma Some_included x y : Some x ≼ Some y ↔ x ≡ y ∨ x ≼ y.
   Proof. rewrite option_included; naive_solver. Qed.
-  Lemma Some_included' `{CMRATotal A} x y : Some x ≼ Some y ↔ x ≼ y.
+  Lemma Some_included_2 x y : x ≼ y → Some x ≼ Some y.
+  Proof. rewrite Some_included; eauto. Qed.
+  Lemma Some_included_total `{CMRATotal A} x y : Some x ≼ Some y ↔ x ≼ y.
   Proof. rewrite Some_included. split. by intros [->|?]. eauto. Qed.
+  Lemma Some_included_exclusive x `{!Exclusive x} y :
+    Some x ≼ Some y → ✓ y → x ≡ y.
+  Proof. move=> /Some_included [//|/exclusive_included]; tauto. Qed.
+
   Lemma is_Some_included mx my : mx ≼ my → is_Some mx → is_Some my.
   Proof. rewrite -!not_eq_None_Some option_included. naive_solver. Qed.
 End option.
@@ -1217,6 +1223,19 @@ End option.
 Arguments optionR : clear implicits.
 Arguments optionUR : clear implicits.
 
+Section option_prod.
+  Context {A B : cmraT}.
+  Lemma Some_pair_included  (x1 x2 : A) (y1 y2 : B) :
+    Some (x1,y1) ≼ Some (x2,y2) → Some x1 ≼ Some x2 ∧ Some y1 ≼ Some y2.
+  Proof. rewrite !Some_included. intros [[??]|[??]%prod_included]; eauto. Qed.
+  Lemma Some_pair_included_total_1 `{CMRATotal A} (x1 x2 : A) (y1 y2 : B) :
+    Some (x1,y1) ≼ Some (x2,y2) → x1 ≼ x2 ∧ Some y1 ≼ Some y2.
+  Proof. intros ?%Some_pair_included. by rewrite -(Some_included_total x1). Qed.
+  Lemma Some_pair_included_total_2 `{CMRATotal B} (x1 x2 : A) (y1 y2 : B) :
+    Some (x1,y1) ≼ Some (x2,y2) → Some x1 ≼ Some x2 ∧ y1 ≼ y2.
+  Proof. intros ?%Some_pair_included. by rewrite -(Some_included_total y1). Qed.
+End option_prod.
+
 Instance option_fmap_cmra_monotone {A B : cmraT} (f: A → B) `{!CMRAMonotone f} :
   CMRAMonotone (fmap f : option A → option B).
 Proof.

algebra/dec_agree.v

@@ -31,21 +31,19 @@ Instance dec_agree_pcore : PCore (dec_agree A) := Some.
 
 Definition dec_agree_ra_mixin : RAMixin (dec_agree A).
 Proof.
-  split.
-  - apply _.
-  - intros x y cx ? [=<-]; eauto.
-  - apply _.
+  apply ra_total_mixin; apply _ || eauto.
   - intros [?|] [?|] [?|]; by repeat (simplify_eq/= || case_match).
   - intros [?|] [?|]; by repeat (simplify_eq/= || case_match).
-  - intros [?|] ? [=<-]; by repeat (simplify_eq/= || case_match).
   - intros [?|]; by repeat (simplify_eq/= || case_match).
-  - intros [?|] [?|] ?? [=<-]; eauto.
   - by intros [?|] [?|] ?.
 Qed.
 
 Canonical Structure dec_agreeR : cmraT :=
   discreteR (dec_agree A) dec_agree_ra_mixin.
 
+Global Instance dec_agree_total : CMRATotal dec_agreeR.
+Proof. intros x. by exists x. Qed.
+
 (* Some properties of this CMRA *)
 Global Instance dec_agree_persistent (x : dec_agreeR) : Persistent x.
 Proof. by constructor. Qed.
@@ -59,8 +57,10 @@ Proof. destruct x; by rewrite /= ?decide_True. Qed.
 Lemma dec_agree_op_inv (x1 x2 : dec_agree A) : ✓ (x1 ⋅ x2) → x1 = x2.
 Proof. destruct x1, x2; by repeat (simplify_eq/= || case_match). Qed.
 
-Lemma DecAgree_included a b : DecAgree a ≼ DecAgree b → a = b.
-Proof. intros [[c|] [=]%leibniz_equiv_iff]. by simplify_option_eq. Qed.
+Lemma DecAgree_included a b : DecAgree a ≼ DecAgree b ↔ a = b.
+Proof.
+  split. intros [[c|] [=]%leibniz_equiv]. by simplify_option_eq. by intros ->.
+Qed.
 End dec_agree.
 
 Arguments dec_agreeC : clear implicits.

algebra/gmap.v

@@ -256,37 +256,29 @@ Global Instance gmap_singleton_persistent i (x : A) :
 Proof. intros. by apply persistent_total, core_singleton'. Qed.
 
 Lemma singleton_includedN n m i x :
-  {[ i := x ]} ≼{n} m ↔ ∃ y, m !! i ≡{n}≡ Some y ∧ (x ≼{n} y ∨ x ≡{n}≡ y).
+  {[ i := x ]} ≼{n} m ↔ ∃ y, m !! i ≡{n}≡ Some y ∧ Some x ≼{n} Some y.
 Proof.
   split.
-  - move=> [m' /(_ i)]; rewrite lookup_op lookup_singleton.
-    case (m' !! i)=> [y|]=> Hm.
-    + exists (x ⋅ y); eauto using cmra_includedN_l.
-    + exists x; eauto.
-  - intros (y&Hi&[[z ?]| ->]).
-    + exists (<[i:=z]>m)=> j; destruct (decide (i = j)) as [->|].
-      * rewrite Hi lookup_op lookup_singleton lookup_insert. by constructor.
-      * by rewrite lookup_op lookup_singleton_ne // lookup_insert_ne // left_id.
-    + exists (delete i m)=> j; destruct (decide (i = j)) as [->|].
-      * by rewrite Hi lookup_op lookup_singleton lookup_delete.
-      * by rewrite lookup_op lookup_singleton_ne // lookup_delete_ne // left_id.
+  - move=> [m' /(_ i)]; rewrite lookup_op lookup_singleton=> Hi.
+    exists (x ⋅? m' !! i). rewrite -Some_op_opM.
+    split. done. apply cmra_includedN_l.
+  - intros (y&Hi&[mz Hy]). exists (partial_alter (λ _, mz) i m).
+    intros j; destruct (decide (i = j)) as [->|].
+    + by rewrite lookup_op lookup_singleton lookup_partial_alter Hi.
+    + by rewrite lookup_op lookup_singleton_ne// lookup_partial_alter_ne// left_id.
 Qed.
 (* We do not have [x ≼ y ↔ ∀ n, x ≼{n} y], so we cannot use the previous lemma *)
 Lemma singleton_included m i x :
-  {[ i := x ]} ≼ m ↔ ∃ y, m !! i ≡ Some y ∧ (x ≼ y ∨ x ≡ y).
+  {[ i := x ]} ≼ m ↔ ∃ y, m !! i ≡ Some y ∧ Some x ≼ Some y.
 Proof.
   split.
   - move=> [m' /(_ i)]; rewrite lookup_op lookup_singleton.
-    case (m' !! i)=> [y|]=> Hm.
-    + exists (x ⋅ y); eauto using cmra_included_l.
-    + exists x; eauto.
-  - intros (y&Hi&[[z ?]| ->]).
-    + exists (<[i:=z]>m)=> j; destruct (decide (i = j)) as [->|].
-      * rewrite Hi lookup_op lookup_singleton lookup_insert. by constructor.
-      * by rewrite lookup_op lookup_singleton_ne // lookup_insert_ne // left_id.
-    + exists (delete i m)=> j; destruct (decide (i = j)) as [->|].
-      * by rewrite Hi lookup_op lookup_singleton lookup_delete.
-      * by rewrite lookup_op lookup_singleton_ne // lookup_delete_ne // left_id.
+    exists (x ⋅? m' !! i). rewrite -Some_op_opM.
+    split. done. apply cmra_included_l.
+  - intros (y&Hi&[mz Hy]). exists (partial_alter (λ _, mz) i m).
+    intros j; destruct (decide (i = j)) as [->|].
+    + by rewrite lookup_op lookup_singleton lookup_partial_alter Hi.
+    + by rewrite lookup_op lookup_singleton_ne// lookup_partial_alter_ne// left_id.
 Qed.
 
 Lemma insert_updateP (P : A → Prop) (Q : gmap K A → Prop) m i x :