counterexamples.v 7.81 KB
Newer Older
1
From iris.bi Require Export bi.
2
From iris.proofmode Require Import tactics.
3
Set Default Proof Using "Type*".
4 5

(** This proves that we need the ▷ in a "Saved Proposition" construction with
Derek Dreyer's avatar
Derek Dreyer committed
6
name-dependent allocation. *)
7
Module savedprop. Section savedprop.
8
  Context `{BiAffine PROP}.
Robbert Krebbers's avatar
Robbert Krebbers committed
9
  Notation "¬ P" := ( (P  False))%I : bi_scope.
10
  Implicit Types P : PROP.
11

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).
22
  Hypothesis sprop_persistent :  i P, Persistent (saved i P).
23
  Hypothesis sprop_alloc_dep :
24
     (P : ident  PROP), (|==>  i, saved i (P i))%I.
25
  Hypothesis sprop_agree :  i P Q, saved i P  saved i Q   (P  Q).
26

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

38
  (** A bad recursive reference: "Assertion with name [i] does not hold" *)
39
  Definition A (i : ident) : PROP := ( P, ¬ P  saved i P)%I.
40

41
  Lemma A_alloc : (|==>  i, saved i (A i))%I.
42
  Proof. by apply sprop_alloc_dep. Qed.
43

44
  Lemma saved_NA i : saved i (A i)  ¬ A i.
45
  Proof.
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.
51 52
  Qed.

53
  Lemma saved_A i : saved i (A i)  A i.
54
  Proof.
55 56
    iIntros "#Hs". iExists (A i). iFrame "#".
    by iApply saved_NA.
57
  Qed.
58 59

  Lemma contradiction : False.
60
  Proof using All.
61
    apply consistency.
Robbert Krebbers's avatar
Robbert Krebbers committed
62
    iMod A_alloc as (i) "#H".
63
    iPoseProof (saved_NA with "H") as "HN".
64
    iApply bupd_intro. iApply "HN". iApply saved_A. done.
65
  Qed.
66
End savedprop. End savedprop.
67

68

69
(** This proves that we need the ▷ when opening invariants. *)
70
Module inv. Section inv.
71
  Context `{BiAffine PROP}.
72
  Implicit Types P : PROP.
73 74

  (** Assumptions *)
75
  (** We have the update modality (two classes: empty/full mask) *)
76
  Inductive mask := M0 | M1.
77 78
  Context (fupd : mask  PROP  PROP).
  Arguments fupd _ _%I.
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.
82
  Hypothesis fupd_frame_l :  E P Q, P  fupd E Q  fupd E (P  Q).
83
  Hypothesis fupd_mask_mono :  P, fupd M0 P  fupd M1 P.
84

85
  (** We have invariants *)
86 87
  Context (name : Type) (inv : name  PROP  PROP).
  Arguments inv _ _%I.
88
  Hypothesis inv_persistent :  i P, Persistent (inv i P).
89
  Hypothesis inv_alloc :  P, P  fupd M1 ( i, inv i P).
90
  Hypothesis inv_open :
91
     i P Q R, (P  Q  fupd M0 (P  R))  (inv i P  Q  fupd M1 R).
92

Ralf Jung's avatar
Ralf Jung committed
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. *)
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 () +_## ()
101
  *)
Ralf Jung's avatar
Ralf Jung committed
102
  Context (gname : Type).
103
  Context (start finished : gname  PROP).
Ralf Jung's avatar
Ralf Jung committed
104

105
  Hypothesis sts_alloc : fupd M0 ( γ, start γ).
106
  Hypotheses start_finish :  γ, start γ  fupd M0 (finished γ).
Ralf Jung's avatar
Ralf Jung committed
107

108
  Hypothesis finished_not_start :  γ, start γ  finished γ  False.
Ralf Jung's avatar
Ralf Jung committed
109

110
  Hypothesis finished_dup :  γ, finished γ  finished γ  finished γ.
111

112
  (** We assume that we cannot update to false. *)
113
  Hypothesis consistency : ¬ (fupd M1 False).
114 115

  (** Some general lemmas and proof mode compatibility. *)
116
  Lemma inv_open' i P R : inv i P  (P - fupd M0 (P  fupd M1 R))  fupd M1 R.
117
  Proof.
118
    iIntros "(#HiP & HP)". iApply fupd_fupd. iApply inv_open; last first.
119 120 121 122
    { iSplit; first done. iExact "HP". }
    iIntros "(HP & HPw)". by iApply "HPw".
  Qed.

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).
126
  Proof.
Robbert Krebbers's avatar
Robbert Krebbers committed
127
    intros P Q; rewrite !bi.equiv_spec=> -[??]; split; by apply fupd_mono.
128 129
  Qed.

130
  Lemma fupd_frame_r E P Q : fupd E P  Q  fupd E (P  Q).
