counter_examples.v 7.73 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 `````` Context (M : ucmraT). Notation iProp := (uPred M). Implicit Types P : iProp. (** Assumptions *) (* We have view shifts (two classes: empty/full mask) *) `````` Robbert Krebbers committed Aug 05, 2016 71 72 `````` Inductive mask := M0 | M1. Context (pvs : mask → iProp → iProp). `````` Ralf Jung committed Aug 05, 2016 73 `````` `````` Robbert Krebbers committed Aug 05, 2016 74 75 76 77 78 `````` Hypothesis pvs_intro : ∀ E P, P ⊢ pvs E P. Hypothesis pvs_mono : ∀ E P Q, (P ⊢ Q) → pvs E P ⊢ pvs E Q. Hypothesis pvs_pvs : ∀ E P, pvs E (pvs E P) ⊢ pvs E P. Hypothesis pvs_frame_l : ∀ E P Q, P ★ pvs E Q ⊢ pvs E (P ★ Q). Hypothesis pvs_mask_mono : ∀ P, pvs M0 P ⊢ pvs M1 P. `````` Ralf Jung committed Aug 05, 2016 79 80 81 `````` (* We have invariants *) Context (name : Type) (inv : name → iProp → iProp). `````` Robbert Krebbers committed Aug 05, 2016 82 `````` Hypothesis inv_persistent : ∀ i P, PersistentP (inv i P). `````` Robbert Krebbers committed Aug 05, 2016 83 `````` Hypothesis inv_alloc : ∀ P, P ⊢ pvs M1 (∃ i, inv i P). `````` Ralf Jung committed Aug 05, 2016 84 `````` Hypothesis inv_open : `````` Robbert Krebbers committed Aug 05, 2016 85 `````` ∀ i P Q R, (P ★ Q ⊢ pvs M0 (P ★ R)) → (inv i P ★ Q ⊢ pvs M1 R). `````` Ralf Jung committed Aug 05, 2016 86 `````` `````` Ralf Jung committed Aug 05, 2016 87 88 89 `````` (* 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. *) `````` Ralf Jung committed Aug 08, 2016 90 91 92 93 94 95 `````` (* Posssible implementations of these axioms: * Using the STS monoid of a two-state STS, where [start] is the authoritative saying the state is exactly [start], and [finish] is the "we are at least in state [finish]" typically owned by threads. * Ex () +_⊥ () *) `````` Ralf Jung committed Aug 05, 2016 96 97 98 `````` Context (gname : Type). Context (start finished : gname → iProp). `````` Robbert Krebbers committed Aug 05, 2016 99 100 `````` Hypothesis sts_alloc : True ⊢ pvs M0 (∃ γ, start γ). Hypotheses start_finish : ∀ γ, start γ ⊢ pvs M0 (finished γ). `````` Ralf Jung committed Aug 05, 2016 101 `````` `````` Robbert Krebbers committed Aug 05, 2016 102 `````` Hypothesis finished_not_start : ∀ γ, start γ ★ finished γ ⊢ False. `````` Ralf Jung committed Aug 05, 2016 103 `````` `````` Robbert Krebbers committed Aug 05, 2016 104 `````` Hypothesis finished_dup : ∀ γ, finished γ ⊢ finished γ ★ finished γ. `````` Ralf Jung committed Aug 05, 2016 105 `````` `````` Ralf Jung committed Aug 05, 2016 106 `````` (* We assume that we cannot view shift to false. *) `````` Robbert Krebbers committed Aug 05, 2016 107 `````` Hypothesis soundness : ¬ (True ⊢ pvs M1 False). `````` Ralf Jung committed Aug 05, 2016 108 109 `````` (** Some general lemmas and proof mode compatibility. *) `````` Robbert Krebbers committed Aug 05, 2016 110 `````` Lemma inv_open' i P R : inv i P ★ (P -★ pvs M0 (P ★ pvs M1 R)) ⊢ pvs M1 R. `````` Ralf Jung committed Aug 05, 2016 111 `````` Proof. `````` Robbert Krebbers committed Aug 05, 2016 112 `````` iIntros "(#HiP & HP)". iApply pvs_pvs. iApply inv_open; last first. `````` Ralf Jung committed Aug 05, 2016 113 114 115 116 `````` { iSplit; first done. iExact "HP". } iIntros "(HP & HPw)". by iApply "HPw". Qed. `````` Robbert Krebbers committed Aug 05, 2016 117 118 119 `````` Instance pvs_mono' E : Proper ((⊢) ==> (⊢)) (pvs E). Proof. intros P Q ?. by apply pvs_mono. Qed. Instance pvs_proper E : Proper ((⊣⊢) ==> (⊣⊢)) (pvs E). `````` Ralf Jung committed Aug 05, 2016 120 `````` Proof. `````` Robbert Krebbers committed Aug 05, 2016 121 `````` intros P Q; rewrite !uPred.equiv_spec=> -[??]; split; by apply pvs_mono. `````` Ralf Jung committed Aug 05, 2016 122 123 `````` Qed. `````` Robbert Krebbers committed Aug 05, 2016 124 125 `````` Lemma pvs_frame_r E P Q : (pvs E P ★ Q) ⊢ pvs E (P ★ Q). Proof. by rewrite comm pvs_frame_l comm. Qed. `````` Ralf Jung committed Aug 05, 2016 126 `````` `````` Robbert Krebbers committed Aug 05, 2016 127 128 `````` Global Instance elim_pvs_pvs E P Q : ElimVs (pvs E P) P (pvs E Q) (pvs E Q). Proof. by rewrite /ElimVs pvs_frame_r uPred.wand_elim_r pvs_pvs. Qed. `````` Ralf Jung committed Aug 05, 2016 129 `````` `````` Robbert Krebbers committed Aug 05, 2016 130 `````` Global Instance elim_pvs0_pvs1 P Q : ElimVs (pvs M0 P) P (pvs M1 Q) (pvs M1 Q). `````` Ralf Jung committed Aug 05, 2016 131 `````` Proof. `````` Robbert Krebbers committed Aug 05, 2016 132 `````` by rewrite /ElimVs pvs_frame_r uPred.wand_elim_r pvs_mask_mono pvs_pvs. `````` Ralf Jung committed Aug 05, 2016 133 134 `````` Qed. `````` Robbert Krebbers committed Aug 05, 2016 135 136 `````` Global Instance exists_split_pvs0 {A} E P (Φ : A → iProp) : FromExist P Φ → FromExist (pvs E P) (λ a, pvs E (Φ a)). `````` Ralf Jung committed Aug 05, 2016 137 138 `````` Proof. rewrite /FromExist=>HP. apply uPred.exist_elim=> a. `````` Robbert Krebbers committed Aug 05, 2016 139 `````` apply pvs_mono. by rewrite -HP -(uPred.exist_intro a). `````` Ralf Jung committed Aug 05, 2016 140 141 `````` Qed. `````` Ralf Jung committed Aug 05, 2016 142 `````` (** Now to the actual counterexample. We start with a weird for of saved propositions. *) `````` Ralf Jung committed Aug 05, 2016 143 `````` Definition saved (γ : gname) (P : iProp) : iProp := `````` Robbert Krebbers committed Aug 05, 2016 144 145 `````` ∃ i, inv i (start γ ∨ (finished γ ★ □ P)). Global Instance saved_persistent γ P : PersistentP (saved γ P) := _. `````` Ralf Jung committed Aug 05, 2016 146 `````` `````` Robbert Krebbers committed Aug 05, 2016 147 `````` Lemma saved_alloc (P : gname → iProp) : True ⊢ pvs M1 (∃ γ, saved γ (P γ)). `````` Ralf Jung committed Aug 05, 2016 148 `````` Proof. `````` Ralf Jung committed Aug 05, 2016 149 150 `````` iIntros "". iVs (sts_alloc) as (γ) "Hs". iVs (inv_alloc (start γ ∨ (finished γ ★ □ (P γ))) with "[Hs]") as (i) "#Hi". `````` Robbert Krebbers committed Aug 05, 2016 151 152 `````` { auto. } iApply pvs_intro. by iExists γ, i. `````` Ralf Jung committed Aug 05, 2016 153 154 `````` Qed. `````` Robbert Krebbers committed Aug 05, 2016 155 `````` Lemma saved_cast γ P Q : saved γ P ★ saved γ Q ★ □ P ⊢ pvs M1 (□ Q). `````` Ralf Jung committed Aug 05, 2016 156 `````` Proof. `````` Ralf Jung committed Aug 05, 2016 157 `````` iIntros "(#HsP & #HsQ & #HP)". iDestruct "HsP" as (i) "HiP". `````` Ralf Jung committed Aug 05, 2016 158 `````` iApply (inv_open' i). iSplit; first done. `````` Robbert Krebbers committed Aug 08, 2016 159 `````` iIntros "HaP". iAssert (pvs M0 (finished γ)) with "[HaP]" as "==> Hf". `````` Ralf Jung committed Aug 05, 2016 160 161 `````` { iDestruct "HaP" as "[Hs | [Hf _]]". - by iApply start_finish. `````` Robbert Krebbers committed Aug 05, 2016 162 `````` - by iApply pvs_intro. } `````` Robbert Krebbers committed Aug 08, 2016 163 `````` iDestruct (finished_dup with "Hf") as "[Hf Hf']". `````` Robbert Krebbers committed Aug 05, 2016 164 `````` iApply pvs_intro. iSplitL "Hf'"; first by eauto. `````` Ralf Jung committed Aug 05, 2016 165 166 167 168 `````` (* 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]]". `````` Robbert Krebbers committed Aug 05, 2016 169 170 171 172 `````` { iExFalso. iApply finished_not_start. by iFrame. } iApply pvs_intro. iSplitL "Hf". { iRight. by iFrame. } by iApply pvs_intro. `````` Ralf Jung committed Aug 05, 2016 173 174 `````` Qed. `````` Ralf Jung committed Aug 05, 2016 175 `````` (** And now we tie a bad knot. *) `````` Robbert Krebbers committed Aug 05, 2016 176 `````` Notation "¬ P" := (□ (P -★ pvs M1 False))%I : uPred_scope. `````` Ralf Jung committed Aug 05, 2016 177 `````` Definition A i : iProp := ∃ P, ¬P ★ saved i P. `````` Robbert Krebbers committed Aug 05, 2016 178 `````` Global Instance A_persistent i : PersistentP (A i) := _. `````` Ralf Jung committed Aug 05, 2016 179 `````` `````` Robbert Krebbers committed Aug 05, 2016 180 `````` Lemma A_alloc : True ⊢ pvs M1 (∃ i, saved i (A i)). `````` Ralf Jung committed Aug 05, 2016 181 `````` Proof. by apply saved_alloc. Qed. `````` Ralf Jung committed Aug 05, 2016 182 `````` `````` Robbert Krebbers committed Aug 05, 2016 183 `````` Lemma alloc_NA i : saved i (A i) ⊢ ¬A i. `````` Ralf Jung committed Aug 05, 2016 184 `````` Proof. `````` Ralf Jung committed Aug 05, 2016 185 186 `````` iIntros "#Hi !# #HA". iPoseProof "HA" as "HA'". iDestruct "HA'" as (P) "#[HNP Hi']". `````` Robbert Krebbers committed Aug 05, 2016 187 188 `````` iVs (saved_cast i with "[]") as "HP". { iSplit; first iExact "Hi". by iFrame "#". } `````` Ralf Jung committed Aug 05, 2016 189 `````` by iApply "HNP". `````` Ralf Jung committed Aug 05, 2016 190 `````` Qed. `````` Ralf Jung committed Aug 05, 2016 191 `````` `````` Robbert Krebbers committed Aug 05, 2016 192 `````` Lemma alloc_A i : saved i (A i) ⊢ A i. `````` Ralf Jung committed Aug 05, 2016 193 `````` Proof. `````` Ralf Jung committed Aug 05, 2016 194 `````` iIntros "#Hi". iPoseProof (alloc_NA with "Hi") as "HNA". `````` Robbert Krebbers committed Aug 05, 2016 195 `````` iExists (A i). by iFrame "#". `````` Ralf Jung committed Aug 05, 2016 196 `````` Qed. `````` Ralf Jung committed Aug 05, 2016 197 `````` `````` Ralf Jung committed Aug 05, 2016 198 199 `````` Lemma contradiction : False. Proof. `````` Ralf Jung committed Aug 05, 2016 200 201 `````` apply soundness. iIntros "". iVs A_alloc as (i) "#H". `````` Ralf Jung committed Aug 05, 2016 202 `````` iPoseProof (alloc_NA with "H") as "HN". `````` Robbert Krebbers committed Aug 05, 2016 203 `````` iApply "HN". iApply alloc_A. done. `````` Ralf Jung committed Aug 05, 2016 204 205 `````` Qed. End inv. End inv.``````