counterexamples.v 7.81 KB
 Robbert Krebbers committed Oct 30, 2017 1 ``````From iris.bi Require Export bi. `````` Ralf Jung committed Aug 04, 2016 2 ``````From iris.proofmode Require Import tactics. `````` Ralf Jung committed Jan 05, 2017 3 ``````Set Default Proof Using "Type*". `````` Ralf Jung committed Aug 04, 2016 4 5 `````` (** This proves that we need the ▷ in a "Saved Proposition" construction with `````` Derek Dreyer committed Aug 08, 2016 6 ``````name-dependent allocation. *) `````` Ralf Jung committed Aug 05, 2016 7 ``````Module savedprop. Section savedprop. `````` Jacques-Henri Jourdan committed Dec 04, 2017 8 `````` Context `{BiAffine PROP}. `````` Robbert Krebbers committed Oct 30, 2017 9 `````` Notation "¬ P" := (□ (P → False))%I : bi_scope. `````` Robbert Krebbers committed Oct 30, 2017 10 `````` Implicit Types P : PROP. `````` Ralf Jung committed Aug 04, 2016 11 `````` `````` Robbert Krebbers committed Oct 30, 2017 12 13 14 15 16 17 18 19 20 21 `````` Context (bupd : PROP → PROP). Notation "|==> Q" := (bupd Q) (at level 99, Q at level 200, format "|==> Q") : bi_scope. Hypothesis bupd_intro : ∀ P, P ⊢ |==> P. Hypothesis bupd_mono : ∀ P Q, (P ⊢ Q) → (|==> P) ⊢ |==> Q. Hypothesis bupd_trans : ∀ P, (|==> |==> P) ⊢ |==> P. Hypothesis bupd_frame_r : ∀ P R, (|==> P) ∗ R ⊢ |==> (P ∗ R). Context (ident : Type) (saved : ident → PROP → PROP). `````` Robbert Krebbers committed Oct 25, 2017 22 `````` Hypothesis sprop_persistent : ∀ i P, Persistent (saved i P). `````` Ralf Jung committed Aug 04, 2016 23 `````` Hypothesis sprop_alloc_dep : `````` Robbert Krebbers committed Oct 30, 2017 24 `````` ∀ (P : ident → PROP), (|==> ∃ i, saved i (P i))%I. `````` Ralf Jung committed Aug 08, 2016 25 `````` Hypothesis sprop_agree : ∀ i P Q, saved i P ∧ saved i Q ⊢ □ (P ↔ Q). `````` Ralf Jung committed Aug 04, 2016 26 `````` `````` Robbert Krebbers committed Oct 30, 2017 27 28 29 30 31 `````` (** We assume that we cannot update to false. *) Hypothesis consistency : ¬(|==> False)%I. Instance bupd_mono' : Proper ((⊢) ==> (⊢)) bupd. Proof. intros P Q ?. by apply bupd_mono. Qed. `````` Robbert Krebbers committed Apr 04, 2018 32 33 34 35 36 `````` Instance elim_modal_bupd p P Q : ElimModal True p false (|==> P) P (|==> Q) (|==> Q). Proof. by rewrite /ElimModal bi.intuitionistically_if_elim bupd_frame_r bi.wand_elim_r bupd_trans. Qed. `````` Robbert Krebbers committed Oct 30, 2017 37 `````` `````` Ralf Jung committed Aug 08, 2016 38 `````` (** A bad recursive reference: "Assertion with name [i] does not hold" *) `````` Robbert Krebbers committed Oct 30, 2017 39 `````` Definition A (i : ident) : PROP := (∃ P, ¬ P ∗ saved i P)%I. `````` Ralf Jung committed Aug 08, 2016 40 `````` `````` 41 `````` Lemma A_alloc : (|==> ∃ i, saved i (A i))%I. `````` Ralf Jung committed Aug 08, 2016 42 `````` Proof. by apply sprop_alloc_dep. Qed. `````` Ralf Jung committed Aug 04, 2016 43 `````` `````` Ralf Jung committed Aug 08, 2016 44 `````` Lemma saved_NA i : saved i (A i) ⊢ ¬ A i. `````` Ralf Jung committed Aug 04, 2016 45 `````` Proof. `````` Ralf Jung committed Aug 08, 2016 46 47 48 49 50 `````` iIntros "#Hs !# #HA". iPoseProof "HA" as "HA'". iDestruct "HA'" as (P) "[#HNP HsP]". iApply "HNP". iDestruct (sprop_agree i P (A i) with "[]") as "#[_ HP]". { eauto. } iApply "HP". done. `````` Ralf Jung committed Aug 04, 2016 51 52 `````` Qed. `````` Ralf Jung committed Aug 08, 2016 53 `````` Lemma saved_A i : saved i (A i) ⊢ A i. `````` Ralf Jung committed Aug 04, 2016 54 `````` Proof. `````` Ralf Jung committed Aug 08, 2016 55 56 `````` iIntros "#Hs". iExists (A i). iFrame "#". by iApply saved_NA. `````` Ralf Jung committed Aug 04, 2016 57 `````` Qed. `````` Robbert Krebbers committed Aug 05, 2016 58 59 `````` Lemma contradiction : False. `````` Ralf Jung committed Jan 05, 2017 60 `````` Proof using All. `````` Robbert Krebbers committed Oct 30, 2017 61 `````` apply consistency. `````` Robbert Krebbers committed Oct 30, 2017 62 `````` iMod A_alloc as (i) "#H". `````` Ralf Jung committed Aug 08, 2016 63 `````` iPoseProof (saved_NA with "H") as "HN". `````` Robbert Krebbers committed Oct 30, 2017 64 `````` iApply bupd_intro. iApply "HN". iApply saved_A. done. `````` Robbert Krebbers committed Aug 05, 2016 65 `````` Qed. `````` Ralf Jung committed Aug 05, 2016 66 ``````End savedprop. End savedprop. `````` Ralf Jung committed Aug 05, 2016 67 `````` `````` Robbert Krebbers committed Oct 30, 2017 68 `````` `````` Ralf Jung committed Aug 05, 2016 69 ``````(** This proves that we need the ▷ when opening invariants. *) `````` Ralf Jung committed Aug 05, 2016 70 ``````Module inv. Section inv. `````` Jacques-Henri Jourdan committed Dec 04, 2017 71 `````` Context `{BiAffine PROP}. `````` Robbert Krebbers committed Oct 30, 2017 72 `````` Implicit Types P : PROP. `````` Ralf Jung committed Aug 05, 2016 73 74 `````` (** Assumptions *) `````` Robbert Krebbers committed Oct 25, 2016 75 `````` (** We have the update modality (two classes: empty/full mask) *) `````` Robbert Krebbers committed Aug 05, 2016 76 `````` Inductive mask := M0 | M1. `````` Robbert Krebbers committed Oct 30, 2017 77 78 `````` Context (fupd : mask → PROP → PROP). Arguments fupd _ _%I. `````` Robbert Krebbers committed Oct 25, 2016 79 80 81 `````` Hypothesis fupd_intro : ∀ E P, P ⊢ fupd E P. Hypothesis fupd_mono : ∀ E P Q, (P ⊢ Q) → fupd E P ⊢ fupd E Q. Hypothesis fupd_fupd : ∀ E P, fupd E (fupd E P) ⊢ fupd E P. `````` Robbert Krebbers committed Nov 03, 2016 82 `````` Hypothesis fupd_frame_l : ∀ E P Q, P ∗ fupd E Q ⊢ fupd E (P ∗ Q). `````` Robbert Krebbers committed Oct 25, 2016 83 `````` Hypothesis fupd_mask_mono : ∀ P, fupd M0 P ⊢ fupd M1 P. `````` Ralf Jung committed Aug 05, 2016 84 `````` `````` Robbert Krebbers committed Oct 25, 2016 85 `````` (** We have invariants *) `````` Robbert Krebbers committed Oct 30, 2017 86 87 `````` Context (name : Type) (inv : name → PROP → PROP). Arguments inv _ _%I. `````` Robbert Krebbers committed Oct 25, 2017 88 `````` Hypothesis inv_persistent : ∀ i P, Persistent (inv i P). `````` Robbert Krebbers committed Oct 25, 2016 89 `````` Hypothesis inv_alloc : ∀ P, P ⊢ fupd M1 (∃ i, inv i P). `````` Ralf Jung committed Aug 05, 2016 90 `````` Hypothesis inv_open : `````` Robbert Krebbers committed Nov 03, 2016 91 `````` ∀ i P Q R, (P ∗ Q ⊢ fupd M0 (P ∗ R)) → (inv i P ∗ Q ⊢ fupd M1 R). `````` Ralf Jung committed Aug 05, 2016 92 `````` `````` Ralf Jung committed Aug 05, 2016 93 94 95 `````` (* 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 96 97 98 99 `````` (* 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. `````` 100 `````` * Ex () +_## () `````` Ralf Jung committed Aug 08, 2016 101 `````` *) `````` Ralf Jung committed Aug 05, 2016 102 `````` Context (gname : Type). `````` Robbert Krebbers committed Oct 30, 2017 103 `````` Context (start finished : gname → PROP). `````` Ralf Jung committed Aug 05, 2016 104 `````` `````` 105 `````` Hypothesis sts_alloc : fupd M0 (∃ γ, start γ). `````` Robbert Krebbers committed Oct 25, 2016 106 `````` Hypotheses start_finish : ∀ γ, start γ ⊢ fupd M0 (finished γ). `````` Ralf Jung committed Aug 05, 2016 107 `````` `````` Robbert Krebbers committed Nov 03, 2016 108 `````` Hypothesis finished_not_start : ∀ γ, start γ ∗ finished γ ⊢ False. `````` Ralf Jung committed Aug 05, 2016 109 `````` `````` Robbert Krebbers committed Nov 03, 2016 110 `````` Hypothesis finished_dup : ∀ γ, finished γ ⊢ finished γ ∗ finished γ. `````` Ralf Jung committed Aug 05, 2016 111 `````` `````` Robbert Krebbers committed Oct 25, 2016 112 `````` (** We assume that we cannot update to false. *) `````` 113 `````` Hypothesis consistency : ¬ (fupd M1 False). `````` Ralf Jung committed Aug 05, 2016 114 115 `````` (** Some general lemmas and proof mode compatibility. *) `````` Robbert Krebbers committed Nov 03, 2016 116 `````` Lemma inv_open' i P R : inv i P ∗ (P -∗ fupd M0 (P ∗ fupd M1 R)) ⊢ fupd M1 R. `````` Ralf Jung committed Aug 05, 2016 117 `````` Proof. `````` Robbert Krebbers committed Oct 25, 2016 118 `````` iIntros "(#HiP & HP)". iApply fupd_fupd. iApply inv_open; last first. `````` Ralf Jung committed Aug 05, 2016 119 120 121 122 `````` { iSplit; first done. iExact "HP". } iIntros "(HP & HPw)". by iApply "HPw". Qed. `````` Robbert Krebbers committed Oct 25, 2016 123 124 125 `````` Instance fupd_mono' E : Proper ((⊢) ==> (⊢)) (fupd E). Proof. intros P Q ?. by apply fupd_mono. Qed. Instance fupd_proper E : Proper ((⊣⊢) ==> (⊣⊢)) (fupd E). `````` Ralf Jung committed Aug 05, 2016 126 `````` Proof. `````` Robbert Krebbers committed Oct 30, 2017 127 `````` intros P Q; rewrite !bi.equiv_spec=> -[??]; split; by apply fupd_mono. `````` Ralf Jung committed Aug 05, 2016 128 129 `````` Qed. `````` 130 `````` Lemma fupd_frame_r E P Q : fupd E P ∗ Q ⊢ fupd E (P ∗ Q). `````` Robbert Krebbers committed Oct 25, 2016 131 `````` Proof. by rewrite comm fupd_frame_l comm. Qed. `````` Ralf Jung committed Aug 05, 2016 132 `````` `````` Robbert Krebbers committed Apr 04, 2018 133 134 135 136 137 138 `````` Global Instance elim_fupd_fupd p E P Q : ElimModal True p false (fupd E P) P (fupd E Q) (fupd E Q). Proof. by rewrite /ElimModal bi.intuitionistically_if_elim fupd_frame_r bi.wand_elim_r fupd_fupd. Qed. `````` Ralf Jung committed Aug 05, 2016 139 `````` `````` Robbert Krebbers committed Apr 04, 2018 140 141 `````` Global Instance elim_fupd0_fupd1 p P Q : ElimModal True p false (fupd M0 P) P (fupd M1 Q) (fupd M1 Q). `````` Ralf Jung committed Aug 05, 2016 142 `````` Proof. `````` Robbert Krebbers committed Apr 04, 2018 143 144 `````` by rewrite /ElimModal bi.intuitionistically_if_elim fupd_frame_r bi.wand_elim_r fupd_mask_mono fupd_fupd. `````` Ralf Jung committed Aug 05, 2016 145 146 `````` Qed. `````` Robbert Krebbers committed Oct 30, 2017 147 `````` Global Instance exists_split_fupd0 {A} E P (Φ : A → PROP) : `````` Robbert Krebbers committed Oct 25, 2016 148 `````` FromExist P Φ → FromExist (fupd E P) (λ a, fupd E (Φ a)). `````` Ralf Jung committed Aug 05, 2016 149 `````` Proof. `````` Robbert Krebbers committed Oct 30, 2017 150 151 `````` rewrite /FromExist=>HP. apply bi.exist_elim=> a. apply fupd_mono. by rewrite -HP -(bi.exist_intro a). `````` Ralf Jung committed Aug 05, 2016 152 153 `````` Qed. `````` Derek Dreyer committed Aug 08, 2016 154 `````` (** Now to the actual counterexample. We start with a weird form of saved propositions. *) `````` Robbert Krebbers committed Oct 30, 2017 155 156 `````` Definition saved (γ : gname) (P : PROP) : PROP := (∃ i, inv i (start γ ∨ (finished γ ∗ □ P)))%I. `````` Robbert Krebbers committed Oct 25, 2017 157 `````` Global Instance saved_persistent γ P : Persistent (saved γ P) := _. `````` Ralf Jung committed Aug 05, 2016 158 `````` `````` Robbert Krebbers committed Oct 30, 2017 159 `````` Lemma saved_alloc (P : gname → PROP) : fupd M1 (∃ γ, saved γ (P γ)). `````` Ralf Jung committed Aug 05, 2016 160 `````` Proof. `````` Robbert Krebbers committed Oct 25, 2016 161 `````` iIntros "". iMod (sts_alloc) as (γ) "Hs". `````` Robbert Krebbers committed Oct 30, 2017 162 `````` iMod (inv_alloc (start γ ∨ (finished γ ∗ □ (P γ)))%I with "[Hs]") as (i) "#Hi". `````` Robbert Krebbers committed Aug 05, 2016 163 `````` { auto. } `````` Robbert Krebbers committed Oct 25, 2016 164 `````` iApply fupd_intro. by iExists γ, i. `````` Ralf Jung committed Aug 05, 2016 165 166 `````` Qed. `````` Robbert Krebbers committed Nov 03, 2016 167 `````` Lemma saved_cast γ P Q : saved γ P ∗ saved γ Q ∗ □ P ⊢ fupd M1 (□ Q). `````` Ralf Jung committed Aug 05, 2016 168 `````` Proof. `````` Ralf Jung committed Aug 05, 2016 169 `````` iIntros "(#HsP & #HsQ & #HP)". iDestruct "HsP" as (i) "HiP". `````` Ralf Jung committed Aug 05, 2016 170 `````` iApply (inv_open' i). iSplit; first done. `````` Robbert Krebbers committed Oct 25, 2016 171 `````` iIntros "HaP". iAssert (fupd M0 (finished γ)) with "[HaP]" as "> Hf". `````` Ralf Jung committed Aug 05, 2016 172 173 `````` { iDestruct "HaP" as "[Hs | [Hf _]]". - by iApply start_finish. `````` Robbert Krebbers committed Oct 25, 2016 174 `````` - by iApply fupd_intro. } `````` Robbert Krebbers committed Aug 08, 2016 175 `````` iDestruct (finished_dup with "Hf") as "[Hf Hf']". `````` Robbert Krebbers committed Oct 25, 2016 176 `````` iApply fupd_intro. iSplitL "Hf'"; first by eauto. `````` Ralf Jung committed Aug 05, 2016 177 `````` (* Step 2: Open the Q-invariant. *) `````` Robbert Krebbers committed Sep 27, 2016 178 `````` iClear (i) "HiP ". iDestruct "HsQ" as (i) "HiQ". `````` Ralf Jung committed Aug 05, 2016 179 180 `````` iApply (inv_open' i). iSplit; first done. iIntros "[HaQ | [_ #HQ]]". `````` Robbert Krebbers committed Aug 05, 2016 181 `````` { iExFalso. iApply finished_not_start. by iFrame. } `````` Robbert Krebbers committed Oct 25, 2016 182 `````` iApply fupd_intro. iSplitL "Hf". `````` Robbert Krebbers committed Aug 05, 2016 183 `````` { iRight. by iFrame. } `````` Robbert Krebbers committed Oct 25, 2016 184 `````` by iApply fupd_intro. `````` Ralf Jung committed Aug 05, 2016 185 186 `````` Qed. `````` Ralf Jung committed Aug 05, 2016 187 `````` (** And now we tie a bad knot. *) `````` Robbert Krebbers committed Oct 30, 2017 188 `````` Notation "¬ P" := (□ (P -∗ fupd M1 False))%I : bi_scope. `````` Robbert Krebbers committed Oct 30, 2017 189 `````` Definition A i : PROP := (∃ P, ¬P ∗ saved i P)%I. `````` Robbert Krebbers committed Oct 25, 2017 190 `````` Global Instance A_persistent i : Persistent (A i) := _. `````` Ralf Jung committed Aug 05, 2016 191 `````` `````` 192 `````` Lemma A_alloc : fupd M1 (∃ i, saved i (A i)). `````` Ralf Jung committed Aug 05, 2016 193 `````` Proof. by apply saved_alloc. Qed. `````` Ralf Jung committed Aug 05, 2016 194 `````` `````` Ralf Jung committed Aug 08, 2016 195 `````` Lemma saved_NA i : saved i (A i) ⊢ ¬A i. `````` Ralf Jung committed Aug 05, 2016 196 `````` Proof. `````` Ralf Jung committed Aug 05, 2016 197 198 `````` iIntros "#Hi !# #HA". iPoseProof "HA" as "HA'". iDestruct "HA'" as (P) "#[HNP Hi']". `````` Robbert Krebbers committed Oct 25, 2016 199 `````` iMod (saved_cast i (A i) P with "[]") as "HP". `````` Ralf Jung committed Aug 08, 2016 200 `````` { eauto. } `````` Ralf Jung committed Aug 05, 2016 201 `````` by iApply "HNP". `````` Ralf Jung committed Aug 05, 2016 202 `````` Qed. `````` Ralf Jung committed Aug 05, 2016 203 `````` `````` Ralf Jung committed Aug 08, 2016 204 `````` Lemma saved_A i : saved i (A i) ⊢ A i. `````` Ralf Jung committed Aug 05, 2016 205 `````` Proof. `````` Ralf Jung committed Aug 08, 2016 206 207 `````` iIntros "#Hi". iExists (A i). iFrame "#". by iApply saved_NA. `````` Ralf Jung committed Aug 05, 2016 208 `````` Qed. `````` Ralf Jung committed Aug 05, 2016 209 `````` `````` Ralf Jung committed Aug 05, 2016 210 `````` Lemma contradiction : False. `````` Ralf Jung committed Jan 05, 2017 211 `````` Proof using All. `````` Ralf Jung committed Oct 07, 2016 212 `````` apply consistency. iIntros "". `````` Robbert Krebbers committed Oct 25, 2016 213 `````` iMod A_alloc as (i) "#H". `````` Ralf Jung committed Aug 08, 2016 214 215 `````` iPoseProof (saved_NA with "H") as "HN". iApply "HN". iApply saved_A. done. `````` Ralf Jung committed Aug 05, 2016 216 217 `````` Qed. End inv. End inv.``````