131
  Proof. by rewrite comm fupd_frame_l comm. Qed.
132

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

140 141
  Global Instance elim_fupd0_fupd1 p P Q :
    ElimModal True p false (fupd M0 P) P (fupd M1 Q) (fupd M1 Q).
142
  Proof.
143 144
    by rewrite /ElimModal bi.intuitionistically_if_elim
      fupd_frame_r bi.wand_elim_r fupd_mask_mono fupd_fupd.
145 146
  Qed.

147
  Global Instance exists_split_fupd0 {A} E P (Φ : A  PROP) :
148
    FromExist P Φ  FromExist (fupd E P) (λ a, fupd E (Φ a)).
149
  Proof.
Robbert Krebbers's avatar
Robbert Krebbers committed
150 151
    rewrite /FromExist=>HP. apply bi.exist_elim=> a.
    apply fupd_mono. by rewrite -HP -(bi.exist_intro a).
152 153
  Qed.

Derek Dreyer's avatar
Derek Dreyer committed
154
  (** Now to the actual counterexample. We start with a weird form of saved propositions. *)
155 156
  Definition saved (γ : gname) (P : PROP) : PROP :=
    ( i, inv i (start γ  (finished γ   P)))%I.
157
  Global Instance saved_persistent γ P : Persistent (saved γ P) := _.
158

159
  Lemma saved_alloc (P : gname  PROP) : fupd M1 ( γ, saved γ (P γ)).
160
  Proof.
161
    iIntros "". iMod (sts_alloc) as (γ) "Hs".
162
    iMod (inv_alloc (start γ  (finished γ   (P γ)))%I with "[Hs]") as (i) "#Hi".
163
    { auto. }
164
    iApply fupd_intro. by iExists γ, i.
165 166
  Qed.

167
  Lemma saved_cast γ P Q : saved γ P  saved γ Q   P  fupd M1 ( Q).
168
  Proof.
Ralf Jung's avatar
Ralf Jung committed
169
    iIntros "(#HsP & #HsQ & #HP)". iDestruct "HsP" as (i) "HiP".
170
    iApply (inv_open' i). iSplit; first done.
171
    iIntros "HaP". iAssert (fupd M0 (finished γ)) with "[HaP]" as "> Hf".
Ralf Jung's avatar
Ralf Jung committed
172 173
    { iDestruct "HaP" as "[Hs | [Hf _]]".
      - by iApply start_finish.
174
      - by iApply fupd_intro. }
175
    iDestruct (finished_dup with "Hf") as "[Hf Hf']".
176
    iApply fupd_intro. iSplitL "Hf'"; first by eauto.
Ralf Jung's avatar
Ralf Jung committed
177
    (* Step 2: Open the Q-invariant. *)
178
    iClear (i) "HiP ". iDestruct "HsQ" as (i) "HiQ".
Ralf Jung's avatar
Ralf Jung committed
179 180
    iApply (inv_open' i). iSplit; first done.
    iIntros "[HaQ | [_ #HQ]]".
181
    { iExFalso. iApply finished_not_start. by iFrame. }
182
    iApply fupd_intro. iSplitL "Hf".
183
    { iRight. by iFrame. }
184
    by iApply fupd_intro.
185 186
  Qed.

187
  (** And now we tie a bad knot. *)
Robbert Krebbers's avatar
Robbert Krebbers committed
188
  Notation "¬ P" := ( (P - fupd M1 False))%I : bi_scope.
189
  Definition A i : PROP := ( P, ¬P  saved i P)%I.
190
  Global Instance A_persistent i : Persistent (A i) := _.
191

192
  Lemma A_alloc : fupd M1 ( i, saved i (A i)).
193
  Proof. by apply saved_alloc. Qed.
194

195
  Lemma saved_NA i : saved i (A i)  ¬A i.
196
  Proof.
Ralf Jung's avatar
Ralf Jung committed
197 198
    iIntros "#Hi !# #HA". iPoseProof "HA" as "HA'".
    iDestruct "HA'" as (P) "#[HNP Hi']".
199
    iMod (saved_cast i (A i) P with "[]") as "HP".
200
    { eauto. }
Ralf Jung's avatar
Ralf Jung committed
201
    by iApply "HNP".
202
  Qed.
203

204
  Lemma saved_A i : saved i (A i)  A i.
205
  Proof.
206 207
    iIntros "#Hi". iExists (A i). iFrame "#".
    by iApply saved_NA.
208
  Qed.
209

210
  Lemma contradiction : False.
211
  Proof using All.
Ralf Jung's avatar
Ralf Jung committed
212
    apply consistency. iIntros "".
213
    iMod A_alloc as (i) "#H".
214 215
    iPoseProof (saved_NA with "H") as "HN".
    iApply "HN". iApply saved_A. done.
216 217
  Qed.
End inv. End inv.