diff --git a/algebra/fin_maps.v b/algebra/fin_maps.v index db841b9f16a5355e8a68ef623fce5c486039458a..2a5afdf23d1b4623607fa2c60a237b4ecbaf0e60 100644 --- a/algebra/fin_maps.v +++ b/algebra/fin_maps.v @@ -223,6 +223,19 @@ Proof. rewrite !cmra_update_updateP; eauto using map_insert_updateP with congruence. Qed. +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. +Proof. eauto using map_singleton_updateP. Qed. +Lemma map_singleton_update i (x y : A) : x ~~> y → {[ i ↦ x ]} ~~> {[ i ↦ y ]}. +Proof. + rewrite !cmra_update_updateP=>?. eapply map_singleton_updateP; first eassumption. + by move=>? ->. +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/program_logic/global_cmra.v b/program_logic/global_cmra.v index 0c42e3a035ec7d99950b5f0bf83e039ce6fad1db..326110b65c9a7531f03e8ca5b1413520ec3e5ac7 100644 --- a/program_logic/global_cmra.v +++ b/program_logic/global_cmra.v @@ -8,23 +8,33 @@ Definition globalC (Σ : gid → iFunctor) : iFunctor := Class InG Λ (Σ : gid → iFunctor) (i : gid) (A : cmraT) := inG : A = Σ i (laterC (iPreProp Λ (globalC Σ))). -Definition to_Σ {Λ} {Σ : gid → iFunctor} (i : gid) - `{!InG Λ Σ i A} (a : A) : Σ i (laterC (iPreProp Λ (globalC Σ))) := - eq_rect A id a _ inG. -Definition to_globalC {Λ} {Σ : gid → iFunctor} - (i : gid) (γ : gid) `{!InG Λ Σ i A} (a : A) : iGst Λ (globalC Σ) := - iprod_singleton i {[ γ ↦ to_Σ _ a ]}. -Definition own {Λ} {Σ : gid → iFunctor} - (i : gid) `{!InG Λ Σ i A} (γ : gid) (a : A) : iProp Λ (globalC Σ) := - ownG (to_globalC i γ a). Section global. Context {Λ : language} {Σ : gid → iFunctor} (i : gid) `{!InG Λ Σ i A}. Implicit Types a : A. -(* Proeprties of to_globalC *) +Definition to_Σ (a : A) : Σ i (laterC (iPreProp Λ (globalC Σ))) := + eq_rect A id a _ inG. +Definition to_globalC (γ : gid) `{!InG Λ Σ i A} (a : A) : iGst Λ (globalC Σ) := + iprod_singleton i {[ γ ↦ to_Σ a ]}. +Definition own (γ : gid) (a : A) : iProp Λ (globalC Σ) := + ownG (to_globalC γ a). + +Definition from_Σ (b : Σ i (laterC (iPreProp Λ (globalC Σ)))) : A := + eq_rect (Σ i _) id b _ (Logic.eq_sym inG). +Definition P_to_Σ (P : A → Prop) (b : Σ i (laterC (iPreProp Λ (globalC Σ)))) : Prop + := P (from_Σ b). + +(* Properties of the transport. *) +Lemma to_from_Σ b : + to_Σ (from_Σ b) = b. +Proof. + rewrite /to_Σ /from_Σ. by destruct inG. +Qed. + +(* Properties of to_globalC *) Lemma globalC_op γ a1 a2 : - to_globalC i γ (a1 ⋅ a2) ≡ to_globalC i γ a1 ⋅ to_globalC i γ a2. + to_globalC γ (a1 ⋅ a2) ≡ to_globalC γ a1 ⋅ to_globalC γ a2. Proof. rewrite /to_globalC iprod_op_singleton map_op_singleton. apply iprod_singleton_proper, (fin_maps.singleton_proper (M:=gmap _)). @@ -32,7 +42,7 @@ Proof. Qed. Lemma globalC_validN n γ a : - ✓{n} (to_globalC i γ a) <-> ✓{n} a. + ✓{n} (to_globalC γ a) <-> ✓{n} a. Proof. rewrite /to_globalC. rewrite -iprod_validN_singleton -map_validN_singleton. @@ -40,7 +50,7 @@ Proof. Qed. Lemma globalC_unit γ a : - unit (to_globalC i γ a) ≡ to_globalC i γ (unit a). + unit (to_globalC γ a) ≡ to_globalC γ (unit a). Proof. rewrite /to_globalC. rewrite iprod_unit_singleton map_unit_singleton. @@ -48,57 +58,92 @@ Proof. by rewrite /to_Σ; destruct inG. Qed. -Global Instance globalC_timeless γ m : Timeless m → Timeless (to_globalC i γ m). +Global Instance globalC_timeless γ m : Timeless m → Timeless (to_globalC γ m). Proof. rewrite /to_globalC => ?. apply iprod_singleton_timeless, map_singleton_timeless. by rewrite /to_Σ; destruct inG. Qed. +(* Properties of the lifted frame-preserving updates *) +Lemma update_to_Σ a P : + a ~~>: P → to_Σ a ~~>: P_to_Σ P. +Proof. + move=>Hu gf n Hf. destruct (Hu (from_Σ gf) n) as [a' Ha']. + { move: Hf. rewrite /to_Σ /from_Σ. by destruct inG. } + exists (to_Σ a'). move:Hf Ha'. + rewrite /P_to_Σ /to_Σ /from_Σ. destruct inG. done. +Qed. + (* Properties of own *) -Global Instance own_ne γ n : Proper (dist n ==> dist n) (own i γ). +Global Instance own_ne γ n : Proper (dist n ==> dist n) (own γ). Proof. intros m m' Hm; apply ownG_ne, iprod_singleton_ne, singleton_ne. by rewrite /to_globalC /to_Σ; destruct inG. Qed. -Global Instance own_proper γ : Proper ((≡) ==> (≡)) (own i γ) := ne_proper _. +Global Instance own_proper γ : Proper ((≡) ==> (≡)) (own γ) := ne_proper _. -Lemma own_op γ a1 a2 : own i γ (a1 ⋅ a2) ≡ (own i γ a1 ★ own i γ a2)%I. +Lemma own_op γ a1 a2 : own γ (a1 ⋅ a2) ≡ (own γ a1 ★ own γ a2)%I. Proof. rewrite /own -ownG_op. apply ownG_proper, globalC_op. Qed. (* TODO: This also holds if we just have ✓a at the current step-idx, as Iris assertion. However, the map_updateP_alloc does not suffice to show this. *) Lemma own_alloc E a : - ✓a → True ⊑ pvs E E (∃ γ, own i γ a). + ✓a → True ⊑ pvs E E (∃ γ, own γ a). Proof. - intros Hm. set (P m := ∃ γ, m = to_globalC i γ a). + intros Ha. set (P m := ∃ γ, m = to_globalC γ a). rewrite -(pvs_mono _ _ (∃ m, ■P m ∧ ownG m)%I). - - rewrite -pvs_updateP_empty //; []. + - rewrite -pvs_ownG_updateP_empty //; []. subst P. eapply (iprod_singleton_updateP_empty i). - + eapply map_updateP_alloc' with (x:=to_Σ i a). + + apply map_updateP_alloc' with (x:=to_Σ a). by rewrite /to_Σ; destruct inG. + simpl. move=>? [γ [-> ?]]. exists γ. done. - - apply exist_elim=>m. apply const_elim_l. - move=>[p ->] {P}. by rewrite -(exist_intro p). + - apply exist_elim=>m. apply const_elim_l=>-[p ->] {P}. + by rewrite -(exist_intro p). Qed. -Lemma always_own_unit γ m : (□ own i γ (unit m))%I ≡ own i γ (unit m). +Lemma always_own_unit γ a : (□ own γ (unit a))%I ≡ own γ (unit a). Proof. rewrite /own -globalC_unit. by apply always_ownG_unit. Qed. -Lemma own_valid γ m : (own i γ m) ⊑ (✓ m). +Lemma own_valid γ a : (own γ a) ⊑ (✓ a). Proof. rewrite /own ownG_valid. apply uPred.valid_mono=>n. by apply globalC_validN. Qed. -Lemma own_valid_r' γ m : (own i γ m) ⊑ (own i γ m ★ ✓ m). +Lemma own_valid_r' γ a : (own γ a) ⊑ (own γ a ★ ✓ a). Proof. apply (uPred.always_entails_r' _ _), own_valid. Qed. -Global Instance ownG_timeless γ m : Timeless m → TimelessP (own i γ m). +Global Instance ownG_timeless γ a : Timeless a → TimelessP (own γ a). Proof. intros. apply ownG_timeless. apply _. Qed. +Lemma pvs_updateP E γ a P : + a ~~>: P → own γ a ⊑ pvs E E (∃ a', ■ P a' ∧ own γ a'). +Proof. + intros Ha. set (P' m := ∃ a', P a' ∧ m = to_globalC γ a'). + rewrite -(pvs_mono _ _ (∃ m, ■P' m ∧ ownG m)%I). + - rewrite -pvs_ownG_updateP; first by rewrite /own. + rewrite /to_globalC. eapply iprod_singleton_updateP. + + (* FIXME RJ: I tried apply... with instead of instantiate, that + does not work. *) + apply map_singleton_updateP'. instantiate (1:=P_to_Σ P). + by apply update_to_Σ. + + simpl. move=>? [y [-> HP]]. exists (from_Σ y). split. + * move: HP. rewrite /P_to_Σ /from_Σ. by destruct inG. + * clear HP. rewrite /to_globalC to_from_Σ; done. + - apply exist_elim=>m. apply const_elim_l=>-[a' [HP ->]]. + rewrite -(exist_intro a'). apply and_intro; last done. + by apply const_intro. +Qed. + +Lemma pvs_update E γ a a' : a ~~> a' → own γ a ⊑ pvs E E (own γ a'). +Proof. + intros; rewrite (pvs_updateP E _ _ (a' =)); last by apply cmra_update_updateP. + by apply pvs_mono, uPred.exist_elim=> m''; apply uPred.const_elim_l=> ->. +Qed. + End global. diff --git a/program_logic/pviewshifts.v b/program_logic/pviewshifts.v index b9728d6430f54be40f9a0ab0a8abf7fccf8511d9..73235c04ea711e82c2b279b3625e3b83402aa7b1 100644 --- a/program_logic/pviewshifts.v +++ b/program_logic/pviewshifts.v @@ -97,7 +97,7 @@ Proof. * by rewrite -(left_id_L ∅ (∪) Ef). * apply uPred_weaken with r n; auto. Qed. -Lemma pvs_updateP E m (P : iGst Λ Σ → Prop) : +Lemma pvs_ownG_updateP E m (P : iGst Λ Σ → Prop) : m ~~>: P → ownG m ⊑ pvs E E (∃ m', ■ P m' ∧ ownG m'). Proof. intros Hup%option_updateP' r [|n] ? Hinv%ownG_spec rf [|k] Ef σ ???; try lia. @@ -105,7 +105,7 @@ Proof. { apply cmra_includedN_le with (S n); auto. } by exists (update_gst m' r); split; [exists m'; split; [|apply ownG_spec]|]. Qed. -Lemma pvs_updateP_empty `{Empty (iGst Λ Σ), !CMRAIdentity (iGst Λ Σ)} +Lemma pvs_ownG_updateP_empty `{Empty (iGst Λ Σ), !CMRAIdentity (iGst Λ Σ)} E (P : iGst Λ Σ → Prop) : ∅ ~~>: P → True ⊑ pvs E E (∃ m', ■ P m' ∧ ownG m'). Proof. @@ -148,9 +148,9 @@ Lemma pvs_mask_weaken E1 E2 P : E1 ⊆ E2 → pvs E1 E1 P ⊑ pvs E2 E2 P. Proof. intros; rewrite (union_difference_L E1 E2) //; apply pvs_mask_frame; auto. Qed. -Lemma pvs_update E m m' : m ~~> m' → ownG m ⊑ pvs E E (ownG m'). +Lemma pvs_ownG_update E m m' : m ~~> m' → ownG m ⊑ pvs E E (ownG m'). Proof. - intros; rewrite (pvs_updateP E _ (m' =)); last by apply cmra_update_updateP. + intros; rewrite (pvs_ownG_updateP E _ (m' =)); last by apply cmra_update_updateP. by apply pvs_mono, uPred.exist_elim=> m''; apply uPred.const_elim_l=> ->. Qed. End pvs. diff --git a/program_logic/viewshifts.v b/program_logic/viewshifts.v index 812844f8730f132207009fb88e5e7f8de12543e4..0db7e66730e28fe2e17060f3442af61ff22186dd 100644 --- a/program_logic/viewshifts.v +++ b/program_logic/viewshifts.v @@ -1,6 +1,8 @@ Require Export program_logic.pviewshifts. Require Import program_logic.ownership. +(* TODO: State lemmas in terms of inv and own. *) + Definition vs {Λ Σ} (E1 E2 : coPset) (P Q : iProp Λ Σ) : iProp Λ Σ := (□ (P → pvs E1 E2 Q))%I. Arguments vs {_ _} _ _ _%I _%I. @@ -25,14 +27,18 @@ Proof. intros; rewrite -{1}always_const; apply always_intro, impl_intro_l. by rewrite always_const (right_id _ _). Qed. + Global Instance vs_ne E1 E2 n : Proper (dist n ==> dist n ==> dist n) (@vs Λ Σ E1 E2). Proof. by intros P P' HP Q Q' HQ; rewrite /vs HP HQ. Qed. + Global Instance vs_proper E1 E2 : Proper ((≡) ==> (≡) ==> (≡)) (@vs Λ Σ E1 E2). Proof. apply ne_proper_2, _. Qed. + Lemma vs_mono E1 E2 P P' Q Q' : P ⊑ P' → Q' ⊑ Q → P' >{E1,E2}> Q' ⊑ P >{E1,E2}> Q. Proof. by intros HP HQ; rewrite /vs -HP HQ. Qed. + Global Instance vs_mono' E1 E2 : Proper (flip (⊑) ==> (⊑) ==> (⊑)) (@vs Λ Σ E1 E2). Proof. by intros until 2; apply vs_mono. Qed. @@ -41,6 +47,7 @@ Lemma vs_false_elim E1 E2 P : False >{E1,E2}> P. Proof. apply vs_alt, False_elim. Qed. Lemma vs_timeless E P : TimelessP P → ▷ P >{E}> P. Proof. by intros ?; apply vs_alt, pvs_timeless. Qed. + Lemma vs_transitive E1 E2 E3 P Q R : E2 ⊆ E1 ∪ E3 → (P >{E1,E2}> Q ∧ Q >{E2,E3}> R) ⊑ P >{E1,E3}> R. Proof. @@ -48,54 +55,67 @@ Proof. rewrite always_and (associative _) (always_elim (P → _)) impl_elim_r. by rewrite pvs_impl_r; apply pvs_trans. Qed. + Lemma vs_transitive' E P Q R : (P >{E}> Q ∧ Q >{E}> R) ⊑ P >{E}> R. Proof. apply vs_transitive; solve_elem_of. Qed. Lemma vs_reflexive E P : P >{E}> P. Proof. apply vs_alt, pvs_intro. Qed. + Lemma vs_impl E P Q : □ (P → Q) ⊑ P >{E}> Q. Proof. apply always_intro, impl_intro_l. by rewrite always_elim impl_elim_r -pvs_intro. Qed. + Lemma vs_frame_l E1 E2 P Q R : P >{E1,E2}> Q ⊑ (R ★ P) >{E1,E2}> (R ★ Q). Proof. apply always_intro, impl_intro_l. rewrite -pvs_frame_l always_and_sep_r -always_wand_impl -(associative _). by rewrite always_elim wand_elim_r. Qed. + Lemma vs_frame_r E1 E2 P Q R : P >{E1,E2}> Q ⊑ (P ★ R) >{E1,E2}> (Q ★ R). Proof. rewrite !(commutative _ _ R); apply vs_frame_l. Qed. + Lemma vs_mask_frame E1 E2 Ef P Q : Ef ∩ (E1 ∪ E2) = ∅ → P >{E1,E2}> Q ⊑ P >{E1 ∪ Ef,E2 ∪ Ef}> Q. Proof. intros ?; apply always_intro, impl_intro_l; rewrite (pvs_mask_frame _ _ Ef)//. by rewrite always_elim impl_elim_r. Qed. + Lemma vs_mask_frame' E Ef P Q : Ef ∩ E = ∅ → P >{E}> Q ⊑ P >{E ∪ Ef}> Q. Proof. intros; apply vs_mask_frame; solve_elem_of. Qed. Lemma vs_open i P : ownI i P >{{[i]},∅}> ▷ P. Proof. intros; apply vs_alt, pvs_open. Qed. + Lemma vs_open' E i P : i ∉ E → ownI i P >{{[i]} ∪ E,E}> ▷ P. Proof. intros; rewrite -{2}(left_id_L ∅ (∪) E) -vs_mask_frame; last solve_elem_of. apply vs_open. Qed. + Lemma vs_close i P : (ownI i P ∧ ▷ P) >{∅,{[i]}}> True. Proof. intros; apply vs_alt, pvs_close. Qed. + Lemma vs_close' E i P : i ∉ E → (ownI i P ∧ ▷ P) >{E,{[i]} ∪ E}> True. Proof. intros; rewrite -{1}(left_id_L ∅ (∪) E) -vs_mask_frame; last solve_elem_of. apply vs_close. Qed. -Lemma vs_updateP E m (P : iGst Λ Σ → Prop) : + +Lemma vs_ownG_updateP E m (P : iGst Λ Σ → Prop) : m ~~>: P → ownG m >{E}> (∃ m', ■ P m' ∧ ownG m'). -Proof. by intros; apply vs_alt, pvs_updateP. Qed. -Lemma vs_updateP_empty `{Empty (iGst Λ Σ), !CMRAIdentity (iGst Λ Σ)} +Proof. by intros; apply vs_alt, pvs_ownG_updateP. Qed. + +Lemma vs_ownG_updateP_empty `{Empty (iGst Λ Σ), !CMRAIdentity (iGst Λ Σ)} E (P : iGst Λ Σ → Prop) : ∅ ~~>: P → True >{E}> (∃ m', ■ P m' ∧ ownG m'). -Proof. by intros; apply vs_alt, pvs_updateP_empty. Qed. +Proof. by intros; apply vs_alt, pvs_ownG_updateP_empty. Qed. + Lemma vs_update E m m' : m ~~> m' → ownG m >{E}> ownG m'. -Proof. by intros; apply vs_alt, pvs_update. Qed. +Proof. by intros; apply vs_alt, pvs_ownG_update. Qed. Lemma vs_alloc E P : ¬set_finite E → ▷ P >{E}> (∃ i, ■ (i ∈ E) ∧ ownI i P). Proof. by intros; apply vs_alt, pvs_alloc. Qed. + End vs.