double_negation.v 14 KB
 Robbert Krebbers committed Oct 25, 2016 1 ``````From iris.base_logic Require Import base_logic. `````` Ralf Jung committed Jan 05, 2017 2 ``````Set Default Proof Using "Type". `````` Joseph Tassarotti committed Aug 28, 2016 3 `````` `````` Robbert Krebbers committed Oct 25, 2016 4 ``````(* In this file we show that the bupd can be thought of a kind of `````` Joseph Tassarotti committed Aug 28, 2016 5 `````` step-indexed double-negation when our meta-logic is classical *) `````` Robbert Krebbers committed Oct 25, 2016 6 ``````Definition uPred_nnupd {M} (P: uPred M) : uPred M := `````` Robbert Krebbers committed Nov 03, 2016 7 `````` ∀ n, (P -∗ ▷^n False) -∗ ▷^n False. `````` Joseph Tassarotti committed Aug 28, 2016 8 `````` `````` Robbert Krebbers committed Oct 25, 2016 9 ``````Notation "|=n=> Q" := (uPred_nnupd Q) `````` Joseph Tassarotti committed Aug 28, 2016 10 11 12 `````` (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. `````` Robbert Krebbers committed Nov 03, 2016 13 14 ``````Notation "P =n=∗ Q" := (P -∗ |=n=> Q)%I (at level 99, Q at level 200, format "P =n=∗ Q") : uPred_scope. `````` Joseph Tassarotti committed Aug 28, 2016 15 16 `````` (* Our goal is to prove that: `````` Robbert Krebbers committed Oct 25, 2016 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 `````` Joseph Tassarotti committed Aug 28, 2016 19 20 ``````*) `````` Robbert Krebbers committed Oct 25, 2016 21 ``````Section bupd_nnupd. `````` Joseph Tassarotti committed Aug 28, 2016 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 *) `````` Ralf Jung committed Nov 22, 2016 30 ``````Lemma laterN_big n a x φ: ✓{n} x → a ≤ n → (▷^a ⌜φ⌝)%I n x → φ. `````` Joseph Tassarotti committed Aug 28, 2016 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. `````` Ralf Jung committed Nov 22, 2016 40 ``````Lemma laterN_small n a x φ: ✓{n} x → n < a → (▷^a ⌜φ⌝)%I n x. `````` Joseph Tassarotti committed Aug 28, 2016 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. `````` Robbert Krebbers committed Oct 25, 2016 52 53 ``````(* It is easy to show that most of the basic properties of bupd that are used throughout Iris hold for nnupd. `````` Joseph Tassarotti committed Aug 31, 2016 54 55 `````` In fact, the first three properties that follow hold for any `````` Robbert Krebbers committed Nov 03, 2016 56 `````` modality of the form (- -∗ Q) -∗ Q for arbitrary Q. The situation `````` Robbert Krebbers committed Oct 25, 2016 57 `````` here is slightly different, because nnupd is of the form `````` Robbert Krebbers committed Nov 03, 2016 58 `````` ∀ n, (- -∗ (Q n)) -∗ (Q n), but the proofs carry over straightforwardly. `````` Joseph Tassarotti committed Aug 31, 2016 59 60 `````` *) `````` Joseph Tassarotti committed Aug 28, 2016 61 `````` `````` Robbert Krebbers committed Oct 25, 2016 62 ``````Lemma nnupd_intro P : P =n=> P. `````` Joseph Tassarotti committed Aug 28, 2016 63 ``````Proof. apply forall_intro=>?. apply wand_intro_l, wand_elim_l. Qed. `````` Robbert Krebbers committed Oct 25, 2016 64 ``````Lemma nnupd_mono P Q : (P ⊢ Q) → (|=n=> P) =n=> Q. `````` Joseph Tassarotti committed Aug 28, 2016 65 66 67 ``````Proof. intros HPQ. apply forall_intro=>n. apply wand_intro_l. rewrite -{1}HPQ. `````` Robbert Krebbers committed Oct 25, 2016 68 `````` rewrite /uPred_nnupd (forall_elim n). `````` Joseph Tassarotti committed Aug 28, 2016 69 70 `````` apply wand_elim_r. Qed. `````` Robbert Krebbers committed Nov 03, 2016 71 ``````Lemma nnupd_frame_r P R : (|=n=> P) ∗ R =n=> P ∗ R. `````` Joseph Tassarotti committed Aug 28, 2016 72 73 74 ``````Proof. apply forall_intro=>n. apply wand_intro_r. rewrite (comm _ P) -wand_curry. `````` Robbert Krebbers committed Oct 25, 2016 75 `````` rewrite /uPred_nnupd (forall_elim n). `````` Joseph Tassarotti committed Aug 28, 2016 76 77 `````` by rewrite -assoc wand_elim_r wand_elim_l. Qed. `````` Robbert Krebbers committed Oct 25, 2016 78 ``````Lemma nnupd_ownM_updateP x (Φ : M → Prop) : `````` Ralf Jung committed Nov 22, 2016 79 `````` x ~~>: Φ → uPred_ownM x =n=> ∃ y, ⌜Φ y⌝ ∧ uPred_ownM y. `````` Joseph Tassarotti committed Aug 31, 2016 80 ``````Proof. `````` Robbert Krebbers committed Oct 25, 2016 81 `````` intros Hbupd. split. rewrite /uPred_nnupd. repeat uPred.unseal. `````` Joseph Tassarotti committed Aug 31, 2016 82 83 84 `````` intros n y ? Hown a. red; rewrite //= => n' yf ??. inversion Hown as (x'&Hequiv). `````` Robbert Krebbers committed Oct 25, 2016 85 `````` edestruct (Hbupd n' (Some (x' ⋅ yf))) as (y'&?&?); eauto. `````` Joseph Tassarotti committed Aug 31, 2016 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 `````` Robbert Krebbers committed Nov 03, 2016 100 `````` modalities of the form (- -∗ Q) -∗ Q. What goes wrong when we quantify `````` Joseph Tassarotti committed Aug 31, 2016 101 102 103 `````` now over n? *) `````` Robbert Krebbers committed Oct 25, 2016 104 ``````Remark nnupd_trans P: (|=n=> |=n=> P) ⊢ (|=n=> P). `````` Joseph Tassarotti committed Aug 31, 2016 105 ``````Proof. `````` Robbert Krebbers committed Oct 25, 2016 106 `````` rewrite /uPred_nnupd. `````` Joseph Tassarotti committed Aug 31, 2016 107 108 `````` apply forall_intro=>a. apply wand_intro_l. rewrite (forall_elim a). `````` Robbert Krebbers committed Nov 03, 2016 109 `````` rewrite (nnupd_intro (P -∗ _)). `````` Robbert Krebbers committed Oct 25, 2016 110 `````` rewrite /uPred_nnupd. `````` Joseph Tassarotti committed Aug 31, 2016 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 `````` Robbert Krebbers committed Oct 25, 2016 115 `````` nnupd is the limit of a the following sequence: `````` Joseph Tassarotti committed Aug 31, 2016 116 `````` `````` Robbert Krebbers committed Nov 03, 2016 117 118 119 `````` (- -∗ False) - ∗ False, (- -∗ ▷ False) - ∗ ▷ False ∧ (- -∗ False) - ∗ False, (- -∗ ▷^2 False) - ∗ ▷^2 False ∧ (- -∗ ▷ False) - ∗ ▷ False ∧ (- -∗ False) - ∗ False, `````` Joseph Tassarotti committed Aug 31, 2016 120 121 122 `````` ... Then, it is easy enough to show that each of the uPreds in this sequence `````` Robbert Krebbers committed Oct 25, 2016 123 `````` is transitive. It turns out that this implies that nnupd is transitive. *) `````` Joseph Tassarotti committed Aug 31, 2016 124 125 126 `````` (* The definition of the sequence above: *) `````` Robbert Krebbers committed Oct 25, 2016 127 ``````Fixpoint uPred_nnupd_k {M} k (P: uPred M) : uPred M := `````` Robbert Krebbers committed Nov 03, 2016 128 `````` ((P -∗ ▷^k False) -∗ ▷^k False) ∧ `````` Joseph Tassarotti committed Aug 31, 2016 129 130 `````` match k with O => True `````` Robbert Krebbers committed Oct 25, 2016 131 `````` | S k' => uPred_nnupd_k k' P `````` Joseph Tassarotti committed Aug 31, 2016 132 133 `````` end. `````` Robbert Krebbers committed Oct 25, 2016 134 ``````Notation "|=n=>_ k Q" := (uPred_nnupd_k k Q) `````` Joseph Tassarotti committed Aug 31, 2016 135 136 137 `````` (at level 99, k at level 9, Q at level 200, format "|=n=>_ k Q") : uPred_scope. `````` Robbert Krebbers committed Oct 25, 2016 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. `````` Joseph Tassarotti committed Aug 28, 2016 140 ``````Proof. `````` Joseph Tassarotti committed Aug 31, 2016 141 `````` induction k. `````` Robbert Krebbers committed Oct 25, 2016 142 `````` - rewrite /uPred_nnupd_k /uPred_nnupd. `````` Joseph Tassarotti committed Aug 31, 2016 143 144 `````` rewrite (forall_elim 0) //= right_id //. - simpl. apply and_intro; auto. `````` Robbert Krebbers committed Oct 25, 2016 145 `````` rewrite /uPred_nnupd. `````` Joseph Tassarotti committed Aug 31, 2016 146 `````` rewrite (forall_elim (S k)) //=. `````` Joseph Tassarotti committed Aug 28, 2016 147 148 ``````Qed. `````` Robbert Krebbers committed Nov 03, 2016 149 ``````Lemma nnupd_k_elim n k P: n ≤ k → ((|=n=>_k P) ∗ (P -∗ (▷^n False)) ⊢ (▷^n False))%I. `````` Joseph Tassarotti committed Aug 31, 2016 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. `````` Robbert Krebbers committed Oct 25, 2016 158 ``````Lemma nnupd_k_unfold k P: `````` Robbert Krebbers committed Nov 03, 2016 159 `````` (|=n=>_(S k) P) ⊣⊢ ((P -∗ (▷^(S k) False)) -∗ (▷^(S k) False)) ∧ (|=n=>_k P). `````` Joseph Tassarotti committed Aug 31, 2016 160 ``````Proof. done. Qed. `````` Robbert Krebbers committed Oct 25, 2016 161 ``````Lemma nnupd_k_unfold' k P n x: `````` Robbert Krebbers committed Nov 03, 2016 162 `````` (|=n=>_(S k) P)%I n x ↔ (((P -∗ (▷^(S k) False)) -∗ (▷^(S k) False)) ∧ (|=n=>_k P))%I n x. `````` Joseph Tassarotti committed Aug 31, 2016 163 164 ``````Proof. done. Qed. `````` Robbert Krebbers committed Oct 25, 2016 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. `````` Joseph Tassarotti committed Aug 31, 2016 167 `````` `````` Robbert Krebbers committed Oct 25, 2016 168 ``````(* Now we are ready to show nnupd is the limit -- ie, for each k, it is within distance k `````` Joseph Tassarotti committed Aug 31, 2016 169 `````` of the kth term of the sequence *) `````` Robbert Krebbers committed Oct 25, 2016 170 ``````Lemma nnupd_nnupd_k_dist k P: (|=n=> P)%I ≡{k}≡ (|=n=>_k P)%I. `````` Joseph Tassarotti committed Aug 31, 2016 171 `````` split; intros n' x Hle Hx. split. `````` Robbert Krebbers committed Oct 25, 2016 172 `````` - by apply (nnupd_trunc1 k). `````` Joseph Tassarotti committed Aug 31, 2016 173 `````` - revert n' x Hle Hx; induction k; intros n' x Hle Hx; `````` Robbert Krebbers committed Oct 25, 2016 174 `````` rewrite ?nnupd_k_unfold' /uPred_nnupd. `````` Joseph Tassarotti committed Aug 31, 2016 175 176 177 178 179 180 181 182 183 184 185 186 187 188 189 190 191 192 `````` * 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. `````` Robbert Krebbers committed Oct 25, 2016 193 `````` **** move:nnupd_k_elim. unseal. intros Hnnupdk. `````` Joseph Tassarotti committed Aug 31, 2016 194 `````` eapply laterN_big; eauto. unseal. `````` Robbert Krebbers committed Oct 25, 2016 195 `````` eapply (Hnnupdk n k); first omega; eauto. `````` Joseph Tassarotti committed Aug 31, 2016 196 197 198 199 200 201 `````` 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. `````` Robbert Krebbers committed Oct 25, 2016 202 203 ``````(* nnupd_k has a number of structural properties, including transitivity *) Lemma nnupd_k_intro k P: P ⊢ (|=n=>_k P). `````` Joseph Tassarotti committed Aug 31, 2016 204 205 206 207 208 209 210 ``````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. `````` Robbert Krebbers committed Oct 25, 2016 211 ``````Lemma nnupd_k_mono k P Q: (P ⊢ Q) → (|=n=>_k P) ⊢ (|=n=>_k Q). `````` Joseph Tassarotti committed Aug 31, 2016 212 213 214 215 216 ``````Proof. induction k; rewrite //= ?right_id=>HPQ. - do 2 (apply wand_mono; auto). - apply and_mono; auto; do 2 (apply wand_mono; auto). Qed. `````` Robbert Krebbers committed Oct 25, 2016 217 218 ``````Instance nnupd_k_mono' k: Proper ((⊢) ==> (⊢)) (@uPred_nnupd_k M k). Proof. by intros P P' HP; apply nnupd_k_mono. Qed. `````` Joseph Tassarotti committed Aug 31, 2016 219 `````` `````` Robbert Krebbers committed Oct 25, 2016 220 ``````Instance nnupd_k_ne k n : Proper (dist n ==> dist n) (@uPred_nnupd_k M k). `````` Joseph Tassarotti committed Aug 31, 2016 221 ``````Proof. induction k; rewrite //= ?right_id=>P P' HP; by rewrite HP. Qed. `````` Robbert Krebbers committed Oct 25, 2016 222 223 224 225 ``````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. `````` Joseph Tassarotti committed Aug 31, 2016 226 `````` `````` Robbert Krebbers committed Oct 25, 2016 227 ``````Lemma nnupd_k_trans k P: (|=n=>_k |=n=>_k P) ⊢ (|=n=>_k P). `````` Joseph Tassarotti committed Aug 31, 2016 228 229 230 231 ``````Proof. revert P. induction k; intros P. - rewrite //= ?right_id. apply wand_intro_l. `````` Robbert Krebbers committed Nov 03, 2016 232 `````` rewrite {1}(nnupd_k_intro 0 (P -∗ False)%I) //= ?right_id. apply wand_elim_r. `````` Robbert Krebbers committed Oct 25, 2016 233 `````` - rewrite {2}(nnupd_k_unfold k P). `````` Joseph Tassarotti committed Aug 31, 2016 234 `````` apply and_intro. `````` Robbert Krebbers committed Oct 25, 2016 235 236 `````` * rewrite (nnupd_k_unfold k P). rewrite and_elim_l. rewrite nnupd_k_unfold. rewrite and_elim_l. `````` Joseph Tassarotti committed Aug 31, 2016 237 `````` apply wand_intro_l. `````` Robbert Krebbers committed Nov 03, 2016 238 `````` rewrite {1}(nnupd_k_intro (S k) (P -∗ ▷^(S k) (False)%I)). `````` Robbert Krebbers committed Oct 25, 2016 239 240 `````` rewrite nnupd_k_unfold and_elim_l. apply wand_elim_r. * do 2 rewrite nnupd_k_weaken //. `````` Joseph Tassarotti committed Aug 31, 2016 241 242 ``````Qed. `````` Robbert Krebbers committed Oct 25, 2016 243 ``````Lemma nnupd_trans P : (|=n=> |=n=> P) =n=> P. `````` Joseph Tassarotti committed Aug 31, 2016 244 245 ``````Proof. split=> n x ? Hnn. `````` Robbert Krebbers committed Oct 25, 2016 246 247 248 249 250 `````` 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. `````` Joseph Tassarotti committed Aug 31, 2016 251 252 ``````Qed. `````` Robbert Krebbers committed Oct 25, 2016 253 254 255 256 ``````(* 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 *) `````` Joseph Tassarotti committed Aug 31, 2016 257 `````` `````` Robbert Krebbers committed Oct 25, 2016 258 ``````Lemma bupd_nnupd P: (|==> P) ⊢ |=n=> P. `````` Joseph Tassarotti committed Aug 31, 2016 259 ``````Proof. `````` Robbert Krebbers committed Oct 25, 2016 260 `````` split. rewrite /uPred_nnupd. repeat uPred.unseal. intros n x ? Hbupd a. `````` Joseph Tassarotti committed Aug 31, 2016 261 `````` red; rewrite //= => n' yf ??. `````` Robbert Krebbers committed Oct 25, 2016 262 `````` edestruct Hbupd as (x'&?&?); eauto. `````` Joseph Tassarotti committed Aug 31, 2016 263 264 265 266 267 268 269 270 271 272 273 274 275 `````` 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). `````` Robbert Krebbers committed Oct 25, 2016 276 ``````Lemma nnupd_bupd P: (|=n=> P) ⊢ (|==> P). `````` Ralf Jung committed Jan 05, 2017 277 ``````Proof using Type*. `````` Robbert Krebbers committed Oct 25, 2016 278 `````` rewrite /uPred_nnupd. `````` Joseph Tassarotti committed Aug 28, 2016 279 280 `````` split. uPred.unseal; red; rewrite //=. intros n x ? Hforall k yf Hle ?. `````` Joseph Tassarotti committed Aug 31, 2016 281 `````` apply not_all_not_ex. `````` Joseph Tassarotti committed Aug 28, 2016 282 283 284 285 286 287 288 289 290 291 `````` 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. `````` Joseph Tassarotti committed Aug 31, 2016 292 ``````End classical. `````` Joseph Tassarotti committed Aug 28, 2016 293 `````` `````` Robbert Krebbers committed Oct 25, 2016 294 295 ``````(* 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 `````` Joseph Tassarotti committed Sep 01, 2016 296 297 `````` this would rely on the classical axiom we needed to prove the equivalence! Can we establish adequacy without axioms? Unfortunately not, because adequacy for `````` Robbert Krebbers committed Oct 25, 2016 298 `````` nnupd would imply double negation elimination, which is classical: *) `````` Joseph Tassarotti committed Sep 01, 2016 299 `````` `````` 300 ``````Lemma nnupd_dne φ: (|=n=> ⌜¬¬ φ → φ⌝: uPred M)%I. `````` Joseph Tassarotti committed Sep 01, 2016 301 ``````Proof. `````` Robbert Krebbers committed Oct 25, 2016 302 `````` rewrite /uPred_nnupd. apply forall_intro=>n. `````` Joseph Tassarotti committed Sep 01, 2016 303 304 305 `````` apply wand_intro_l. rewrite ?right_id. assert (∀ φ, ¬¬¬¬φ → ¬¬φ) by naive_solver. assert (Hdne: ¬¬ (¬¬φ → φ)) by naive_solver. `````` Robbert Krebbers committed Oct 25, 2016 306 `````` split. unseal. intros n' ?? Hupd. `````` Joseph Tassarotti committed Sep 01, 2016 307 308 309 `````` case (decide (n' < n)). - intros. move: laterN_small. unseal. naive_solver. - intros. assert (n ≤ n'). omega. `````` Robbert Krebbers committed Oct 25, 2016 310 `````` exfalso. specialize (Hupd n' ∅). `````` Joseph Tassarotti committed Sep 01, 2016 311 312 `````` eapply Hdne. intros Hfal. eapply laterN_big; eauto. `````` Robbert Krebbers committed Oct 25, 2016 313 `````` unseal. rewrite right_id in Hupd *; naive_solver. `````` Joseph Tassarotti committed Sep 01, 2016 314 315 ``````Qed. `````` Joseph Tassarotti committed Sep 07, 2016 316 ``````(* Nevertheless, we can prove a weaker form of adequacy (which is equvialent to adequacy `````` Robbert Krebbers committed Oct 25, 2016 317 `````` under classical axioms) directly without passing through the proofs for bupd: *) `````` Joseph Tassarotti committed Sep 07, 2016 318 319 320 321 322 ``````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. `````` Robbert Krebbers committed Oct 25, 2016 323 `````` - rewrite /uPred_nnupd. unseal=> k P x Hx Hf1 Hf2. `````` Joseph Tassarotti committed Sep 07, 2016 324 325 326 327 328 329 330 331 332 333 334 335 336 337 338 339 `````` 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. `````` Joseph Tassarotti committed Sep 01, 2016 340 `````` `````` Joseph Tassarotti committed Sep 07, 2016 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. `````` Joseph Tassarotti committed Aug 28, 2016 351 `````` `````` 352 ``````Lemma adequacy φ n : Nat.iter n (λ P, |=n=> ▷ P)%I ⌜φ⌝%I → ¬¬ φ. `````` Joseph Tassarotti committed Sep 07, 2016 353 ``````Proof. `````` Ralf Jung committed Nov 22, 2016 354 `````` cut (∀ x, ✓{S n} x → Nat.iter n (λ P, |=n=> ▷ P)%I ⌜φ⌝%I (S n) x → ¬¬φ). `````` Joseph Tassarotti committed Sep 07, 2016 355 356 357 358 359 360 361 362 363 `````` { 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. `````` Joseph Tassarotti committed Aug 28, 2016 364 `````` `````` Joseph Tassarotti committed Sep 07, 2016 365 ``````(* Open question: `````` Joseph Tassarotti committed Aug 31, 2016 366 `````` `````` Robbert Krebbers committed Oct 25, 2016 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 |==>? `````` Joseph Tassarotti committed Sep 07, 2016 369 ``````*) `````` Joseph Tassarotti committed Aug 31, 2016 370 `````` `````` Robbert Krebbers committed Oct 25, 2016 371 ``End bupd_nnupd.``