counter_examples.v 7.73 KB
Newer Older
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
5
name-dependend allocation. *)
6
Module savedprop. Section savedprop.
7
8
  Context (M : ucmraT).
  Notation iProp := (uPred M).
9
10
  Notation "¬ P" := ( (P  False))%I : uPred_scope.
  Implicit Types P : iProp.
11

12
  (* Saved Propositions and view shifts. *)
13
  Context (sprop : Type) (saved : sprop  iProp  iProp).
14
  Hypothesis sprop_persistent :  i P, PersistentP (saved i P).
15
  Hypothesis sprop_alloc_dep :
16
     (P : sprop  iProp), True =r=> ( i, saved i (P i)).
17
  Hypothesis sprop_agree :  i P Q, saved i P  saved i Q  P  Q.
18
19

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

  (* "Assertion with name [i]" is equivalent to any assertion P s.t. [saved i P] *)
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).
31
  Proof.
Robbert Krebbers's avatar
Robbert Krebbers committed
32
    iIntros "#HS !#". iSplit.
33
34
    - iDestruct 1 as (Q) "[#HSQ HQ]".
      iApply (sprop_agree i P Q with "[]"); eauto.
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).
41
  Lemma Q_self_contradiction i : Q i   (A i  ¬ A i).
Robbert Krebbers's avatar
Robbert Krebbers committed
42
  Proof. iIntros "#HQ !#". by iApply (saved_is_A i (¬A i)). Qed.
43
44

  (* We can obtain such a [Q i]. *)
45
  Lemma make_Q : True =r=>  i, Q i.
46
  Proof. apply sprop_alloc_dep. Qed.
47
48

  (* Put together all the pieces to derive a contradiction. *)
49
  Lemma rvs_false : (True : uPred M) =r=> False.
50
  Proof.
51
    rewrite make_Q. apply uPred.rvs_mono. iDestruct 1 as (i) "HQ".
52
    iApply (no_self_contradiction (A i)). by iApply Q_self_contradiction.
53
  Qed.
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.
60
End savedprop. End savedprop.
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. *)
64
Module inv. Section inv.
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) *)
71
72
  Inductive mask := M0 | M1.
  Context (pvs : mask  iProp  iProp).
73

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.
79
80
81

  (* We have invariants *)
  Context (name : Type) (inv : name  iProp  iProp).
82
  Hypothesis inv_persistent :  i P, PersistentP (inv i P).
83
  Hypothesis inv_alloc :  P, P  pvs M1 ( i, inv i P).
84
  Hypothesis inv_open :
85
     i P Q R, (P  Q  pvs M0 (P  R))  (inv i P  Q  pvs M1 R).
86

Ralf Jung's avatar
Ralf Jung committed
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. *)
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's avatar
Ralf Jung committed
96
97
98
  Context (gname : Type).
  Context (start finished : gname  iProp).

99
100
  Hypothesis sts_alloc : True  pvs M0 ( γ, start γ).
  Hypotheses start_finish :  γ, start γ  pvs M0 (finished γ).
Ralf Jung's avatar
Ralf Jung committed
101

102
  Hypothesis finished_not_start :  γ, start γ  finished γ  False.
Ralf Jung's avatar
Ralf Jung committed
103

104
  Hypothesis finished_dup :  γ, finished γ  finished γ  finished γ.
105

Ralf Jung's avatar
Ralf Jung committed
106
  (* We assume that we cannot view shift to false. *)
107
  Hypothesis soundness : ¬ (True  pvs M1 False).
108
109

  (** Some general lemmas and proof mode compatibility. *)
110
  Lemma inv_open' i P R : inv i P  (P - pvs M0 (P  pvs M1 R))  pvs M1 R.
111
  Proof.
112
    iIntros "(#HiP & HP)". iApply pvs_pvs. iApply inv_open; last first.
113
114
115
116
    { iSplit; first done. iExact "HP". }
    iIntros "(HP & HPw)". by iApply "HPw".
  Qed.

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).
120
  Proof.
121
    intros P Q; rewrite !uPred.equiv_spec=> -[??]; split; by apply pvs_mono.
122
123
  Qed.

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.
126

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.
129

130
  Global Instance elim_pvs0_pvs1 P Q : ElimVs (pvs M0 P) P (pvs M1 Q) (pvs M1 Q).
