diff --git a/modures/cmra.v b/modures/cmra.v index ed96b1f5894667589fc129f3a1ea1fb8d2586d62..0f443ad52914237c28738638d70128675cfee781 100644 --- a/modures/cmra.v +++ b/modures/cmra.v @@ -318,6 +318,15 @@ 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. +Proof. by intros ? z n ?; exists x. Qed. +Lemma ra_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. End cmra. Hint Extern 0 (_ ≼{0} _) => apply cmra_includedN_0. @@ -384,14 +393,14 @@ Section discrete. Qed. Definition discreteRA : cmraT := CMRAT (cofe_mixin A) discrete_cmra_mixin discrete_extend_mixin. - Lemma discrete_updateP (x : A) (P : A → Prop) `{!Inhabited (sig P)} : - (∀ z, ✓ (x ⋅ z) → ∃ y, P y ∧ ✓ (y ⋅ z)) → (x : discreteRA) ⇝: P. + Lemma discrete_updateP (x : discreteRA) (P : A → Prop) `{!Inhabited (sig P)} : + (∀ 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. - Lemma discrete_update (x y : A) : - (∀ z, ✓ (x ⋅ z) → ✓ (y ⋅ z)) → (x : discreteRA) ⇝ y. + Lemma discrete_update (x y : discreteRA) : + (∀ z, ✓ (x ⋅ z) → ✓ (y ⋅ z)) → x ⇝ y. Proof. intros Hvalid z [|n]; [done|apply Hvalid]. Qed. End discrete. @@ -465,6 +474,15 @@ Section prod. * by split; rewrite /=left_id. * by intros ? [??]; split; apply (timeless _). 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 → (∀ y, P1 (y.1) → P2 (y.2) → P y) → 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. + exists (a,b); repeat split; auto. + Qed. End prod. Arguments prodRA : clear implicits.