Merge branch 'v2.0' of gitlab.mpi-sws.org:FP/iris-coq into v2.0

modures/cmra.v

@@ -318,15 +318,32 @@ Proof.
   * by intros Hx z ?; exists y; split; [done|apply (Hx z)].
   * by intros Hx z n ?; destruct (Hx z n) as (?&<-&?).
 Qed.
-Lemma ra_updateP_id (P : A → Prop) x : P x → x ⇝: P.
+Lemma cmra_updateP_id (P : A → Prop) x : P x → x ⇝: P.
 Proof. by intros ? z n ?; exists x. Qed.
-Lemma ra_updateP_compose (P Q : A → Prop) x :
+Lemma cmra_updateP_compose (P Q : A → Prop) x :
   x ⇝: P → (∀ y, P y → y ⇝: Q) → x ⇝: Q.
 Proof.
   intros Hx Hy z n ?. destruct (Hx z n) as (y&?&?); auto. by apply (Hy y).
 Qed.
-Lemma ra_updateP_weaken (P Q : A → Prop) x : x ⇝: P → (∀ y, P y → Q y) → x ⇝: Q.
-Proof. eauto using ra_updateP_compose, ra_updateP_id. Qed.
+Lemma cmra_updateP_weaken (P Q : A → Prop) x : x ⇝: P → (∀ y, P y → Q y) → x ⇝: Q.
+Proof. eauto using cmra_updateP_compose, cmra_updateP_id. Qed.
+
+Lemma cmra_updateP_op (P1 P2 Q : A → Prop) x1 x2 :
+  x1 ⇝: P1 → x2 ⇝: P2 → (∀ y1 y2, P1 y1 → P2 y2 → Q (y1 ⋅ y2)) → x1 ⋅ x2 ⇝: Q.
+Proof.
+  intros Hx1 Hx2 Hy z n ?.
+  destruct (Hx1 (x2 ⋅ z) n) as (y1&?&?); first by rewrite associative.
+  destruct (Hx2 (y1 ⋅ z) n) as (y2&?&?);
+    first by rewrite associative (commutative _ x2) -associative.
+  exists (y1 ⋅ y2); split; last rewrite (commutative _ y1) -associative; auto.
+Qed.
+Lemma cmra_updateP_op' (P1 P2 : A → Prop) x1 x2 :
+  x1 ⇝: P1 → x2 ⇝: P2 → x1 ⋅ x2 ⇝: λ y, ∃ y1 y2, y = y1 ⋅ y2 ∧ P1 y1 ∧ P2 y2.
+Proof. eauto 10 using cmra_updateP_op. Qed.
+Lemma cmra_update_op x1 x2 y1 y2 : x1 ⇝ y1 → x2 ⇝ y2 → x1 ⋅ x2 ⇝ y1 ⋅ y2.
+Proof.
+  rewrite !cmra_update_updateP; eauto using cmra_updateP_op with congruence.
+Qed.
 End cmra.
 
 Hint Extern 0 (_ ≼{0} _) => apply cmra_includedN_0.
@@ -473,13 +490,16 @@ Section prod.
   Qed.
   Lemma prod_update x y : x.1 ⇝ y.1 → x.2 ⇝ y.2 → x ⇝ y.
   Proof. intros ?? z n [??]; split; simpl in *; auto. Qed.
-  Lemma prod_updateP (P : A * B → Prop) P1 P2 x :
-    x.1 ⇝: P1 → x.2 ⇝: P2 → (∀ a b, P1 a → P2 b → P (a,b)) → x ⇝: P.
+  Lemma prod_updateP P1 P2 (Q : A * B → Prop)  x :
+    x.1 ⇝: P1 → x.2 ⇝: P2 → (∀ a b, P1 a → P2 b → Q (a,b)) → x ⇝: Q.
   Proof.
     intros Hx1 Hx2 HP z n [??]; simpl in *.
     destruct (Hx1 (z.1) n) as (a&?&?), (Hx2 (z.2) n) as (b&?&?); auto.
     exists (a,b); repeat split; auto.
   Qed.
+  Lemma prod_updateP' P1 P2 x :
+    x.1 ⇝: P1 → x.2 ⇝: P2 → x ⇝: λ y, P1 (y.1) ∧ P2 (y.2).
+  Proof. eauto using prod_updateP. Qed.
 End prod.
 Arguments prodRA : clear implicits.
 

modures/fin_maps.v

@@ -164,7 +164,7 @@ Proof. by move=> /(_ i) Hm Hi; move:Hm; 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_equality. Qed.
 Lemma map_insert_op m1 m2 i x :
