derived.v 39.1 KB
 Robbert Krebbers committed Oct 25, 2016 1 ``````From iris.base_logic Require Export primitive. `````` Ralf Jung committed Jan 05, 2017 2 ``````Set Default Proof Using "Type". `````` Robbert Krebbers committed Dec 13, 2016 3 ``````Import upred.uPred primitive.uPred. `````` Robbert Krebbers committed Oct 25, 2016 4 5 6 7 8 `````` Definition uPred_iff {M} (P Q : uPred M) : uPred M := ((P → Q) ∧ (Q → P))%I. Instance: Params (@uPred_iff) 1. Infix "↔" := uPred_iff : uPred_scope. `````` Robbert Krebbers committed Nov 27, 2016 9 10 11 12 13 14 15 16 17 18 ``````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, P at level 20, format "▷^ n P") : uPred_scope. Notation "▷? p P" := (uPred_laterN (Nat.b2n p) P) (at level 20, p at level 9, P at level 20, format "▷? p P") : uPred_scope. `````` Robbert Krebbers committed Oct 25, 2016 19 20 21 22 23 ``````Definition uPred_always_if {M} (p : bool) (P : uPred M) : uPred M := (if p then □ P else P)%I. Instance: Params (@uPred_always_if) 2. Arguments uPred_always_if _ !_ _/. Notation "□? p P" := (uPred_always_if p P) `````` Robbert Krebbers committed Nov 27, 2016 24 `````` (at level 20, p at level 9, P at level 20, format "□? p P"). `````` Robbert Krebbers committed Oct 25, 2016 25 `````` `````` Robbert Krebbers committed Oct 25, 2016 26 27 ``````Definition uPred_except_0 {M} (P : uPred M) : uPred M := ▷ False ∨ P. Notation "◇ P" := (uPred_except_0 P) `````` Robbert Krebbers committed Oct 25, 2016 28 `````` (at level 20, right associativity) : uPred_scope. `````` Robbert Krebbers committed Oct 25, 2016 29 30 ``````Instance: Params (@uPred_except_0) 1. Typeclasses Opaque uPred_except_0. `````` Robbert Krebbers committed Oct 25, 2016 31 32 33 34 35 36 37 `````` Class TimelessP {M} (P : uPred M) := timelessP : ▷ P ⊢ ◇ P. Arguments timelessP {_} _ {_}. Class PersistentP {M} (P : uPred M) := persistentP : P ⊢ □ P. Arguments persistentP {_} _ {_}. `````` Robbert Krebbers committed Dec 13, 2016 38 ``````Module uPred. `````` Robbert Krebbers committed Oct 25, 2016 39 40 41 42 43 44 45 46 47 48 ``````Section derived. Context {M : ucmraT}. Implicit Types φ : Prop. Implicit Types P Q : uPred M. Implicit Types A : Type. Notation "P ⊢ Q" := (@uPred_entails M P%I Q%I). (* Force implicit argument M *) Notation "P ⊣⊢ Q" := (equiv (A:=uPred M) P%I Q%I). (* Force implicit argument M *) (* Derived logical stuff *) Lemma False_elim P : False ⊢ P. `````` Robbert Krebbers committed Nov 22, 2016 49 ``````Proof. by apply (pure_elim' False). Qed. `````` Robbert Krebbers committed Oct 25, 2016 50 51 52 53 54 55 56 57 58 59 60 61 62 63 64 65 66 67 68 69 70 71 72 73 74 75 76 77 78 79 80 ``````Lemma True_intro P : P ⊢ True. Proof. by apply pure_intro. Qed. Lemma and_elim_l' P Q R : (P ⊢ R) → P ∧ Q ⊢ R. Proof. by rewrite and_elim_l. Qed. Lemma and_elim_r' P Q R : (Q ⊢ R) → P ∧ Q ⊢ R. Proof. by rewrite and_elim_r. Qed. Lemma or_intro_l' P Q R : (P ⊢ Q) → P ⊢ Q ∨ R. Proof. intros ->; apply or_intro_l. Qed. Lemma or_intro_r' P Q R : (P ⊢ R) → P ⊢ Q ∨ R. Proof. intros ->; apply or_intro_r. Qed. Lemma exist_intro' {A} P (Ψ : A → uPred M) a : (P ⊢ Ψ a) → P ⊢ ∃ a, Ψ a. Proof. intros ->; apply exist_intro. Qed. Lemma forall_elim' {A} P (Ψ : A → uPred M) : (P ⊢ ∀ a, Ψ a) → ∀ a, P ⊢ Ψ a. Proof. move=> HP a. by rewrite HP forall_elim. Qed. Hint Resolve pure_intro. Hint Resolve or_elim or_intro_l' or_intro_r'. Hint Resolve and_intro and_elim_l' and_elim_r'. Hint Immediate True_intro False_elim. Lemma impl_intro_l P Q R : (Q ∧ P ⊢ R) → P ⊢ Q → R. Proof. intros HR; apply impl_intro_r; rewrite -HR; auto. Qed. Lemma impl_elim_l P Q : (P → Q) ∧ P ⊢ Q. Proof. apply impl_elim with P; auto. Qed. Lemma impl_elim_r P Q : P ∧ (P → Q) ⊢ Q. Proof. apply impl_elim with P; auto. Qed. Lemma impl_elim_l' P Q R : (P ⊢ Q → R) → P ∧ Q ⊢ R. Proof. intros; apply impl_elim with Q; auto. Qed. Lemma impl_elim_r' P Q R : (Q ⊢ P → R) → P ∧ Q ⊢ R. Proof. intros; apply impl_elim with P; auto. Qed. `````` 81 ``````Lemma impl_entails P Q : (P → Q)%I → P ⊢ Q. `````` Robbert Krebbers committed Oct 25, 2016 82 ``````Proof. intros HPQ; apply impl_elim with P; rewrite -?HPQ; auto. Qed. `````` 83 84 ``````Lemma entails_impl P Q : (P ⊢ Q) → (P → Q)%I. Proof. intro. apply impl_intro_l. auto. Qed. `````` Robbert Krebbers committed Oct 25, 2016 85 86 87 88 89 90 91 92 93 94 95 96 97 98 99 100 101 102 103 104 105 106 107 108 109 110 111 112 113 114 115 116 117 118 119 120 121 122 123 124 125 126 `````` Lemma and_mono P P' Q Q' : (P ⊢ Q) → (P' ⊢ Q') → P ∧ P' ⊢ Q ∧ Q'. Proof. auto. Qed. Lemma and_mono_l P P' Q : (P ⊢ Q) → P ∧ P' ⊢ Q ∧ P'. Proof. by intros; apply and_mono. Qed. Lemma and_mono_r P P' Q' : (P' ⊢ Q') → P ∧ P' ⊢ P ∧ Q'. Proof. by apply and_mono. Qed. Lemma or_mono P P' Q Q' : (P ⊢ Q) → (P' ⊢ Q') → P ∨ P' ⊢ Q ∨ Q'. Proof. auto. Qed. Lemma or_mono_l P P' Q : (P ⊢ Q) → P ∨ P' ⊢ Q ∨ P'. Proof. by intros; apply or_mono. Qed. Lemma or_mono_r P P' Q' : (P' ⊢ Q') → P ∨ P' ⊢ P ∨ Q'. Proof. by apply or_mono. Qed. Lemma impl_mono P P' Q Q' : (Q ⊢ P) → (P' ⊢ Q') → (P → P') ⊢ Q → Q'. Proof. intros HP HQ'; apply impl_intro_l; rewrite -HQ'. apply impl_elim with P; eauto. Qed. Lemma forall_mono {A} (Φ Ψ : A → uPred M) : (∀ a, Φ a ⊢ Ψ a) → (∀ a, Φ a) ⊢ ∀ a, Ψ a. Proof. intros HP. apply forall_intro=> a; rewrite -(HP a); apply forall_elim. Qed. Lemma exist_mono {A} (Φ Ψ : A → uPred M) : (∀ a, Φ a ⊢ Ψ a) → (∃ a, Φ a) ⊢ ∃ a, Ψ a. Proof. intros HΦ. apply exist_elim=> a; rewrite (HΦ a); apply exist_intro. Qed. Global Instance and_mono' : Proper ((⊢) ==> (⊢) ==> (⊢)) (@uPred_and M). Proof. by intros P P' HP Q Q' HQ; apply and_mono. Qed. Global Instance and_flip_mono' : Proper (flip (⊢) ==> flip (⊢) ==> flip (⊢)) (@uPred_and M). Proof. by intros P P' HP Q Q' HQ; apply and_mono. Qed. Global Instance or_mono' : Proper ((⊢) ==> (⊢) ==> (⊢)) (@uPred_or M). Proof. by intros P P' HP Q Q' HQ; apply or_mono. Qed. Global Instance or_flip_mono' : Proper (flip (⊢) ==> flip (⊢) ==> flip (⊢)) (@uPred_or M). Proof. by intros P P' HP Q Q' HQ; apply or_mono. Qed. Global Instance impl_mono' : Proper (flip (⊢) ==> (⊢) ==> (⊢)) (@uPred_impl M). Proof. by intros P P' HP Q Q' HQ; apply impl_mono. Qed. `````` Robbert Krebbers committed Oct 28, 2016 127 128 129 ``````Global Instance impl_flip_mono' : Proper ((⊢) ==> flip (⊢) ==> flip (⊢)) (@uPred_impl M). Proof. by intros P P' HP Q Q' HQ; apply impl_mono. Qed. `````` Robbert Krebbers committed Oct 25, 2016 130 131 132 ``````Global Instance forall_mono' A : Proper (pointwise_relation _ (⊢) ==> (⊢)) (@uPred_forall M A). Proof. intros P1 P2; apply forall_mono. Qed. `````` Robbert Krebbers committed Oct 28, 2016 133 134 135 ``````Global Instance forall_flip_mono' A : Proper (pointwise_relation _ (flip (⊢)) ==> flip (⊢)) (@uPred_forall M A). Proof. intros P1 P2; apply forall_mono. Qed. `````` Robbert Krebbers committed Oct 25, 2016 136 ``````Global Instance exist_mono' A : `````` Robbert Krebbers committed Oct 28, 2016 137 138 139 140 `````` Proper (pointwise_relation _ (flip (⊢)) ==> flip (⊢)) (@uPred_exist M A). Proof. intros P1 P2; apply exist_mono. Qed. Global Instance exist_flip_mono' A : Proper (pointwise_relation _ (flip (⊢)) ==> flip (⊢)) (@uPred_exist M A). `````` Robbert Krebbers committed Oct 25, 2016 141 142 143 144 145 146 147 148 149 150 151 152 153 154 155 156 157 158 159 160 161 162 163 164 165 166 167 168 169 170 171 172 173 174 175 176 ``````Proof. intros P1 P2; apply exist_mono. Qed. Global Instance and_idem : IdemP (⊣⊢) (@uPred_and M). Proof. intros P; apply (anti_symm (⊢)); auto. Qed. Global Instance or_idem : IdemP (⊣⊢) (@uPred_or M). Proof. intros P; apply (anti_symm (⊢)); auto. Qed. Global Instance and_comm : Comm (⊣⊢) (@uPred_and M). Proof. intros P Q; apply (anti_symm (⊢)); auto. Qed. Global Instance True_and : LeftId (⊣⊢) True%I (@uPred_and M). Proof. intros P; apply (anti_symm (⊢)); auto. Qed. Global Instance and_True : RightId (⊣⊢) True%I (@uPred_and M). Proof. intros P; apply (anti_symm (⊢)); auto. Qed. Global Instance False_and : LeftAbsorb (⊣⊢) False%I (@uPred_and M). Proof. intros P; apply (anti_symm (⊢)); auto. Qed. Global Instance and_False : RightAbsorb (⊣⊢) False%I (@uPred_and M). Proof. intros P; apply (anti_symm (⊢)); auto. Qed. Global Instance True_or : LeftAbsorb (⊣⊢) True%I (@uPred_or M). Proof. intros P; apply (anti_symm (⊢)); auto. Qed. Global Instance or_True : RightAbsorb (⊣⊢) True%I (@uPred_or M). Proof. intros P; apply (anti_symm (⊢)); auto. Qed. Global Instance False_or : LeftId (⊣⊢) False%I (@uPred_or M). Proof. intros P; apply (anti_symm (⊢)); auto. Qed. Global Instance or_False : RightId (⊣⊢) False%I (@uPred_or M). Proof. intros P; apply (anti_symm (⊢)); auto. Qed. Global Instance and_assoc : Assoc (⊣⊢) (@uPred_and M). Proof. intros P Q R; apply (anti_symm (⊢)); auto. Qed. Global Instance or_comm : Comm (⊣⊢) (@uPred_or M). Proof. intros P Q; apply (anti_symm (⊢)); auto. Qed. Global Instance or_assoc : Assoc (⊣⊢) (@uPred_or M). Proof. intros P Q R; apply (anti_symm (⊢)); auto. Qed. Global Instance True_impl : LeftId (⊣⊢) True%I (@uPred_impl M). Proof. intros P; apply (anti_symm (⊢)). - by rewrite -(left_id True%I uPred_and (_ → _)%I) impl_elim_r. - by apply impl_intro_l; rewrite left_id. Qed. `````` Robbert Krebbers committed Nov 21, 2016 177 178 179 180 181 ``````Lemma False_impl P : (False → P) ⊣⊢ True. Proof. apply (anti_symm (⊢)); [by auto|]. apply impl_intro_l. rewrite left_absorb. auto. Qed. `````` Robbert Krebbers committed Oct 25, 2016 182 183 184 185 186 187 188 189 190 191 192 193 194 195 196 197 198 199 200 201 202 203 204 205 206 207 208 209 210 211 212 213 214 215 216 217 `````` Lemma exists_impl_forall {A} P (Ψ : A → uPred M) : ((∃ x : A, Ψ x) → P) ⊣⊢ ∀ x : A, Ψ x → P. Proof. apply equiv_spec; split. - apply forall_intro=>x. by rewrite -exist_intro. - apply impl_intro_r, impl_elim_r', exist_elim=>x. apply impl_intro_r. by rewrite (forall_elim x) impl_elim_r. Qed. Lemma or_and_l P Q R : P ∨ Q ∧ R ⊣⊢ (P ∨ Q) ∧ (P ∨ R). Proof. apply (anti_symm (⊢)); first auto. do 2 (apply impl_elim_l', or_elim; apply impl_intro_l); auto. Qed. Lemma or_and_r P Q R : P ∧ Q ∨ R ⊣⊢ (P ∨ R) ∧ (Q ∨ R). Proof. by rewrite -!(comm _ R) or_and_l. Qed. Lemma and_or_l P Q R : P ∧ (Q ∨ R) ⊣⊢ P ∧ Q ∨ P ∧ R. Proof. apply (anti_symm (⊢)); last auto. apply impl_elim_r', or_elim; apply impl_intro_l; auto. Qed. Lemma and_or_r P Q R : (P ∨ Q) ∧ R ⊣⊢ P ∧ R ∨ Q ∧ R. Proof. by rewrite -!(comm _ R) and_or_l. Qed. Lemma and_exist_l {A} P (Ψ : A → uPred M) : P ∧ (∃ a, Ψ a) ⊣⊢ ∃ a, P ∧ Ψ a. Proof. apply (anti_symm (⊢)). - apply impl_elim_r'. apply exist_elim=>a. apply impl_intro_l. by rewrite -(exist_intro a). - apply exist_elim=>a. apply and_intro; first by rewrite and_elim_l. by rewrite -(exist_intro a) and_elim_r. Qed. Lemma and_exist_r {A} P (Φ: A → uPred M) : (∃ a, Φ a) ∧ P ⊣⊢ ∃ a, Φ a ∧ P. Proof. rewrite -(comm _ P) and_exist_l. apply exist_proper=>a. by rewrite comm. Qed. `````` Robbert Krebbers committed Nov 17, 2016 218 219 220 221 222 223 224 ``````Lemma or_exist {A} (Φ Ψ : A → uPred M) : (∃ a, Φ a ∨ Ψ a) ⊣⊢ (∃ a, Φ a) ∨ (∃ a, Ψ a). Proof. apply (anti_symm (⊢)). - apply exist_elim=> a. by rewrite -!(exist_intro a). - apply or_elim; apply exist_elim=> a; rewrite -(exist_intro a); auto. Qed. `````` Robbert Krebbers committed Oct 25, 2016 225 `````` `````` Ralf Jung committed Nov 22, 2016 226 ``````Lemma pure_elim φ Q R : (Q ⊢ ⌜φ⌝) → (φ → Q ⊢ R) → Q ⊢ R. `````` Robbert Krebbers committed Nov 22, 2016 227 228 229 230 ``````Proof. intros HQ HQR. rewrite -(idemp uPred_and Q) {1}HQ. apply impl_elim_l', pure_elim'=> ?. by apply entails_impl, HQR. Qed. `````` Ralf Jung committed Nov 22, 2016 231 ``````Lemma pure_mono φ1 φ2 : (φ1 → φ2) → ⌜φ1⌝ ⊢ ⌜φ2⌝. `````` Robbert Krebbers committed Oct 25, 2016 232 233 234 ``````Proof. intros; apply pure_elim with φ1; eauto. Qed. Global Instance pure_mono' : Proper (impl ==> (⊢)) (@uPred_pure M). Proof. intros φ1 φ2; apply pure_mono. Qed. `````` Ralf Jung committed Nov 22, 2016 235 ``````Lemma pure_iff φ1 φ2 : (φ1 ↔ φ2) → ⌜φ1⌝ ⊣⊢ ⌜φ2⌝. `````` Robbert Krebbers committed Oct 25, 2016 236 ``````Proof. intros [??]; apply (anti_symm _); auto using pure_mono. Qed. `````` Ralf Jung committed Nov 22, 2016 237 ``````Lemma pure_intro_l φ Q R : φ → (⌜φ⌝ ∧ Q ⊢ R) → Q ⊢ R. `````` Robbert Krebbers committed Oct 25, 2016 238 ``````Proof. intros ? <-; auto using pure_intro. Qed. `````` Ralf Jung committed Nov 22, 2016 239 ``````Lemma pure_intro_r φ Q R : φ → (Q ∧ ⌜φ⌝ ⊢ R) → Q ⊢ R. `````` Robbert Krebbers committed Oct 25, 2016 240 ``````Proof. intros ? <-; auto. Qed. `````` Ralf Jung committed Nov 22, 2016 241 ``````Lemma pure_intro_impl φ Q R : φ → (Q ⊢ ⌜φ⌝ → R) → Q ⊢ R. `````` Robbert Krebbers committed Oct 25, 2016 242 ``````Proof. intros ? ->. eauto using pure_intro_l, impl_elim_r. Qed. `````` Ralf Jung committed Nov 22, 2016 243 ``````Lemma pure_elim_l φ Q R : (φ → Q ⊢ R) → ⌜φ⌝ ∧ Q ⊢ R. `````` Robbert Krebbers committed Oct 25, 2016 244 ``````Proof. intros; apply pure_elim with φ; eauto. Qed. `````` Ralf Jung committed Nov 22, 2016 245 ``````Lemma pure_elim_r φ Q R : (φ → Q ⊢ R) → Q ∧ ⌜φ⌝ ⊢ R. `````` Robbert Krebbers committed Oct 25, 2016 246 ``````Proof. intros; apply pure_elim with φ; eauto. Qed. `````` Robbert Krebbers committed Nov 21, 2016 247 `````` `````` Ralf Jung committed Nov 22, 2016 248 ``````Lemma pure_True (φ : Prop) : φ → ⌜φ⌝ ⊣⊢ True. `````` Robbert Krebbers committed Oct 25, 2016 249 ``````Proof. intros; apply (anti_symm _); auto. Qed. `````` Ralf Jung committed Nov 22, 2016 250 ``````Lemma pure_False (φ : Prop) : ¬φ → ⌜φ⌝ ⊣⊢ False. `````` Robbert Krebbers committed Nov 21, 2016 251 ``````Proof. intros; apply (anti_symm _); eauto using pure_elim. Qed. `````` Robbert Krebbers committed Oct 25, 2016 252 `````` `````` Ralf Jung committed Nov 22, 2016 253 ``````Lemma pure_and φ1 φ2 : ⌜φ1 ∧ φ2⌝ ⊣⊢ ⌜φ1⌝ ∧ ⌜φ2⌝. `````` Robbert Krebbers committed Oct 25, 2016 254 255 256 257 258 ``````Proof. apply (anti_symm _). - eapply pure_elim=> // -[??]; auto. - eapply (pure_elim φ1); [auto|]=> ?. eapply (pure_elim φ2); auto. Qed. `````` Ralf Jung committed Nov 22, 2016 259 ``````Lemma pure_or φ1 φ2 : ⌜φ1 ∨ φ2⌝ ⊣⊢ ⌜φ1⌝ ∨ ⌜φ2⌝. `````` Robbert Krebbers committed Oct 25, 2016 260 261 262 263 264 ``````Proof. apply (anti_symm _). - eapply pure_elim=> // -[?|?]; auto. - apply or_elim; eapply pure_elim; eauto. Qed. `````` Ralf Jung committed Nov 22, 2016 265 ``````Lemma pure_impl φ1 φ2 : ⌜φ1 → φ2⌝ ⊣⊢ (⌜φ1⌝ → ⌜φ2⌝). `````` Robbert Krebbers committed Oct 25, 2016 266 267 268 269 ``````Proof. apply (anti_symm _). - apply impl_intro_l. rewrite -pure_and. apply pure_mono. naive_solver. - rewrite -pure_forall_2. apply forall_intro=> ?. `````` Robbert Krebbers committed Nov 21, 2016 270 `````` by rewrite -(left_id True uPred_and (_→_))%I (pure_True φ1) // impl_elim_r. `````` Robbert Krebbers committed Oct 25, 2016 271 ``````Qed. `````` Ralf Jung committed Nov 22, 2016 272 ``````Lemma pure_forall {A} (φ : A → Prop) : ⌜∀ x, φ x⌝ ⊣⊢ ∀ x, ⌜φ x⌝. `````` Robbert Krebbers committed Oct 25, 2016 273 274 275 276 ``````Proof. apply (anti_symm _); auto using pure_forall_2. apply forall_intro=> x. eauto using pure_mono. Qed. `````` Ralf Jung committed Nov 22, 2016 277 ``````Lemma pure_exist {A} (φ : A → Prop) : ⌜∃ x, φ x⌝ ⊣⊢ ∃ x, ⌜φ x⌝. `````` Robbert Krebbers committed Oct 25, 2016 278 279 280 281 282 283 ``````Proof. apply (anti_symm _). - eapply pure_elim=> // -[x ?]. rewrite -(exist_intro x); auto. - apply exist_elim=> x. eauto using pure_mono. Qed. `````` Ralf Jung committed Nov 22, 2016 284 ``````Lemma internal_eq_refl' {A : ofeT} (a : A) P : P ⊢ a ≡ a. `````` Robbert Krebbers committed Oct 25, 2016 285 286 ``````Proof. rewrite (True_intro P). apply internal_eq_refl. Qed. Hint Resolve internal_eq_refl'. `````` Ralf Jung committed Nov 22, 2016 287 ``````Lemma equiv_internal_eq {A : ofeT} P (a b : A) : a ≡ b → P ⊢ a ≡ b. `````` Robbert Krebbers committed Oct 25, 2016 288 ``````Proof. by intros ->. Qed. `````` Ralf Jung committed Nov 22, 2016 289 ``````Lemma internal_eq_sym {A : ofeT} (a b : A) : a ≡ b ⊢ b ≡ a. `````` Robbert Krebbers committed Oct 25, 2016 290 ``````Proof. apply (internal_eq_rewrite a b (λ b, b ≡ a)%I); auto. solve_proper. Qed. `````` Ralf Jung committed Dec 05, 2016 291 292 293 ``````Lemma internal_eq_rewrite_contractive {A : ofeT} a b (Ψ : A → uPred M) P {HΨ : Contractive Ψ} : (P ⊢ ▷ (a ≡ b)) → (P ⊢ Ψ a) → P ⊢ Ψ b. Proof. `````` Robbert Krebbers committed Dec 05, 2016 294 295 `````` move: HΨ=> /contractiveI HΨ Heq ?. apply (internal_eq_rewrite (Ψ a) (Ψ b) id _)=>//=. by rewrite -HΨ. `````` Ralf Jung committed Dec 05, 2016 296 ``````Qed. `````` Robbert Krebbers committed Oct 25, 2016 297 `````` `````` Ralf Jung committed Nov 22, 2016 298 ``````Lemma pure_impl_forall φ P : (⌜φ⌝ → P) ⊣⊢ (∀ _ : φ, P). `````` Robbert Krebbers committed Nov 20, 2016 299 300 ``````Proof. apply (anti_symm _). `````` Robbert Krebbers committed Nov 21, 2016 301 `````` - apply forall_intro=> ?. by rewrite pure_True // left_id. `````` Robbert Krebbers committed Nov 20, 2016 302 303 `````` - apply impl_intro_l, pure_elim_l=> Hφ. by rewrite (forall_elim Hφ). Qed. `````` Ralf Jung committed Nov 22, 2016 304 ``````Lemma pure_alt φ : ⌜φ⌝ ⊣⊢ ∃ _ : φ, True. `````` Robbert Krebbers committed Oct 25, 2016 305 306 307 308 309 310 311 312 313 314 315 316 317 318 319 320 321 322 323 324 325 326 327 ``````Proof. apply (anti_symm _). - eapply pure_elim; eauto=> H. rewrite -(exist_intro H); auto. - by apply exist_elim, pure_intro. Qed. Lemma and_alt P Q : P ∧ Q ⊣⊢ ∀ b : bool, if b then P else Q. Proof. apply (anti_symm _); first apply forall_intro=> -[]; auto. apply and_intro. by rewrite (forall_elim true). by rewrite (forall_elim false). Qed. Lemma or_alt P Q : P ∨ Q ⊣⊢ ∃ b : bool, if b then P else Q. Proof. apply (anti_symm _); last apply exist_elim=> -[]; auto. apply or_elim. by rewrite -(exist_intro true). by rewrite -(exist_intro false). Qed. Global Instance iff_ne n : Proper (dist n ==> dist n ==> dist n) (@uPred_iff M). Proof. unfold uPred_iff; solve_proper. Qed. Global Instance iff_proper : Proper ((⊣⊢) ==> (⊣⊢) ==> (⊣⊢)) (@uPred_iff M) := ne_proper_2 _. Lemma iff_refl Q P : Q ⊢ P ↔ P. Proof. rewrite /uPred_iff; apply and_intro; apply impl_intro_l; auto. Qed. `````` 328 ``````Lemma iff_equiv P Q : (P ↔ Q)%I → (P ⊣⊢ Q). `````` Robbert Krebbers committed Oct 25, 2016 329 330 ``````Proof. intros HPQ; apply (anti_symm (⊢)); `````` 331 `````` apply impl_entails; rewrite /uPred_valid HPQ /uPred_iff; auto. `````` Robbert Krebbers committed Oct 25, 2016 332 ``````Qed. `````` 333 ``````Lemma equiv_iff P Q : (P ⊣⊢ Q) → (P ↔ Q)%I. `````` Robbert Krebbers committed Oct 25, 2016 334 ``````Proof. intros ->; apply iff_refl. Qed. `````` Robbert Krebbers committed Oct 25, 2016 335 ``````Lemma internal_eq_iff P Q : P ≡ Q ⊢ P ↔ Q. `````` Robbert Krebbers committed Oct 25, 2016 336 ``````Proof. `````` Robbert Krebbers committed Oct 25, 2016 337 338 `````` apply (internal_eq_rewrite P Q (λ Q, P ↔ Q))%I; first solve_proper; auto using iff_refl. `````` Robbert Krebbers committed Oct 25, 2016 339 340 341 342 ``````Qed. (* Derived BI Stuff *) Hint Resolve sep_mono. `````` Robbert Krebbers committed Nov 03, 2016 343 ``````Lemma sep_mono_l P P' Q : (P ⊢ Q) → P ∗ P' ⊢ Q ∗ P'. `````` Robbert Krebbers committed Oct 25, 2016 344 ``````Proof. by intros; apply sep_mono. Qed. `````` Robbert Krebbers committed Nov 03, 2016 345 ``````Lemma sep_mono_r P P' Q' : (P' ⊢ Q') → P ∗ P' ⊢ P ∗ Q'. `````` Robbert Krebbers committed Oct 25, 2016 346 347 348 349 350 351 ``````Proof. by apply sep_mono. Qed. Global Instance sep_mono' : Proper ((⊢) ==> (⊢) ==> (⊢)) (@uPred_sep M). Proof. by intros P P' HP Q Q' HQ; apply sep_mono. Qed. Global Instance sep_flip_mono' : Proper (flip (⊢) ==> flip (⊢) ==> flip (⊢)) (@uPred_sep M). Proof. by intros P P' HP Q Q' HQ; apply sep_mono. Qed. `````` Robbert Krebbers committed Nov 03, 2016 352 ``````Lemma wand_mono P P' Q Q' : (Q ⊢ P) → (P' ⊢ Q') → (P -∗ P') ⊢ Q -∗ Q'. `````` Robbert Krebbers committed Oct 25, 2016 353 354 355 356 357 ``````Proof. intros HP HQ; apply wand_intro_r. rewrite HP -HQ. by apply wand_elim_l'. Qed. Global Instance wand_mono' : Proper (flip (⊢) ==> (⊢) ==> (⊢)) (@uPred_wand M). Proof. by intros P P' HP Q Q' HQ; apply wand_mono. Qed. `````` Robbert Krebbers committed Oct 28, 2016 358 359 360 ``````Global Instance wand_flip_mono' : Proper ((⊢) ==> flip (⊢) ==> flip (⊢)) (@uPred_wand M). Proof. by intros P P' HP Q Q' HQ; apply wand_mono. Qed. `````` Robbert Krebbers committed Oct 25, 2016 361 362 363 364 365 366 367 368 369 370 371 372 `````` Global Instance sep_comm : Comm (⊣⊢) (@uPred_sep M). Proof. intros P Q; apply (anti_symm _); auto using sep_comm'. Qed. Global Instance sep_assoc : Assoc (⊣⊢) (@uPred_sep M). Proof. intros P Q R; apply (anti_symm _); auto using sep_assoc'. by rewrite !(comm _ P) !(comm _ _ R) sep_assoc'. Qed. Global Instance True_sep : LeftId (⊣⊢) True%I (@uPred_sep M). Proof. intros P; apply (anti_symm _); auto using True_sep_1, True_sep_2. Qed. Global Instance sep_True : RightId (⊣⊢) True%I (@uPred_sep M). Proof. by intros P; rewrite comm left_id. Qed. `````` Robbert Krebbers committed Nov 03, 2016 373 ``````Lemma sep_elim_l P Q : P ∗ Q ⊢ P. `````` Robbert Krebbers committed Oct 25, 2016 374 ``````Proof. by rewrite (True_intro Q) right_id. Qed. `````` Robbert Krebbers committed Nov 03, 2016 375 376 377 ``````Lemma sep_elim_r P Q : P ∗ Q ⊢ Q. Proof. by rewrite (comm (∗))%I; apply sep_elim_l. Qed. Lemma sep_elim_l' P Q R : (P ⊢ R) → P ∗ Q ⊢ R. `````` Robbert Krebbers committed Oct 25, 2016 378 ``````Proof. intros ->; apply sep_elim_l. Qed. `````` Robbert Krebbers committed Nov 03, 2016 379 ``````Lemma sep_elim_r' P Q R : (Q ⊢ R) → P ∗ Q ⊢ R. `````` Robbert Krebbers committed Oct 25, 2016 380 381 ``````Proof. intros ->; apply sep_elim_r. Qed. Hint Resolve sep_elim_l' sep_elim_r'. `````` 382 ``````Lemma sep_intro_True_l P Q R : P%I → (R ⊢ Q) → R ⊢ P ∗ Q. `````` Robbert Krebbers committed Oct 25, 2016 383 ``````Proof. by intros; rewrite -(left_id True%I uPred_sep R); apply sep_mono. Qed. `````` 384 ``````Lemma sep_intro_True_r P Q R : (R ⊢ P) → Q%I → R ⊢ P ∗ Q. `````` Robbert Krebbers committed Oct 25, 2016 385 ``````Proof. by intros; rewrite -(right_id True%I uPred_sep R); apply sep_mono. Qed. `````` 386 ``````Lemma sep_elim_True_l P Q R : P → (P ∗ R ⊢ Q) → R ⊢ Q. `````` Robbert Krebbers committed Oct 25, 2016 387 ``````Proof. by intros HP; rewrite -HP left_id. Qed. `````` 388 ``````Lemma sep_elim_True_r P Q R : P → (R ∗ P ⊢ Q) → R ⊢ Q. `````` Robbert Krebbers committed Oct 25, 2016 389 ``````Proof. by intros HP; rewrite -HP right_id. Qed. `````` Robbert Krebbers committed Nov 03, 2016 390 ``````Lemma wand_intro_l P Q R : (Q ∗ P ⊢ R) → P ⊢ Q -∗ R. `````` Robbert Krebbers committed Oct 25, 2016 391 ``````Proof. rewrite comm; apply wand_intro_r. Qed. `````` Robbert Krebbers committed Nov 03, 2016 392 ``````Lemma wand_elim_l P Q : (P -∗ Q) ∗ P ⊢ Q. `````` Robbert Krebbers committed Oct 25, 2016 393 ``````Proof. by apply wand_elim_l'. Qed. `````` Robbert Krebbers committed Nov 03, 2016 394 ``````Lemma wand_elim_r P Q : P ∗ (P -∗ Q) ⊢ Q. `````` Robbert Krebbers committed Oct 25, 2016 395 ``````Proof. rewrite (comm _ P); apply wand_elim_l. Qed. `````` Robbert Krebbers committed Nov 03, 2016 396 ``````Lemma wand_elim_r' P Q R : (Q ⊢ P -∗ R) → P ∗ Q ⊢ R. `````` Robbert Krebbers committed Oct 25, 2016 397 ``````Proof. intros ->; apply wand_elim_r. Qed. `````` Robbert Krebbers committed Nov 03, 2016 398 ``````Lemma wand_apply P Q R S : (P ⊢ Q -∗ R) → (S ⊢ P ∗ Q) → S ⊢ R. `````` Ralf Jung committed Nov 01, 2016 399 ``````Proof. intros HR%wand_elim_l' HQ. by rewrite HQ. Qed. `````` Robbert Krebbers committed Nov 03, 2016 400 ``````Lemma wand_frame_l P Q R : (Q -∗ R) ⊢ P ∗ Q -∗ P ∗ R. `````` Robbert Krebbers committed Oct 25, 2016 401 ``````Proof. apply wand_intro_l. rewrite -assoc. apply sep_mono_r, wand_elim_r. Qed. `````` Robbert Krebbers committed Nov 03, 2016 402 ``````Lemma wand_frame_r P Q R : (Q -∗ R) ⊢ Q ∗ P -∗ R ∗ P. `````` Robbert Krebbers committed Oct 25, 2016 403 ``````Proof. `````` Robbert Krebbers committed Nov 03, 2016 404 `````` apply wand_intro_l. rewrite ![(_ ∗ P)%I]comm -assoc. `````` Robbert Krebbers committed Oct 25, 2016 405 406 `````` apply sep_mono_r, wand_elim_r. Qed. `````` Robbert Krebbers committed Nov 03, 2016 407 ``````Lemma wand_diag P : (P -∗ P) ⊣⊢ True. `````` Robbert Krebbers committed Oct 25, 2016 408 ``````Proof. apply (anti_symm _); auto. apply wand_intro_l; by rewrite right_id. Qed. `````` Robbert Krebbers committed Nov 03, 2016 409 ``````Lemma wand_True P : (True -∗ P) ⊣⊢ P. `````` Robbert Krebbers committed Oct 25, 2016 410 411 ``````Proof. apply (anti_symm _); last by auto using wand_intro_l. `````` 412 `````` eapply sep_elim_True_l; last by apply wand_elim_r. done. `````` Robbert Krebbers committed Oct 25, 2016 413 ``````Qed. `````` 414 ``````Lemma wand_entails P Q : (P -∗ Q)%I → P ⊢ Q. `````` Robbert Krebbers committed Oct 25, 2016 415 416 417 ``````Proof. intros HPQ. eapply sep_elim_True_r; first exact: HPQ. by rewrite wand_elim_r. Qed. `````` 418 419 ``````Lemma entails_wand P Q : (P ⊢ Q) → (P -∗ Q)%I. Proof. intro. apply wand_intro_l. auto. Qed. `````` Robbert Krebbers committed Nov 03, 2016 420 ``````Lemma wand_curry P Q R : (P -∗ Q -∗ R) ⊣⊢ (P ∗ Q -∗ R). `````` Robbert Krebbers committed Oct 25, 2016 421 422 423 424 425 426 ``````Proof. apply (anti_symm _). - apply wand_intro_l. by rewrite (comm _ P) -assoc !wand_elim_r. - do 2 apply wand_intro_l. by rewrite assoc (comm _ Q) wand_elim_r. Qed. `````` Robbert Krebbers committed Nov 03, 2016 427 ``````Lemma sep_and P Q : (P ∗ Q) ⊢ (P ∧ Q). `````` Robbert Krebbers committed Oct 25, 2016 428 ``````Proof. auto. Qed. `````` Robbert Krebbers committed Nov 03, 2016 429 ``````Lemma impl_wand P Q : (P → Q) ⊢ P -∗ Q. `````` Robbert Krebbers committed Oct 25, 2016 430 ``````Proof. apply wand_intro_r, impl_elim with P; auto. Qed. `````` Ralf Jung committed Nov 22, 2016 431 ``````Lemma pure_elim_sep_l φ Q R : (φ → Q ⊢ R) → ⌜φ⌝ ∗ Q ⊢ R. `````` Robbert Krebbers committed Oct 25, 2016 432 ``````Proof. intros; apply pure_elim with φ; eauto. Qed. `````` Ralf Jung committed Nov 22, 2016 433 ``````Lemma pure_elim_sep_r φ Q R : (φ → Q ⊢ R) → Q ∗ ⌜φ⌝ ⊢ R. `````` Robbert Krebbers committed Oct 25, 2016 434 435 436 437 438 439 440 ``````Proof. intros; apply pure_elim with φ; eauto. Qed. Global Instance sep_False : LeftAbsorb (⊣⊢) False%I (@uPred_sep M). Proof. intros P; apply (anti_symm _); auto. Qed. Global Instance False_sep : RightAbsorb (⊣⊢) False%I (@uPred_sep M). Proof. intros P; apply (anti_symm _); auto. Qed. `````` Jacques-Henri Jourdan committed Dec 23, 2016 441 ``````Lemma entails_equiv_and P Q : (P ⊣⊢ Q ∧ P) ↔ (P ⊢ Q). `````` Robbert Krebbers committed Dec 27, 2016 442 ``````Proof. split. by intros ->; auto. intros; apply (anti_symm _); auto. Qed. `````` Robbert Krebbers committed Nov 03, 2016 443 ``````Lemma sep_and_l P Q R : P ∗ (Q ∧ R) ⊢ (P ∗ Q) ∧ (P ∗ R). `````` Robbert Krebbers committed Oct 25, 2016 444 ``````Proof. auto. Qed. `````` Robbert Krebbers committed Nov 03, 2016 445 ``````Lemma sep_and_r P Q R : (P ∧ Q) ∗ R ⊢ (P ∗ R) ∧ (Q ∗ R). `````` Robbert Krebbers committed Oct 25, 2016 446 ``````Proof. auto. Qed. `````` Robbert Krebbers committed Nov 03, 2016 447 ``````Lemma sep_or_l P Q R : P ∗ (Q ∨ R) ⊣⊢ (P ∗ Q) ∨ (P ∗ R). `````` Robbert Krebbers committed Oct 25, 2016 448 449 450 451 ``````Proof. apply (anti_symm (⊢)); last by eauto 8. apply wand_elim_r', or_elim; apply wand_intro_l; auto. Qed. `````` Robbert Krebbers committed Nov 03, 2016 452 ``````Lemma sep_or_r P Q R : (P ∨ Q) ∗ R ⊣⊢ (P ∗ R) ∨ (Q ∗ R). `````` Robbert Krebbers committed Oct 25, 2016 453 ``````Proof. by rewrite -!(comm _ R) sep_or_l. Qed. `````` Robbert Krebbers committed Nov 03, 2016 454 ``````Lemma sep_exist_l {A} P (Ψ : A → uPred M) : P ∗ (∃ a, Ψ a) ⊣⊢ ∃ a, P ∗ Ψ a. `````` Robbert Krebbers committed Oct 25, 2016 455 456 457 458 459 460 ``````Proof. intros; apply (anti_symm (⊢)). - apply wand_elim_r', exist_elim=>a. apply wand_intro_l. by rewrite -(exist_intro a). - apply exist_elim=> a; apply sep_mono; auto using exist_intro. Qed. `````` Robbert Krebbers committed Nov 03, 2016 461 ``````Lemma sep_exist_r {A} (Φ: A → uPred M) Q: (∃ a, Φ a) ∗ Q ⊣⊢ ∃ a, Φ a ∗ Q. `````` Robbert Krebbers committed Oct 25, 2016 462 ``````Proof. setoid_rewrite (comm _ _ Q); apply sep_exist_l. Qed. `````` Robbert Krebbers committed Nov 03, 2016 463 ``````Lemma sep_forall_l {A} P (Ψ : A → uPred M) : P ∗ (∀ a, Ψ a) ⊢ ∀ a, P ∗ Ψ a. `````` Robbert Krebbers committed Oct 25, 2016 464 ``````Proof. by apply forall_intro=> a; rewrite forall_elim. Qed. `````` Robbert Krebbers committed Nov 03, 2016 465 ``````Lemma sep_forall_r {A} (Φ : A → uPred M) Q : (∀ a, Φ a) ∗ Q ⊢ ∀ a, Φ a ∗ Q. `````` Robbert Krebbers committed Oct 25, 2016 466 467 468 469 470 471 472 473 474 475 476 477 478 ``````Proof. by apply forall_intro=> a; rewrite forall_elim. Qed. (* Always derived *) Hint Resolve always_mono always_elim. Global Instance always_mono' : Proper ((⊢) ==> (⊢)) (@uPred_always M). Proof. intros P Q; apply always_mono. Qed. Global Instance always_flip_mono' : Proper (flip (⊢) ==> flip (⊢)) (@uPred_always M). Proof. intros P Q; apply always_mono. Qed. Lemma always_intro' P Q : (□ P ⊢ Q) → □ P ⊢ □ Q. Proof. intros <-. apply always_idemp. Qed. `````` Ralf Jung committed Nov 22, 2016 479 ``````Lemma always_pure φ : □ ⌜φ⌝ ⊣⊢ ⌜φ⌝. `````` Robbert Krebbers committed Oct 25, 2016 480 481 482 483 484 485 486 487 488 489 490 491 492 493 494 495 496 497 498 499 ``````Proof. apply (anti_symm _); auto using always_pure_2. Qed. Lemma always_forall {A} (Ψ : A → uPred M) : (□ ∀ a, Ψ a) ⊣⊢ (∀ a, □ Ψ a). Proof. apply (anti_symm _); auto using always_forall_2. apply forall_intro=> x. by rewrite (forall_elim x). Qed. Lemma always_exist {A} (Ψ : A → uPred M) : (□ ∃ a, Ψ a) ⊣⊢ (∃ a, □ Ψ a). Proof. apply (anti_symm _); auto using always_exist_1. apply exist_elim=> x. by rewrite (exist_intro x). Qed. Lemma always_and P Q : □ (P ∧ Q) ⊣⊢ □ P ∧ □ Q. Proof. rewrite !and_alt always_forall. by apply forall_proper=> -[]. Qed. Lemma always_or P Q : □ (P ∨ Q) ⊣⊢ □ P ∨ □ Q. Proof. rewrite !or_alt always_exist. by apply exist_proper=> -[]. Qed. Lemma always_impl P Q : □ (P → Q) ⊢ □ P → □ Q. Proof. apply impl_intro_l; rewrite -always_and. apply always_mono, impl_elim with P; auto. Qed. `````` Ralf Jung committed Nov 22, 2016 500 ``````Lemma always_internal_eq {A:ofeT} (a b : A) : □ (a ≡ b) ⊣⊢ a ≡ b. `````` Robbert Krebbers committed Oct 25, 2016 501 502 ``````Proof. apply (anti_symm (⊢)); auto using always_elim. `````` Robbert Krebbers committed Oct 25, 2016 503 `````` apply (internal_eq_rewrite a b (λ b, □ (a ≡ b))%I); auto. `````` Robbert Krebbers committed Oct 25, 2016 504 `````` { intros n; solve_proper. } `````` Robbert Krebbers committed Oct 25, 2016 505 `````` rewrite -(internal_eq_refl a) always_pure; auto. `````` Robbert Krebbers committed Oct 25, 2016 506 507 ``````Qed. `````` Robbert Krebbers committed Nov 03, 2016 508 ``````Lemma always_and_sep P Q : □ (P ∧ Q) ⊣⊢ □ (P ∗ Q). `````` Robbert Krebbers committed Oct 25, 2016 509 ``````Proof. apply (anti_symm (⊢)); auto using always_and_sep_1. Qed. `````` Robbert Krebbers committed Nov 03, 2016 510 ``````Lemma always_and_sep_l' P Q : □ P ∧ Q ⊣⊢ □ P ∗ Q. `````` Robbert Krebbers committed Oct 25, 2016 511 ``````Proof. apply (anti_symm (⊢)); auto using always_and_sep_l_1. Qed. `````` Robbert Krebbers committed Nov 03, 2016 512 ``````Lemma always_and_sep_r' P Q : P ∧ □ Q ⊣⊢ P ∗ □ Q. `````` Robbert Krebbers committed Oct 25, 2016 513 ``````Proof. by rewrite !(comm _ P) always_and_sep_l'. Qed. `````` Robbert Krebbers committed Nov 03, 2016 514 ``````Lemma always_sep P Q : □ (P ∗ Q) ⊣⊢ □ P ∗ □ Q. `````` Robbert Krebbers committed Oct 25, 2016 515 ``````Proof. by rewrite -always_and_sep -always_and_sep_l' always_and. Qed. `````` Robbert Krebbers committed Nov 03, 2016 516 ``````Lemma always_sep_dup' P : □ P ⊣⊢ □ P ∗ □ P. `````` Robbert Krebbers committed Oct 25, 2016 517 518 ``````Proof. by rewrite -always_sep -always_and_sep (idemp _). Qed. `````` Robbert Krebbers committed Nov 03, 2016 519 ``````Lemma always_wand P Q : □ (P -∗ Q) ⊢ □ P -∗ □ Q. `````` Robbert Krebbers committed Oct 25, 2016 520 ``````Proof. by apply wand_intro_r; rewrite -always_sep wand_elim_l. Qed. `````` Robbert Krebbers committed Nov 03, 2016 521 ``````Lemma always_wand_impl P Q : □ (P -∗ Q) ⊣⊢ □ (P → Q). `````` Robbert Krebbers committed Oct 25, 2016 522 523 524 525 526 ``````Proof. apply (anti_symm (⊢)); [|by rewrite -impl_wand]. apply always_intro', impl_intro_r. by rewrite always_and_sep_l' always_elim wand_elim_l. Qed. `````` Robbert Krebbers committed Nov 03, 2016 527 ``````Lemma always_entails_l' P Q : (P ⊢ □ Q) → P ⊢ □ Q ∗ P. `````` Robbert Krebbers committed Oct 25, 2016 528 ``````Proof. intros; rewrite -always_and_sep_l'; auto. Qed. `````` Robbert Krebbers committed Nov 03, 2016 529 ``````Lemma always_entails_r' P Q : (P ⊢ □ Q) → P ⊢ P ∗ □ Q. `````` Robbert Krebbers committed Oct 25, 2016 530 531 ``````Proof. intros; rewrite -always_and_sep_r'; auto. Qed. `````` Robbert Krebbers committed Nov 27, 2016 532 533 534 535 ``````Lemma always_laterN n P : □ ▷^n P ⊣⊢ ▷^n □ P. Proof. induction n as [|n IH]; simpl; auto. by rewrite always_later IH. Qed. `````` Robbert Krebbers committed Oct 25, 2016 536 537 538 539 540 541 542 543 544 545 546 547 548 549 550 551 552 553 554 555 556 557 558 559 560 561 562 563 564 565 566 567 568 569 570 571 ``````(* Later derived *) Lemma later_proper P Q : (P ⊣⊢ Q) → ▷ P ⊣⊢ ▷ Q. Proof. by intros ->. Qed. Hint Resolve later_mono later_proper. Global Instance later_mono' : Proper ((⊢) ==> (⊢)) (@uPred_later M). Proof. intros P Q; apply later_mono. Qed. Global Instance later_flip_mono' : Proper (flip (⊢) ==> flip (⊢)) (@uPred_later M). Proof. intros P Q; apply later_mono. Qed. Lemma later_intro P : P ⊢ ▷ P. Proof. rewrite -(and_elim_l (▷ P) P) -(löb (▷ P ∧ P)). apply impl_intro_l. by rewrite {1}(and_elim_r (▷ P)). Qed. Lemma later_True : ▷ True ⊣⊢ True. Proof. apply (anti_symm (⊢)); auto using later_intro. Qed. Lemma later_forall {A} (Φ : A → uPred M) : (▷ ∀ a, Φ a) ⊣⊢ (∀ a, ▷ Φ a). Proof. apply (anti_symm _); auto using later_forall_2. apply forall_intro=> x. by rewrite (forall_elim x). Qed. Lemma later_exist `{Inhabited A} (Φ : A → uPred M) : ▷ (∃ a, Φ a) ⊣⊢ (∃ a, ▷ Φ a). Proof. apply: anti_symm; [|apply exist_elim; eauto using exist_intro]. rewrite later_exist_false. apply or_elim; last done. rewrite -(exist_intro inhabitant); auto. Qed. Lemma later_and P Q : ▷ (P ∧ Q) ⊣⊢ ▷ P ∧ ▷ Q. Proof. rewrite !and_alt later_forall. by apply forall_proper=> -[]. Qed. Lemma later_or P Q : ▷ (P ∨ Q) ⊣⊢ ▷ P ∨ ▷ Q. Proof. rewrite !or_alt later_exist. by apply exist_proper=> -[]. Qed. Lemma later_impl P Q : ▷ (P → Q) ⊢ ▷ P → ▷ Q. Proof. apply impl_intro_l; rewrite -later_and; eauto using impl_elim. Qed. `````` Robbert Krebbers committed Nov 03, 2016 572 ``````Lemma later_wand P Q : ▷ (P -∗ Q) ⊢ ▷ P -∗ ▷ Q. `````` Robbert Krebbers committed Oct 25, 2016 573 574 575 576 577 ``````Proof. apply wand_intro_r; rewrite -later_sep; eauto using wand_elim_l. Qed. Lemma later_iff P Q : ▷ (P ↔ Q) ⊢ ▷ P ↔ ▷ Q. Proof. by rewrite /uPred_iff later_and !later_impl. Qed. `````` Robbert Krebbers committed Nov 27, 2016 578 579 580 581 582 583 584 585 586 587 588 589 590 591 592 593 594 595 596 597 598 599 600 601 602 603 604 605 606 607 608 609 610 611 612 613 614 615 616 617 618 619 620 621 622 623 624 625 626 627 628 629 ``````(* Iterated later modality *) Global Instance laterN_ne n m : Proper (dist n ==> dist n) (@uPred_laterN M m). Proof. induction m; simpl. by intros ???. solve_proper. Qed. Global Instance laterN_proper m : Proper ((⊣⊢) ==> (⊣⊢)) (@uPred_laterN M m) := ne_proper _. Lemma laterN_0 P : ▷^0 P ⊣⊢ P. Proof. done. Qed. Lemma later_laterN n P : ▷^(S n) P ⊣⊢ ▷ ▷^n P. Proof. done. Qed. Lemma laterN_later n P : ▷^(S n) P ⊣⊢ ▷^n ▷ P. Proof. induction n; simpl; auto. Qed. Lemma laterN_plus n1 n2 P : ▷^(n1 + n2) P ⊣⊢ ▷^n1 ▷^n2 P. Proof. induction n1; simpl; auto. Qed. Lemma laterN_le n1 n2 P : n1 ≤ n2 → ▷^n1 P ⊢ ▷^n2 P. Proof. induction 1; simpl; by rewrite -?later_intro. Qed. Lemma laterN_mono n P Q : (P ⊢ Q) → ▷^n P ⊢ ▷^n Q. Proof. induction n; simpl; auto. Qed. Global Instance laterN_mono' n : Proper ((⊢) ==> (⊢)) (@uPred_laterN M n). Proof. intros P Q; apply laterN_mono. Qed. Global Instance laterN_flip_mono' n : Proper (flip (⊢) ==> flip (⊢)) (@uPred_laterN M n). Proof. intros P Q; apply laterN_mono. Qed. Lemma laterN_intro n P : P ⊢ ▷^n P. Proof. induction n as [|n IH]; simpl; by rewrite -?later_intro. Qed. Lemma laterN_True n : ▷^n True ⊣⊢ True. Proof. apply (anti_symm (⊢)); auto using laterN_intro. Qed. Lemma laterN_forall {A} n (Φ : A → uPred M) : (▷^n ∀ a, Φ a) ⊣⊢ (∀ a, ▷^n Φ a). Proof. induction n as [|n IH]; simpl; rewrite -?later_forall; auto. Qed. Lemma laterN_exist `{Inhabited A} n (Φ : A → uPred M) : (▷^n ∃ a, Φ a) ⊣⊢ ∃ a, ▷^n Φ a. Proof. induction n as [|n IH]; simpl; rewrite -?later_exist; auto. Qed. Lemma laterN_and n P Q : ▷^n (P ∧ Q) ⊣⊢ ▷^n P ∧ ▷^n Q. Proof. induction n as [|n IH]; simpl; rewrite -?later_and; auto. Qed. Lemma laterN_or n P Q : ▷^n (P ∨ Q) ⊣⊢ ▷^n P ∨ ▷^n Q. Proof. induction n as [|n IH]; simpl; rewrite -?later_or; auto. Qed. Lemma laterN_impl n P Q : ▷^n (P → Q) ⊢ ▷^n P → ▷^n Q. Proof. apply impl_intro_l; rewrite -laterN_and; eauto using impl_elim, laterN_mono. Qed. Lemma laterN_sep n P Q : ▷^n (P ∗ Q) ⊣⊢ ▷^n P ∗ ▷^n Q. Proof. induction n as [|n IH]; simpl; rewrite -?later_sep; auto. Qed. Lemma laterN_wand n P Q : ▷^n (P -∗ Q) ⊢ ▷^n P -∗ ▷^n Q. Proof. apply wand_intro_r; rewrite -laterN_sep; eauto using wand_elim_l,laterN_mono. Qed. Lemma laterN_iff n P Q : ▷^n (P ↔ Q) ⊢ ▷^n P ↔ ▷^n Q. Proof. by rewrite /uPred_iff laterN_and !laterN_impl. Qed. `````` Robbert Krebbers committed Oct 25, 2016 630 631 632 633 634 635 636 637 638 639 640 641 642 ``````(* Conditional always *) Global Instance always_if_ne n p : Proper (dist n ==> dist n) (@uPred_always_if M p). Proof. solve_proper. Qed. Global Instance always_if_proper p : Proper ((⊣⊢) ==> (⊣⊢)) (@uPred_always_if M p). Proof. solve_proper. Qed. Global Instance always_if_mono p : Proper ((⊢) ==> (⊢)) (@uPred_always_if M p). Proof. solve_proper. Qed. Lemma always_if_elim p P : □?p P ⊢ P. Proof. destruct p; simpl; auto using always_elim. Qed. Lemma always_elim_if p P : □ P ⊢ □?p P. Proof. destruct p; simpl; auto using always_elim. Qed. `````` Ralf Jung committed Nov 22, 2016 643 ``````Lemma always_if_pure p φ : □?p ⌜φ⌝ ⊣⊢ ⌜φ⌝. `````` Robbert Krebbers committed Oct 25, 2016 644 645 646 647 648 649 650 ``````Proof. destruct p; simpl; auto using always_pure. Qed. Lemma always_if_and p P Q : □?p (P ∧ Q) ⊣⊢ □?p P ∧ □?p Q. Proof. destruct p; simpl; auto using always_and. Qed. Lemma always_if_or p P Q : □?p (P ∨ Q) ⊣⊢ □?p P ∨ □?p Q. Proof. destruct p; simpl; auto using always_or. Qed. Lemma always_if_exist {A} p (Ψ : A → uPred M) : (□?p ∃ a, Ψ a) ⊣⊢ ∃ a, □?p Ψ a. Proof. destruct p; simpl; auto using always_exist. Qed. `````` Robbert Krebbers committed Nov 03, 2016 651 ``````Lemma always_if_sep p P Q : □?p (P ∗ Q) ⊣⊢ □?p P ∗ □?p Q. `````` Robbert Krebbers committed Oct 25, 2016 652 653 654 655 656 657 ``````Proof. destruct p; simpl; auto using always_sep. Qed. Lemma always_if_later p P : □?p ▷ P ⊣⊢ ▷ □?p P. Proof. destruct p; simpl; auto using always_later. Qed. (* True now *) `````` Robbert Krebbers committed Oct 25, 2016 658 ``````Global Instance except_0_ne n : Proper (dist n ==> dist n) (@uPred_except_0 M). `````` Robbert Krebbers committed Oct 25, 2016 659 ``````Proof. solve_proper. Qed. `````` Robbert Krebbers committed Oct 25, 2016 660 ``````Global Instance except_0_proper : Proper ((⊣⊢) ==> (⊣⊢)) (@uPred_except_0 M). `````` Robbert Krebbers committed Oct 25, 2016 661 ``````Proof. solve_proper. Qed. `````` Robbert Krebbers committed Oct 25, 2016 662 ``````Global Instance except_0_mono' : Proper ((⊢) ==> (⊢)) (@uPred_except_0 M). `````` Robbert Krebbers committed Oct 25, 2016 663 ``````Proof. solve_proper. Qed. `````` Robbert Krebbers committed Oct 25, 2016 664 665 ``````Global Instance except_0_flip_mono' : Proper (flip (⊢) ==> flip (⊢)) (@uPred_except_0 M). `````` Robbert Krebbers committed Oct 25, 2016 666 667 ``````Proof. solve_proper. Qed. `````` Robbert Krebbers committed Oct 25, 2016 668 669 670 ``````Lemma except_0_intro P : P ⊢ ◇ P. Proof. rewrite /uPred_except_0; auto. Qed. Lemma except_0_mono P Q : (P ⊢ Q) → ◇ P ⊢ ◇ Q. `````` Robbert Krebbers committed Oct 25, 2016 671 ``````Proof. by intros ->. Qed. `````` Robbert Krebbers committed Oct 25, 2016 672 673 674 675 676 677 678 679 680 ``````Lemma except_0_idemp P : ◇ ◇ P ⊢ ◇ P. Proof. rewrite /uPred_except_0; auto. Qed. Lemma except_0_True : ◇ True ⊣⊢ True. Proof. rewrite /uPred_except_0. apply (anti_symm _); auto. Qed. Lemma except_0_or P Q : ◇ (P ∨ Q) ⊣⊢ ◇ P ∨ ◇ Q. Proof. rewrite /uPred_except_0. apply (anti_symm _); auto. Qed. Lemma except_0_and P Q : ◇ (P ∧ Q) ⊣⊢ ◇ P ∧ ◇ Q. Proof. by rewrite /uPred_except_0 or_and_l. Qed. `````` Robbert Krebbers committed Nov 03, 2016 681 ``````Lemma except_0_sep P Q : ◇ (P ∗ Q) ⊣⊢ ◇ P ∗ ◇ Q. `````` Robbert Krebbers committed Oct 25, 2016 682 683 ``````Proof. rewrite /uPred_except_0. apply (anti_symm _). `````` Robbert Krebbers committed Oct 25, 2016 684 685 686 687 `````` - apply or_elim; last by auto. by rewrite -!or_intro_l -always_pure -always_later -always_sep_dup'. - rewrite sep_or_r sep_elim_l sep_or_l; auto. Qed. `````` Robbert Krebbers committed Oct 25, 2016 688 ``````Lemma except_0_forall {A} (Φ : A → uPred M) : ◇ (∀ a, Φ a) ⊢ ∀ a, ◇ Φ a. `````` Robbert Krebbers committed Oct 25, 2016 689 ``````Proof. apply forall_intro=> a. by rewrite (forall_elim a). Qed. `````` Robbert Krebbers committed Oct 25, 2016 690 ``````Lemma except_0_exist {A} (Φ : A → uPred M) : (∃ a, ◇ Φ a) ⊢ ◇ ∃ a, Φ a. `````` Robbert Krebbers committed Oct 25, 2016 691 ``````Proof. apply exist_elim=> a. by rewrite (exist_intro a). Qed. `````` Robbert Krebbers committed Oct 25, 2016 692 693 694 695 696 697 ``````Lemma except_0_later P : ◇ ▷ P ⊢ ▷ P. Proof. by rewrite /uPred_except_0 -later_or False_or. Qed. Lemma except_0_always P : ◇ □ P ⊣⊢ □ ◇ P. Proof. by rewrite /uPred_except_0 always_or always_later always_pure. Qed. Lemma except_0_always_if p P : ◇ □?p P ⊣⊢ □?p ◇ P. Proof. destruct p; simpl; auto using except_0_always. Qed. `````` Robbert Krebbers committed Nov 03, 2016 698 ``````Lemma except_0_frame_l P Q : P ∗ ◇ Q ⊢ ◇ (P ∗ Q). `````` Robbert Krebbers committed Oct 25, 2016 699 ``````Proof. by rewrite {1}(except_0_intro P) except_0_sep. Qed. `````` Robbert Krebbers committed Nov 03, 2016 700 ``````Lemma except_0_frame_r P Q : ◇ P ∗ Q ⊢ ◇ (P ∗ Q). `````` Robbert Krebbers committed Oct 25, 2016 701 ``````Proof. by rewrite {1}(except_0_intro Q) except_0_sep. Qed. `````` Robbert Krebbers committed Oct 25, 2016 702 703 704 705 706 707 708 709 710 711 712 713 `````` (* Own and valid derived *) Lemma always_ownM (a : M) : Persistent a → □ uPred_ownM a ⊣⊢ uPred_ownM a. Proof. intros; apply (anti_symm _); first by apply:always_elim. by rewrite {1}always_ownM_core persistent_core. Qed. Lemma ownM_invalid (a : M) : ¬ ✓{0} a → uPred_ownM a ⊢ False. Proof. by intros; rewrite ownM_valid cmra_valid_elim. Qed. Global Instance ownM_mono : Proper (flip (≼) ==> (⊢)) (@uPred_ownM M). Proof. intros a b [b' ->]. rewrite ownM_op. eauto. Qed. Lemma ownM_empty' : uPred_ownM ∅ ⊣⊢ True. `````` 714 ``````Proof. apply (anti_symm _); first by auto. apply ownM_empty. Qed. `````` Robbert Krebbers committed Oct 25, 2016 715 716 717 718 719 720 721 722 723 724 725 ``````Lemma always_cmra_valid {A : cmraT} (a : A) : □ ✓ a ⊣⊢ ✓ a. Proof. intros; apply (anti_symm _); first by apply:always_elim. apply:always_cmra_valid_1. Qed. (** * Derived rules *) Global Instance bupd_mono' : Proper ((⊢) ==> (⊢)) (@uPred_bupd M). Proof. intros P Q; apply bupd_mono. Qed. Global Instance bupd_flip_mono' : Proper (flip (⊢) ==> flip (⊢)) (@uPred_bupd M). Proof. intros P Q; apply bupd_mono. Qed. `````` Robbert Krebbers committed Nov 03, 2016 726 ``````Lemma bupd_frame_l R Q : (R ∗ |==> Q) ==∗ R ∗ Q. `````` Robbert Krebbers committed Oct 25, 2016 727 ``````Proof. rewrite !(comm _ R); apply bupd_frame_r. Qed. `````` Robbert Krebbers committed Nov 03, 2016 728 ``````Lemma bupd_wand_l P Q : (P -∗ Q) ∗ (|==> P) ==∗ Q. `````` Robbert Krebbers committed Oct 25, 2016 729 ``````Proof. by rewrite bupd_frame_l wand_elim_l. Qed. `````` Robbert Krebbers committed Nov 03, 2016 730 ``````Lemma bupd_wand_r P Q : (|==> P) ∗ (P -∗ Q) ==∗ Q. `````` Robbert Krebbers committed Oct 25, 2016 731 ``````Proof. by rewrite bupd_frame_r wand_elim_r. Qed. `````` Robbert Krebbers committed Nov 03, 2016 732 ``````Lemma bupd_sep P Q : (|==> P) ∗ (|==> Q) ==∗ P ∗ Q. `````` Robbert Krebbers committed Oct 25, 2016 733 734 735 736 737 738 ``````Proof. by rewrite bupd_frame_r bupd_frame_l bupd_trans. Qed. Lemma bupd_ownM_update x y : x ~~> y → uPred_ownM x ⊢ |==> uPred_ownM y. Proof. intros; rewrite (bupd_ownM_updateP _ (y =)); last by apply cmra_update_updateP. by apply bupd_mono, exist_elim=> y'; apply pure_elim_l=> ->. Qed. `````` Robbert Krebbers committed Oct 25, 2016 739 ``````Lemma except_0_bupd P : ◇ (|==> P) ⊢ (|==> ◇ P). `````` Robbert Krebbers committed Oct 25, 2016 740 ``````Proof. `````` Robbert Krebbers committed Oct 25, 2016 741 `````` rewrite /uPred_except_0. apply or_elim; auto using bupd_mono. `````` Robbert Krebbers committed Oct 25, 2016 742 743 744 745 `````` by rewrite -bupd_intro -or_intro_l. Qed. (* Timeless instances *) `````` Ralf Jung committed Nov 22, 2016 746 ``````Global Instance pure_timeless φ : TimelessP (⌜φ⌝ : uPred M)%I. `````` Robbert Krebbers committed Oct 25, 2016 747 748 749 750 751 752 753 ``````Proof. rewrite /TimelessP pure_alt later_exist_false. by setoid_rewrite later_True. Qed. Global Instance valid_timeless {A : cmraT} `{CMRADiscrete A} (a : A) : TimelessP (✓ a : uPred M)%I. Proof. rewrite /TimelessP !discrete_valid. apply (timelessP _). Qed. Global Instance and_timeless P Q: TimelessP P → TimelessP Q → TimelessP (P ∧ Q). `````` Robbert Krebbers committed Oct 25, 2016 754 ``````Proof. intros; rewrite /TimelessP except_0_and later_and; auto. Qed. `````` Robbert Krebbers committed Oct 25, 2016 755 ``````Global Instance or_timeless P Q : TimelessP P → TimelessP Q → TimelessP (P ∨ Q). `````` Robbert Krebbers committed Oct 25, 2016 756 ``````Proof. intros; rewrite /TimelessP except_0_or later_or; auto. Qed. `````` Robbert Krebbers committed Oct 25, 2016 757 758 759 760 761 ``````Global Instance impl_timeless P Q : TimelessP Q → TimelessP (P → Q). Proof. rewrite /TimelessP=> HQ. rewrite later_false_excluded_middle. apply or_mono, impl_intro_l; first done. rewrite -{2}(löb Q); apply impl_intro_l. `````` Robbert Krebbers committed Oct 25, 2016 762 `````` rewrite HQ /uPred_except_0 !and_or_r. apply or_elim; last auto. `````` Robbert Krebbers committed Oct 25, 2016 763 764 `````` by rewrite assoc (comm _ _ P) -assoc !impl_elim_r. Qed. `````` Robbert Krebbers committed Nov 03, 2016 765 ``````Global Instance sep_timeless P Q: TimelessP P → TimelessP Q → TimelessP (P ∗ Q). `````` Robbert Krebbers committed Oct 25, 2016 766 ``````Proof. intros; rewrite /TimelessP except_0_sep later_sep; auto. Qed. `````` Robbert Krebbers committed Nov 03, 2016 767 ``````Global Instance wand_timeless P Q : TimelessP Q → TimelessP (P -∗ Q). `````` Robbert Krebbers committed Oct 25, 2016 768 769 770 771 ``````Proof. rewrite /TimelessP=> HQ. rewrite later_false_excluded_middle. apply or_mono, wand_intro_l; first done. rewrite -{2}(löb Q); apply impl_intro_l. `````` Robbert Krebbers committed Oct 25, 2016 772 `````` rewrite HQ /uPred_except_0 !and_or_r. apply or_elim; last auto. `````` Robbert Krebbers committed Oct 25, 2016 773 774 775 776 777 778 779 780 781 `````` rewrite -(always_pure) -always_later always_and_sep_l'. by rewrite assoc (comm _ _ P) -assoc -always_and_sep_l' impl_elim_r wand_elim_r. Qed. Global Instance forall_timeless {A} (Ψ : A → uPred M) : (∀ x, TimelessP (Ψ x)) → TimelessP (∀ x, Ψ x). Proof. rewrite /TimelessP=> HQ. rewrite later_false_excluded_middle. apply or_mono; first done. apply forall_intro=> x. rewrite -(löb (Ψ x)); apply impl_intro_l. `````` Robbert Krebbers committed Oct 25, 2016 782 `````` rewrite HQ /uPred_except_0 !and_or_r. apply or_elim; last auto. `````` Robbert Krebbers committed Oct 25, 2016 783 784 785 786 787 788 `````` by rewrite impl_elim_r (forall_elim x). Qed. Global Instance exist_timeless {A} (Ψ : A → uPred M) : (∀ x, TimelessP (Ψ x)) → TimelessP (∃ x, Ψ x). Proof. rewrite /TimelessP=> ?. rewrite later_exist_false. apply or_elim. `````` Robbert Krebbers committed Oct 25, 2016 789 `````` - rewrite /uPred_except_0; auto. `````` Robbert Krebbers committed Oct 25, 2016 790 791 792 `````` - apply exist_elim=> x. rewrite -(exist_intro x); auto. Qed. Global Instance always_timeless P : TimelessP P → TimelessP (□ P). `````` Robbert Krebbers committed Oct 25, 2016 793 ``````Proof. intros; rewrite /TimelessP except_0_always -always_later; auto. Qed. `````` Robbert Krebbers committed Oct 25, 2016 794 795 ``````Global Instance always_if_timeless p P : TimelessP P → TimelessP (□?p P). Proof. destruct p; apply _. Qed. `````` Ralf Jung committed Nov 22, 2016 796 ``````Global Instance eq_timeless {A : ofeT} (a b : A) : `````` Robbert Krebbers committed Oct 25, 2016 797 798 799 800 801 `````` Timeless a → TimelessP (a ≡ b : uPred M)%I. Proof. intros. rewrite /TimelessP !timeless_eq. apply (timelessP _). Qed. Global Instance ownM_timeless (a : M) : Timeless a → TimelessP (uPred_ownM a). Proof. intros ?. rewrite /TimelessP later_ownM. apply exist_elim=> b. `````` Robbert Krebbers committed Oct 25, 2016 802 `````` rewrite (timelessP (a≡b)) (except_0_intro (uPred_ownM b)) -except_0_and. `````` Robbert Krebbers committed Oct 25, 2016 803 804 `````` apply except_0_mono. rewrite internal_eq_sym. apply (internal_eq_rewrite b a (uPred_ownM)); first apply _; auto. `````` Robbert Krebbers committed Oct 25, 2016 805 ``````Qed. `````` Robbert Krebbers committed Nov 29, 2016 806 807 808 ``````Global Instance from_option_timeless {A} P (Ψ : A → uPred M) (mx : option A) : (∀ x, TimelessP (Ψ x)) → TimelessP P → TimelessP (from_option Ψ P mx). Proof. destruct mx; apply _. Qed. `````` Robbert Krebbers committed Oct 25, 2016 809 810 `````` (* Persistence *) `````` Ralf Jung committed Nov 22, 2016 811 ``````Global Instance pure_persistent φ : PersistentP (⌜φ⌝ : uPred M)%I. `````` Robbert Krebbers committed Oct 25, 2016 812 813 814 815 816 817 818 819 820 821 ``````Proof. by rewrite /PersistentP always_pure. Qed. Global Instance always_persistent P : PersistentP (□ P). Proof. by intros; apply always_intro'. Qed. Global Instance and_persistent P Q : PersistentP P → PersistentP Q → PersistentP (P ∧ Q). Proof. by intros; rewrite /PersistentP always_and; apply and_mono. Qed. Global Instance or_persistent P Q : PersistentP P → PersistentP Q → PersistentP (P ∨ Q). Proof. by intros; rewrite /PersistentP always_or; apply or_mono. Qed. Global Instance sep_persistent P Q : `````` Robbert Krebbers committed Nov 03, 2016 822 `````` PersistentP P → PersistentP Q → PersistentP (P ∗ Q). `````` Robbert Krebbers committed Oct 25, 2016 823 824 825 826 827 828 829 ``````Proof. by intros; rewrite /PersistentP always_sep; apply sep_mono. Qed. Global Instance forall_persistent {A} (Ψ : A → uPred M) : (∀ x, PersistentP (Ψ x)) → PersistentP (∀ x, Ψ x). Proof. by intros; rewrite /PersistentP always_forall; apply forall_mono. Qed. Global Instance exist_persistent {A} (Ψ : A → uPred M) : (∀ x, PersistentP (Ψ x)) → PersistentP (∃ x, Ψ x). Proof. by intros; rewrite /PersistentP always_exist; apply exist_mono. Qed. `````` Ralf Jung committed Nov 22, 2016 830 ``````Global Instance internal_eq_persistent {A : ofeT} (a b : A) : `````` Robbert Krebbers committed Oct 25, 2016 831 `````` PersistentP (a ≡ b : uPred M)%I. `````` Robbert Krebbers committed Oct 25, 2016 832 ``````Proof. by intros; rewrite /PersistentP always_internal_eq. Qed. `````` Robbert Krebbers committed Oct 25, 2016 833 834 835 836 837 ``````Global Instance cmra_valid_persistent {A : cmraT} (a : A) : PersistentP (✓ a : uPred M)%I. Proof. by intros; rewrite /PersistentP always_cmra_valid. Qed. Global Instance later_persistent P : PersistentP P → PersistentP (▷ P). Proof. by intros; rewrite /PersistentP always_later; apply later_mono. Qed. `````` Robbert Krebbers committed Nov 27, 2016 838 839 ``````Global Instance laterN_persistent n P : PersistentP P → PersistentP (▷^n P). Proof. induction n; apply _. Qed. `````` Robbert Krebbers committed Oct 25, 2016 840 841 842 843 844 845 846 847 848 849 850 851 852 ``````Global Instance ownM_persistent : Persistent a → PersistentP (@uPred_ownM M a). Proof. intros. by rewrite /PersistentP always_ownM. Qed. Global Instance from_option_persistent {A} P (Ψ : A → uPred M) (mx : option A) : (∀ x, PersistentP (Ψ x)) → PersistentP P → PersistentP (from_option Ψ P mx). Proof. destruct mx; apply _. Qed. (* Derived lemmas for persistence *) Lemma always_always P `{!PersistentP P} : □ P ⊣⊢ P. Proof. apply (anti_symm (⊢)); auto using always_elim. Qed. Lemma always_if_always p P `{!PersistentP P} : □?p P ⊣⊢ P. Proof. destruct p; simpl; auto using always_always. Qed. Lemma always_intro P Q `{!PersistentP P} : (P ⊢ Q) → P ⊢ □ Q. Proof. rewrite -(always_always P); apply always_intro'. Qed. `````` Robbert Krebbers committed Nov 03, 2016 853 ``````Lemma always_and_sep_l P Q `{!PersistentP P} : P ∧ Q ⊣⊢ P ∗ Q. `````` Robbert Krebbers committed Oct 25, 2016 854 ``````Proof. by rewrite -(always_always P) always_and_sep_l'. Qed. `````` Robbert Krebbers committed Nov 03, 2016 855 ``````Lemma always_and_sep_r P Q `{!PersistentP Q} : P ∧ Q ⊣⊢ P ∗ Q. `````` Robbert Krebbers committed Oct 25, 2016 856 ``````Proof. by rewrite -(always_always Q) always_and_sep_r'. Qed. `````` Robbert Krebbers committed Nov 03, 2016 857 ``````Lemma always_sep_dup P `{!PersistentP P} : P ⊣⊢ P ∗ P. `````` Robbert Krebbers committed Oct 25, 2016 858 ``````Proof. by rewrite -(always_always P) -always_sep_dup'. Qed. `````` Robbert Krebbers committed Nov 03, 2016 859 ``````Lemma always_entails_l P Q `{!PersistentP Q} : (P ⊢ Q) → P ⊢ Q ∗ P. `````` Robbert Krebbers committed Oct 25, 2016 860 ``````Proof. by rewrite -(always_always Q); apply always_entails_l'. Qed. `````` Robbert Krebbers committed Nov 03, 2016 861 ``````Lemma always_entails_r P Q `{!PersistentP Q} : (P ⊢ Q) → P ⊢ P ∗ Q. `````` Robbert Krebbers committed Oct 25, 2016 862 863 ``````Proof. by rewrite -(always_always Q); apply always_entails_r'. Qed. End derived. `````` Robbert Krebbers committed Dec 13, 2016 864 ``End uPred.``