double_negation.v 14 KB
Newer Older
1
From iris.base_logic Require Import base_logic.
2

3
(* In this file we show that the bupd can be thought of a kind of
4
   step-indexed double-negation when our meta-logic is classical *)
5
Definition uPred_nnupd {M} (P: uPred M) : uPred M :=
6
   n, (P - ^n False) - ^n False.
7

8
Notation "|=n=> Q" := (uPred_nnupd Q)
9
10
11
  (at level 99, Q at level 200, format "|=n=>  Q") : uPred_scope.
Notation "P =n=> Q" := (P  |=n=> Q)
  (at level 99, Q at level 200, only parsing) : C_scope.
12
13
Notation "P =n=∗ Q" := (P - |=n=> Q)%I
  (at level 99, Q at level 200, format "P  =n=∗  Q") : uPred_scope.
14
15

(* Our goal is to prove that:
16
17
  (1) |=n=> has (nearly) all the properties of the |==> modality that are used in Iris
  (2) If our meta-logic is classical, then |=n=> and |==> are equivalent
18
19
*)

20
Section bupd_nnupd.
21
22
23
24
25
26
27
28
Context {M : ucmraT}.
Implicit Types φ : Prop.
Implicit Types P Q : uPred M.
Implicit Types A : Type.
Implicit Types x : M.
Import uPred.

