counter_examples.v 8.9 KB
 Ralf Jung committed Aug 04, 2016 1 2 3 4 ``````From iris.algebra Require Import upred. From iris.proofmode Require Import tactics. (** This proves that we need the ▷ in a "Saved Proposition" construction with `````` Robbert Krebbers committed Aug 05, 2016 5 ``````name-dependend allocation. *) `````` Ralf Jung committed Aug 05, 2016 6 ``````Module savedprop. Section savedprop. `````` Ralf Jung committed Aug 04, 2016 7 8 `````` Context (M : ucmraT). Notation iProp := (uPred M). `````` Robbert Krebbers committed Aug 04, 2016 9 10 `````` Notation "¬ P" := (□ (P → False))%I : uPred_scope. Implicit Types P : iProp. `````` Ralf Jung committed Aug 04, 2016 11 `````` `````` Ralf Jung committed Aug 04, 2016 12 `````` (* Saved Propositions and view shifts. *) `````` Robbert Krebbers committed Aug 05, 2016 13 `````` Context (sprop : Type) (saved : sprop → iProp → iProp). `````` Robbert Krebbers committed Aug 04, 2016 14 `````` Hypothesis sprop_persistent : ∀ i P, PersistentP (saved i P). `````` Ralf Jung committed Aug 04, 2016 15 `````` Hypothesis sprop_alloc_dep : `````` Robbert Krebbers committed Aug 05, 2016 16 `````` ∀ (P : sprop → iProp), True =r=> (∃ i, saved i (P i)). `````` Robbert Krebbers committed Aug 04, 2016 17 `````` Hypothesis sprop_agree : ∀ i P Q, saved i P ∧ saved i Q ⊢ P ↔ Q. `````` Ralf Jung committed Aug 04, 2016 18 19 `````` (* Self-contradicting assertions are inconsistent *) `````` Robbert Krebbers committed Aug 04, 2016 20 `````` Lemma no_self_contradiction P `{!PersistentP P} : □ (P ↔ ¬ P) ⊢ False. `````` Robbert Krebbers committed Aug 04, 2016 21 22 `````` Proof. iIntros "#[H1 H2]". `````` Ralf Jung committed Aug 04, 2016 23 `````` iAssert P as "#HP". `````` Robbert Krebbers committed Aug 05, 2016 24 `````` { iApply "H2". iIntros "!# #HP". by iApply ("H1" with "[#]"). } `````` Robbert Krebbers committed Aug 04, 2016 25 `````` by iApply ("H1" with "[#]"). `````` Ralf Jung committed Aug 04, 2016 26 27 28 `````` Qed. (* "Assertion with name [i]" is equivalent to any assertion P s.t. [saved i P] *) `````` Robbert Krebbers committed Aug 04, 2016 29 30 `````` Definition A (i : sprop) : iProp := ∃ P, saved i P ★ □ P. Lemma saved_is_A i P `{!PersistentP P} : saved i P ⊢ □ (A i ↔ P). `````` Ralf Jung committed Aug 04, 2016 31 `````` Proof. `````` Robbert Krebbers committed Aug 05, 2016 32 `````` iIntros "#HS !#". iSplit. `````` Robbert Krebbers committed Aug 04, 2016 33 34 `````` - iDestruct 1 as (Q) "[#HSQ HQ]". iApply (sprop_agree i P Q with "[]"); eauto. `````` Ralf Jung committed Aug 04, 2016 35 36 37 38 39 40 `````` - iIntros "#HP". iExists P. by iSplit. Qed. (* Define [Q i] to be "negated assertion with name [i]". Show that this implies that assertion with name [i] is equivalent to its own negation. *) Definition Q i := saved i (¬ A i). `````` Robbert Krebbers committed Aug 04, 2016 41 `````` Lemma Q_self_contradiction i : Q i ⊢ □ (A i ↔ ¬ A i). `````` Robbert Krebbers committed Aug 05, 2016 42 `````` Proof. iIntros "#HQ !#". by iApply (saved_is_A i (¬A i)). Qed. `````` Ralf Jung committed Aug 04, 2016 43 44 `````` (* We can obtain such a [Q i]. *) `````` Robbert Krebbers committed Aug 05, 2016 45 `````` Lemma make_Q : True =r=> ∃ i, Q i. `````` Robbert Krebbers committed Aug 04, 2016 46 `````` Proof. apply sprop_alloc_dep. Qed. `````` Ralf Jung committed Aug 04, 2016 47 48 `````` (* Put together all the pieces to derive a contradiction. *) `````` Robbert Krebbers committed Aug 05, 2016 49 `````` Lemma rvs_false : (True : uPred M) =r=> False. `````` Ralf Jung committed Aug 04, 2016 50 `````` Proof. `````` Robbert Krebbers committed Aug 05, 2016 51 `````` rewrite make_Q. apply uPred.rvs_mono. iDestruct 1 as (i) "HQ". `````` Robbert Krebbers committed Aug 04, 2016 52 `````` iApply (no_self_contradiction (A i)). by iApply Q_self_contradiction. `````` Ralf Jung committed Aug 04, 2016 53 `````` Qed. `````` Robbert Krebbers committed Aug 05, 2016 54 55 56 57 58 59 `````` Lemma contradiction : False. Proof. apply (@uPred.adequacy M False 1); simpl. rewrite -uPred.later_intro. apply rvs_false. Qed. `````` Ralf Jung committed Aug 05, 2016 60 ``````End savedprop. End savedprop. `````` Ralf Jung committed Aug 05, 2016 61 62 63 `````` (** This proves that we need the ▷ when opening invariants. *) (** We fork in [uPred M] for any M, but the proof would work in any BI. *) `````` Ralf Jung committed Aug 05, 2016 64 ``````Module inv. Section inv. `````` Ralf Jung committed Aug 05, 2016 65 66 67 68 69 70 71 72 73 74 75 76 77 78 79 80 81 82 83 84 85 86 87 `````` Context (M : ucmraT). Notation iProp := (uPred M). Implicit Types P : iProp. (** Assumptions *) (* We have view shifts (two classes: empty/full mask) *) Context (pvs0 pvs1 : iProp → iProp). Hypothesis pvs0_intro : forall P, P ⊢ pvs0 P. Hypothesis pvs0_mono : forall P Q, (P ⊢ Q) → pvs0 P ⊢ pvs0 Q. Hypothesis pvs0_pvs0 : forall P, pvs0 (pvs0 P) ⊢ pvs0 P. Hypothesis pvs0_frame_l : forall P Q, P ★ pvs0 Q ⊢ pvs0 (P ★ Q). Hypothesis pvs1_mono : forall P Q, (P ⊢ Q) → pvs1 P ⊢ pvs1 Q. Hypothesis pvs1_pvs1 : forall P, pvs1 (pvs1 P) ⊢ pvs1 P. Hypothesis pvs1_frame_l : forall P Q, P ★ pvs1 Q ⊢ pvs1 (P ★ Q). Hypothesis pvs0_pvs1 : forall P, pvs0 P ⊢ pvs1 P. (* We have invariants *) Context (name : Type) (inv : name → iProp → iProp). Hypothesis inv_persistent : forall i P, PersistentP (inv i P). `````` Ralf Jung committed Aug 05, 2016 88 89 `````` Hypothesis inv_alloc : forall (P : iProp), P ⊢ pvs1 (∃ i, inv i P). `````` Ralf Jung committed Aug 05, 2016 90 91 92 `````` Hypothesis inv_open : forall i P Q R, (P ★ Q ⊢ pvs0 (P ★ R)) → (inv i P ★ Q ⊢ pvs1 R). `````` Ralf Jung committed Aug 05, 2016 93 94 95 96 97 98 99 100 101 102 103 104 `````` (* We have tokens for a little "two-state STS": [start] -> [finish]. state. [start] also asserts the exact state; it is only ever owned by the invariant. [finished] is duplicable. *) Context (gname : Type). Context (start finished : gname → iProp). Hypothesis sts_alloc : True ⊢ pvs0 (∃ γ, start γ). Hypotheses start_finish : forall γ, start γ ⊢ pvs0 (finished γ). Hypothesis finished_not_start : forall γ, start γ ★ finished γ ⊢ False. Hypothesis finished_dup : forall γ, finished γ ⊢ finished γ ★ finished γ. `````` Ralf Jung committed Aug 05, 2016 105 106 107 `````` (* We have that we cannot view shift from the initial state to false (because the initial state is actually achievable). *) `````` Ralf Jung committed Aug 05, 2016 108 `````` Hypothesis soundness : ¬ (True ⊢ pvs1 False). `````` Ralf Jung committed Aug 05, 2016 109 110 111 112 113 114 115 116 117 118 119 120 121 122 123 124 125 126 127 128 129 130 131 132 133 134 135 136 137 138 139 140 141 142 143 144 145 146 147 148 149 150 151 152 153 154 155 156 157 158 159 160 161 162 163 164 165 `````` (** Some general lemmas and proof mode compatibility. *) Lemma inv_open' i P R: inv i P ★ (P -★ pvs0 (P ★ pvs1 R)) ⊢ pvs1 R. Proof. iIntros "(#HiP & HP)". iApply pvs1_pvs1. iApply inv_open; last first. { iSplit; first done. iExact "HP". } iIntros "(HP & HPw)". by iApply "HPw". Qed. Lemma pvs1_intro P : P ⊢ pvs1 P. Proof. rewrite -pvs0_pvs1. apply pvs0_intro. Qed. Instance pvs0_mono' : Proper ((⊢) ==> (⊢)) pvs0. Proof. intros ?**. by apply pvs0_mono. Qed. Instance pvs0_proper : Proper ((⊣⊢) ==> (⊣⊢)) pvs0. Proof. intros P Q Heq. apply (anti_symm (⊢)); apply pvs0_mono; by rewrite ?Heq -?Heq. Qed. Instance pvs1_mono' : Proper ((⊢) ==> (⊢)) pvs1. Proof. intros ?**. by apply pvs1_mono. Qed. Instance pvs1_proper : Proper ((⊣⊢) ==> (⊣⊢)) pvs1. Proof. intros P Q Heq. apply (anti_symm (⊢)); apply pvs1_mono; by rewrite ?Heq -?Heq. Qed. Lemma pvs0_frame_r : forall P Q, (pvs0 P ★ Q) ⊢ pvs0 (P ★ Q). Proof. intros. rewrite comm pvs0_frame_l. apply pvs0_mono. by rewrite comm. Qed. Lemma pvs1_frame_r : forall P Q, (pvs1 P ★ Q) ⊢ pvs1 (P ★ Q). Proof. intros. rewrite comm pvs1_frame_l. apply pvs1_mono. by rewrite comm. Qed. Global Instance elim_pvs0_pvs0 P Q : ElimVs (pvs0 P) P (pvs0 Q) (pvs0 Q). Proof. rewrite /ElimVs. etrans; last eapply pvs0_pvs0. rewrite pvs0_frame_r. apply pvs0_mono. by rewrite uPred.wand_elim_r. Qed. Global Instance elim_pvs1_pvs1 P Q : ElimVs (pvs1 P) P (pvs1 Q) (pvs1 Q). Proof. rewrite /ElimVs. etrans; last eapply pvs1_pvs1. rewrite pvs1_frame_r. apply pvs1_mono. by rewrite uPred.wand_elim_r. Qed. Global Instance elim_pvs0_pvs1 P Q : ElimVs (pvs0 P) P (pvs1 Q) (pvs1 Q). Proof. rewrite /ElimVs. rewrite pvs0_pvs1. apply elim_pvs1_pvs1. Qed. `````` Ralf Jung committed Aug 05, 2016 166 167 168 169 170 171 172 173 174 175 176 177 178 179 `````` Global Instance exists_split_pvs0 {A} P (Φ : A → iProp) : FromExist P Φ → FromExist (pvs0 P) (λ a, pvs0 (Φ a)). Proof. rewrite /FromExist=>HP. apply uPred.exist_elim=> a. apply pvs0_mono. by rewrite -HP -(uPred.exist_intro a). Qed. Global Instance exists_split_pvs1 {A} P (Φ : A → iProp) : FromExist P Φ → FromExist (pvs1 P) (λ a, pvs1 (Φ a)). Proof. rewrite /FromExist=>HP. apply uPred.exist_elim=> a. apply pvs1_mono. by rewrite -HP -(uPred.exist_intro a). Qed. `````` Ralf Jung committed Aug 05, 2016 180 `````` (** Now to the actual counterexample. We start with a weird for of saved propositions. *) `````` Ralf Jung committed Aug 05, 2016 181 182 183 `````` Definition saved (γ : gname) (P : iProp) : iProp := ∃ i, inv i (start γ ∨ (finished γ ★ □P)). Global Instance : forall γ P, PersistentP (saved γ P) := _. `````` Ralf Jung committed Aug 05, 2016 184 `````` `````` Ralf Jung committed Aug 05, 2016 185 186 `````` Lemma saved_alloc (P : gname → iProp) : True ⊢ pvs1 (∃ γ, saved γ (P γ)). `````` Ralf Jung committed Aug 05, 2016 187 `````` Proof. `````` Ralf Jung committed Aug 05, 2016 188 189 `````` iIntros "". iVs (sts_alloc) as (γ) "Hs". iVs (inv_alloc (start γ ∨ (finished γ ★ □ (P γ))) with "[Hs]") as (i) "#Hi". `````` Ralf Jung committed Aug 05, 2016 190 `````` { iLeft. done. } `````` Ralf Jung committed Aug 05, 2016 191 `````` iApply pvs1_intro. iExists γ, i. done. `````` Ralf Jung committed Aug 05, 2016 192 193 `````` Qed. `````` Ralf Jung committed Aug 05, 2016 194 195 `````` Lemma saved_cast γ P Q : saved γ P ★ saved γ Q ★ □ P ⊢ pvs1 (□ Q). `````` Ralf Jung committed Aug 05, 2016 196 `````` Proof. `````` Ralf Jung committed Aug 05, 2016 197 `````` iIntros "(#HsP & #HsQ & #HP)". iDestruct "HsP" as (i) "HiP". `````` Ralf Jung committed Aug 05, 2016 198 199 `````` iApply (inv_open' i). iSplit; first done. (* Can I state a view-shift and immediately run it? *) `````` Ralf Jung committed Aug 05, 2016 200 201 202 203 204 205 206 207 208 209 210 211 212 213 `````` iIntros "HaP". iAssert (pvs0 (finished γ)) with "[HaP]" as "Hf". { iDestruct "HaP" as "[Hs | [Hf _]]". - by iApply start_finish. - by iApply pvs0_intro. } iVs "Hf" as "Hf". iDestruct (finished_dup with "Hf") as "[Hf Hf']". iApply pvs0_intro. iSplitL "Hf'"; first by eauto. (* Step 2: Open the Q-invariant. *) iClear "HiP". clear i. iDestruct "HsQ" as (i) "HiQ". iApply (inv_open' i). iSplit; first done. iIntros "[HaQ | [_ #HQ]]". { iExFalso. iApply finished_not_start. iSplitL "HaQ"; done. } iApply pvs0_intro. iSplitL "Hf". { iRight. by iSplitL "Hf". } by iApply pvs1_intro. `````` Ralf Jung committed Aug 05, 2016 214 215 `````` Qed. `````` Ralf Jung committed Aug 05, 2016 216 `````` (** And now we tie a bad knot. *) `````` Ralf Jung committed Aug 05, 2016 217 `````` Notation "¬ P" := (□ (P -★ pvs1 False))%I : uPred_scope. `````` Ralf Jung committed Aug 05, 2016 218 `````` Definition A i : iProp := ∃ P, ¬P ★ saved i P. `````` Ralf Jung committed Aug 05, 2016 219 `````` Global Instance : forall i, PersistentP (A i) := _. `````` Ralf Jung committed Aug 05, 2016 220 `````` `````` Ralf Jung committed Aug 05, 2016 221 `````` Lemma A_alloc : `````` Ralf Jung committed Aug 05, 2016 222 `````` True ⊢ pvs1 (∃ i, saved i (A i)). `````` Ralf Jung committed Aug 05, 2016 223 `````` Proof. by apply saved_alloc. Qed. `````` Ralf Jung committed Aug 05, 2016 224 `````` `````` Ralf Jung committed Aug 05, 2016 225 226 227 `````` Lemma alloc_NA i : saved i (A i) ⊢ (¬A i). Proof. `````` Ralf Jung committed Aug 05, 2016 228 229 230 231 232 `````` iIntros "#Hi !# #HA". iPoseProof "HA" as "HA'". iDestruct "HA'" as (P) "#[HNP Hi']". iVs ((saved_cast i) with "[]") as "HP". { iSplit; first iExact "Hi". iSplit; first iExact "Hi'". done. } by iApply "HNP". `````` Ralf Jung committed Aug 05, 2016 233 `````` Qed. `````` Ralf Jung committed Aug 05, 2016 234 `````` `````` Ralf Jung committed Aug 05, 2016 235 236 237 `````` Lemma alloc_A i : saved i (A i) ⊢ A i. Proof. `````` Ralf Jung committed Aug 05, 2016 238 239 `````` iIntros "#Hi". iPoseProof (alloc_NA with "Hi") as "HNA". iExists (A i). iSplit; done. `````` Ralf Jung committed Aug 05, 2016 240 `````` Qed. `````` Ralf Jung committed Aug 05, 2016 241 `````` `````` Ralf Jung committed Aug 05, 2016 242 243 `````` Lemma contradiction : False. Proof. `````` Ralf Jung committed Aug 05, 2016 244 245 `````` apply soundness. iIntros "". iVs A_alloc as (i) "#H". `````` Ralf Jung committed Aug 05, 2016 246 247 `````` iPoseProof (alloc_NA with "H") as "HN". iApply "HN". `````` Ralf Jung committed Aug 05, 2016 248 249 `````` iApply alloc_A. done. Qed. `````` Ralf Jung committed Aug 05, 2016 250 `````` `````` Ralf Jung committed Aug 05, 2016 251 ``End inv. End inv.``