131
  Proof.
132
    by rewrite /ElimVs pvs_frame_r uPred.wand_elim_r pvs_mask_mono pvs_pvs.
133
134
  Qed.

135
136
  Global Instance exists_split_pvs0 {A} E P (Φ : A  iProp) :
    FromExist P Φ  FromExist (pvs E P) (λ a, pvs E (Φ a)).
137
138
  Proof.
    rewrite /FromExist=>HP. apply uPred.exist_elim=> a.
139
    apply pvs_mono. by rewrite -HP -(uPred.exist_intro a).
140
141
  Qed.

142
  (** Now to the actual counterexample. We start with a weird for of saved propositions. *)
Ralf Jung's avatar
Ralf Jung committed
143
  Definition saved (γ : gname) (P : iProp) : iProp :=
144
145
     i, inv i (start γ  (finished γ   P)).
  Global Instance saved_persistent γ P : PersistentP (saved γ P) := _.
146

147
  Lemma saved_alloc (P : gname  iProp) : True  pvs M1 ( γ, saved γ (P γ)).
148
  Proof.
Ralf Jung's avatar
Ralf Jung committed
149
150
    iIntros "". iVs (sts_alloc) as (γ) "Hs".
    iVs (inv_alloc (start γ  (finished γ   (P γ))) with "[Hs]") as (i) "#Hi".
151
152
    { auto. }
    iApply pvs_intro. by iExists γ, i.
153
154
  Qed.

155
  Lemma saved_cast γ P Q : saved γ P  saved γ Q   P  pvs M1 ( Q).
156
  Proof.
Ralf Jung's avatar
Ralf Jung committed
157
    iIntros "(#HsP & #HsQ & #HP)". iDestruct "HsP" as (i) "HiP".
158
    iApply (inv_open' i). iSplit; first done.
159
    iIntros "HaP". iAssert (pvs M0 (finished γ)) with "[HaP]" as "==> Hf".
Ralf Jung's avatar
Ralf Jung committed
160
161
    { iDestruct "HaP" as "[Hs | [Hf _]]".
      - by iApply start_finish.
162
      - by iApply pvs_intro. }
163
    iDestruct (finished_dup with "Hf") as "[Hf Hf']".
164
    iApply pvs_intro. iSplitL "Hf'"; first by eauto.
Ralf Jung's avatar
Ralf Jung committed
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]]".
169
170
171
172
    { iExFalso. iApply finished_not_start. by iFrame. }
    iApply pvs_intro. iSplitL "Hf".
    { iRight. by iFrame. }
    by iApply pvs_intro.
173
174
  Qed.

175
  (** And now we tie a bad knot. *)
176
  Notation "¬ P" := ( (P - pvs M1 False))%I : uPred_scope.
177
  Definition A i : iProp :=  P, ¬P  saved i P.
178
  Global Instance A_persistent i : PersistentP (A i) := _.
179

180
  Lemma A_alloc : True  pvs M1 ( i, saved i (A i)).
181
  Proof. by apply saved_alloc. Qed.
182

183
  Lemma alloc_NA i : saved i (A i)  ¬A i.
184
  Proof.
Ralf Jung's avatar
Ralf Jung committed
185
186
    iIntros "#Hi !# #HA". iPoseProof "HA" as "HA'".
    iDestruct "HA'" as (P) "#[HNP Hi']".
187
188
    iVs (saved_cast i with "[]") as "HP".
    { iSplit; first iExact "Hi". by iFrame "#". }
Ralf Jung's avatar
Ralf Jung committed
189
    by iApply "HNP".
190
  Qed.
191

192
  Lemma alloc_A i : saved i (A i)  A i.
193
  Proof.
Ralf Jung's avatar
Ralf Jung committed
194
    iIntros "#Hi". iPoseProof (alloc_NA with "Hi") as "HNA".
195
    iExists (A i). by iFrame "#".
196
  Qed.
197

198
199
  Lemma contradiction : False.
  Proof.
Ralf Jung's avatar
Ralf Jung committed
200
201
    apply soundness. iIntros "".
    iVs A_alloc as (i) "#H".
202
    iPoseProof (alloc_NA with "H") as "HN".
203
    iApply "HN". iApply alloc_A. done.
204
205
  Qed.
End inv. End inv.