(* Helper lemmas about iterated later modalities *)
Ralf Jung's avatar
Ralf Jung committed
29
Lemma laterN_big n a x φ: {n} x   a  n  (^a ⌜φ⌝)%I n x  φ.
30
31
32
33
34
35
36
37
38
Proof.
  induction 2 as [| ?? IHle].
  - induction a; repeat (rewrite //= || uPred.unseal). 
    intros Hlater. apply IHa; auto using cmra_validN_S.
    move:Hlater; repeat (rewrite //= || uPred.unseal). 
  - intros. apply IHle; auto using cmra_validN_S.
    eapply uPred_closed; eauto using cmra_validN_S.
Qed.

Ralf Jung's avatar
Ralf Jung committed
39
Lemma laterN_small n a x φ: {n} x   n < a  (^a ⌜φ⌝)%I n x.
40
41
42
43
44
45
46
47
48
49
50
Proof.
  induction 2.
  - induction n as [| n IHn]; [| move: IHn];
      repeat (rewrite //= || uPred.unseal).
    naive_solver eauto using cmra_validN_S.
  - induction n as [| n IHn]; [| move: IHle];
      repeat (rewrite //= || uPred.unseal).
    red; rewrite //=. intros.
    eapply (uPred_closed _ _ (S n)); eauto using cmra_validN_S.
Qed.

51
52
(* It is easy to show that most of the basic properties of bupd that
   are used throughout Iris hold for nnupd. 
53
54

   In fact, the first three properties that follow hold for any
55
   modality of the form (- -∗ Q) -∗ Q for arbitrary Q. The situation
56
   here is slightly different, because nnupd is of the form 
57
   ∀ n, (- -∗ (Q n)) -∗ (Q n), but the proofs carry over straightforwardly.
58
59

 *)
60

61
Lemma nnupd_intro P : P =n=> P.
62
Proof. apply forall_intro=>?. apply wand_intro_l, wand_elim_l. Qed.
63
Lemma nnupd_mono P Q : (P  Q)  (|=n=> P) =n=> Q.
64
65
66
Proof.
  intros HPQ. apply forall_intro=>n.
  apply wand_intro_l.  rewrite -{1}HPQ.
67
  rewrite /uPred_nnupd (forall_elim n).
68
69
  apply wand_elim_r.
Qed.
70
Lemma nnupd_frame_r P R : (|=n=> P)  R =n=> P  R.
71
72
73
Proof.
  apply forall_intro=>n. apply wand_intro_r.
  rewrite (comm _ P) -wand_curry.
74
  rewrite /uPred_nnupd (forall_elim n).
75
76
  by rewrite -assoc wand_elim_r wand_elim_l.
Qed.
77
Lemma nnupd_ownM_updateP x (Φ : M  Prop) :
Ralf Jung's avatar
Ralf Jung committed
78
  x ~~>: Φ  uPred_ownM x =n=>  y, ⌜Φ y  uPred_ownM y.
79
Proof. 
80
  intros Hbupd. split. rewrite /uPred_nnupd. repeat uPred.unseal. 
81
82
83
  intros n y ? Hown a.
  red; rewrite //= => n' yf ??.
  inversion Hown as (x'&Hequiv).
84
  edestruct (Hbupd n' (Some (x'  yf))) as (y'&?&?); eauto.
85
86
87
88
89
90
91
92
93
94
95
96
97
98
  { by rewrite //= assoc -(dist_le _ _ _ _ Hequiv). }
  case (decide (a  n')).
  - intros Hle Hwand.
    exfalso. eapply laterN_big; last (uPred.unseal; eapply (Hwand n' (y'  x'))); eauto.
    * rewrite comm -assoc. done. 
    * rewrite comm -assoc. done. 
    * eexists. split; eapply uPred_mono; red; rewrite //=; eauto.
  - intros; assert (n' < a). omega.
    move: laterN_small. uPred.unseal.
    naive_solver.
Qed.

(* However, the transitivity property seems to be much harder to
   prove. This is surprising, because transitivity does hold for 
99
   modalities of the form (- -∗ Q) -∗ Q. What goes wrong when we quantify
100
101
102
   now over n? 
 *)

103
Remark nnupd_trans P: (|=n=> |=n=> P)  (|=n=> P).
104
Proof.
105
  rewrite /uPred_nnupd.
106
107
  apply forall_intro=>a. apply wand_intro_l.
  rewrite (forall_elim a).
108
  rewrite (nnupd_intro (P - _)).
109
  rewrite /uPred_nnupd.
110
111
112
113
  (* Oops -- the exponents of the later modality don't match up! *)
Abort.

(* Instead, we will need to prove this in the model. We start by showing that 
114
   nnupd is the limit of a the following sequence:
115

116
117
118
   (- -∗ False) - ∗ False,
   (- -∗ ▷ False) - ∗ ▷ False ∧ (- -∗ False) - ∗ False,
   (- -∗ ▷^2 False) - ∗ ▷^2 False ∧ (- -∗ ▷ False) - ∗ ▷ False ∧ (- -∗ False) - ∗ False,
119
120
121
   ...

   Then, it is easy enough to show that each of the uPreds in this sequence
122
   is transitive. It turns out that this implies that nnupd is transitive. *)
123
124
125
   

(* The definition of the sequence above: *)
126
Fixpoint uPred_nnupd_k {M} k (P: uPred M) : uPred M :=
127
  ((P - ^k False) - ^k False) 
128
129
  match k with 
    O => True
130
  | S k' => uPred_nnupd_k k' P
131
132
  end.

133
Notation "|=n=>_ k Q" := (uPred_nnupd_k k Q)
134
135
136
  (at level 99, k at level 9, Q at level 200, format "|=n=>_ k  Q") : uPred_scope.


137
138
(* One direction of the limiting process is easy -- nnupd implies nnupd_k for each k *)
Lemma nnupd_trunc1 k P: (|=n=> P)  |=n=>_k P.
139
Proof.
140
  induction k. 
141
  - rewrite /uPred_nnupd_k /uPred_nnupd. 
142
143
    rewrite (forall_elim 0) //= right_id //.
  - simpl. apply and_intro; auto.
144
    rewrite /uPred_nnupd. 
145
    rewrite (forall_elim (S k)) //=.
146
147
Qed.

148
Lemma nnupd_k_elim n k P: n  k  ((|=n=>_k P)  (P - (^n False))   (^n False))%I.
149
150
151
152
153
154
155
156
Proof.
  induction k.
  - inversion 1; subst; rewrite //= ?right_id. apply wand_elim_l.
  - inversion 1; subst; rewrite //= ?right_id.
    * rewrite and_elim_l. apply wand_elim_l.
    * rewrite and_elim_r IHk //.
Qed.

157
Lemma nnupd_k_unfold k P:
158
  (|=n=>_(S k) P)  ((P - (^(S k) False)) - (^(S k) False))  (|=n=>_k P).
159
Proof. done.  Qed.
160
Lemma nnupd_k_unfold' k P n x:
161
  (|=n=>_(S k) P)%I n x  (((P - (^(S k) False)) - (^(S k) False))  (|=n=>_k P))%I n x.
162
163
Proof. done.  Qed.

164
165
Lemma nnupd_k_weaken k P: (|=n=>_(S k) P)  |=n=>_k P.
Proof. by rewrite nnupd_k_unfold and_elim_r. Qed.
166

167
(* Now we are ready to show nnupd is the limit -- ie, for each k, it is within distance k
168
   of the kth term of the sequence *)
169
Lemma nnupd_nnupd_k_dist k P: (|=n=> P)%I {k} (|=n=>_k P)%I.
170
  split; intros n' x Hle Hx. split.
171
  - by apply (nnupd_trunc1 k).
172
  - revert n' x Hle Hx; induction k; intros n' x Hle Hx;
173
      rewrite ?nnupd_k_unfold' /uPred_nnupd.
174
175
176
177
178
179
180
181
182
183
184
185
186
187
188
189
190
191
    * rewrite //=. unseal.
      inversion Hle; subst.
      intros (HnnP&_) n k' x' ?? HPF.
      case (decide (k' < n)).
      ** move: laterN_small; uPred.unseal; naive_solver.
      ** intros. exfalso. eapply HnnP; eauto.
         assert (n  k'). omega.
         intros n'' x'' ???.
         specialize (HPF n'' x''). exfalso.
         eapply laterN_big; last (unseal; eauto).
         eauto. omega.
    * inversion Hle; subst.
      ** unseal. intros (HnnP&HnnP_IH) n k' x' ?? HPF.
         case (decide (k' < n)).
         *** move: laterN_small; uPred.unseal; naive_solver.
         *** intros. exfalso. assert (n  k'). omega.
             assert (n = S k  n < S k) as [->|] by omega.
             **** eapply laterN_big; eauto; unseal. eapply HnnP; eauto.
192
             **** move:nnupd_k_elim. unseal. intros Hnnupdk. 
193
                  eapply laterN_big; eauto. unseal.
194
                  eapply (Hnnupdk n k); first omega; eauto.
195
196
197
198
199
200
                  exists x, x'. split_and!; eauto. eapply uPred_closed; eauto.
                  eapply cmra_validN_op_l; eauto.
      ** intros HP. eapply IHk; auto.
         move:HP. unseal. intros (?&?); naive_solver.
Qed.

201
202
(* nnupd_k has a number of structural properties, including transitivity *)
Lemma nnupd_k_intro k P: P  (|=n=>_k P).
203
204
205
206
207
208
209
Proof.
  induction k; rewrite //= ?right_id.
  - apply wand_intro_l. apply wand_elim_l.
  - apply and_intro; auto. 
    apply wand_intro_l. apply wand_elim_l.
Qed.

210
Lemma nnupd_k_mono k P Q: (P  Q)  (|=n=>_k P)  (|=n=>_k Q).
211
212
213
214
215
Proof.
  induction k; rewrite //= ?right_id=>HPQ. 
  - do 2 (apply wand_mono; auto).
  - apply and_mono; auto; do 2 (apply wand_mono; auto).
Qed.
216
217
Instance nnupd_k_mono' k: Proper (() ==> ()) (@uPred_nnupd_k M k).
Proof. by intros P P' HP; apply nnupd_k_mono. Qed.
218

219
Instance nnupd_k_ne k n : Proper (dist n ==> dist n) (@uPred_nnupd_k M k).
220
Proof. induction k; rewrite //= ?right_id=>P P' HP; by rewrite HP. Qed.
221
222
223
224
Lemma nnupd_k_proper k P Q: (P  Q)  (|=n=>_k P)  (|=n=>_k Q).
Proof. intros HP; apply (anti_symm ()); eapply nnupd_k_mono; by rewrite HP. Qed.
Instance nnupd_k_proper' k: Proper (() ==> ()) (@uPred_nnupd_k M k).
Proof. by intros P P' HP; apply nnupd_k_proper. Qed.
225

226
Lemma nnupd_k_trans k P: (|=n=>_k |=n=>_k P)  (|=n=>_k P).
227
228
229
230
Proof.
  revert P.
  induction k; intros P.
  - rewrite //= ?right_id. apply wand_intro_l. 
231
    rewrite {1}(nnupd_k_intro 0 (P - False)%I) //= ?right_id. apply wand_elim_r. 
232
  - rewrite {2}(nnupd_k_unfold k P).
233
    apply and_intro.
234
235
    * rewrite (nnupd_k_unfold k P). rewrite and_elim_l.
      rewrite nnupd_k_unfold. rewrite and_elim_l.
236
      apply wand_intro_l. 
237
      rewrite {1}(nnupd_k_intro (S k) (P - ^(S k) (False)%I)).
238
239
      rewrite nnupd_k_unfold and_elim_l. apply wand_elim_r.
    * do 2 rewrite nnupd_k_weaken //.
240
241
Qed.

242
Lemma nnupd_trans P : (|=n=> |=n=> P) =n=> P.
243
244
Proof.
  split=> n x ? Hnn.
245
246
247
248
249
  eapply nnupd_nnupd_k_dist in Hnn; eauto.
  eapply (nnupd_k_ne (n) n ((|=n=>_(n) P)%I)) in Hnn; eauto;
    [| symmetry; eapply nnupd_nnupd_k_dist].
  eapply nnupd_nnupd_k_dist; eauto.
  by apply nnupd_k_trans.
250
251
Qed.

252
253
254
255
(* Now that we have shown nnupd has all of the desired properties of
   bupd, we go further and show it is in fact equivalent to bupd! The
   direction from bupd to nnupd is similar to the proof of
   nnupd_ownM_updateP *)
256

257
Lemma bupd_nnupd P: (|==> P)  |=n=> P.
258
Proof.
259
  split. rewrite /uPred_nnupd. repeat uPred.unseal. intros n x ? Hbupd a.
260
  red; rewrite //= => n' yf ??.
261
  edestruct Hbupd as (x'&?&?); eauto.
262
263
264
265
266
267
268
269
270
271
272
273
274
  case (decide (a  n')).
  - intros Hle Hwand.
    exfalso. eapply laterN_big; last (uPred.unseal; eapply (Hwand n' x')); eauto.
    * rewrite comm. done. 
    * rewrite comm. done. 
  - intros; assert (n' < a). omega.
    move: laterN_small. uPred.unseal.
    naive_solver.
Qed.

(* However, the other direction seems to need a classical axiom: *)
Section classical.
Context (not_all_not_ex:  (P : M  Prop), ¬ ( n : M, ¬ P n)   n : M, P n).
275
Lemma nnupd_bupd P:  (|=n=> P)  (|==> P).
276
Proof.
277
  rewrite /uPred_nnupd.
278
279
  split. uPred.unseal; red; rewrite //=.
  intros n x ? Hforall k yf Hle ?.
280
  apply not_all_not_ex.
281
282
283
284
285
286
287
288
289
290
  intros Hfal.
  specialize (Hforall k k).
  eapply laterN_big; last (uPred.unseal; red; rewrite //=; eapply Hforall);
    eauto.
  red; rewrite //= => n' x' ???.
  case (decide (n' = k)); intros.
  - subst. exfalso. eapply Hfal. rewrite (comm op); eauto.
  - assert (n' < k). omega.
    move: laterN_small. uPred.unseal. naive_solver.
Qed.
291
End classical.
292

293
294
(* We might wonder whether we can prove an adequacy lemma for nnupd. We could combine
   the adequacy lemma for bupd with the previous result to get adquacy for nnupd, but 
295
296
   this would rely on the classical axiom we needed to prove the equivalence! Can
   we establish adequacy without axioms? Unfortunately not, because adequacy for 
297
   nnupd would imply double negation elimination, which is classical: *)
298

299
Lemma nnupd_dne φ: (|=n=> ¬¬ φ  φ⌝: uPred M)%I.
300
Proof.
301
  rewrite /uPred_nnupd. apply forall_intro=>n.
302
303
304
  apply wand_intro_l. rewrite ?right_id. 
  assert ( φ, ¬¬¬¬φ  ¬¬φ) by naive_solver.
  assert (Hdne: ¬¬ (¬¬φ  φ)) by naive_solver.
305
  split. unseal. intros n' ?? Hupd.
306
307
308
  case (decide (n' < n)).
  - intros. move: laterN_small. unseal. naive_solver.
  - intros. assert (n  n'). omega. 
309
    exfalso. specialize (Hupd n' ).
310
311
    eapply Hdne. intros Hfal.
    eapply laterN_big; eauto. 
312
    unseal. rewrite right_id in Hupd *; naive_solver.
313
314
Qed.

315
(* Nevertheless, we can prove a weaker form of adequacy (which is equvialent to adequacy
316
   under classical axioms) directly without passing through the proofs for bupd: *)
317
318
319
320
321
Lemma adequacy_helper1 P n k x:
  {S n + k} x  ¬¬ (Nat.iter (S n) (λ P, |=n=>  P)%I P (S n + k) x) 
             ¬¬ ( x', {n + k} (x')  Nat.iter n (λ P, |=n=>  P)%I P (n + k) (x')).
Proof.
  revert k P x. induction n.
322
  - rewrite /uPred_nnupd. unseal=> k P x Hx Hf1 Hf2.
323
324
325
326
327
328
329
330
331
332
333
334
335
336
337
338
    eapply Hf1. intros Hf3.
    eapply (laterN_big (S k) (S k)); eauto.
    specialize (Hf3 (S k) (S k) ). rewrite right_id in Hf3 *. unseal.
    intros Hf3. eapply Hf3; eauto.
    intros ??? Hx'. rewrite left_id in Hx' *=> Hx'.
    unseal. 
    assert (n' < S k  n' = S k) as [|] by omega.
    * intros. move:(laterN_small n' (S k) x' False). rewrite //=. unseal. intros Hsmall. 
      eapply Hsmall; eauto.
    * subst. intros. exfalso. eapply Hf2. exists x'. split; eauto using cmra_validN_S.
  - intros k P x Hx. rewrite ?Nat_iter_S_r. 
    replace (S (S n) + k) with (S n + (S k)) by omega.
    replace (S n + k) with (n + (S k)) by omega.
    intros. eapply IHn. replace (S n + S k) with (S (S n) + k) by omega. eauto.
    rewrite ?Nat_iter_S_r. eauto.
Qed.
339

340
341
342
343
344
345
346
347
348
349
Lemma adequacy_helper2 P n k x:
  {S n + k} x  ¬¬ (Nat.iter (S n) (λ P, |=n=>  P)%I P (S n + k) x) 
             ¬¬ ( x', {k} (x')  Nat.iter 0 (λ P, |=n=>  P)%I P k (x')).
Proof.
  revert x. induction n.
  - specialize (adequacy_helper1 P 0). rewrite //=. naive_solver.
  - intros ?? Hfal%adequacy_helper1; eauto using cmra_validN_S.
    intros Hfal'. eapply Hfal. intros (x''&?&?).
    eapply IHn; eauto.
Qed.
350

351
Lemma adequacy φ n : Nat.iter n (λ P, |=n=>  P)%I ⌜φ⌝%I  ¬¬ φ.
352
Proof.
Ralf Jung's avatar
Ralf Jung committed
353
  cut ( x, {S n} x  Nat.iter n (λ P, |=n=>  P)%I ⌜φ⌝%I (S n) x  ¬¬φ).
354
355
356
357
358
359
360
361
362
  { intros help H. eapply (help ); eauto using ucmra_unit_validN.
    eapply H; try unseal; eauto using ucmra_unit_validN. red; rewrite //=. }
  destruct n.
  - rewrite //=; unseal; auto.
  - intros ??? Hfal.
    eapply (adequacy_helper2 _ n 1); (replace (S n + 1) with (S (S n)) by omega); eauto.
    unseal. intros (x'&?&Hphi). simpl in *.
    eapply Hfal. auto.
Qed.
363

364
(* Open question:
365

366
367
   Do the basic properties of the |==> modality (bupd_intro, bupd_mono, rvs_trans, rvs_frame_r,
      bupd_ownM_updateP, and adequacy) uniquely characterize |==>?
368
*)
369

370
End bupd_nnupd.