counter_examples.v 2.31 KB
Newer Older
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).
10
11
  Notation "¬ P" := ( (P  False))%I : uPred_scope.
  Implicit Types P : iProp.
12

13
14
  (* Saved Propositions and view shifts. *)
  Context (sprop : Type) (saved : sprop  iProp  iProp) (pvs : iProp  iProp).
15
16
  Hypothesis pvs_mono :  P Q, (P  Q)  pvs P  pvs Q.
  Hypothesis sprop_persistent :  i P, PersistentP (saved i P).
17
  Hypothesis sprop_alloc_dep :
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.
20
21

  (* Self-contradicting assertions are inconsistent *)
22
  Lemma no_self_contradiction P `{!PersistentP P} :  (P  ¬ P)  False.
Robbert Krebbers's avatar
Robbert Krebbers committed
23
24
  Proof.
    iIntros "#[H1 H2]".
25
    iAssert P as "#HP".
26
27
    { iApply "H2". iIntros "! #HP". by iApply ("H1" with "[#]"). }
    by iApply ("H1" with "[#]").
28
29
30
  Qed.

  (* "Assertion with name [i]" is equivalent to any assertion P s.t. [saved i P] *)
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).
33
  Proof.
Robbert Krebbers's avatar
Robbert Krebbers committed
34
    iIntros "#HS !". iSplit.
35
36
    - iDestruct 1 as (Q) "[#HSQ HQ]".
      iApply (sprop_agree i P Q with "[]"); eauto.
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).
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.
45
46

  (* We can obtain such a [Q i]. *)
47
48
  Lemma make_Q : True  pvs ( i, Q i).
  Proof. apply sprop_alloc_dep. Qed.
49
50

  (* Put together all the pieces to derive a contradiction. *)
51
52
  (* TODO: Have a lemma in upred.v that says that we cannot view shift to False. *)
  Lemma contradiction : True  pvs False.
53
  Proof.
54
55
    rewrite make_Q. apply pvs_mono. iDestruct 1 as (i) "HQ".
    iApply (no_self_contradiction (A i)). by iApply Q_self_contradiction.
56
57
  Qed.
End savedprop.