counter_examples.v 8.9 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
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
  Context (M : ucmraT).
  Notation iProp := (uPred M).
  Implicit Types P : iProp.

  (** Assumptions *)
  (* We have view shifts (two classes: empty/full mask) *)
  Context (pvs0 pvs1 : iProp  iProp).

  Hypothesis pvs0_intro : forall P, P  pvs0 P.

  Hypothesis pvs0_mono : forall P Q, (P  Q)  pvs0 P  pvs0 Q.
  Hypothesis pvs0_pvs0 : forall P, pvs0 (pvs0 P)  pvs0 P.
  Hypothesis pvs0_frame_l : forall P Q, P  pvs0 Q  pvs0 (P  Q).

  Hypothesis pvs1_mono : forall P Q, (P  Q)  pvs1 P  pvs1 Q.
  Hypothesis pvs1_pvs1 : forall P, pvs1 (pvs1 P)  pvs1 P.
  Hypothesis pvs1_frame_l : forall P Q, P  pvs1 Q  pvs1 (P  Q).

  Hypothesis pvs0_pvs1 : forall P, pvs0 P  pvs1 P.

  (* We have invariants *)
  Context (name : Type) (inv : name  iProp  iProp).
  Hypothesis inv_persistent : forall i P, PersistentP (inv i P).
88
89
  Hypothesis inv_alloc :
    forall (P : iProp), P  pvs1 ( i, inv i P).
90
91
92
  Hypothesis inv_open :
    forall i P Q R, (P  Q  pvs0 (P  R))  (inv i P  Q  pvs1 R).

Ralf Jung's avatar
Ralf Jung committed
93
94
95
96
97
98
99
100
101
102
103
104
  (* 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. *)
  Context (gname : Type).
  Context (start finished : gname  iProp).

  Hypothesis sts_alloc : True  pvs0 ( γ, start γ).
  Hypotheses start_finish : forall γ, start γ  pvs0 (finished γ).

  Hypothesis finished_not_start : forall γ, start γ  finished γ  False.

  Hypothesis finished_dup : forall γ, finished γ  finished γ  finished γ.
105
106
107

  (* We have that we cannot view shift from the initial state to false
     (because the initial state is actually achievable). *)
Ralf Jung's avatar
Ralf Jung committed
108
  Hypothesis soundness : ¬ (True  pvs1 False).
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
156
157
158
159
160
161
162
163
164
165

  (** Some general lemmas and proof mode compatibility. *)
  Lemma inv_open' i P R:
    inv i P  (P - pvs0 (P  pvs1 R))  pvs1 R.
  Proof.
    iIntros "(#HiP & HP)". iApply pvs1_pvs1. iApply inv_open; last first.
    { iSplit; first done. iExact "HP". }
    iIntros "(HP & HPw)". by iApply "HPw".
  Qed.

  Lemma pvs1_intro P : P  pvs1 P.
  Proof. rewrite -pvs0_pvs1. apply pvs0_intro. Qed.

  Instance pvs0_mono' : Proper (() ==> ()) pvs0.
  Proof. intros ?**. by apply pvs0_mono. Qed.
  Instance pvs0_proper : Proper (() ==> ()) pvs0.
  Proof.
    intros P Q Heq.
    apply (anti_symm ()); apply pvs0_mono; by rewrite ?Heq -?Heq.
  Qed.
  Instance pvs1_mono' : Proper (() ==> ()) pvs1.
  Proof. intros ?**. by apply pvs1_mono. Qed.
  Instance pvs1_proper : Proper (() ==> ()) pvs1.
  Proof.
    intros P Q Heq.
    apply (anti_symm ()); apply pvs1_mono; by rewrite ?Heq -?Heq.
  Qed.

  Lemma pvs0_frame_r : forall P Q, (pvs0 P  Q)  pvs0 (P  Q).
  Proof.
    intros. rewrite comm pvs0_frame_l. apply pvs0_mono. by rewrite comm.
  Qed.
  Lemma pvs1_frame_r : forall P Q, (pvs1 P  Q)  pvs1 (P  Q).
  Proof.
    intros. rewrite comm pvs1_frame_l. apply pvs1_mono. by rewrite comm.
  Qed.

  Global Instance elim_pvs0_pvs0 P Q :
    ElimVs (pvs0 P) P (pvs0 Q) (pvs0 Q).
  Proof.
    rewrite /ElimVs. etrans; last eapply pvs0_pvs0.
    rewrite pvs0_frame_r. apply pvs0_mono. by rewrite uPred.wand_elim_r.
  Qed.

  Global Instance elim_pvs1_pvs1 P Q :
    ElimVs (pvs1 P) P (pvs1 Q) (pvs1 Q).
  Proof.
    rewrite /ElimVs. etrans; last eapply pvs1_pvs1.
    rewrite pvs1_frame_r. apply pvs1_mono. by rewrite uPred.wand_elim_r.
  Qed.

  Global Instance elim_pvs0_pvs1 P Q :
    ElimVs (pvs0 P) P (pvs1 Q) (pvs1 Q).
  Proof.
    rewrite /ElimVs. rewrite pvs0_pvs1. apply elim_pvs1_pvs1.
  Qed.

