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

iris/wsat.v

@@ -129,7 +129,7 @@ Lemma wsat_update_gst n E σ r rf m1 (P : iGst Λ Σ → Prop) :
   wsat (S n) E σ (r ⋅ rf) → ∃ m2, wsat (S n) E σ (update_gst m2 r ⋅ rf) ∧ P m2.
 Proof.
   intros [mf Hr] Hup [rs [(?&?&?) Hσ HE Hwld]].
-  destruct (Hup (mf ⋅ gst (rf ⋅ big_opM rs)) (S n)) as (m2&?&Hval').
+  destruct (Hup (mf ⋅ gst (rf ⋅ big_opM rs)) n) as (m2&?&Hval').
   { by rewrite /= (associative _ m1) -Hr (associative _). }
   exists m2; split; [exists rs; split; split_ands'; auto|done].
 Qed.

modures/cmra.v

@@ -142,11 +142,11 @@ Class CMRAMonotone {A B : cmraT} (f : A → B) := {
 
 (** * Frame preserving updates *)
 Definition cmra_updateP {A : cmraT} (x : A) (P : A → Prop) := ∀ z n,
-  ✓{n} (x ⋅ z) → ∃ y, P y ∧ ✓{n} (y ⋅ z).
+  ✓{S n} (x ⋅ z) → ∃ y, P y ∧ ✓{S n} (y ⋅ z).
 Instance: Params (@cmra_updateP) 3.
 Infix "⇝:" := cmra_updateP (at level 70).
 Definition cmra_update {A : cmraT} (x y : A) := ∀ z n,
-  ✓{n} (x ⋅ z) → ✓{n} (y ⋅ z).
+  ✓{S n} (x ⋅ z) → ✓{S n} (y ⋅ z).
 Infix "⇝" := cmra_update (at level 70).
 Instance: Params (@cmra_update) 3.
 
@@ -393,15 +393,12 @@ Section discrete.
   Qed.
   Definition discreteRA : cmraT :=
     CMRAT (cofe_mixin A) discrete_cmra_mixin discrete_extend_mixin.
-  Lemma discrete_updateP (x : discreteRA) (P : A → Prop) `{!Inhabited (sig P)} :
+  Lemma discrete_updateP (x : discreteRA) (P : A → Prop) :
     (∀ z, ✓ (x ⋅ z) → ∃ y, P y ∧ ✓ (y ⋅ z)) → x ⇝: P.
-  Proof.
-    intros Hvalid z [|n]; [|apply Hvalid].
-    by destruct (_ : Inhabited (sig P)) as [[y ?]]; exists y.
-  Qed.
+  Proof. intros Hvalid z n; apply Hvalid. Qed.
   Lemma discrete_update (x y : discreteRA) :
     (∀ z, ✓ (x ⋅ z) → ✓ (y ⋅ z)) → x ⇝ y.
-  Proof. intros Hvalid z [|n]; [done|apply Hvalid]. Qed.
+  Proof. intros Hvalid z n; apply Hvalid. Qed.
 End discrete.
 
 (** ** CMRA for the unit type *)
@@ -477,7 +474,7 @@ Section prod.
   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 → (∀ y, P1 (y.1) → P2 (y.2) → P y) → x ⇝: P.
+    x.1 ⇝: P1 → x.2 ⇝: P2 → (∀ a b, P1 a → P2 b → P (a,b)) → x ⇝: P.
   Proof.
     intros Hx1 Hx2 HP z n [??]; simpl in *.
     destruct (Hx1 (z.1) n) as (a&?&?), (Hx2 (z.2) n) as (b&?&?); auto.

modures/excl.v

@@ -142,6 +142,8 @@ Qed.
 (* Updates *)
 Lemma excl_update (x : A) y : ✓ y → Excl x ⇝ y.
 Proof. by destruct y; intros ? [?| |]. Qed.
+Lemma excl_updateP (P : excl A → Prop) x y : ✓ y → P y → Excl x ⇝: P.
+Proof. intros ?? z n ?; exists y. by destruct y, z as [?| |]. Qed.
 End excl.
 
 Arguments exclC : clear implicits.

modures/option.v

@@ -61,7 +61,6 @@ Instance option_fmap_ne {A B : cofeT} (f : A → B) n:
   Proper (dist n ==> dist n) f → Proper (dist n==>dist n) (fmap (M:=option) f).
 Proof. by intros Hf; destruct 1; constructor; apply Hf. Qed.
 
-
 (* CMRA *)
 Section cmra.
 Context {A : cmraT}.
@@ -131,14 +130,28 @@ Qed.
 Canonical Structure optionRA :=
   CMRAT option_cofe_mixin option_cmra_mixin option_cmra_extend_mixin.
 
-Lemma op_is_Some x y : is_Some (x ⋅ y) ↔ is_Some x ∨ is_Some y.
+Lemma op_is_Some mx my : is_Some (mx ⋅ my) ↔ is_Some mx ∨ is_Some my.
+Proof.
+  destruct mx, my; rewrite /op /option_op /= -!not_eq_None_Some; naive_solver.
+Qed.
+Lemma option_op_positive_dist_l n mx my : mx ⋅ my ={n}= None → mx ={n}= None.
+Proof. by destruct mx, my; inversion_clear 1. Qed.
+Lemma option_op_positive_dist_r n mx my : mx ⋅ my ={n}= None → my ={n}= None.
+Proof. by destruct mx, my; inversion_clear 1. Qed.
+
+Lemma option_updateP (P : A → Prop) (Q : option A → Prop) x :
+  x ⇝: P → (∀ y, P y → Q (Some y)) → Some x ⇝: Q.
+Proof.
+  intros Hx Hy [y|] n ?.
+  { destruct (Hx y n) as (y'&?&?); auto. exists (Some y'); auto. }
+  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_update x y : x ⇝ y → Some x ⇝ Some y.
 Proof.
-  destruct x, y; rewrite /op /option_op /= -!not_eq_None_Some; naive_solver.
+  intros; apply cmra_update_updateP, (option_updateP (y=)); [|naive_solver].
+  by apply cmra_update_updateP.
 Qed.
-Lemma option_op_positive_dist_l n x y : x ⋅ y ={n}= None → x ={n}= None.
-Proof. by destruct x, y; inversion_clear 1. Qed.
-Lemma option_op_positive_dist_r n x y : x ⋅ y ={n}= None → y ={n}= None.
-Proof. by destruct x, y; inversion_clear 1. Qed.
 End cmra.
 
 Arguments optionRA : clear implicits.