pviewshifts.v 7.68 KB
 Ralf Jung committed Feb 08, 2016 1 2 3 ``````Require Export prelude.co_pset. Require Export program_logic.model. Require Import program_logic.ownership program_logic.wsat. `````` Robbert Krebbers committed Jan 17, 2016 4 5 6 7 8 9 10 ``````Local Hint Extern 10 (_ ≤ _) => omega. Local Hint Extern 100 (@eq coPset _ _) => solve_elem_of. Local Hint Extern 100 (_ ∉ _) => solve_elem_of. Local Hint Extern 10 (✓{_} _) => repeat match goal with H : wsat _ _ _ _ |- _ => apply wsat_valid in H end; solve_validN. `````` Robbert Krebbers committed Feb 01, 2016 11 ``````Program Definition pvs {Λ Σ} (E1 E2 : coPset) (P : iProp Λ Σ) : iProp Λ Σ := `````` Robbert Krebbers committed Jan 17, 2016 12 13 14 15 16 `````` {| uPred_holds n r1 := ∀ rf k Ef σ, 1 < k ≤ n → (E1 ∪ E2) ∩ Ef = ∅ → wsat k (E1 ∪ Ef) σ (r1 ⋅ rf) → ∃ r2, P k r2 ∧ wsat k (E2 ∪ Ef) σ (r2 ⋅ rf) |}. Next Obligation. `````` Robbert Krebbers committed Feb 01, 2016 17 `````` intros Λ Σ E1 E2 P r1 r2 n HP Hr rf k Ef σ ?? Hwsat; simpl in *. `````` Robbert Krebbers committed Jan 17, 2016 18 19 `````` apply HP; auto. by rewrite (dist_le _ _ _ _ Hr); last lia. Qed. `````` Robbert Krebbers committed Feb 01, 2016 20 ``````Next Obligation. intros Λ Σ E1 E2 P r rf k Ef σ; simpl in *; lia. Qed. `````` Robbert Krebbers committed Jan 17, 2016 21 ``````Next Obligation. `````` Robbert Krebbers committed Feb 01, 2016 22 `````` intros Λ Σ E1 E2 P r1 r2 n1 n2 HP [r3 ?] Hn ? rf k Ef σ ?? Hws; setoid_subst. `````` Robbert Krebbers committed Jan 17, 2016 23 24 `````` destruct (HP (r3⋅rf) k Ef σ) as (r'&?&Hws'); rewrite ?(associative op); auto. exists (r' ⋅ r3); rewrite -(associative _); split; last done. `````` Robbert Krebbers committed Feb 01, 2016 25 `````` apply uPred_weaken with r' k; eauto using cmra_included_l. `````` Robbert Krebbers committed Jan 17, 2016 26 ``````Qed. `````` Robbert Krebbers committed Feb 01, 2016 27 28 ``````Arguments pvs {_ _} _ _ _%I : simpl never. Instance: Params (@pvs) 4. `````` Robbert Krebbers committed Jan 17, 2016 29 30 `````` Section pvs. `````` Robbert Krebbers committed Feb 01, 2016 31 32 33 ``````Context {Λ : language} {Σ : iFunctor}. Implicit Types P Q : iProp Λ Σ. Implicit Types m : iGst Λ Σ. `````` Robbert Krebbers committed Jan 19, 2016 34 ``````Transparent uPred_holds. `````` Robbert Krebbers committed Jan 17, 2016 35 `````` `````` Robbert Krebbers committed Feb 01, 2016 36 ``````Global Instance pvs_ne E1 E2 n : Proper (dist n ==> dist n) (@pvs Λ Σ E1 E2). `````` Robbert Krebbers committed Jan 17, 2016 37 38 39 40 41 ``````Proof. intros P Q HPQ r1 n' ??; simpl; split; intros HP rf k Ef σ ???; destruct (HP rf k Ef σ) as (r2&?&?); auto; exists r2; split_ands; auto; apply HPQ; eauto. Qed. `````` Robbert Krebbers committed Feb 01, 2016 42 ``````Global Instance pvs_proper E1 E2 : Proper ((≡) ==> (≡)) (@pvs Λ Σ E1 E2). `````` Robbert Krebbers committed Jan 17, 2016 43 44 45 46 47 48 49 50 51 52 53 54 55 56 57 58 ``````Proof. apply ne_proper, _. Qed. Lemma pvs_intro E P : P ⊑ pvs E E P. Proof. intros r n ? HP rf k Ef σ ???; exists r; split; last done. apply uPred_weaken with r n; eauto. Qed. Lemma pvs_mono E1 E2 P Q : P ⊑ Q → pvs E1 E2 P ⊑ pvs E1 E2 Q. Proof. intros HPQ r n ? HP rf k Ef σ ???. destruct (HP rf k Ef σ) as (r2&?&?); eauto; exists r2; eauto. Qed. Lemma pvs_timeless E P : TimelessP P → (▷ P) ⊑ pvs E E P. Proof. rewrite uPred.timelessP_spec=> HP r [|n] ? HP' rf k Ef σ ???; first lia. exists r; split; last done. `````` Robbert Krebbers committed Feb 01, 2016 59 `````` apply HP, uPred_weaken with r n; eauto using cmra_validN_le. `````` Robbert Krebbers committed Jan 17, 2016 60 61 62 63 64 65 66 67 68 69 70 71 72 73 74 75 76 77 78 79 80 81 ``````Qed. Lemma pvs_trans E1 E2 E3 P : E2 ⊆ E1 ∪ E3 → pvs E1 E2 (pvs E2 E3 P) ⊑ pvs E1 E3 P. Proof. intros ? r1 n ? HP1 rf k Ef σ ???. destruct (HP1 rf k Ef σ) as (r2&HP2&?); auto. Qed. Lemma pvs_mask_frame E1 E2 Ef P : Ef ∩ (E1 ∪ E2) = ∅ → pvs E1 E2 P ⊑ pvs (E1 ∪ Ef) (E2 ∪ Ef) P. Proof. intros ? r n ? HP rf k Ef' σ ???. destruct (HP rf k (Ef∪Ef') σ) as (r'&?&?); rewrite ?(associative_L _); eauto. by exists r'; rewrite -(associative_L _). Qed. Lemma pvs_frame_r E1 E2 P Q : (pvs E1 E2 P ★ Q) ⊑ pvs E1 E2 (P ★ Q). Proof. intros r n ? (r1&r2&Hr&HP&?) rf k Ef σ ???. destruct (HP (r2 ⋅ rf) k Ef σ) as (r'&?&?); eauto. { by rewrite (associative _) -(dist_le _ _ _ _ Hr); last lia. } exists (r' ⋅ r2); split; last by rewrite -(associative _). exists r', r2; split_ands; auto; apply uPred_weaken with r2 n; auto. Qed. `````` Ralf Jung committed Feb 09, 2016 82 ``````Lemma pvs_openI i P : ownI i P ⊑ pvs {[ i ]} ∅ (▷ P). `````` Robbert Krebbers committed Jan 17, 2016 83 84 ``````Proof. intros r [|n] ? Hinv rf [|k] Ef σ ???; try lia. `````` Ralf Jung committed Feb 09, 2016 85 `````` apply ownI_spec in Hinv; last auto. `````` Robbert Krebbers committed Jan 17, 2016 86 87 88 `````` destruct (wsat_open k Ef σ (r ⋅ rf) i P) as (rP&?&?); auto. { rewrite lookup_wld_op_l ?Hinv; eauto; apply dist_le with (S n); eauto. } exists (rP ⋅ r); split; last by rewrite (left_id_L _ _) -(associative _). `````` Robbert Krebbers committed Feb 01, 2016 89 `````` eapply uPred_weaken with rP (S k); eauto using cmra_included_l. `````` Robbert Krebbers committed Jan 17, 2016 90 ``````Qed. `````` Ralf Jung committed Feb 09, 2016 91 ``````Lemma pvs_closeI i P : (ownI i P ∧ ▷ P) ⊑ pvs ∅ {[ i ]} True. `````` Robbert Krebbers committed Jan 17, 2016 92 93 94 ``````Proof. intros r [|n] ? [? HP] rf [|k] Ef σ ? HE ?; try lia; exists ∅; split; [done|]. rewrite (left_id _ _); apply wsat_close with P r. `````` Ralf Jung committed Feb 09, 2016 95 `````` * apply ownI_spec, uPred_weaken with r (S n); auto. `````` Robbert Krebbers committed Jan 17, 2016 96 97 98 99 `````` * solve_elem_of +HE. * by rewrite -(left_id_L ∅ (∪) Ef). * apply uPred_weaken with r n; auto. Qed. `````` Ralf Jung committed Feb 08, 2016 100 ``````Lemma pvs_ownG_updateP E m (P : iGst Λ Σ → Prop) : `````` Ralf Jung committed Feb 03, 2016 101 `````` m ~~>: P → ownG m ⊑ pvs E E (∃ m', ■ P m' ∧ ownG m'). `````` Robbert Krebbers committed Jan 17, 2016 102 ``````Proof. `````` Robbert Krebbers committed Feb 08, 2016 103 104 `````` intros Hup%option_updateP' r [|n] ? Hinv%ownG_spec rf [|k] Ef σ ???; try lia. destruct (wsat_update_gst k (E ∪ Ef) σ r rf (Some m) P) as (m'&?&?); eauto. `````` Robbert Krebbers committed Feb 04, 2016 105 `````` { apply cmra_includedN_le with (S n); auto. } `````` Robbert Krebbers committed Jan 17, 2016 106 107 `````` by exists (update_gst m' r); split; [exists m'; split; [|apply ownG_spec]|]. Qed. `````` Ralf Jung committed Feb 08, 2016 108 ``````Lemma pvs_ownG_updateP_empty `{Empty (iGst Λ Σ), !CMRAIdentity (iGst Λ Σ)} `````` Robbert Krebbers committed Feb 08, 2016 109 110 111 112 113 114 115 116 117 118 `````` E (P : iGst Λ Σ → Prop) : ∅ ~~>: P → True ⊑ pvs E E (∃ m', ■ P m' ∧ ownG m'). Proof. intros Hup r [|n] ? _ rf [|k] Ef σ ???; try lia. destruct (wsat_update_gst k (E ∪ Ef) σ r rf ∅ P) as (m'&?&?); eauto. { apply cmra_empty_leastN. } { apply cmra_updateP_compose_l with (Some ∅), option_updateP with P; auto using option_update_None. } by exists (update_gst m' r); split; [exists m'; split; [|apply ownG_spec]|]. Qed. `````` Ralf Jung committed Feb 09, 2016 119 ``````Lemma pvs_allocI E P : ¬set_finite E → ▷ P ⊑ pvs E E (∃ i, ■ (i ∈ E) ∧ ownI i P). `````` Robbert Krebbers committed Jan 17, 2016 120 121 122 123 124 125 126 127 ``````Proof. intros ? r [|n] ? HP rf [|k] Ef σ ???; try lia. destruct (wsat_alloc k E Ef σ rf P r) as (i&?&?&?); auto. { apply uPred_weaken with r n; eauto. } exists (Res {[ i ↦ to_agree (Later (iProp_unfold P)) ]} ∅ ∅). by split; [by exists i; split; rewrite /uPred_holds /=|]. Qed. `````` Robbert Krebbers committed Feb 09, 2016 128 ``````(** * Derived rules *) `````` Robbert Krebbers committed Feb 01, 2016 129 ``````Opaque uPred_holds. `````` Robbert Krebbers committed Jan 17, 2016 130 ``````Import uPred. `````` Robbert Krebbers committed Feb 01, 2016 131 ``````Global Instance pvs_mono' E1 E2 : Proper ((⊑) ==> (⊑)) (@pvs Λ Σ E1 E2). `````` Robbert Krebbers committed Jan 17, 2016 132 133 134 ``````Proof. intros P Q; apply pvs_mono. Qed. Lemma pvs_trans' E P : pvs E E (pvs E E P) ⊑ pvs E E P. Proof. apply pvs_trans; solve_elem_of. Qed. `````` Ralf Jung committed Feb 10, 2016 135 136 ``````Lemma pvs_strip_pvs E P Q : P ⊑ pvs E E Q → pvs E E P ⊑ pvs E E Q. Proof. move=>->. by rewrite pvs_trans'. Qed. `````` Robbert Krebbers committed Jan 17, 2016 137 138 ``````Lemma pvs_frame_l E1 E2 P Q : (P ★ pvs E1 E2 Q) ⊑ pvs E1 E2 (P ★ Q). Proof. rewrite !(commutative _ P); apply pvs_frame_r. Qed. `````` Robbert Krebbers committed Jan 18, 2016 139 140 141 142 143 144 ``````Lemma pvs_always_l E1 E2 P Q `{!AlwaysStable P} : (P ∧ pvs E1 E2 Q) ⊑ pvs E1 E2 (P ∧ Q). Proof. by rewrite !always_and_sep_l' pvs_frame_l. Qed. Lemma pvs_always_r E1 E2 P Q `{!AlwaysStable Q} : (pvs E1 E2 P ∧ Q) ⊑ pvs E1 E2 (P ∧ Q). Proof. by rewrite !always_and_sep_r' pvs_frame_r. Qed. `````` Robbert Krebbers committed Jan 17, 2016 145 146 147 148 ``````Lemma pvs_impl_l E1 E2 P Q : (□ (P → Q) ∧ pvs E1 E2 P) ⊑ pvs E1 E2 Q. Proof. by rewrite pvs_always_l always_elim impl_elim_l. Qed. Lemma pvs_impl_r E1 E2 P Q : (pvs E1 E2 P ∧ □ (P → Q)) ⊑ pvs E1 E2 Q. Proof. by rewrite (commutative _) pvs_impl_l. Qed. `````` Ralf Jung committed Feb 09, 2016 149 `````` `````` Ralf Jung committed Feb 09, 2016 150 151 152 ``````Lemma pvs_mask_frame' E1 E1' E2 E2' P : E1' ⊆ E1 → E2' ⊆ E2 → E1 ∖ E1' = E2 ∖ E2' → pvs E1' E2' P ⊑ pvs E1 E2 P. Proof. `````` Robbert Krebbers committed Feb 09, 2016 153 154 155 `````` intros HE1 HE2 HEE. rewrite (pvs_mask_frame _ _ (E1 ∖ E1')); last solve_elem_of. by rewrite {2}HEE -!union_difference_L. `````` Ralf Jung committed Feb 09, 2016 156 ``````Qed. `````` Ralf Jung committed Feb 09, 2016 157 158 159 160 161 162 `````` Lemma pvs_mask_frame_mono E1 E1' E2 E2' P Q : E1' ⊆ E1 → E2' ⊆ E2 → E1 ∖ E1' = E2 ∖ E2' → P ⊑ Q → pvs E1' E2' P ⊑ pvs E1 E2 Q. Proof. intros HE1 HE2 HEE ->. by apply pvs_mask_frame'. Qed. `````` Robbert Krebbers committed Feb 09, 2016 163 ``````(** It should be possible to give a stronger version of this rule `````` Ralf Jung committed Feb 09, 2016 164 165 `````` that does not force the conclusion view shift to have twice the same mask. However, even expressing the side-conditions on the `````` Robbert Krebbers committed Feb 09, 2016 166 `````` mask becomes really ugly then, and we have not found an instance `````` Ralf Jung committed Feb 09, 2016 167 `````` where that would be useful. *) `````` Ralf Jung committed Feb 09, 2016 168 169 ``````Lemma pvs_trans3 E1 E2 Q : E2 ⊆ E1 → pvs E1 E2 (pvs E2 E2 (pvs E2 E1 Q)) ⊑ pvs E1 E1 Q. `````` Robbert Krebbers committed Feb 09, 2016 170 ``````Proof. intros HE. rewrite !pvs_trans; solve_elem_of. Qed. `````` Ralf Jung committed Feb 09, 2016 171 `````` `````` Robbert Krebbers committed Jan 17, 2016 172 ``````Lemma pvs_mask_weaken E1 E2 P : E1 ⊆ E2 → pvs E1 E1 P ⊑ pvs E2 E2 P. `````` Robbert Krebbers committed Feb 09, 2016 173 ``````Proof. auto using pvs_mask_frame'. Qed. `````` Ralf Jung committed Feb 09, 2016 174 `````` `````` Ralf Jung committed Feb 08, 2016 175 ``````Lemma pvs_ownG_update E m m' : m ~~> m' → ownG m ⊑ pvs E E (ownG m'). `````` Robbert Krebbers committed Jan 17, 2016 176 ``````Proof. `````` Ralf Jung committed Feb 08, 2016 177 `````` intros; rewrite (pvs_ownG_updateP E _ (m' =)); last by apply cmra_update_updateP. `````` Robbert Krebbers committed Jan 17, 2016 178 179 `````` by apply pvs_mono, uPred.exist_elim=> m''; apply uPred.const_elim_l=> ->. Qed. `````` Ralf Jung committed Feb 09, 2016 180 `````` `````` Robbert Krebbers committed Jan 17, 2016 181 ``End pvs.``