Library iris.program_logic.ghost_ownership
From iris.prelude Require Export functions.
From iris.algebra Require Export iprod.
From iris.program_logic Require Export pviewshifts pstepshifts global_functor.
From iris.program_logic Require Import ownership.
Import uPred.
Definition own_def `{inG Λ Σ (gmapUR gname A)} (γ : gname) (a : A) : iPropG Λ Σ :=
ownG (to_globalF γ a).
Definition own_aux : { x | x = @own_def }. by eexists. Qed.
Definition own {Λ Σ A i} := proj1_sig own_aux Λ Σ A i.
Definition own_eq : @own = @own_def := proj2_sig own_aux.
Instance: Params (@own) 5.
Typeclasses Opaque own.
Definition ownl_def `{inG Λ Σ (gmapUR gname A)} (γ : gname) (a : A) : iPropG Λ Σ :=
ownGl (to_globalF γ a).
Definition ownl_aux : { x | x = @ownl_def }. by eexists. Qed.
Definition ownl {Λ Σ A i} := proj1_sig ownl_aux Λ Σ A i.
Definition ownl_eq : @ownl = @ownl_def := proj2_sig ownl_aux.
Instance: Params (@ownl) 5.
Typeclasses Opaque ownl.
Definition owne_def `{inG Λ Σ A} (a : A) : iPropG Λ Σ :=
ownG (to_globalFe a).
Definition owne_aux : { x | x = @owne_def }. by eexists. Qed.
Definition owne {Λ Σ A i} := proj1_sig owne_aux Λ Σ A i.
Definition owne_eq : @owne = @owne_def := proj2_sig owne_aux.
Instance: Params (@owne) 4.
Typeclasses Opaque owne.
Definition ownle_def `{inG Λ Σ A} (a : A) : iPropG Λ Σ :=
ownGl (to_globalFe a).
Definition ownle_aux : { x | x = @ownle_def }. by eexists. Qed.
Definition ownle {Λ Σ A i} := proj1_sig ownle_aux Λ Σ A i.
Definition ownle_eq : @ownle = @ownle_def := proj2_sig ownle_aux.
Instance: Params (@ownle) 4.
Typeclasses Opaque ownle.
From iris.algebra Require Export iprod.
From iris.program_logic Require Export pviewshifts pstepshifts global_functor.
From iris.program_logic Require Import ownership.
Import uPred.
Definition own_def `{inG Λ Σ (gmapUR gname A)} (γ : gname) (a : A) : iPropG Λ Σ :=
ownG (to_globalF γ a).
Definition own_aux : { x | x = @own_def }. by eexists. Qed.
Definition own {Λ Σ A i} := proj1_sig own_aux Λ Σ A i.
Definition own_eq : @own = @own_def := proj2_sig own_aux.
Instance: Params (@own) 5.
Typeclasses Opaque own.
Definition ownl_def `{inG Λ Σ (gmapUR gname A)} (γ : gname) (a : A) : iPropG Λ Σ :=
ownGl (to_globalF γ a).
Definition ownl_aux : { x | x = @ownl_def }. by eexists. Qed.
Definition ownl {Λ Σ A i} := proj1_sig ownl_aux Λ Σ A i.
Definition ownl_eq : @ownl = @ownl_def := proj2_sig ownl_aux.
Instance: Params (@ownl) 5.
Typeclasses Opaque ownl.
Definition owne_def `{inG Λ Σ A} (a : A) : iPropG Λ Σ :=
ownG (to_globalFe a).
Definition owne_aux : { x | x = @owne_def }. by eexists. Qed.
Definition owne {Λ Σ A i} := proj1_sig owne_aux Λ Σ A i.
Definition owne_eq : @owne = @owne_def := proj2_sig owne_aux.
Instance: Params (@owne) 4.
Typeclasses Opaque owne.
Definition ownle_def `{inG Λ Σ A} (a : A) : iPropG Λ Σ :=
ownGl (to_globalFe a).
Definition ownle_aux : { x | x = @ownle_def }. by eexists. Qed.
Definition ownle {Λ Σ A i} := proj1_sig ownle_aux Λ Σ A i.
Definition ownle_eq : @ownle = @ownle_def := proj2_sig ownle_aux.
Instance: Params (@ownle) 4.
Typeclasses Opaque ownle.
Properties about ghost ownership
Global Instance own_ne γ n : Proper (dist n ==> dist n) (@own Λ Σ A _ γ).
Proof. rewrite !own_eq. solve_proper. Qed.
Global Instance own_proper γ :
Proper ((≡) ==> (⊣⊢)) (@own Λ Σ A _ γ) := ne_proper _.
Lemma own_op γ a1 a2 : own γ (a1 ⋅ a2) ⊣⊢ own γ a1 ★ own γ a2.
Proof. by rewrite !own_eq /own_def -ownG_op to_globalF_op. Qed.
Global Instance own_mono γ : Proper (flip (≼) ==> (⊢)) (@own Λ Σ A _ γ).
Proof.
move⇒a b [c ->]. rewrite own_op own_eq /own. apply sep_elim_l.
Qed.
Lemma own_valid γ a : own γ a ⊢ ⧆✓ a.
Proof.
rewrite !own_eq /own_def ownG_valid /to_globalF.
rewrite iprod_validI (forall_elim (inG_id i)) iprod_lookup_singleton.
apply affine_mono.
trans (✓ ucmra_transport (@inG_prf _ _ _ i) {[γ := a]} : iPropG Λ Σ)%I;
last destruct inG_prf; auto.
by rewrite gmap_validI (forall_elim γ) lookup_singleton option_validI.
Qed.
Lemma own_valid_r γ a : own γ a ⊢ (own γ a ★ ⧆✓ a).
Proof. apply: uPred.relevant_entails_r. apply own_valid. Qed.
Lemma own_valid_l γ a : own γ a ⊢ (⧆✓ a ★ own γ a).
Proof. by rewrite comm -own_valid_r. Qed.
Global Instance own_atimeless γ a : Timeless a → ATimelessP (own γ a).
Proof. rewrite !own_eq /own_def; apply _. Qed.
Global Instance own_affine γ a : AffineP (own γ a).
Proof. rewrite !own_eq /own_def; apply _. Qed.
Global Instance own_core_persistent γ a : Persistent a → RelevantP (own γ a).
Proof. rewrite !own_eq /own_def; apply _. Qed.
Lemma own_alloc_strong a E (G : gset gname) :
✓ a → Emp ⊢ |={E}=> ∃ γ, ■(γ ∉ G) ∧ own γ a.
Proof.
intros Ha.
rewrite -(pvs_mono _ _ (∃ m, ■ (∃ γ, γ ∉ G ∧ m = to_globalF γ a) ∧ ownG m)%I).
- rewrite ownG_empty. eapply pvs_ownG_updateP.
eapply (iprod_singleton_updateP_empty (inG_id i)
(λ y, ∃ γ, γ ∉ G ∧ iprod_singleton (inG_id i) y = to_globalF γ a)).
× rewrite -ucmra_transport_unit.
eapply ucmra_transport_updateP. eapply alloc_updateP_strong'; eauto.
intros ? (γ&?&?&?); subst.
∃ γ. split_and!; eauto.
× naive_solver.
- apply exist_elim⇒m; apply pure_elim_l=>-[γ [Hfresh ->]].
by rewrite !own_eq -(exist_intro γ) pure_equiv // left_id.
Qed.
Lemma own_alloc_strong' a E (G : gset gname) :
✓ a → Emp ⊢ |={E}=> ∃ γ, ⧆■(γ ∉ G) ★ own γ a.
Proof.
intros Ha. rewrite (own_alloc_strong a E G); auto.
apply pvs_mono, exist_mono=>?.
rewrite -(affine_affine (own _ _)) affine_and_r.
by rewrite relevant_and_sep_l_1.
Qed.
Lemma own_alloc a E : ✓ a → Emp ⊢ (|={E}=> ∃ γ, own γ a).
Proof.
intros Ha. rewrite (own_alloc_strong a E ∅) //; [].
apply pvs_mono, exist_mono=>?. eauto with I.
Qed.
Lemma own_updateP P γ a E : a ~~>: P → own γ a ={E}=> ∃ a', ■ P a' ∧ own γ a'.
Proof.
intros Ha. rewrite !own_eq.
rewrite -(pvs_mono _ _ (∃ m, ■ (∃ a', m = to_globalF γ a' ∧ P a') ∧ ownG m)%I).
- eapply pvs_ownG_updateP, iprod_singleton_updateP;
first by (apply ucmra_transport_updateP', singleton_updateP', Ha).
naive_solver.
- apply exist_elim⇒m; apply pure_elim_l=>-[a' [-> HP]].
rewrite -(exist_intro a'). by apply and_intro; [apply pure_intro|].
Qed.
Lemma own_update γ a a' E : a ~~> a' → own γ a ={E}=> own γ a'.
Proof.
intros; rewrite (own_updateP (a' =)); last by apply cmra_update_updateP.
by apply pvs_mono, exist_elim⇒ a''; apply pure_elim_l⇒ →.
Qed.
End global.
Arguments own_valid {_ _ _} [_] _ _.
Arguments own_valid_l {_ _ _} [_] _ _.
Arguments own_valid_r {_ _ _} [_] _ _.
Arguments own_updateP {_ _ _} [_] _ _ _ _ _.
Arguments own_update {_ _ _} [_] _ _ _ _ _.
Section global_empty.
Context `{i : inG Λ Σ (gmapUR gname (A:ucmraT))}.
Implicit Types a : A.
Lemma own_empty γ E : Emp ={E}=> own γ (∅:A).
Proof.
rewrite ownG_empty !own_eq /own_def.
apply pvs_ownG_update, cmra_update_updateP.
eapply (iprod_singleton_updateP_empty (inG_id i)
(λ y, iprod_singleton (inG_id i) y = to_globalF γ ∅)).
- rewrite -(ucmra_transport_unit inG_prf).
eapply ucmra_transport_updateP;
first eapply (alloc_unit_singleton_updateP' _ ∅).
× apply ucmra_unit_valid.
× apply _.
× apply cmra_update_updateP, ucmra_update_unit.
× naive_solver.
- naive_solver.
Qed.
End global_empty.
Proof. rewrite !own_eq. solve_proper. Qed.
Global Instance own_proper γ :
Proper ((≡) ==> (⊣⊢)) (@own Λ Σ A _ γ) := ne_proper _.
Lemma own_op γ a1 a2 : own γ (a1 ⋅ a2) ⊣⊢ own γ a1 ★ own γ a2.
Proof. by rewrite !own_eq /own_def -ownG_op to_globalF_op. Qed.
Global Instance own_mono γ : Proper (flip (≼) ==> (⊢)) (@own Λ Σ A _ γ).
Proof.
move⇒a b [c ->]. rewrite own_op own_eq /own. apply sep_elim_l.
Qed.
Lemma own_valid γ a : own γ a ⊢ ⧆✓ a.
Proof.
rewrite !own_eq /own_def ownG_valid /to_globalF.
rewrite iprod_validI (forall_elim (inG_id i)) iprod_lookup_singleton.
apply affine_mono.
trans (✓ ucmra_transport (@inG_prf _ _ _ i) {[γ := a]} : iPropG Λ Σ)%I;
last destruct inG_prf; auto.
by rewrite gmap_validI (forall_elim γ) lookup_singleton option_validI.
Qed.
Lemma own_valid_r γ a : own γ a ⊢ (own γ a ★ ⧆✓ a).
Proof. apply: uPred.relevant_entails_r. apply own_valid. Qed.
Lemma own_valid_l γ a : own γ a ⊢ (⧆✓ a ★ own γ a).
Proof. by rewrite comm -own_valid_r. Qed.
Global Instance own_atimeless γ a : Timeless a → ATimelessP (own γ a).
Proof. rewrite !own_eq /own_def; apply _. Qed.
Global Instance own_affine γ a : AffineP (own γ a).
Proof. rewrite !own_eq /own_def; apply _. Qed.
Global Instance own_core_persistent γ a : Persistent a → RelevantP (own γ a).
Proof. rewrite !own_eq /own_def; apply _. Qed.
Lemma own_alloc_strong a E (G : gset gname) :
✓ a → Emp ⊢ |={E}=> ∃ γ, ■(γ ∉ G) ∧ own γ a.
Proof.
intros Ha.
rewrite -(pvs_mono _ _ (∃ m, ■ (∃ γ, γ ∉ G ∧ m = to_globalF γ a) ∧ ownG m)%I).
- rewrite ownG_empty. eapply pvs_ownG_updateP.
eapply (iprod_singleton_updateP_empty (inG_id i)
(λ y, ∃ γ, γ ∉ G ∧ iprod_singleton (inG_id i) y = to_globalF γ a)).
× rewrite -ucmra_transport_unit.
eapply ucmra_transport_updateP. eapply alloc_updateP_strong'; eauto.
intros ? (γ&?&?&?); subst.
∃ γ. split_and!; eauto.
× naive_solver.
- apply exist_elim⇒m; apply pure_elim_l=>-[γ [Hfresh ->]].
by rewrite !own_eq -(exist_intro γ) pure_equiv // left_id.
Qed.
Lemma own_alloc_strong' a E (G : gset gname) :
✓ a → Emp ⊢ |={E}=> ∃ γ, ⧆■(γ ∉ G) ★ own γ a.
Proof.
intros Ha. rewrite (own_alloc_strong a E G); auto.
apply pvs_mono, exist_mono=>?.
rewrite -(affine_affine (own _ _)) affine_and_r.
by rewrite relevant_and_sep_l_1.
Qed.
Lemma own_alloc a E : ✓ a → Emp ⊢ (|={E}=> ∃ γ, own γ a).
Proof.
intros Ha. rewrite (own_alloc_strong a E ∅) //; [].
apply pvs_mono, exist_mono=>?. eauto with I.
Qed.
Lemma own_updateP P γ a E : a ~~>: P → own γ a ={E}=> ∃ a', ■ P a' ∧ own γ a'.
Proof.
intros Ha. rewrite !own_eq.
rewrite -(pvs_mono _ _ (∃ m, ■ (∃ a', m = to_globalF γ a' ∧ P a') ∧ ownG m)%I).
- eapply pvs_ownG_updateP, iprod_singleton_updateP;
first by (apply ucmra_transport_updateP', singleton_updateP', Ha).
naive_solver.
- apply exist_elim⇒m; apply pure_elim_l=>-[a' [-> HP]].
rewrite -(exist_intro a'). by apply and_intro; [apply pure_intro|].
Qed.
Lemma own_update γ a a' E : a ~~> a' → own γ a ={E}=> own γ a'.
Proof.
intros; rewrite (own_updateP (a' =)); last by apply cmra_update_updateP.
by apply pvs_mono, exist_elim⇒ a''; apply pure_elim_l⇒ →.
Qed.
End global.
Arguments own_valid {_ _ _} [_] _ _.
Arguments own_valid_l {_ _ _} [_] _ _.
Arguments own_valid_r {_ _ _} [_] _ _.
Arguments own_updateP {_ _ _} [_] _ _ _ _ _.
Arguments own_update {_ _ _} [_] _ _ _ _ _.
Section global_empty.
Context `{i : inG Λ Σ (gmapUR gname (A:ucmraT))}.
Implicit Types a : A.
Lemma own_empty γ E : Emp ={E}=> own γ (∅:A).
Proof.
rewrite ownG_empty !own_eq /own_def.
apply pvs_ownG_update, cmra_update_updateP.
eapply (iprod_singleton_updateP_empty (inG_id i)
(λ y, iprod_singleton (inG_id i) y = to_globalF γ ∅)).
- rewrite -(ucmra_transport_unit inG_prf).
eapply ucmra_transport_updateP;
first eapply (alloc_unit_singleton_updateP' _ ∅).
× apply ucmra_unit_valid.
× apply _.
× apply cmra_update_updateP, ucmra_update_unit.
× naive_solver.
- naive_solver.
Qed.
End global_empty.
Properties about ghost ownership in the nameless case
Global Instance owne_ne n : Proper (dist n ==> dist n) (@owne Λ Σ A _).
Proof. rewrite !owne_eq. solve_proper. Qed.
Global Instance owne_proper : Proper ((≡) ==> (⊣⊢)) (@owne Λ Σ A _) := ne_proper _.
Lemma owne_op a1 a2 : owne (a1 ⋅ a2) ⊣⊢ (owne a1 ★ owne a2).
Proof. by rewrite !owne_eq /owne_def -ownG_op to_globalFe_op. Qed.
Global Instance owne_mono : Proper (flip (≼) ==> (⊢)) (@owne Λ Σ A _).
Proof. move⇒a b [c ->]. rewrite !owne_eq /owne_def //= /to_globalFe.
eapply ownG_mono. simpl.
rewrite ucmra_transport_op -iprod_op_singleton.
eexists; eauto.
Qed.
Lemma owne_valid a : owne a ⊢ ⧆✓ a.
Proof.
rewrite !owne_eq /owne_def ownG_valid /to_globalFe.
rewrite iprod_validI (forall_elim (inG_id i)) iprod_lookup_singleton.
apply affine_mono.
trans (✓ ucmra_transport inG_prf a : iPropG Λ Σ)%I; last destruct inG_prf; auto.
Qed.
Lemma owne_valid_r a : owne a ⊢ (owne a ★ ⧆✓ a).
Proof. apply: uPred.relevant_entails_r. apply owne_valid. Qed.
Lemma owne_valid_l a : owne a ⊢ (⧆✓ a ★ owne a).
Proof. by rewrite comm -owne_valid_r. Qed.
Global Instance owne_atimeless a : Timeless a → ATimelessP (owne a).
Proof. rewrite !owne_eq /owne_def; apply _. Qed.
Global Instance owne_affine a : AffineP (owne a).
Proof. rewrite !owne_eq /owne_def; apply _. Qed.
Global Instance owne_core_persistent a : Persistent a → RelevantP (owne a).
Proof. rewrite !owne_eq /owne_def; apply _. Qed.
Lemma owne_updateP P a E :
a ~~>: P → owne a ⊢ (|={E}=> ∃ a', ■ P a' ∧ owne a').
Proof.
intros Ha. rewrite !owne_eq.
rewrite -(pvs_mono _ _ (∃ m, ■ (∃ a', m = to_globalFe a' ∧ P a') ∧ ownG m)%I).
- eapply pvs_ownG_updateP, iprod_singleton_updateP;
first by (apply ucmra_transport_updateP', Ha).
naive_solver.
- apply exist_elim⇒m; apply pure_elim_l=>-[a' [-> HP]].
rewrite -(exist_intro a'). by apply and_intro; [apply pure_intro|].
Qed.
Lemma owne_update a a' E : a ~~> a' → owne a ⊢ (|={E}=> owne a').
Proof.
intros; rewrite (owne_updateP (a' =)); last by apply cmra_update_updateP.
by apply pvs_mono, exist_elim⇒ a''; apply pure_elim_l⇒ →.
Qed.
Lemma owne_empty E :
Emp ={E}=> owne (∅:A).
Proof.
rewrite ownG_empty !owne_eq /owne_def. apply pvs_ownG_update, cmra_update_updateP.
eapply (iprod_singleton_updateP_empty (inG_id i)
(λ y, iprod_singleton (inG_id i) y = to_globalFe ∅)).
- rewrite -(ucmra_transport_unit inG_prf).
eapply ucmra_transport_updateP;
first eapply cmra_update_updateP, ucmra_update_unit.
naive_solver.
- naive_solver.
Qed.
Section globale_step.
Definition trivial_step (A: cmraT) :=
∀ (a a': A) n, a ⤳_(n) a'.
Context (AltTriv: ∀ (gid': gid Σ) A, gid' ≠ (inG_id i) ∧
A = projT2 Σ gid' (iPreProp Λ (globalF Σ)) →
trivial_step A).
Lemma owne_stepP P (a al: A) E :
a # al ~~>>: P → (owne a ★ ownle al)
⊢ (|={E}=>> ∃ a' al', ⧆■ P a' al' ★ owne a' ★ ownle al').
Proof.
rewrite owne_eq /owne_def ownle_eq /ownle_def cmra_total_step_updateP⇒Ha.
rewrite -(psvs_mono _ _ (∃ m ml, ⧆■ (∃ a' al', m = to_globalFe a' ∧ ml = to_globalFe al'
∧ P a' al') ★ ownG m ★ ownGl ml)%I).
- eapply psvs_stepP, cmra_total_step_updateP. intros n zf Hval.
specialize (Ha n (ucmra_transport (Coq.Init.Logic.eq_sym inG_prf) (zf (inG_id i)))).
generalize (Hval (inG_id i)).
unfold to_globalFe.
rewrite ?iprod_lookup_op ?iprod_lookup_singleton.
rewrite -(ucmra_transport_validN (Init.Logic.eq_sym inG_prf)).
rewrite !ucmra_transport_op !ucmra_transport_sym_inv.
intros Hval_inG. edestruct (Ha Hval_inG) as (y&yl&?&Hval'&Hstep).
∃ (to_globalFe y), (to_globalFe yl); split_and!.
× do 2 eexists; eauto.
× unfold to_globalFe.
intro X.
rewrite ?iprod_lookup_op.
case (decide (X = (inG_id i))).
** intros →. rewrite ?iprod_lookup_singleton.
rewrite -(ucmra_transport_validN (Init.Logic.eq_sym inG_prf)).
rewrite !ucmra_transport_op !ucmra_transport_sym_inv.
auto.
** specialize (Hval X). unfold to_globalFe in Hval.
intros; rewrite ?iprod_lookup_op ?iprod_lookup_singleton_ne in Hval *; eauto.
× intro X. case (decide (X = (inG_id i))).
** intros →. unfold to_globalFe. rewrite ?iprod_lookup_singleton.
apply ucmra_transport_stepN. eauto.
** intros. eapply (AltTriv X); eauto.
- apply exist_elim⇒m. apply exist_elim⇒ml.
apply pure_elim_sep_l. intros (a'&al'&Heq_m&Heq_ml&HP).
subst. rewrite -(exist_intro a') -(exist_intro al').
rewrite pure_equiv; auto. rewrite -emp_True left_id. auto.
Qed.
End globale_step.
End globale.
Section globalle.
Context `{i : inG Λ Σ A}.
Implicit Types a : A.
Proof. rewrite !owne_eq. solve_proper. Qed.
Global Instance owne_proper : Proper ((≡) ==> (⊣⊢)) (@owne Λ Σ A _) := ne_proper _.
Lemma owne_op a1 a2 : owne (a1 ⋅ a2) ⊣⊢ (owne a1 ★ owne a2).
Proof. by rewrite !owne_eq /owne_def -ownG_op to_globalFe_op. Qed.
Global Instance owne_mono : Proper (flip (≼) ==> (⊢)) (@owne Λ Σ A _).
Proof. move⇒a b [c ->]. rewrite !owne_eq /owne_def //= /to_globalFe.
eapply ownG_mono. simpl.
rewrite ucmra_transport_op -iprod_op_singleton.
eexists; eauto.
Qed.
Lemma owne_valid a : owne a ⊢ ⧆✓ a.
Proof.
rewrite !owne_eq /owne_def ownG_valid /to_globalFe.
rewrite iprod_validI (forall_elim (inG_id i)) iprod_lookup_singleton.
apply affine_mono.
trans (✓ ucmra_transport inG_prf a : iPropG Λ Σ)%I; last destruct inG_prf; auto.
Qed.
Lemma owne_valid_r a : owne a ⊢ (owne a ★ ⧆✓ a).
Proof. apply: uPred.relevant_entails_r. apply owne_valid. Qed.
Lemma owne_valid_l a : owne a ⊢ (⧆✓ a ★ owne a).
Proof. by rewrite comm -owne_valid_r. Qed.
Global Instance owne_atimeless a : Timeless a → ATimelessP (owne a).
Proof. rewrite !owne_eq /owne_def; apply _. Qed.
Global Instance owne_affine a : AffineP (owne a).
Proof. rewrite !owne_eq /owne_def; apply _. Qed.
Global Instance owne_core_persistent a : Persistent a → RelevantP (owne a).
Proof. rewrite !owne_eq /owne_def; apply _. Qed.
Lemma owne_updateP P a E :
a ~~>: P → owne a ⊢ (|={E}=> ∃ a', ■ P a' ∧ owne a').
Proof.
intros Ha. rewrite !owne_eq.
rewrite -(pvs_mono _ _ (∃ m, ■ (∃ a', m = to_globalFe a' ∧ P a') ∧ ownG m)%I).
- eapply pvs_ownG_updateP, iprod_singleton_updateP;
first by (apply ucmra_transport_updateP', Ha).
naive_solver.
- apply exist_elim⇒m; apply pure_elim_l=>-[a' [-> HP]].
rewrite -(exist_intro a'). by apply and_intro; [apply pure_intro|].
Qed.
Lemma owne_update a a' E : a ~~> a' → owne a ⊢ (|={E}=> owne a').
Proof.
intros; rewrite (owne_updateP (a' =)); last by apply cmra_update_updateP.
by apply pvs_mono, exist_elim⇒ a''; apply pure_elim_l⇒ →.
Qed.
Lemma owne_empty E :
Emp ={E}=> owne (∅:A).
Proof.
rewrite ownG_empty !owne_eq /owne_def. apply pvs_ownG_update, cmra_update_updateP.
eapply (iprod_singleton_updateP_empty (inG_id i)
(λ y, iprod_singleton (inG_id i) y = to_globalFe ∅)).
- rewrite -(ucmra_transport_unit inG_prf).
eapply ucmra_transport_updateP;
first eapply cmra_update_updateP, ucmra_update_unit.
naive_solver.
- naive_solver.
Qed.
Section globale_step.
Definition trivial_step (A: cmraT) :=
∀ (a a': A) n, a ⤳_(n) a'.
Context (AltTriv: ∀ (gid': gid Σ) A, gid' ≠ (inG_id i) ∧
A = projT2 Σ gid' (iPreProp Λ (globalF Σ)) →
trivial_step A).
Lemma owne_stepP P (a al: A) E :
a # al ~~>>: P → (owne a ★ ownle al)
⊢ (|={E}=>> ∃ a' al', ⧆■ P a' al' ★ owne a' ★ ownle al').
Proof.
rewrite owne_eq /owne_def ownle_eq /ownle_def cmra_total_step_updateP⇒Ha.
rewrite -(psvs_mono _ _ (∃ m ml, ⧆■ (∃ a' al', m = to_globalFe a' ∧ ml = to_globalFe al'
∧ P a' al') ★ ownG m ★ ownGl ml)%I).
- eapply psvs_stepP, cmra_total_step_updateP. intros n zf Hval.
specialize (Ha n (ucmra_transport (Coq.Init.Logic.eq_sym inG_prf) (zf (inG_id i)))).
generalize (Hval (inG_id i)).
unfold to_globalFe.
rewrite ?iprod_lookup_op ?iprod_lookup_singleton.
rewrite -(ucmra_transport_validN (Init.Logic.eq_sym inG_prf)).
rewrite !ucmra_transport_op !ucmra_transport_sym_inv.
intros Hval_inG. edestruct (Ha Hval_inG) as (y&yl&?&Hval'&Hstep).
∃ (to_globalFe y), (to_globalFe yl); split_and!.
× do 2 eexists; eauto.
× unfold to_globalFe.
intro X.
rewrite ?iprod_lookup_op.
case (decide (X = (inG_id i))).
** intros →. rewrite ?iprod_lookup_singleton.
rewrite -(ucmra_transport_validN (Init.Logic.eq_sym inG_prf)).
rewrite !ucmra_transport_op !ucmra_transport_sym_inv.
auto.
** specialize (Hval X). unfold to_globalFe in Hval.
intros; rewrite ?iprod_lookup_op ?iprod_lookup_singleton_ne in Hval *; eauto.
× intro X. case (decide (X = (inG_id i))).
** intros →. unfold to_globalFe. rewrite ?iprod_lookup_singleton.
apply ucmra_transport_stepN. eauto.
** intros. eapply (AltTriv X); eauto.
- apply exist_elim⇒m. apply exist_elim⇒ml.
apply pure_elim_sep_l. intros (a'&al'&Heq_m&Heq_ml&HP).
subst. rewrite -(exist_intro a') -(exist_intro al').
rewrite pure_equiv; auto. rewrite -emp_True left_id. auto.
Qed.
End globale_step.
End globale.
Section globalle.
Context `{i : inG Λ Σ A}.
Implicit Types a : A.
Global Instance ownle_ne n : Proper (dist n ==> dist n) (@ownle Λ Σ A _).
Proof. intros x y Heq. rewrite !ownle_eq /ownle_def. solve_proper. Qed.
Global Instance ownle_proper : Proper ((≡) ==> (⊣⊢)) (@ownle Λ Σ A _) := ne_proper _.
Lemma ownle_op a1 a2 : ownle (a1 ⋅ a2) ⊣⊢ (ownle a1 ★ ownle a2).
Proof. by rewrite !ownle_eq /ownle_def -ownGl_op to_globalFe_op. Qed.
Lemma ownle_valid a : ownle a ⊣⊢ (ownle a ★ ⧆✓ a).
Proof.
apply (anti_symm (⊢)); last apply (sep_elim_l).
rewrite !ownle_eq /ownle_def {1}ownGl_valid_r /to_globalFe.
rewrite iprod_validI (forall_elim (inG_id i)) iprod_lookup_singleton.
apply sep_mono; auto.
trans (⧆✓ ucmra_transport inG_prf a : iPropG Λ Σ)%I; last destruct inG_prf; auto.
Qed.
Lemma ownle_valid_r a : ownle a ⊢ (ownle a ★ ⧆✓ a).
Proof. rewrite {1}ownle_valid //=. Qed.
Lemma ownle_valid_l a : ownle a ⊢ (⧆✓ a ★ ownle a).
Proof. by rewrite comm -ownle_valid_r. Qed.
Global Instance ownle_core_persistent a : Persistent a → RelevantP (ownle a).
Proof. rewrite !ownle_eq /ownle_def; apply _. Qed.
End globalle.
Proof. intros x y Heq. rewrite !ownle_eq /ownle_def. solve_proper. Qed.
Global Instance ownle_proper : Proper ((≡) ==> (⊣⊢)) (@ownle Λ Σ A _) := ne_proper _.
Lemma ownle_op a1 a2 : ownle (a1 ⋅ a2) ⊣⊢ (ownle a1 ★ ownle a2).
Proof. by rewrite !ownle_eq /ownle_def -ownGl_op to_globalFe_op. Qed.
Lemma ownle_valid a : ownle a ⊣⊢ (ownle a ★ ⧆✓ a).
Proof.
apply (anti_symm (⊢)); last apply (sep_elim_l).
rewrite !ownle_eq /ownle_def {1}ownGl_valid_r /to_globalFe.
rewrite iprod_validI (forall_elim (inG_id i)) iprod_lookup_singleton.
apply sep_mono; auto.
trans (⧆✓ ucmra_transport inG_prf a : iPropG Λ Σ)%I; last destruct inG_prf; auto.
Qed.
Lemma ownle_valid_r a : ownle a ⊢ (ownle a ★ ⧆✓ a).
Proof. rewrite {1}ownle_valid //=. Qed.
Lemma ownle_valid_l a : ownle a ⊢ (⧆✓ a ★ ownle a).
Proof. by rewrite comm -ownle_valid_r. Qed.
Global Instance ownle_core_persistent a : Persistent a → RelevantP (ownle a).
Proof. rewrite !ownle_eq /ownle_def; apply _. Qed.
End globalle.