diff --git a/algebra/cmra.v b/algebra/cmra.v index 8861dbc82a5b42eb9851fa5dcab703a46ef8ab49..75c08848036832353a71d178eb8d5bbf8cff5556 100644 --- a/algebra/cmra.v +++ b/algebra/cmra.v @@ -396,27 +396,16 @@ 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/program_logic/ghost_ownership.v b/program_logic/ghost_ownership.v index a1c60d307fe5191f1e3298717db36b79f2ab3ae3..421f0506715401c67e3c1ca6ab5eec5733f490d4 100644 --- a/program_logic/ghost_ownership.v +++ b/program_logic/ghost_ownership.v @@ -23,7 +23,7 @@ Section global. Context {Λ : language} {Σ : gid → iFunctor} (i : gid) `{!InG Λ Σ i A}. Implicit Types a : A. -(* Properties of to_globalC *) +(** * Properties of to_globalC *) Instance to_globalC_ne γ n : Proper (dist n ==> dist n) (to_globalC i γ). Proof. by intros a a' Ha; apply iprod_singleton_ne; rewrite Ha. Qed. Lemma to_globalC_validN n γ a : ✓{n} (to_globalC i γ a) ↔ ✓{n} a. @@ -44,7 +44,19 @@ Qed. Instance to_globalC_timeless γ m : Timeless m → Timeless (to_globalC i γ m). Proof. rewrite /to_globalC; apply _. Qed. -(* Properties of own *) +(** * Transport empty *) +Instance inG_empty `{Empty A} : Empty (Σ i (laterC (iPreProp Λ (globalC Σ)))) := + cmra_transport inG ∅. +Instance inG_empty_spec `{Empty A} : + CMRAIdentity A → CMRAIdentity (Σ i (laterC (iPreProp Λ (globalC Σ)))). +Proof. + split. + * apply cmra_transport_valid, cmra_empty_valid. + * intros x; rewrite /empty /inG_empty; destruct inG. by rewrite left_id. + * apply _. +Qed. + +(** * Properties of own *) Global Instance own_ne γ n : Proper (dist n ==> dist n) (own i γ). Proof. by intros m m' Hm; rewrite /own Hm. Qed. Global Instance own_proper γ : Proper ((≡) ==> (≡)) (own i γ) := ne_proper _. @@ -91,17 +103,11 @@ Lemma own_updateP_empty `{Empty A, !CMRAIdentity A} E γ a P : Proof. intros Hemp. rewrite -(pvs_mono _ _ (∃ m, ■ (∃ a', m = to_globalC i γ a' ∧ P a') ∧ ownG m)%I). - * eapply pvs_ownG_updateP_empty, iprod_singleton_updateP_empty with (x:=i); - first by (eapply map_singleton_updateP_empty', cmra_transport_updateP', Hemp). + * eapply pvs_ownG_updateP_empty, iprod_singleton_updateP_empty; + first eapply map_singleton_updateP_empty', cmra_transport_updateP', Hemp. naive_solver. * apply exist_elim=>m; apply const_elim_l=>-[a' [-> HP]]. rewrite -(exist_intro a'). by apply and_intro; [apply const_intro|]. -Unshelve. -(* We have to prove that we actually follow the identity laws on the "other side". *) -split. -- apply cmra_transport_valid, cmra_empty_valid. -- move=>b. by rewrite -cmra_transport_back_op_r left_id cmra_transport_back_and. -- apply _. Qed. Lemma own_update E γ a a' : a ~~> a' → own i γ a ⊑ pvs E E (own i γ a').