Commit d64e67b0 by Ralf Jung

change notation for view shifts to ={E}=>

parent f6909092
 ... @@ -36,7 +36,7 @@ Proof. ... @@ -36,7 +36,7 @@ Proof. by rewrite -wp_value; apply const_intro. by rewrite -wp_value; apply const_intro. Qed. Qed. Lemma ht_vs E P P' Q Q' e : 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 }}. ⊑ {{ P }} e @ E {{ Q }}. Proof. Proof. apply (always_intro' _ _), impl_intro_l. apply (always_intro' _ _), impl_intro_l. ... @@ -47,7 +47,7 @@ Proof. ... @@ -47,7 +47,7 @@ Proof. Qed. Qed. Lemma ht_atomic E1 E2 P P' Q Q' e : Lemma ht_atomic E1 E2 P P' Q Q' e : E2 ⊆ E1 → atomic 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 }}. ⊑ {{ P }} e @ E1 {{ Q }}. Proof. Proof. intros ??; apply (always_intro' _ _), impl_intro_l. intros ??; apply (always_intro' _ _), impl_intro_l. ... ...
 ... @@ -20,8 +20,8 @@ Lemma ht_lift_step E1 E2 ... @@ -20,8 +20,8 @@ Lemma ht_lift_step E1 E2 E1 ⊆ E2 → to_val e1 = None → E1 ⊆ E2 → to_val e1 = None → reducible e1 σ1 → reducible e1 σ1 → (∀ e2 σ2 ef, prim_step e1 σ1 e2 σ2 ef → φ e2 σ2 ef) → (∀ e2 σ2 ef, prim_step e1 σ1 e2 σ2 ef → φ e2 σ2 ef) → ((P >{E2,E1}=> ownP σ1 ★ ▷ P') ∧ ∀ 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) ∧ (■ φ e2 σ2 ef ★ ownP σ2 ★ P' ={E1,E2}=> Q1 e2 σ2 ef ★ Q2 e2 σ2 ef) ∧ {{ Q1 e2 σ2 ef }} e2 @ E2 {{ R }} ∧ {{ Q1 e2 σ2 ef }} e2 @ E2 {{ R }} ∧ {{ Q2 e2 σ2 ef }} ef ?@ coPset_all {{ λ _, True }}) {{ Q2 e2 σ2 ef }} ef ?@ coPset_all {{ λ _, True }}) ⊑ {{ P }} e1 @ E2 {{ R }}. ⊑ {{ P }} e1 @ E2 {{ R }}. ... ...
 ... @@ -6,22 +6,22 @@ Definition vs {Λ Σ} (E1 E2 : coPset) (P Q : iProp Λ Σ) : iProp Λ Σ := ... @@ -6,22 +6,22 @@ Definition vs {Λ Σ} (E1 E2 : coPset) (P Q : iProp Λ Σ) : iProp Λ Σ := (□ (P → pvs E1 E2 Q))%I. (□ (P → pvs E1 E2 Q))%I. Arguments vs {_ _} _ _ _%I _%I. Arguments vs {_ _} _ _ _%I _%I. Instance: Params (@vs) 4. Instance: Params (@vs) 4. Notation "P >{ E1 , E2 }=> Q" := (vs E1 E2 P%I Q%I) Notation "P ={ E1 , E2 }=> Q" := (vs E1 E2 P%I Q%I) (at level 199, E1 at level 1, E2 at level 1, (at level 199, E1 at level 1, E2 at level 1, format "P >{ E1 , E2 }=> Q") : uPred_scope. format "P ={ E1 , E2 }=> Q") : uPred_scope. Notation "P >{ E1 , E2 }=> Q" := (True ⊑ vs E1 E2 P%I Q%I) Notation "P ={ E1 , E2 }=> Q" := (True ⊑ vs E1 E2 P%I Q%I) (at level 199, E1 at level 1, E2 at level 1, (at level 199, E1 at level 1, E2 at level 1, format "P >{ E1 , E2 }=> Q") : C_scope. format "P ={ E1 , E2 }=> Q") : C_scope. Notation "P >{ E }=> Q" := (vs E E P%I Q%I) Notation "P ={ E }=> Q" := (vs E E P%I Q%I) (at level 199, E at level 1, format "P >{ E }=> Q") : uPred_scope. (at level 199, E at level 1, format "P ={ E }=> Q") : uPred_scope. Notation "P >{ E }=> Q" := (True ⊑ vs E E P%I Q%I) Notation "P ={ E }=> Q" := (True ⊑ vs E E P%I Q%I) (at level 199, E at level 1, format "P >{ E }=> Q") : C_scope. (at level 199, E at level 1, format "P ={ E }=> Q") : C_scope. Section vs. Section vs. Context {Λ : language} {Σ : iFunctor}. Context {Λ : language} {Σ : iFunctor}. Implicit Types P Q R : iProp Λ Σ. 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. Proof. intros; rewrite -{1}always_const; apply always_intro, impl_intro_l. intros; rewrite -{1}always_const; apply always_intro, impl_intro_l. by rewrite always_const (right_id _ _). by rewrite always_const (right_id _ _). ... @@ -35,60 +35,60 @@ Global Instance vs_proper E1 E2 : Proper ((≡) ==> (≡) ==> (≡)) (@vs Λ Σ ... @@ -35,60 +35,60 @@ Global Instance vs_proper E1 E2 : Proper ((≡) ==> (≡) ==> (≡)) (@vs Λ Σ Proof. apply ne_proper_2, _. Qed. Proof. apply ne_proper_2, _. Qed. Lemma vs_mono E1 E2 P P' Q Q' : 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. Proof. by intros HP HQ; rewrite /vs -HP HQ. Qed. Global Instance vs_mono' E1 E2 : Global Instance vs_mono' E1 E2 : Proper (flip (⊑) ==> (⊑) ==> (⊑)) (@vs Λ Σ E1 E2). Proper (flip (⊑) ==> (⊑) ==> (⊑)) (@vs Λ Σ E1 E2). Proof. by intros until 2; apply vs_mono. Qed. 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. 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. Proof. by intros ?; apply vs_alt, pvs_timeless. Qed. Lemma vs_transitive E1 E2 E3 P Q R : 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. Proof. intros; rewrite -always_and; apply always_intro, impl_intro_l. intros; rewrite -always_and; apply always_intro, impl_intro_l. rewrite always_and (associative _) (always_elim (P → _)) impl_elim_r. rewrite always_and (associative _) (always_elim (P → _)) impl_elim_r. by rewrite pvs_impl_r; apply pvs_trans. by rewrite pvs_impl_r; apply pvs_trans. Qed. 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. 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. 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. Proof. apply always_intro, impl_intro_l. apply always_intro, impl_intro_l. by rewrite always_elim impl_elim_r -pvs_intro. by rewrite always_elim impl_elim_r -pvs_intro. Qed. 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. Proof. apply always_intro, impl_intro_l. apply always_intro, impl_intro_l. rewrite -pvs_frame_l always_and_sep_r -always_wand_impl -(associative _). rewrite -pvs_frame_l always_and_sep_r -always_wand_impl -(associative _). by rewrite always_elim wand_elim_r. by rewrite always_elim wand_elim_r. Qed. 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. Proof. rewrite !(commutative _ _ R); apply vs_frame_l. Qed. Lemma vs_mask_frame E1 E2 Ef P Q : 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. Proof. intros ?; apply always_intro, impl_intro_l; rewrite (pvs_mask_frame _ _ Ef)//. intros ?; apply always_intro, impl_intro_l; rewrite (pvs_mask_frame _ _ Ef)//. by rewrite always_elim impl_elim_r. by rewrite always_elim impl_elim_r. Qed. 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. Proof. intros; apply vs_mask_frame; solve_elem_of. Qed. Lemma vs_open_close N E P Q R : Lemma vs_open_close N E P Q R : nclose N ⊆ E → nclose N ⊆ E → (inv N R ∧ (▷ R ★ P >{E ∖ nclose N}=> ▷ R ★ Q)) ⊑ (P >{E}=> Q). (inv N R ∧ (▷ R ★ P ={E ∖ nclose N}=> ▷ R ★ Q)) ⊑ (P ={E}=> Q). Proof. Proof. intros; apply (always_intro' _ _), impl_intro_l. intros; apply (always_intro' _ _), impl_intro_l. rewrite associative (commutative _ P) -associative. rewrite associative (commutative _ P) -associative. ... @@ -99,7 +99,7 @@ Proof. ... @@ -99,7 +99,7 @@ Proof. by rewrite /vs always_elim impl_elim_r. by rewrite /vs always_elim impl_elim_r. Qed. Qed. Lemma vs_alloc (N : namespace) P : ▷ P >{N}=> inv N P. Lemma vs_alloc (N : namespace) P : ▷ P ={N}=> inv N P. Proof. by intros; apply vs_alt, pvs_alloc. Qed. Proof. by intros; apply vs_alt, pvs_alloc. Qed. End vs. End vs. ... @@ -110,14 +110,14 @@ Implicit Types a : A. ... @@ -110,14 +110,14 @@ Implicit Types a : A. Implicit Types P Q R : iProp Λ (globalC Σ). Implicit Types P Q R : iProp Λ (globalC Σ). Lemma vs_own_updateP E γ a φ : Lemma vs_own_updateP E γ a φ : a ~~>: φ → own i γ a >{E}=> ∃ a', ■ φ a' ∧ own i γ a'. a ~~>: φ → own i γ a ={E}=> ∃ a', ■ φ a' ∧ own i γ a'. Proof. by intros; apply vs_alt, own_updateP. Qed. Proof. by intros; apply vs_alt, own_updateP. Qed. Lemma vs_own_updateP_empty `{Empty A, !CMRAIdentity A} E γ φ : Lemma vs_own_updateP_empty `{Empty A, !CMRAIdentity A} E γ φ : ∅ ~~>: φ → True >{E}=> ∃ a', ■ φ a' ∧ own i γ a'. ∅ ~~>: φ → True ={E}=> ∃ a', ■ φ a' ∧ own i γ a'. Proof. by intros; eapply vs_alt, own_updateP_empty. Qed. Proof. by intros; eapply vs_alt, own_updateP_empty. Qed. Lemma vs_update E γ a a' : a ~~> a' → own i γ a >{E}=> own i γ a'. Lemma vs_update E γ a a' : a ~~> a' → own i γ a ={E}=> own i γ a'. Proof. by intros; apply vs_alt, own_update. Qed. Proof. by intros; apply vs_alt, own_update. Qed. End vs_ghost. End vs_ghost.
Markdown is supported
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!