Commit f8efeaaf by Ralf Jung

### derive rules for inv and own for view shifts; change notation for view shifts

parent b902393a
 ... ... @@ -37,7 +37,7 @@ Proof. by rewrite -wp_value -pvs_intro; apply const_intro. Qed. Lemma ht_vs E P P' Q Q' e : (P >{E}> P' ∧ {{ P' }} e @ E {{ Q' }} ∧ ∀ v, Q' v >{E}> Q v) (P ={E}=> P' ∧ {{ P' }} e @ E {{ Q' }} ∧ ∀ v, Q' v ={E}=> Q v) ⊑ {{ P }} e @ E {{ Q }}. Proof. apply (always_intro' _ _), impl_intro_l. ... ... @@ -48,7 +48,7 @@ Proof. Qed. Lemma ht_atomic E1 E2 P P' Q Q' e : E2 ⊆ E1 → atomic e → (P >{E1,E2}> P' ∧ {{ P' }} e @ E2 {{ Q' }} ∧ ∀ v, Q' v >{E2,E1}> Q v) (P ={E1,E2}=> P' ∧ {{ P' }} e @ E2 {{ Q' }} ∧ ∀ v, Q' v ={E2,E1}=> Q v) ⊑ {{ P }} e @ E1 {{ Q }}. Proof. intros ??; apply (always_intro' _ _), impl_intro_l. ... ...
 ... ... @@ -20,8 +20,8 @@ Lemma ht_lift_step E1 E2 E1 ⊆ E2 → to_val e1 = None → reducible e1 σ1 → (∀ e2 σ2 ef, prim_step e1 σ1 e2 σ2 ef → φ e2 σ2 ef) → (P >{E2,E1}> (ownP σ1 ★ ▷ P') ∧ ∀ e2 σ2 ef, (■ φ e2 σ2 ef ★ ownP σ2 ★ P') >{E1,E2}> (Q1 e2 σ2 ef ★ Q2 e2 σ2 ef) ∧ (P ={E2,E1}=> (ownP σ1 ★ ▷ P') ∧ ∀ e2 σ2 ef, (■ φ e2 σ2 ef ★ ownP σ2 ★ P') ={E1,E2}=> (Q1 e2 σ2 ef ★ Q2 e2 σ2 ef) ∧ {{ Q1 e2 σ2 ef }} e2 @ E2 {{ R }} ∧ {{ Q2 e2 σ2 ef }} ef ?@ coPset_all {{ λ _, True }}) ⊑ {{ P }} e1 @ E2 {{ R }}. ... ...
 ... ... @@ -70,12 +70,11 @@ Proof. by rewrite always_always. Qed. triples will have to prove its own version of the open_close rule by unfolding `inv`. *) (* TODO Can we prove something that helps for both open_close lemmas? *) Lemma pvs_open_close E N P Q R : Lemma pvs_open_close E N P Q : nclose N ⊆ E → P ⊑ (inv N R ∧ (▷R -★ pvs (E ∖ nclose N) (E ∖ nclose N) (▷R ★ Q)))%I → P ⊑ pvs E E Q. (inv N P ∧ (▷P -★ pvs (E ∖ nclose N) (E ∖ nclose N) (▷P ★ Q))) ⊑ pvs E E Q. Proof. move=>HN -> {P}. move=>HN. rewrite /inv and_exist_r. apply exist_elim=>i. rewrite -associative. apply const_elim_l=>HiN. rewrite -(pvs_trans3 E (E ∖ {[encode i]})) //; last by solve_elem_of+. ... ... @@ -84,18 +83,17 @@ Proof. rewrite always_and_sep_l' (always_sep_dup' (ownI _ _)). rewrite {1}pvs_openI !pvs_frame_r. apply pvs_mask_frame_mono ; [solve_elem_of..|]. rewrite (commutative _ (▷R)%I) -associative wand_elim_r pvs_frame_l. rewrite (commutative _ (▷_)%I) -associative wand_elim_r pvs_frame_l. apply pvs_mask_frame_mono; [solve_elem_of..|]. rewrite associative -always_and_sep_l' pvs_closeI pvs_frame_r left_id. apply pvs_mask_frame'; solve_elem_of. Qed. Lemma wp_open_close E e N P (Q : val Λ → iProp Λ Σ) R : Lemma wp_open_close E e N P (Q : val Λ → iProp Λ Σ) : atomic e → nclose N ⊆ E → P ⊑ (inv N R ∧ (▷R -★ wp (E ∖ nclose N) e (λ v, ▷R ★ Q v)))%I → P ⊑ wp E e Q. (inv N P ∧ (▷P -★ wp (E ∖ nclose N) e (λ v, ▷P ★ Q v)))%I ⊑ wp E e Q. Proof. move=>He HN -> {P}. move=>He HN. rewrite /inv and_exist_r. apply exist_elim=>i. rewrite -associative. apply const_elim_l=>HiN. rewrite -(wp_atomic E (E ∖ {[encode i]})) //; last by solve_elem_of+. ... ... @@ -104,7 +102,7 @@ Proof. rewrite always_and_sep_l' (always_sep_dup' (ownI _ _)). rewrite {1}pvs_openI !pvs_frame_r. apply pvs_mask_frame_mono; [solve_elem_of..|]. rewrite (commutative _ (▷R)%I) -associative wand_elim_r wp_frame_l. rewrite (commutative _ (▷_)%I) -associative wand_elim_r wp_frame_l. apply wp_mask_frame_mono; [solve_elem_of..|]=>v. rewrite associative -always_and_sep_l' pvs_closeI pvs_frame_r left_id. apply pvs_mask_frame'; solve_elem_of. ... ...
 Require Export program_logic.pviewshifts. Require Import program_logic.ownership. (* TODO: State lemmas in terms of inv and own. *) Require Export program_logic.pviewshifts program_logic.invariants program_logic.ghost_ownership. Import uPred. Definition vs {Λ Σ} (E1 E2 : coPset) (P Q : iProp Λ Σ) : iProp Λ Σ := (□ (P → pvs E1 E2 Q))%I. Arguments vs {_ _} _ _ _%I _%I. Instance: Params (@vs) 4. Notation "P >{ E1 , E2 }> Q" := (vs E1 E2 P%I Q%I) (at level 69, E1 at level 1, format "P >{ E1 , E2 }> Q") : uPred_scope. Notation "P >{ E1 , E2 }> Q" := (True ⊑ vs E1 E2 P%I Q%I) (at level 69, E1 at level 1, format "P >{ E1 , E2 }> Q") : C_scope. Notation "P >{ E }> Q" := (vs E E P%I Q%I) (at level 69, E at level 1, format "P >{ E }> Q") : uPred_scope. Notation "P >{ E }> Q" := (True ⊑ vs E E P%I Q%I) (at level 69, E at level 1, format "P >{ E }> Q") : C_scope. Notation "P ={ E1 , E2 }=> Q" := (vs E1 E2 P%I Q%I) (at level 69, E1 at level 1, format "P ={ E1 , E2 }=> Q") : uPred_scope. Notation "P ={ E1 , E2 }=> Q" := (True ⊑ vs E1 E2 P%I Q%I) (at level 69, E1 at level 1, format "P ={ E1 , E2 }=> Q") : C_scope. Notation "P ={ E }=> Q" := (vs E E P%I Q%I) (at level 69, E at level 1, format "P ={ E }=> Q") : uPred_scope. Notation "P ={ E }=> Q" := (True ⊑ vs E E P%I Q%I) (at level 69, E at level 1, format "P ={ E }=> Q") : C_scope. Section vs. Context {Λ : language} {Σ : iFunctor}. Implicit Types P Q : iProp Λ Σ. Implicit Types m : iGst Λ Σ. Import uPred. Implicit Types P Q R : iProp Λ Σ. Lemma vs_alt E1 E2 P Q : (P ⊑ pvs E1 E2 Q) → P >{E1,E2}> Q. Lemma vs_alt E1 E2 P Q : (P ⊑ pvs E1 E2 Q) → P ={E1,E2}=> Q. Proof. intros; rewrite -{1}always_const; apply always_intro, impl_intro_l. by rewrite always_const (right_id _ _). ... ... @@ -36,86 +33,92 @@ Global Instance vs_proper E1 E2 : Proper ((≡) ==> (≡) ==> (≡)) (@vs Λ Σ 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. 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. Lemma vs_false_elim E1 E2 P : False >{E1,E2}> P. 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. 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. E2 ⊆ E1 ∪ E3 → (P ={E1,E2}=> Q ∧ Q ={E2,E3}=> R) ⊑ P ={E1,E3}=> R. Proof. intros; rewrite -always_and; apply always_intro, impl_intro_l. 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. 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. 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. 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). 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). 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. 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. 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_openI. Qed. Lemma vs_open' E i P : i ∉ E → ownI i P >{{[i]} ∪ E,E}> ▷ P. (* FIXME I really should not need parenthesis around the pre- and postcondition of a view shift. *) Lemma vs_open_close N E P Q R : nclose N ⊆ E → (inv N R ∧ (▷R ★ P) ={E ∖ nclose N}=> (▷R ★ Q)) ⊑ P ={E}=> Q. Proof. intros; rewrite -{2}(left_id_L ∅ (∪) E) -vs_mask_frame; last solve_elem_of. apply vs_open. intros HN. apply always_intro'; first by apply _. apply impl_intro_l. rewrite associative (commutative _ P) -associative. rewrite -pvs_open_close; first (apply and_mono; first done); last done. apply wand_intro_l. (* Oh wow, this is annyoing... *) rewrite always_and_sep_r' associative -always_and_sep_r'. by rewrite /vs always_elim impl_elim_r. Qed. Lemma vs_close i P : (ownI i P ∧ ▷ P) >{∅,{[i]}}> True. Proof. intros; apply vs_alt, pvs_closeI. Qed. Lemma vs_alloc (N : namespace) P : ▷ P ={N}=> inv N P. Proof. by intros; apply vs_alt, pvs_alloc. 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. End vs. 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_ownG_updateP. Qed. Section vs_ghost. Context {Λ : language} {Σ : gid → iFunctor} (i : gid) `{!InG Λ Σ i A}. Implicit Types a : A. Implicit Types P Q R : iProp Λ (globalC Σ). 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_ownG_updateP_empty. Qed. Lemma vs_own_updateP E γ a (P : A → Prop) : a ~~>: P → own i γ a ={E}=> (∃ a', ■ P a' ∧ own i γ a'). Proof. by intros; apply vs_alt, own_updateP. Qed. Lemma vs_update E m m' : m ~~> m' → ownG m >{E}> ownG m'. 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_allocI. Qed. Lemma vs_own_updateP_empty `{Empty A, !CMRAIdentity A} E γ (P : A → Prop) : ∅ ~~>: P → True ={E}=> (∃ a', ■ P a' ∧ own i γ a'). Proof. by intros; eapply vs_alt, own_updateP_empty. Qed. End vs. Lemma vs_update E γ a a' : a ~~> a' → own i γ a ={E}=> own i γ a'. Proof. by intros; apply vs_alt, own_update. Qed. End vs_ghost.
Supports Markdown
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!