166
167
168
169
170
171
172
173
174
175
176
177
178
179
  Global Instance exists_split_pvs0 {A} P (Φ : A  iProp) :
    FromExist P Φ  FromExist (pvs0 P) (λ a, pvs0 (Φ a)).
  Proof.
    rewrite /FromExist=>HP. apply uPred.exist_elim=> a.
    apply pvs0_mono. by rewrite -HP -(uPred.exist_intro a).
  Qed.

  Global Instance exists_split_pvs1 {A} P (Φ : A  iProp) :
    FromExist P Φ  FromExist (pvs1 P) (λ a, pvs1 (Φ a)).
  Proof.
    rewrite /FromExist=>HP. apply uPred.exist_elim=> a.
    apply pvs1_mono. by rewrite -HP -(uPred.exist_intro a).
  Qed.

180
  (** Now to the actual counterexample. We start with a weird for of saved propositions. *)
Ralf Jung's avatar
Ralf Jung committed
181
182
183
  Definition saved (γ : gname) (P : iProp) : iProp :=
     i, inv i (start γ  (finished γ  P)).
  Global Instance : forall γ P, PersistentP (saved γ P) := _.
184

Ralf Jung's avatar
Ralf Jung committed
185
186
  Lemma saved_alloc (P : gname  iProp) :
    True  pvs1 ( γ, saved γ (P γ)).
187
  Proof.
Ralf Jung's avatar
Ralf Jung committed
188
189
    iIntros "". iVs (sts_alloc) as (γ) "Hs".
    iVs (inv_alloc (start γ  (finished γ   (P γ))) with "[Hs]") as (i) "#Hi".
190
    { iLeft. done. }
Ralf Jung's avatar
Ralf Jung committed
191
    iApply pvs1_intro. iExists γ, i. done.
192
193
  Qed.

Ralf Jung's avatar
Ralf Jung committed
194
195
  Lemma saved_cast γ P Q :
    saved γ P  saved γ Q   P  pvs1 ( Q).
196
  Proof.
Ralf Jung's avatar
Ralf Jung committed
197
    iIntros "(#HsP & #HsQ & #HP)". iDestruct "HsP" as (i) "HiP".
198
199
    iApply (inv_open' i). iSplit; first done.
    (* Can I state a view-shift and immediately run it? *)
Ralf Jung's avatar
Ralf Jung committed
200
201
202
203
204
205
206
207
208
209
210
211
212
213
    iIntros "HaP". iAssert (pvs0 (finished γ)) with "[HaP]" as "Hf".
    { iDestruct "HaP" as "[Hs | [Hf _]]".
      - by iApply start_finish.
      - by iApply pvs0_intro. }
    iVs "Hf" as "Hf". iDestruct (finished_dup with "Hf") as "[Hf Hf']".
    iApply pvs0_intro. iSplitL "Hf'"; first by eauto.
    (* 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]]".
    { iExFalso. iApply finished_not_start. iSplitL "HaQ"; done. }
    iApply pvs0_intro. iSplitL "Hf".
    { iRight. by iSplitL "Hf". }
    by iApply pvs1_intro.
214
215
  Qed.

216
  (** And now we tie a bad knot. *)
Ralf Jung's avatar
Ralf Jung committed
217
  Notation "¬ P" := ( (P - pvs1 False))%I : uPred_scope.
218
  Definition A i : iProp :=  P, ¬P  saved i P.
Ralf Jung's avatar
Ralf Jung committed
219
  Global Instance : forall i, PersistentP (A i) := _.
220

221
  Lemma A_alloc :
Ralf Jung's avatar
Ralf Jung committed
222
    True  pvs1 ( i, saved i (A i)).
223
  Proof. by apply saved_alloc. Qed.
224

225
226
227
  Lemma alloc_NA i :
    saved i (A i)  (¬A i).
  Proof.
Ralf Jung's avatar
Ralf Jung committed
228
229
230
231
232
    iIntros "#Hi !# #HA". iPoseProof "HA" as "HA'".
    iDestruct "HA'" as (P) "#[HNP Hi']".
    iVs ((saved_cast i) with "[]") as "HP".
    { iSplit; first iExact "Hi". iSplit; first iExact "Hi'". done. }
    by iApply "HNP".
233
  Qed.
234

235
236
237
  Lemma alloc_A i :
    saved i (A i)  A i.
  Proof.
Ralf Jung's avatar
Ralf Jung committed
238
239
    iIntros "#Hi". iPoseProof (alloc_NA with "Hi") as "HNA".
    iExists (A i). iSplit; done.
240
  Qed.
241

242
243
  Lemma contradiction : False.
  Proof.
Ralf Jung's avatar
Ralf Jung committed
244
245
    apply soundness. iIntros "".
    iVs A_alloc as (i) "#H".
246
247
    iPoseProof (alloc_NA with "H") as "HN".
    iApply "HN".
248
249
    iApply alloc_A. done.
  Qed.
250

251
End inv. End inv.