double_negation.v 14.1 KB
Newer Older
1
From iris.base_logic Require Import base_logic.
2
Set Default Proof Using "Type".
3

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

9
Notation "|=n=> Q" := (uPred_nnupd Q)
Robbert Krebbers's avatar
Robbert Krebbers committed
10
  (at level 99, Q at level 200, format "|=n=>  Q") : bi_scope.
11 12
Notation "P =n=> Q" := (P  |=n=> Q)
  (at level 99, Q at level 200, only parsing) : C_scope.
13
Notation "P =n=∗ Q" := (P - |=n=> Q)%I
Robbert Krebbers's avatar
Robbert Krebbers committed
14
  (at level 99, Q at level 200, format "P  =n=∗  Q") : bi_scope.
15 16

(* Our goal is to prove that:
17 18
  (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
19 20
*)

21
Section bupd_nnupd.
22 23 24 25 26 27 28 29
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 *)
Robbert Krebbers's avatar
Robbert Krebbers committed
30
Lemma laterN_big n a x φ: {n} x   a  n  (^a ⌜φ⌝ : uPred M)%I n x  φ.
31 32 33 34 35 36 37 38 39
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.

Robbert Krebbers's avatar
Robbert Krebbers committed
40
Lemma laterN_small n a x φ: {n} x   n < a  (^a ⌜φ⌝ : uPred M)%I n x.
41 42 43 44 45 46 47 48 49 50 51
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.

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

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

 *)
61

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

104
Remark nnupd_trans P: (|=n=> |=n=> P)  (|=n=> P).
105
Proof.
106
  rewrite /uPred_nnupd.
107 108
  apply forall_intro=>a. apply wand_intro_l.
  rewrite (forall_elim a).
109
  rewrite (nnupd_intro (P - _)).
110
  rewrite /uPred_nnupd.
111 112 113 114
  (* 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 
115
   nnupd is the limit of a the following sequence:
116

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

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

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

134
Notation "|=n=>_ k Q" := (uPred_nnupd_k k Q)
Robbert Krebbers's avatar
Robbert Krebbers committed
135
  (at level 99, k at level 9, Q at level 200, format "|=n=>_ k  Q") : bi_scope.
136 137


138 139
(* 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.
140
Proof.
141
  induction k. 
142
  - rewrite /uPred_nnupd_k /uPred_nnupd. 
143 144
    rewrite (forall_elim 0) //= right_id //.
  - simpl. apply and_intro; auto.
145
    rewrite /uPred_nnupd. 
146
    rewrite (forall_elim (S k)) //=.
147 148
Qed.

149
Lemma nnupd_k_elim n k P: n  k  ((|=n=>_k P)  (P - (^n False))   (^n False))%I.
150 151 152 153 154 155 156 157
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.

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

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

168
(* Now we are ready to show nnupd is the limit -- ie, for each k, it is within distance k
169
   of the kth term of the sequence *)
170
Lemma nnupd_nnupd_k_dist k P: (|=n=> P)%I {k} (|=n=>_k P)%I.
171
  split; intros n' x Hle Hx. split.
172
  - by apply (nnupd_trunc1 k).
173
  - revert n' x Hle Hx; induction k; intros n' x Hle Hx;
174
      rewrite ?nnupd_k_unfold' /uPred_nnupd.
175 176 177 178 179 180 181 182 183 184 185
    * 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.
Robbert Krebbers's avatar
Robbert Krebbers committed
186
    * inversion Hle; simpl; subst.
187 188 189 190 191
      ** 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.
Robbert Krebbers's avatar
Robbert Krebbers committed
192 193
             **** eapply laterN_big; eauto; unseal.
                  eapply HnnP; eauto. move: HPF; by unseal.
194
             **** move:nnupd_k_elim. unseal. intros Hnnupdk. 
195
                  eapply laterN_big; eauto. unseal.
196
                  eapply (Hnnupdk n k); first omega; eauto.
197 198 199 200 201 202
                  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.

203 204
(* nnupd_k has a number of structural properties, including transitivity *)
Lemma nnupd_k_intro k P: P  (|=n=>_k P).
205 206 207 208 209 210 211
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.

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

221 222
Instance nnupd_k_ne k : NonExpansive (@uPred_nnupd_k M k).
Proof. intros n. induction k; rewrite //= ?right_id=>P P' HP; by rewrite HP. Qed.
223 224 225 226
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.
227

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

244
Lemma nnupd_trans P : (|=n=> |=n=> P) =n=> P.
245 246
Proof.
  split=> n x ? Hnn.
247 248 249 250 251
  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.
252 253
Qed.

254 255 256 257
(* 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 *)
258

259
Lemma bupd_nnupd P: (|==> P)  |=n=> P.
260
Proof.
261
  split. rewrite /uPred_nnupd. repeat uPred.unseal. intros n x ? Hbupd a.
262
  red; rewrite //= => n' yf ??.
263
  edestruct Hbupd as (x'&?&?); eauto.
264 265 266 267 268 269 270 271 272 273 274 275 276
  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).
277
Lemma nnupd_bupd P:  (|=n=> P)  (|==> P).
278
Proof using Type*.
279
  rewrite /uPred_nnupd.
280 281
  split. uPred.unseal; red; rewrite //=.
  intros n x ? Hforall k yf Hle ?.
282
  apply not_all_not_ex.
283 284 285 286 287 288 289 290 291 292
  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.
293
End classical.
294

295 296
(* 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 
297 298
   this would rely on the classical axiom we needed to prove the equivalence! Can
   we establish adequacy without axioms? Unfortunately not, because adequacy for 
299
   nnupd would imply double negation elimination, which is classical: *)
300

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

317
(* Nevertheless, we can prove a weaker form of adequacy (which is equvialent to adequacy
318
   under classical axioms) directly without passing through the proofs for bupd: *)
319 320 321 322 323
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.
324
  - rewrite /uPred_nnupd. unseal=> k P x Hx Hf1 Hf2.
325 326
    eapply Hf1. intros Hf3.
    eapply (laterN_big (S k) (S k)); eauto.
Robbert Krebbers's avatar
Robbert Krebbers committed
327
    specialize (Hf3 (S k) (S k) ε). rewrite right_id in Hf3 *. unseal.
328 329 330 331 332 333 334 335 336 337 338 339
    intros Hf3. eapply Hf3; eauto.
    intros ??? Hx'. rewrite left_id in Hx' *=> Hx'.
    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.
340

341 342 343 344 345 346 347 348 349 350
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.
351

352
Lemma adequacy φ n : Nat.iter n (λ P, |=n=>  P)%I ⌜φ⌝%I  ¬¬ φ.
353
Proof.
Ralf Jung's avatar
Ralf Jung committed
354
  cut ( x, {S n} x  Nat.iter n (λ P, |=n=>  P)%I ⌜φ⌝%I (S n) x  ¬¬φ).
355
  { intros help H. eapply (help ); eauto using ucmra_unit_validN.
Robbert Krebbers's avatar
Robbert Krebbers committed
356
    eapply H; eauto using ucmra_unit_validN. by unseal. }
357 358 359 360 361 362 363
  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.
364

365
(* Open question:
366

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

371
End bupd_nnupd.