From e7e5856e34cab2dbbc878d79a55a6e5d0ee7980e Mon Sep 17 00:00:00 2001
From: Robbert Krebbers <mail@robbertkrebbers.nl>
Date: Tue, 2 Feb 2016 16:08:19 +0100
Subject: [PATCH] =?UTF-8?q?Frame=20preserving=20updates=20only=20from=20st?=
 =?UTF-8?q?eps=20=E2=89=A0=200.?=
MIME-Version: 1.0
Content-Type: text/plain; charset=UTF-8
Content-Transfer-Encoding: 8bit

---
 iris/wsat.v    |  2 +-
 modures/cmra.v | 15 ++++++---------
 2 files changed, 7 insertions(+), 10 deletions(-)

diff --git a/iris/wsat.v b/iris/wsat.v
index 6281065b6..9b57849ed 100644
--- a/iris/wsat.v
+++ b/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.
diff --git a/modures/cmra.v b/modures/cmra.v
index 0f443ad52..d0abf150a 100644
--- a/modures/cmra.v
+++ b/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.
-- 
GitLab