pviewshifts.v 6.63 KB
 Robbert Krebbers committed Feb 04, 2016 1 2 ``````Require Export program_logic.ownership prelude.co_pset. Require Import program_logic.wsat. `````` Robbert Krebbers committed Jan 17, 2016 3 4 5 6 7 8 9 ``````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 10 ``````Program Definition pvs {Λ Σ} (E1 E2 : coPset) (P : iProp Λ Σ) : iProp Λ Σ := `````` Robbert Krebbers committed Jan 17, 2016 11 12 13 14 15 `````` {| 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 16 `````` intros Λ Σ E1 E2 P r1 r2 n HP Hr rf k Ef σ ?? Hwsat; simpl in *. `````` Robbert Krebbers committed Jan 17, 2016 17 18 `````` apply HP; auto. by rewrite (dist_le _ _ _ _ Hr); last lia. Qed. `````` Robbert Krebbers committed Feb 01, 2016 19 ``````Next Obligation. intros Λ Σ E1 E2 P r rf k Ef σ; simpl in *; lia. Qed. `````` Robbert Krebbers committed Jan 17, 2016 20 ``````Next Obligation. `````` Robbert Krebbers committed Feb 01, 2016 21 `````` intros Λ Σ E1 E2 P r1 r2 n1 n2 HP [r3 ?] Hn ? rf k Ef σ ?? Hws; setoid_subst. `````` Robbert Krebbers committed Jan 17, 2016 22 23 `````` 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 24 `````` apply uPred_weaken with r' k; eauto using cmra_included_l. `````` Robbert Krebbers committed Jan 17, 2016 25 ``````Qed. `````` Robbert Krebbers committed Feb 01, 2016 26 27 ``````Arguments pvs {_ _} _ _ _%I : simpl never. Instance: Params (@pvs) 4. `````` Robbert Krebbers committed Jan 17, 2016 28 29 `````` Section pvs. `````` Robbert Krebbers committed Feb 01, 2016 30 31 32 ``````Context {Λ : language} {Σ : iFunctor}. Implicit Types P Q : iProp Λ Σ. Implicit Types m : iGst Λ Σ. `````` Robbert Krebbers committed Jan 19, 2016 33 ``````Transparent uPred_holds. `````` Robbert Krebbers committed Jan 17, 2016 34 `````` `````` Robbert Krebbers committed Feb 01, 2016 35 ``````Global Instance pvs_ne E1 E2 n : Proper (dist n ==> dist n) (@pvs Λ Σ E1 E2). `````` Robbert Krebbers committed Jan 17, 2016 36 37 38 39 40 ``````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 41 ``````Global Instance pvs_proper E1 E2 : Proper ((≡) ==> (≡)) (@pvs Λ Σ E1 E2). `````` Robbert Krebbers committed Jan 17, 2016 42 43 44 45 46 47 48 49 50 51 52 53 54 55 56 57 ``````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 58 `````` apply HP, uPred_weaken with r n; eauto using cmra_validN_le. `````` Robbert Krebbers committed Jan 17, 2016 59 60 61 62 63 64 65 66 67 68 69 70 71 72 73 74 75 76 77 78 79 80 ``````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 08, 2016 81 ``````Lemma pvs_open i P : ownI i P ⊑ pvs {[ i ]} ∅ (▷ P). `````` Robbert Krebbers committed Jan 17, 2016 82 83 84 85 86 87 ``````Proof. intros r [|n] ? Hinv rf [|k] Ef σ ???; try lia. apply inv_spec in Hinv; last auto. 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 88 `````` eapply uPred_weaken with rP (S k); eauto using cmra_included_l. `````` Robbert Krebbers committed Jan 17, 2016 89 ``````Qed. `````` Ralf Jung committed Feb 08, 2016 90 ``````Lemma pvs_close i P : (ownI i P ∧ ▷ P) ⊑ pvs ∅ {[ i ]} True. `````` Robbert Krebbers committed Jan 17, 2016 91 92 93 94 95 96 97 98 ``````Proof. intros r [|n] ? [? HP] rf [|k] Ef σ ? HE ?; try lia; exists ∅; split; [done|]. rewrite (left_id _ _); apply wsat_close with P r. * apply inv_spec, uPred_weaken with r (S n); auto. * solve_elem_of +HE. * by rewrite -(left_id_L ∅ (∪) Ef). * apply uPred_weaken with r n; auto. Qed. `````` Robbert Krebbers committed Feb 01, 2016 99 ``````Lemma pvs_updateP E m (P : iGst Λ Σ → Prop) : `````` Ralf Jung committed Feb 03, 2016 100 `````` m ~~>: P → ownG m ⊑ pvs E E (∃ m', ■ P m' ∧ ownG m'). `````` Robbert Krebbers committed Jan 17, 2016 101 ``````Proof. `````` Robbert Krebbers committed Feb 08, 2016 102 103 `````` 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 104 `````` { apply cmra_includedN_le with (S n); auto. } `````` Robbert Krebbers committed Jan 17, 2016 105 106 `````` by exists (update_gst m' r); split; [exists m'; split; [|apply ownG_spec]|]. Qed. `````` Robbert Krebbers committed Feb 08, 2016 107 108 109 110 111 112 113 114 115 116 117 ``````Lemma pvs_updateP_empty `{Empty (iGst Λ Σ), !CMRAIdentity (iGst Λ Σ)} 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 08, 2016 118 ``````Lemma pvs_alloc E P : ¬set_finite E → ▷ P ⊑ pvs E E (∃ i, ■ (i ∈ E) ∧ ownI i P). `````` Robbert Krebbers committed Jan 17, 2016 119 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. (* Derived rules *) `````` Robbert Krebbers committed Feb 01, 2016 128 ``````Opaque uPred_holds. `````` Robbert Krebbers committed Jan 17, 2016 129 ``````Import uPred. `````` Robbert Krebbers committed Feb 01, 2016 130 ``````Global Instance pvs_mono' E1 E2 : Proper ((⊑) ==> (⊑)) (@pvs Λ Σ E1 E2). `````` Robbert Krebbers committed Jan 17, 2016 131 132 133 134 135 ``````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. 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 136 137 138 139 140 141 ``````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 142 143 144 145 146 147 148 149 ``````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. 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. `````` Ralf Jung committed Feb 03, 2016 150 ``````Lemma pvs_update E m m' : m ~~> m' → ownG m ⊑ pvs E E (ownG m'). `````` Robbert Krebbers committed Jan 17, 2016 151 ``````Proof. `````` Robbert Krebbers committed Feb 08, 2016 152 `````` intros; rewrite (pvs_updateP E _ (m' =)); last by apply cmra_update_updateP. `````` Robbert Krebbers committed Jan 17, 2016 153 154 155 `````` by apply pvs_mono, uPred.exist_elim=> m''; apply uPred.const_elim_l=> ->. Qed. End pvs.``````