counter_examples.v 2.31 KB
 Ralf Jung committed Aug 04, 2016 1 2 3 4 5 6 7 8 9 ``````From iris.algebra Require Import upred. From iris.proofmode Require Import tactics. (** This proves that we need the ▷ in a "Saved Proposition" construction with name-dependend allocation. *) (** We fork in [uPred M] for any M, but the proof would work in any BI. *) Section savedprop. Context (M : ucmraT). Notation iProp := (uPred M). `````` Robbert Krebbers committed Aug 04, 2016 10 11 `````` Notation "¬ P" := (□ (P → False))%I : uPred_scope. Implicit Types P : iProp. `````` Ralf Jung committed Aug 04, 2016 12 `````` `````` Ralf Jung committed Aug 04, 2016 13 14 `````` (* Saved Propositions and view shifts. *) Context (sprop : Type) (saved : sprop → iProp → iProp) (pvs : iProp → iProp). `````` Robbert Krebbers committed Aug 04, 2016 15 16 `````` Hypothesis pvs_mono : ∀ P Q, (P ⊢ Q) → pvs P ⊢ pvs Q. Hypothesis sprop_persistent : ∀ i P, PersistentP (saved i P). `````` Ralf Jung committed Aug 04, 2016 17 `````` Hypothesis sprop_alloc_dep : `````` Robbert Krebbers committed Aug 04, 2016 18 19 `````` ∀ (P : sprop → iProp), True ⊢ pvs (∃ i, saved i (P i)). Hypothesis sprop_agree : ∀ i P Q, saved i P ∧ saved i Q ⊢ P ↔ Q. `````` Ralf Jung committed Aug 04, 2016 20 21 `````` (* Self-contradicting assertions are inconsistent *) `````` Robbert Krebbers committed Aug 04, 2016 22 `````` Lemma no_self_contradiction P `{!PersistentP P} : □ (P ↔ ¬ P) ⊢ False. `````` Robbert Krebbers committed Aug 04, 2016 23 24 `````` Proof. iIntros "#[H1 H2]". `````` Ralf Jung committed Aug 04, 2016 25 `````` iAssert P as "#HP". `````` Robbert Krebbers committed Aug 04, 2016 26 27 `````` { iApply "H2". iIntros "! #HP". by iApply ("H1" with "[#]"). } by iApply ("H1" with "[#]"). `````` Ralf Jung committed Aug 04, 2016 28 29 30 `````` Qed. (* "Assertion with name [i]" is equivalent to any assertion P s.t. [saved i P] *) `````` Robbert Krebbers committed Aug 04, 2016 31 32 `````` 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 33 `````` Proof. `````` Robbert Krebbers committed Aug 04, 2016 34 `````` iIntros "#HS !". iSplit. `````` Robbert Krebbers committed Aug 04, 2016 35 36 `````` - iDestruct 1 as (Q) "[#HSQ HQ]". iApply (sprop_agree i P Q with "[]"); eauto. `````` Ralf Jung committed Aug 04, 2016 37 38 39 40 41 42 `````` - 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 43 44 `````` Lemma Q_self_contradiction i : Q i ⊢ □ (A i ↔ ¬ A i). Proof. iIntros "#HQ !". by iApply (saved_is_A i (¬A i)). Qed. `````` Ralf Jung committed Aug 04, 2016 45 46 `````` (* We can obtain such a [Q i]. *) `````` Robbert Krebbers committed Aug 04, 2016 47 48 `````` Lemma make_Q : True ⊢ pvs (∃ i, Q i). Proof. apply sprop_alloc_dep. Qed. `````` Ralf Jung committed Aug 04, 2016 49 50 `````` (* Put together all the pieces to derive a contradiction. *) `````` Ralf Jung committed Aug 04, 2016 51 52 `````` (* TODO: Have a lemma in upred.v that says that we cannot view shift to False. *) Lemma contradiction : True ⊢ pvs False. `````` Ralf Jung committed Aug 04, 2016 53 `````` Proof. `````` Robbert Krebbers committed Aug 04, 2016 54 55 `````` rewrite make_Q. apply pvs_mono. iDestruct 1 as (i) "HQ". iApply (no_self_contradiction (A i)). by iApply Q_self_contradiction. `````` Ralf Jung committed Aug 04, 2016 56 57 `````` Qed. End savedprop.``````