double_negation.v 14.4 KB
Newer Older
1
From iris.base_logic Require Import base_logic.
2 3
Import upred.

4
(* In this file we show that the bupd can be thought of a kind of
5 6 7 8 9 10 11 12 13 14
   step-indexed double-negation when our meta-logic is classical *)

(* To define this, we need a way to talk about iterated later modalities: *)
Definition uPred_laterN {M} (n : nat) (P : uPred M) : uPred M :=
  Nat.iter n uPred_later P.
Instance: Params (@uPred_laterN) 2.
Notation "▷^ n P" := (uPred_laterN n P)
  (at level 20, n at level 9, right associativity,
   format "▷^ n  P") : uPred_scope.

15
Definition uPred_nnupd {M} (P: uPred M) : uPred M :=
16
   n, (P - ^n False) - ^n False.
17

18
Notation "|=n=> Q" := (uPred_nnupd Q)
19 20 21
  (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.
22 23
Notation "P =n=∗ Q" := (P - |=n=> Q)%I
  (at level 99, Q at level 200, format "P  =n=∗  Q") : uPred_scope.
24 25

(* Our goal is to prove that:
26 27
  (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
28 29
*)

30
Section bupd_nnupd.
31 32 33 34 35 36 37 38 39 40 41 42 43 44 45 46 47 48 49 50 51 52 53 54 55 56 57 58 59 60
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 *)
Lemma laterN_big n a x φ: {n} x   a  n  (^a ( φ))%I n x  φ.
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.

Lemma laterN_small n a x φ: {n} x   n < a  (^a ( φ))%I n x.
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.

61 62
(* It is easy to show that most of the basic properties of bupd that
   are used throughout Iris hold for nnupd. 
63 64

   In fact, the first three properties that follow hold for any
65
   modality of the form (- -∗ Q) -∗ Q for arbitrary Q. The situation
66
   here is slightly different, because nnupd is of the form 
67
   ∀ n, (- -∗ (Q n)) -∗ (Q n), but the proofs carry over straightforwardly.
68 69

 *)
70

71
Lemma nnupd_intro P : P =n=> P.
72
Proof. apply forall_intro=>?. apply wand_intro_l, wand_elim_l. Qed.
73
Lemma nnupd_mono P Q : (P  Q)  (|=n=> P) =n=> Q.
74 75 76
Proof.
  intros HPQ. apply forall_intro=>n.
  apply wand_intro_l.  rewrite -{1}HPQ.
77
  rewrite /uPred_nnupd (forall_elim n).
78 79
  apply wand_elim_r.
Qed.
80
Lemma nnupd_frame_r P R : (|=n=> P)  R =n=> P  R.
81 82 83
Proof.
  apply forall_intro=>n. apply wand_intro_r.
  rewrite (comm _ P) -wand_curry.
84
  rewrite /uPred_nnupd (forall_elim n).
85 86
  by rewrite -assoc wand_elim_r wand_elim_l.
Qed.
87
Lemma nnupd_ownM_updateP x (Φ : M  Prop) :
88
  x ~~>: Φ  uPred_ownM x =n=>  y,  Φ y  uPred_ownM y.
89
Proof. 
90
  intros Hbupd. split. rewrite /uPred_nnupd. repeat uPred.unseal. 
91 92 93
  intros n y ? Hown a.
  red; rewrite //= => n' yf ??.
  inversion Hown as (x'&Hequiv).
94
  edestruct (Hbupd n' (Some (x'  yf))) as (y'&?&?); eauto.
95 96 97 98 99 100 101 102 103 104 105 106 107 108
  { 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 
109
   modalities of the form (- -∗ Q) -∗ Q. What goes wrong when we quantify
110 111 112
   now over n? 
 *)

113
Remark nnupd_trans P: (|=n=> |=n=> P)  (|=n=> P).
114
Proof.
115
  rewrite /uPred_nnupd.
116 117
  apply forall_intro=>a. apply wand_intro_l.
  rewrite (forall_elim a).
118
  rewrite (nnupd_intro (P - _)).
119
  rewrite /uPred_nnupd.
120 121 122 123
  (* 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 
124
   nnupd is the limit of a the following sequence:
125

126 127 128
   (- -∗ False) - ∗ False,
   (- -∗ ▷ False) - ∗ ▷ False ∧ (- -∗ False) - ∗ False,
   (- -∗ ▷^2 False) - ∗ ▷^2 False ∧ (- -∗ ▷ False) - ∗ ▷ False ∧ (- -∗ False) - ∗ False,
129 130 131
   ...

   Then, it is easy enough to show that each of the uPreds in this sequence
132
   is transitive. It turns out that this implies that nnupd is transitive. *)
133 134 135
   

(* The definition of the sequence above: *)
136
Fixpoint uPred_nnupd_k {M} k (P: uPred M) : uPred M :=
137
  ((P - ^k False) - ^k False) 
138 139
  match k with 
    O => True
140
  | S k' => uPred_nnupd_k k' P
141 142
  end.

143
Notation "|=n=>_ k Q" := (uPred_nnupd_k k Q)
144 145 146
  (at level 99, k at level 9, Q at level 200, format "|=n=>_ k  Q") : uPred_scope.


147 148
(* 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.
149
Proof.
150
  induction k. 
151
  - rewrite /uPred_nnupd_k /uPred_nnupd. 
152 153
    rewrite (forall_elim 0) //= right_id //.
  - simpl. apply and_intro; auto.
154
    rewrite /uPred_nnupd. 
155
    rewrite (forall_elim (S k)) //=.
156 157
Qed.

158
Lemma nnupd_k_elim n k P: n  k  ((|=n=>_k P)  (P - (^n False))   (^n False))%I.
159 160 161 162 163 164 165 166
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.

167
Lemma nnupd_k_unfold k P:
168
  (|=n=>_(S k) P)  ((P - (^(S k) False)) - (^(S k) False))  (|=n=>_k P).
169
Proof. done.  Qed.
170
Lemma nnupd_k_unfold' k P n x:
171
  (|=n=>_(S k) P)%I n x  (((P - (^(S k) False)) - (^(S k) False))  (|=n=>_k P))%I n x.
172 173
Proof. done.  Qed.

174 175
Lemma nnupd_k_weaken k P: (|=n=>_(S k) P)  |=n=>_k P.
Proof. by rewrite nnupd_k_unfold and_elim_r. Qed.
176

177
(* Now we are ready to show nnupd is the limit -- ie, for each k, it is within distance k
178
   of the kth term of the sequence *)
179
Lemma nnupd_nnupd_k_dist k P: (|=n=> P)%I {k} (|=n=>_k P)%I.
180
  split; intros n' x Hle Hx. split.
181
  - by apply (nnupd_trunc1 k).
182
  - revert n' x Hle Hx; induction k; intros n' x Hle Hx;
183
      rewrite ?nnupd_k_unfold' /uPred_nnupd.
184 185 186 187 188 189 190 191 192 193 194 195 196 197 198 199 200 201
    * 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.
202
             **** move:nnupd_k_elim. unseal. intros Hnnupdk. 
203
                  eapply laterN_big; eauto. unseal.
204
                  eapply (Hnnupdk n k); first omega; eauto.
205 206 207 208 209 210
                  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.

211 212
(* nnupd_k has a number of structural properties, including transitivity *)
Lemma nnupd_k_intro k P: P  (|=n=>_k P).
213 214 215 216 217 218 219
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.

220
Lemma nnupd_k_mono k P Q: (P  Q)  (|=n=>_k P)  (|=n=>_k Q).
221 222 223 224 225
Proof.
  induction k; rewrite //= ?right_id=>HPQ. 
  - do 2 (apply wand_mono; auto).
  - apply and_mono; auto; do 2 (apply wand_mono; auto).
Qed.
226 227
Instance nnupd_k_mono' k: Proper (() ==> ()) (@uPred_nnupd_k M k).
Proof. by intros P P' HP; apply nnupd_k_mono. Qed.
228

229
Instance nnupd_k_ne k n : Proper (dist n ==> dist n) (@uPred_nnupd_k M k).
230
Proof. induction k; rewrite //= ?right_id=>P P' HP; by rewrite HP. Qed.
231 232 233 234
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.
235

236
Lemma nnupd_k_trans k P: (|=n=>_k |=n=>_k P)  (|=n=>_k P).
237 238 239 240
Proof.
  revert P.
  induction k; intros P.
  - rewrite //= ?right_id. apply wand_intro_l. 
241
    rewrite {1}(nnupd_k_intro 0 (P - False)%I) //= ?right_id. apply wand_elim_r. 
242
  - rewrite {2}(nnupd_k_unfold k P).
243
    apply and_intro.
244 245
    * rewrite (nnupd_k_unfold k P). rewrite and_elim_l.
      rewrite nnupd_k_unfold. rewrite and_elim_l.
246
      apply wand_intro_l. 
247
      rewrite {1}(nnupd_k_intro (S k) (P - ^(S k) (False)%I)).
248 249
      rewrite nnupd_k_unfold and_elim_l. apply wand_elim_r.
    * do 2 rewrite nnupd_k_weaken //.
250 251
Qed.

252
Lemma nnupd_trans P : (|=n=> |=n=> P) =n=> P.
253 254
Proof.
  split=> n x ? Hnn.
255 256 257 258 259
  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.
260 261
Qed.

262 263 264 265
(* 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 *)
266

267
Lemma bupd_nnupd P: (|==> P)  |=n=> P.
268
Proof.
269
  split. rewrite /uPred_nnupd. repeat uPred.unseal. intros n x ? Hbupd a.
270
  red; rewrite //= => n' yf ??.
271
  edestruct Hbupd as (x'&?&?); eauto.
272 273 274 275 276 277 278 279 280 281 282 283 284
  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).
285
Lemma nnupd_bupd P:  (|=n=> P)  (|==> P).
286
Proof.
287
  rewrite /uPred_nnupd.
288 289
  split. uPred.unseal; red; rewrite //=.
  intros n x ? Hforall k yf Hle ?.
290
  apply not_all_not_ex.
291 292 293 294 295 296 297 298 299 300
  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.
301
End classical.
302

303 304
(* 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 
305 306
   this would rely on the classical axiom we needed to prove the equivalence! Can
   we establish adequacy without axioms? Unfortunately not, because adequacy for 
307
   nnupd would imply double negation elimination, which is classical: *)
308

309
Lemma nnupd_dne φ: True  (|=n=> ((¬¬ φ  φ)): uPred M)%I.
310
Proof.
311
  rewrite /uPred_nnupd. apply forall_intro=>n.
312 313 314
  apply wand_intro_l. rewrite ?right_id. 
  assert ( φ, ¬¬¬¬φ  ¬¬φ) by naive_solver.
  assert (Hdne: ¬¬ (¬¬φ  φ)) by naive_solver.
315
  split. unseal. intros n' ?? Hupd.
316 317 318
  case (decide (n' < n)).
  - intros. move: laterN_small. unseal. naive_solver.
  - intros. assert (n  n'). omega. 
319
    exfalso. specialize (Hupd n' ).
320 321
    eapply Hdne. intros Hfal.
    eapply laterN_big; eauto. 
322
    unseal. rewrite right_id in Hupd *; naive_solver.
323 324
Qed.

325
(* Nevertheless, we can prove a weaker form of adequacy (which is equvialent to adequacy
326
   under classical axioms) directly without passing through the proofs for bupd: *)
327 328 329 330 331
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.
332
  - rewrite /uPred_nnupd. unseal=> k P x Hx Hf1 Hf2.
333 334 335 336 337 338 339 340 341 342 343 344 345 346 347 348
    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.
349

350 351 352 353 354 355 356 357 358 359
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.
360

361 362 363 364 365 366 367 368 369 370 371 372
Lemma adequacy φ n : (True  Nat.iter n (λ P, |=n=>  P) ( φ))  ¬¬ φ.
Proof.
  cut ( x, {S n} x  Nat.iter n (λ P, |=n=>  P)%I ( φ)%I (S n) x  ¬¬φ).
  { 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.
373

374
(* Open question:
375

376 377
   Do the basic properties of the |==> modality (bupd_intro, bupd_mono, rvs_trans, rvs_frame_r,
      bupd_ownM_updateP, and adequacy) uniquely characterize |==>?
378
*)
379

380
End bupd_nnupd.