From b7d3100596fee51f783af170afef3318c0c0e66c Mon Sep 17 00:00:00 2001 From: Ralf Jung Date: Tue, 9 Feb 2016 19:13:38 +0100 Subject: [PATCH] algebra: prove some frame-preserving updates from empty --- algebra/cmra.v | 11 +++++++++++ algebra/fin_maps.v | 22 +++++++++++++++++++++- algebra/iprod.v | 9 ++++++--- 3 files changed, 38 insertions(+), 4 deletions(-) diff --git a/algebra/cmra.v b/algebra/cmra.v index 75c08848..8861dbc8 100644 --- a/algebra/cmra.v +++ b/algebra/cmra.v @@ -396,16 +396,27 @@ End cmra_monotone. (** * Transporting a CMRA equality *) Definition cmra_transport {A B : cmraT} (H : A = B) (x : A) : B := eq_rect A id x _ H. +Definition cmra_transport_back {A B : cmraT} (H : A = B) (x : B) : A := + eq_rect B id x _ (eq_sym H). Section cmra_transport. Context {A B : cmraT} (H : A = B). Notation T := (cmra_transport H). + Notation T' := (cmra_transport_back H). Global Instance cmra_transport_ne n : Proper (dist n ==> dist n) T. Proof. by intros ???; destruct H. Qed. Global Instance cmra_transport_proper : Proper ((≡) ==> (≡)) T. Proof. by intros ???; destruct H. Qed. + Lemma cmra_transport_and_back x : T' (T x) = x. + Proof. by destruct H. Qed. + Lemma cmra_transport_back_and x : T (T' x) = x. + Proof. by destruct H. Qed. Lemma cmra_transport_op x y : T (x ⋅ y) = T x ⋅ T y. Proof. by destruct H. Qed. + Lemma cmra_transport_back_op_r y x : T (x ⋅ T' y) = T x ⋅ y. + Proof. by destruct H. Qed. + Lemma cmra_transport_back_op_l y x : T (T' x ⋅ y) = x ⋅ T y. + Proof. by destruct H. Qed. Lemma cmra_transport_unit x : T (unit x) = unit (T x). Proof. by destruct H. Qed. Lemma cmra_transport_validN n x : ✓{n} (T x) ↔ ✓{n} x. diff --git a/algebra/fin_maps.v b/algebra/fin_maps.v index 1feea5ec..d7202814 100644 --- a/algebra/fin_maps.v +++ b/algebra/fin_maps.v @@ -228,11 +228,31 @@ Lemma map_singleton_updateP (P : A → Prop) (Q : gmap K A → Prop) i x : x ~~>: P → (∀ y, P y → Q {[ i ↦ y ]}) → {[ i ↦ x ]} ~~>: Q. Proof. apply map_insert_updateP. Qed. Lemma map_singleton_updateP' (P : A → Prop) i x : - x ~~>: P → {[ i ↦ x ]} ~~>: λ m', ∃ y, m' = {[ i ↦ y ]} ∧ P y. + x ~~>: P → {[ i ↦ x ]} ~~>: λ m, ∃ y, m = {[ i ↦ y ]} ∧ P y. Proof. apply map_insert_updateP'. Qed. Lemma map_singleton_update i (x y : A) : x ~~> y → {[ i ↦ x ]} ~~> {[ i ↦ y ]}. Proof. apply map_insert_update. Qed. +Lemma map_singleton_updateP_empty `{Empty A, !CMRAIdentity A} + (P : A → Prop) (Q : gmap K A → Prop) i : + ∅ ~~>: P → (∀ y, P y → Q {[ i ↦ y ]}) → ∅ ~~>: Q. + Proof. + intros Hx HQ gf n Hg. + destruct (Hx (default ∅ (gf !! i) id) n) as (y&?&Hy). + { move:(Hg i). rewrite !left_id. case _: (gf !! i); first done. + intros. apply cmra_empty_valid. } + exists {[ i ↦ y]}. split; first by apply HQ. + intros i'. rewrite lookup_op. + destruct (decide (i' = i)). + - subst i'. rewrite lookup_singleton. move:Hy. + case _: (gf !! i); first done. + by rewrite right_id. + - move:(Hg i'). rewrite lookup_singleton_ne // !left_id. done. +Qed. +Lemma map_singleton_updateP_empty' `{Empty A, !CMRAIdentity A} (P : A → Prop) i : + ∅ ~~>: P → ∅ ~~>: λ m, ∃ y, m = {[ i ↦ y ]} ∧ P y. +Proof. eauto using map_singleton_updateP_empty. Qed. + Context `{Fresh K (gset K), !FreshSpec K (gset K)}. Lemma map_updateP_alloc (Q : gmap K A → Prop) m x : ✓ x → (∀ i, m !! i = None → Q (<[i:=x]>m)) → m ~~>: Q. diff --git a/algebra/iprod.v b/algebra/iprod.v index 211f92f3..39acaa80 100644 --- a/algebra/iprod.v +++ b/algebra/iprod.v @@ -48,7 +48,7 @@ Section iprod_cofe. Section empty. Context `{∀ x, Empty (B x)}. Definition iprod_lookup_empty x : ∅ x = ∅ := eq_refl. - Instance iprod_empty_timeless : + Global Instance iprod_empty_timeless : (∀ x : A, Timeless (∅ : B x)) → Timeless (∅ : iprod B). Proof. intros ? f Hf x. by apply (timeless _). Qed. End empty. @@ -168,7 +168,7 @@ Section iprod_cmra. intros ?; split. * intros n x; apply cmra_empty_valid. * by intros f x; rewrite iprod_lookup_op left_id. - * by intros f Hf x; apply (timeless _). + * by apply _. Qed. (** Properties of iprod_insert. *) @@ -230,7 +230,7 @@ Section iprod_cmra. Proof. rewrite /iprod_singleton; eauto using iprod_insert_updateP. Qed. Lemma iprod_singleton_updateP' x (P : B x → Prop) y1 : y1 ~~>: P → - iprod_singleton x y1 ~~>: λ g', ∃ y2, g' = iprod_singleton x y2 ∧ P y2. + iprod_singleton x y1 ~~>: λ g, ∃ y2, g = iprod_singleton x y2 ∧ P y2. Proof. eauto using iprod_singleton_updateP. Qed. Lemma iprod_singleton_update x y1 y2 : y1 ~~> y2 → iprod_singleton x y1 ~~> iprod_singleton x y2. @@ -245,6 +245,9 @@ Section iprod_cmra. * by rewrite iprod_lookup_op iprod_lookup_singleton. * rewrite iprod_lookup_op iprod_lookup_singleton_ne //. apply Hg. Qed. + Lemma iprod_singleton_updateP_empty' x (P : B x → Prop) : + ∅ ~~>: P → ∅ ~~>: λ g, ∃ y2, g = iprod_singleton x y2 ∧ P y2. + Proof. eauto using iprod_singleton_updateP_empty. Qed. End iprod_cmra. Arguments iprodRA {_} _. -- GitLab