double_negation.v 14.4 KB
 Joseph Tassarotti committed Aug 28, 2016 1 2 3 ``````From iris.algebra Require Import upred. Import upred. `````` 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 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. `````` Robbert Krebbers committed Oct 25, 2016 15 ``````Definition uPred_nnupd {M} (P: uPred M) : uPred M := `````` Joseph Tassarotti committed Aug 28, 2016 16 17 `````` ∀ n, (P -★ ▷^n False) -★ ▷^n False. `````` Robbert Krebbers committed Oct 25, 2016 18 ``````Notation "|=n=> Q" := (uPred_nnupd Q) `````` Joseph Tassarotti committed Aug 28, 2016 19 20 21 22 23 24 25 26 27 28 29 `````` (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. Notation "P =n=★ Q" := (P -★ |=n=> Q)%I (at level 99, Q at level 200, format "P =n=★ Q") : uPred_scope. (* Our goal is to prove that: (1) |=n=> has (nearly) all the properties of the |=r=> modality that are used in Iris (2) If our meta-logic is classical, then |=n=> and |=r=> are equivalent *) `````` Robbert Krebbers committed Oct 25, 2016 30 ``````Section bupd_nnupd. `````` Joseph Tassarotti committed Aug 28, 2016 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. `````` Robbert Krebbers committed Oct 25, 2016 61 62 ``````(* 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 63 64 65 `````` In fact, the first three properties that follow hold for any modality of the form (- -★ Q) -★ Q for arbitrary Q. The situation `````` Robbert Krebbers committed Oct 25, 2016 66 `````` here is slightly different, because nnupd is of the form `````` Joseph Tassarotti committed Aug 31, 2016 67 68 69 `````` ∀ n, (- -★ (Q n)) -★ (Q n), but the proofs carry over straightforwardly. *) `````` Joseph Tassarotti committed Aug 28, 2016 70 `````` `````` Robbert Krebbers committed Oct 25, 2016 71 ``````Lemma nnupd_intro P : P =n=> P. `````` Joseph Tassarotti committed Aug 28, 2016 72 ``````Proof. apply forall_intro=>?. apply wand_intro_l, wand_elim_l. Qed. `````` Robbert Krebbers committed Oct 25, 2016 73 ``````Lemma nnupd_mono P Q : (P ⊢ Q) → (|=n=> P) =n=> Q. `````` Joseph Tassarotti committed Aug 28, 2016 74 75 76 ``````Proof. intros HPQ. apply forall_intro=>n. apply wand_intro_l. rewrite -{1}HPQ. `````` Robbert Krebbers committed Oct 25, 2016 77 `````` rewrite /uPred_nnupd (forall_elim n). `````` Joseph Tassarotti committed Aug 28, 2016 78 79 `````` apply wand_elim_r. Qed. `````` Robbert Krebbers committed Oct 25, 2016 80 ``````Lemma nnupd_frame_r P R : (|=n=> P) ★ R =n=> P ★ R. `````` Joseph Tassarotti committed Aug 28, 2016 81 82 83 ``````Proof. apply forall_intro=>n. apply wand_intro_r. rewrite (comm _ P) -wand_curry. `````` Robbert Krebbers committed Oct 25, 2016 84 `````` rewrite /uPred_nnupd (forall_elim n). `````` Joseph Tassarotti committed Aug 28, 2016 85 86 `````` by rewrite -assoc wand_elim_r wand_elim_l. Qed. `````` Robbert Krebbers committed Oct 25, 2016 87 ``````Lemma nnupd_ownM_updateP x (Φ : M → Prop) : `````` Joseph Tassarotti committed Aug 28, 2016 88 `````` x ~~>: Φ → uPred_ownM x =n=> ∃ y, ■ Φ y ∧ uPred_ownM y. `````` Joseph Tassarotti committed Aug 31, 2016 89 ``````Proof. `````` Robbert Krebbers committed Oct 25, 2016 90 `````` intros Hbupd. split. rewrite /uPred_nnupd. repeat uPred.unseal. `````` Joseph Tassarotti committed Aug 31, 2016 91 92 93 `````` intros n y ? Hown a. red; rewrite //= => n' yf ??. inversion Hown as (x'&Hequiv). `````` Robbert Krebbers committed Oct 25, 2016 94 `````` edestruct (Hbupd n' (Some (x' ⋅ yf))) as (y'&?&?); eauto. `````` Joseph Tassarotti committed Aug 31, 2016 95 96 97 98 99 100 101 102 103 104 105 106 107 108 109 110 111 112 `````` { 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 modalities of the form (- -★ Q) -★ Q. What goes wrong when we quantify now over n? *) `````` Robbert Krebbers committed Oct 25, 2016 113 ``````Remark nnupd_trans P: (|=n=> |=n=> P) ⊢ (|=n=> P). `````` Joseph Tassarotti committed Aug 31, 2016 114 ``````Proof. `````` Robbert Krebbers committed Oct 25, 2016 115 `````` rewrite /uPred_nnupd. `````` Joseph Tassarotti committed Aug 31, 2016 116 117 `````` apply forall_intro=>a. apply wand_intro_l. rewrite (forall_elim a). `````` Robbert Krebbers committed Oct 25, 2016 118 119 `````` rewrite (nnupd_intro (P -★ _)). rewrite /uPred_nnupd. `````` Joseph Tassarotti committed Aug 31, 2016 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 `````` Robbert Krebbers committed Oct 25, 2016 124 `````` nnupd is the limit of a the following sequence: `````` Joseph Tassarotti committed Aug 31, 2016 125 126 127 128 129 130 131 `````` (- -★ False) - ★ False, (- -★ ▷ False) - ★ ▷ False ∧ (- -★ False) - ★ False, (- -★ ▷^2 False) - ★ ▷^2 False ∧ (- -★ ▷ False) - ★ ▷ False ∧ (- -★ False) - ★ False, ... Then, it is easy enough to show that each of the uPreds in this sequence `````` Robbert Krebbers committed Oct 25, 2016 132 `````` is transitive. It turns out that this implies that nnupd is transitive. *) `````` Joseph Tassarotti committed Aug 31, 2016 133 134 135 `````` (* The definition of the sequence above: *) `````` Robbert Krebbers committed Oct 25, 2016 136 ``````Fixpoint uPred_nnupd_k {M} k (P: uPred M) : uPred M := `````` Joseph Tassarotti committed Aug 31, 2016 137 138 139 `````` ((P -★ ▷^k False) -★ ▷^k False) ∧ match k with O => True `````` Robbert Krebbers committed Oct 25, 2016 140 `````` | S k' => uPred_nnupd_k k' P `````` Joseph Tassarotti committed Aug 31, 2016 141 142 `````` end. `````` Robbert Krebbers committed Oct 25, 2016 143 ``````Notation "|=n=>_ k Q" := (uPred_nnupd_k k Q) `````` Joseph Tassarotti committed Aug 31, 2016 144 145 146 `````` (at level 99, k at level 9, Q at level 200, format "|=n=>_ k Q") : uPred_scope. `````` Robbert Krebbers committed Oct 25, 2016 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. `````` Joseph Tassarotti committed Aug 28, 2016 149 ``````Proof. `````` Joseph Tassarotti committed Aug 31, 2016 150 `````` induction k. `````` Robbert Krebbers committed Oct 25, 2016 151 `````` - rewrite /uPred_nnupd_k /uPred_nnupd. `````` Joseph Tassarotti committed Aug 31, 2016 152 153 `````` rewrite (forall_elim 0) //= right_id //. - simpl. apply and_intro; auto. `````` Robbert Krebbers committed Oct 25, 2016 154 `````` rewrite /uPred_nnupd. `````` Joseph Tassarotti committed Aug 31, 2016 155 `````` rewrite (forall_elim (S k)) //=. `````` Joseph Tassarotti committed Aug 28, 2016 156 157 ``````Qed. `````` Robbert Krebbers committed Oct 25, 2016 158 ``````Lemma nnupd_k_elim n k P: n ≤ k → ((|=n=>_k P) ★ (P -★ (▷^n False)) ⊢ (▷^n False))%I. `````` Joseph Tassarotti committed Aug 31, 2016 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. `````` Robbert Krebbers committed Oct 25, 2016 167 ``````Lemma nnupd_k_unfold k P: `````` Joseph Tassarotti committed Aug 31, 2016 168 169 `````` (|=n=>_(S k) P) ⊣⊢ ((P -★ (▷^(S k) False)) -★ (▷^(S k) False)) ∧ (|=n=>_k P). Proof. done. Qed. `````` Robbert Krebbers committed Oct 25, 2016 170 ``````Lemma nnupd_k_unfold' k P n x: `````` Joseph Tassarotti committed Aug 31, 2016 171 172 173 `````` (|=n=>_(S k) P)%I n x ↔ (((P -★ (▷^(S k) False)) -★ (▷^(S k) False)) ∧ (|=n=>_k P))%I n x. Proof. done. Qed. `````` Robbert Krebbers committed Oct 25, 2016 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. `````` Joseph Tassarotti committed Aug 31, 2016 176 `````` `````` Robbert Krebbers committed Oct 25, 2016 177 ``````(* 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 178 `````` of the kth term of the sequence *) `````` Robbert Krebbers committed Oct 25, 2016 179 ``````Lemma nnupd_nnupd_k_dist k P: (|=n=> P)%I ≡{k}≡ (|=n=>_k P)%I. `````` Joseph Tassarotti committed Aug 31, 2016 180 `````` split; intros n' x Hle Hx. split. `````` Robbert Krebbers committed Oct 25, 2016 181 `````` - by apply (nnupd_trunc1 k). `````` Joseph Tassarotti committed Aug 31, 2016 182 `````` - revert n' x Hle Hx; induction k; intros n' x Hle Hx; `````` Robbert Krebbers committed Oct 25, 2016 183 `````` rewrite ?nnupd_k_unfold' /uPred_nnupd. `````` Joseph Tassarotti committed Aug 31, 2016 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. `````` Robbert Krebbers committed Oct 25, 2016 202 `````` **** move:nnupd_k_elim. unseal. intros Hnnupdk. `````` Joseph Tassarotti committed Aug 31, 2016 203 `````` eapply laterN_big; eauto. unseal. `````` Robbert Krebbers committed Oct 25, 2016 204 `````` eapply (Hnnupdk n k); first omega; eauto. `````` Joseph Tassarotti committed Aug 31, 2016 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. `````` Robbert Krebbers committed Oct 25, 2016 211 212 ``````(* 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 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. `````` Robbert Krebbers committed Oct 25, 2016 220 ``````Lemma nnupd_k_mono k P Q: (P ⊢ Q) → (|=n=>_k P) ⊢ (|=n=>_k Q). `````` Joseph Tassarotti committed Aug 31, 2016 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. `````` Robbert Krebbers committed Oct 25, 2016 226 227 ``````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 228 `````` `````` Robbert Krebbers committed Oct 25, 2016 229 ``````Instance nnupd_k_ne k n : Proper (dist n ==> dist n) (@uPred_nnupd_k M k). `````` Joseph Tassarotti committed Aug 31, 2016 230 ``````Proof. induction k; rewrite //= ?right_id=>P P' HP; by rewrite HP. Qed. `````` Robbert Krebbers committed Oct 25, 2016 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. `````` Joseph Tassarotti committed Aug 31, 2016 235 `````` `````` Robbert Krebbers committed Oct 25, 2016 236 ``````Lemma nnupd_k_trans k P: (|=n=>_k |=n=>_k P) ⊢ (|=n=>_k P). `````` Joseph Tassarotti committed Aug 31, 2016 237 238 239 240 ``````Proof. revert P. induction k; intros P. - rewrite //= ?right_id. apply wand_intro_l. `````` Robbert Krebbers committed Oct 25, 2016 241 242 `````` rewrite {1}(nnupd_k_intro 0 (P -★ False)%I) //= ?right_id. apply wand_elim_r. - rewrite {2}(nnupd_k_unfold k P). `````` Joseph Tassarotti committed Aug 31, 2016 243 `````` apply and_intro. `````` Robbert Krebbers committed Oct 25, 2016 244 245 `````` * rewrite (nnupd_k_unfold k P). rewrite and_elim_l. rewrite nnupd_k_unfold. rewrite and_elim_l. `````` Joseph Tassarotti committed Aug 31, 2016 246 `````` apply wand_intro_l. `````` Robbert Krebbers committed Oct 25, 2016 247 248 249 `````` rewrite {1}(nnupd_k_intro (S k) (P -★ ▷^(S k) (False)%I)). rewrite nnupd_k_unfold and_elim_l. apply wand_elim_r. * do 2 rewrite nnupd_k_weaken //. `````` Joseph Tassarotti committed Aug 31, 2016 250 251 ``````Qed. `````` Robbert Krebbers committed Oct 25, 2016 252 ``````Lemma nnupd_trans P : (|=n=> |=n=> P) =n=> P. `````` Joseph Tassarotti committed Aug 31, 2016 253 254 ``````Proof. split=> n x ? Hnn. `````` Robbert Krebbers committed Oct 25, 2016 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. `````` Joseph Tassarotti committed Aug 31, 2016 260 261 ``````Qed. `````` Robbert Krebbers committed Oct 25, 2016 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 *) `````` Joseph Tassarotti committed Aug 31, 2016 266 `````` `````` Robbert Krebbers committed Oct 25, 2016 267 ``````Lemma bupd_nnupd P: (|=r=> P) ⊢ |=n=> P. `````` Joseph Tassarotti committed Aug 31, 2016 268 ``````Proof. `````` Robbert Krebbers committed Oct 25, 2016 269 `````` split. rewrite /uPred_nnupd. repeat uPred.unseal. intros n x ? Hbupd a. `````` Joseph Tassarotti committed Aug 31, 2016 270 `````` red; rewrite //= => n' yf ??. `````` Robbert Krebbers committed Oct 25, 2016 271 `````` edestruct Hbupd as (x'&?&?); eauto. `````` Joseph Tassarotti committed Aug 31, 2016 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). `````` Robbert Krebbers committed Oct 25, 2016 285 ``````Lemma nnupd_bupd P: (|=n=> P) ⊢ (|=r=> P). `````` Joseph Tassarotti committed Aug 28, 2016 286 ``````Proof. `````` Robbert Krebbers committed Oct 25, 2016 287 `````` rewrite /uPred_nnupd. `````` Joseph Tassarotti committed Aug 28, 2016 288 289 `````` split. uPred.unseal; red; rewrite //=. intros n x ? Hforall k yf Hle ?. `````` Joseph Tassarotti committed Aug 31, 2016 290 `````` apply not_all_not_ex. `````` Joseph Tassarotti committed Aug 28, 2016 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. `````` Joseph Tassarotti committed Aug 31, 2016 301 ``````End classical. `````` Joseph Tassarotti committed Aug 28, 2016 302 `````` `````` Robbert Krebbers committed Oct 25, 2016 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 `````` Joseph Tassarotti committed Sep 01, 2016 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 `````` Robbert Krebbers committed Oct 25, 2016 307 `````` nnupd would imply double negation elimination, which is classical: *) `````` Joseph Tassarotti committed Sep 01, 2016 308 `````` `````` Robbert Krebbers committed Oct 25, 2016 309 ``````Lemma nnupd_dne φ: True ⊢ (|=n=> (■(¬¬ φ → φ)): uPred M)%I. `````` Joseph Tassarotti committed Sep 01, 2016 310 ``````Proof. `````` Robbert Krebbers committed Oct 25, 2016 311 `````` rewrite /uPred_nnupd. apply forall_intro=>n. `````` Joseph Tassarotti committed Sep 01, 2016 312 313 314 `````` apply wand_intro_l. rewrite ?right_id. assert (∀ φ, ¬¬¬¬φ → ¬¬φ) by naive_solver. assert (Hdne: ¬¬ (¬¬φ → φ)) by naive_solver. `````` Robbert Krebbers committed Oct 25, 2016 315 `````` split. unseal. intros n' ?? Hupd. `````` Joseph Tassarotti committed Sep 01, 2016 316 317 318 `````` case (decide (n' < n)). - intros. move: laterN_small. unseal. naive_solver. - intros. assert (n ≤ n'). omega. `````` Robbert Krebbers committed Oct 25, 2016 319 `````` exfalso. specialize (Hupd n' ∅). `````` Joseph Tassarotti committed Sep 01, 2016 320 321 `````` eapply Hdne. intros Hfal. eapply laterN_big; eauto. `````` Robbert Krebbers committed Oct 25, 2016 322 `````` unseal. rewrite right_id in Hupd *; naive_solver. `````` Joseph Tassarotti committed Sep 01, 2016 323 324 ``````Qed. `````` Joseph Tassarotti committed Sep 07, 2016 325 ``````(* Nevertheless, we can prove a weaker form of adequacy (which is equvialent to adequacy `````` Robbert Krebbers committed Oct 25, 2016 326 `````` under classical axioms) directly without passing through the proofs for bupd: *) `````` Joseph Tassarotti committed Sep 07, 2016 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. `````` Robbert Krebbers committed Oct 25, 2016 332 `````` - rewrite /uPred_nnupd. unseal=> k P x Hx Hf1 Hf2. `````` Joseph Tassarotti committed Sep 07, 2016 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. `````` Joseph Tassarotti committed Sep 01, 2016 349 `````` `````` Joseph Tassarotti committed Sep 07, 2016 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. `````` Joseph Tassarotti committed Aug 28, 2016 360 `````` `````` Joseph Tassarotti committed Sep 07, 2016 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. `````` Joseph Tassarotti committed Aug 28, 2016 373 `````` `````` Joseph Tassarotti committed Sep 07, 2016 374 ``````(* Open question: `````` Joseph Tassarotti committed Aug 31, 2016 375 `````` `````` Robbert Krebbers committed Oct 25, 2016 376 377 `````` Do the basic properties of the |=r=> modality (bupd_intro, bupd_mono, rvs_trans, rvs_frame_r, bupd_ownM_updateP, and adequacy) uniquely characterize |=r=>? `````` Joseph Tassarotti committed Sep 07, 2016 378 ``````*) `````` Joseph Tassarotti committed Aug 31, 2016 379 `````` `````` Robbert Krebbers committed Oct 25, 2016 380 ``End bupd_nnupd.``