-  m2 !! i = None →  <[i:=x]>(m1 ⋅ m2) = <[i:=x]>m1 ⋅ m2.
+  m2 !! i = None → <[i:=x]>(m1 ⋅ m2) = <[i:=x]>m1 ⋅ m2.
 Proof. by intros Hi; apply (insert_merge_l _ m1 m2); rewrite Hi. Qed.
 Lemma map_unit_singleton (i : K) (x : A) :
   unit ({[ i ↦ x ]} : gmap K A) = {[ i ↦ unit x ]}.
@@ -185,26 +185,45 @@ Proof.
     + by rewrite Hi; apply Some_Some_includedN, cmra_included_includedN.
     + apply None_includedN.
 Qed.
-Lemma map_dom_op (m1 m2 : gmap K A) :
-  dom (gset K) (m1 ⋅ m2) ≡ dom _ m1 ∪ dom _ m2.
+Lemma map_dom_op m1 m2 : dom (gset K) (m1 ⋅ m2) ≡ dom _ m1 ∪ dom _ m2.
 Proof.
   apply elem_of_equiv; intros i; rewrite elem_of_union !elem_of_dom.
   unfold is_Some; setoid_rewrite lookup_op.
   destruct (m1 !! i), (m2 !! i); naive_solver.
 Qed.
 
+Lemma map_insert_updateP (P : A → Prop) (Q : gmap K A → Prop) m i x :
+  x ⇝: P → (∀ y, P y → Q (<[i:=y]>m)) → <[i:=x]>m ⇝: Q.
+Proof.
+  intros Hx%option_updateP' HP mf n Hm.
+  destruct (Hx (mf !! i) n) as ([y|]&?&?); try done.
+  { by generalize (Hm i); rewrite lookup_op; simplify_map_equality. }
+  exists (<[i:=y]> m); split; first by auto.
+  intros j; move: (Hm j)=>{Hm}; rewrite !lookup_op=>Hm.
+  destruct (decide (i = j)); simplify_map_equality'; auto.
+Qed.
+Lemma map_insert_updateP' (P : A → Prop) (Q : gmap K A → Prop) m i x :
+  x ⇝: P → <[i:=x]>m ⇝: λ m', ∃ y, m' = <[i:=y]>m ∧ P y.
+Proof. eauto using map_insert_updateP. Qed.
+Lemma map_insert_update m i x y : x ⇝ y → <[i:=x]>m ⇝ <[i:=y]>m.
+Proof.
+  rewrite !cmra_update_updateP; eauto using map_insert_updateP with congruence.
+Qed.
+
 Context `{Fresh K (gset K), !FreshSpec K (gset K)}.
-Lemma map_update_alloc (m : gmap K A) x :
-  ✓ x → m ⇝: λ m', ∃ i, m' = <[i:=x]>m ∧ m !! i = None.
+Lemma map_updateP_alloc (Q : gmap K A → Prop) m x :
+  ✓ x → (∀ i, m !! i = None → Q (<[i:=x]>m)) → m ⇝: Q.
 Proof.
-  intros ? mf n Hm. set (i := fresh (dom (gset K) (m ⋅ mf))).
+  intros ? HQ mf n Hm. set (i := fresh (dom (gset K) (m ⋅ mf))).
   assert (i ∉ dom (gset K) m ∧ i ∉ dom (gset K) mf) as [??].
   { rewrite -not_elem_of_union -map_dom_op; apply is_fresh. }
-  exists (<[i:=x]>m); split; [exists i; split; [done|]|].
-  * by apply not_elem_of_dom.
-  * rewrite -map_insert_op; last by apply not_elem_of_dom.
-    by apply map_insert_validN; [apply cmra_valid_validN|].
+  exists (<[i:=x]>m); split; first by apply HQ, not_elem_of_dom.
+  rewrite -map_insert_op; last by apply not_elem_of_dom.
+  by apply map_insert_validN; [apply cmra_valid_validN|].
 Qed.
+Lemma map_updateP_alloc' m x :
+  ✓ x → m ⇝: λ m', ∃ i, m' = <[i:=x]>m ∧ m !! i = None.
+Proof. eauto using map_updateP_alloc. Qed.
 End properties.
 
 Instance map_fmap_ne `{Countable K} {A B : cofeT} (f : A → B) n :

modures/option.v

@@ -147,10 +147,12 @@ Proof.
   destruct (Hx (unit x) n) as (y'&?&?); rewrite ?cmra_unit_r; auto.
   by exists (Some y'); split; [auto|apply cmra_validN_op_l with (unit x)].
 Qed.
+Lemma option_updateP' (P : A → Prop) x :
+  x ⇝: P → Some x ⇝: λ y, default False y P.
+Proof. eauto using option_updateP. Qed.
 Lemma option_update x y : x ⇝ y → Some x ⇝ Some y.
 Proof.
-  intros; apply cmra_update_updateP, (option_updateP (y=)); [|naive_solver].
-  by apply cmra_update_updateP.
+  rewrite !cmra_update_updateP; eauto using option_updateP with congruence.
 Qed.
 End cmra.