derived.v 55.5 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, 2017 19 ``````Definition uPred_persistently_if {M} (p : bool) (P : uPred M) : uPred M := `````` Robbert Krebbers committed Oct 25, 2016 20 `````` (if p then □ P else P)%I. `````` Robbert Krebbers committed Oct 25, 2017 21 22 23 ``````Instance: Params (@uPred_persistently_if) 2. Arguments uPred_persistently_if _ !_ _/. Notation "□? p P" := (uPred_persistently_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 `````` `````` Robbert Krebbers committed Oct 25, 2017 32 ``````Class Timeless {M} (P : uPred M) := timelessP : ▷ P ⊢ ◇ P. `````` Robbert Krebbers committed Oct 25, 2016 33 ``````Arguments timelessP {_} _ {_}. `````` Robbert Krebbers committed Oct 25, 2017 34 35 ``````Hint Mode Timeless + ! : typeclass_instances. Instance: Params (@Timeless) 1. `````` Robbert Krebbers committed Oct 25, 2016 36 `````` `````` Robbert Krebbers committed Oct 25, 2017 37 38 39 40 ``````Class Persistent {M} (P : uPred M) := persistent : P ⊢ □ P. Arguments persistent {_} _ {_}. Hint Mode Persistent + ! : typeclass_instances. Instance: Params (@Persistent) 1. `````` Robbert Krebbers committed Oct 25, 2016 41 `````` `````` Amin Timany committed Oct 26, 2017 42 43 44 45 46 ``````Class Plain {M} (P : uPred M) := plain : P ⊢ ■ P. Arguments plain {_} _ {_}. Hint Mode Plain + ! : typeclass_instances. Instance: Params (@Plain) 1. `````` Robbert Krebbers committed Dec 13, 2016 47 ``````Module uPred. `````` Robbert Krebbers committed Oct 25, 2016 48 49 50 51 52 53 54 55 56 57 ``````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 58 ``````Proof. by apply (pure_elim' False). Qed. `````` Robbert Krebbers committed Oct 25, 2016 59 60 61 62 63 64 65 66 67 68 69 70 71 72 73 74 75 76 77 78 79 80 81 82 83 84 85 86 87 88 89 ``````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. `````` 90 ``````Lemma impl_entails P Q : (P → Q)%I → P ⊢ Q. `````` Robbert Krebbers committed Oct 25, 2016 91 ``````Proof. intros HPQ; apply impl_elim with P; rewrite -?HPQ; auto. Qed. `````` 92 93 ``````Lemma entails_impl P Q : (P ⊢ Q) → (P → Q)%I. Proof. intro. apply impl_intro_l. auto. Qed. `````` Robbert Krebbers committed Oct 25, 2016 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 127 128 129 130 131 132 133 134 135 `````` 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 136 137 138 ``````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 139 140 141 ``````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 142 143 144 ``````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 145 ``````Global Instance exist_mono' A : `````` Jacques-Henri Jourdan committed Aug 07, 2017 146 `````` Proper (pointwise_relation _ (⊢) ==> (⊢)) (@uPred_exist M A). `````` Robbert Krebbers committed Oct 28, 2016 147 148 149 ``````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 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 177 178 179 180 181 182 183 184 185 ``````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 186 187 188 189 190 ``````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 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 218 219 220 221 222 223 224 225 226 `````` 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 227 228 229 230 231 232 233 ``````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 234 `````` `````` Ralf Jung committed Nov 22, 2016 235 ``````Lemma pure_elim φ Q R : (Q ⊢ ⌜φ⌝) → (φ → Q ⊢ R) → Q ⊢ R. `````` Robbert Krebbers committed Nov 22, 2016 236 237 238 239 ``````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 240 ``````Lemma pure_mono φ1 φ2 : (φ1 → φ2) → ⌜φ1⌝ ⊢ ⌜φ2⌝. `````` Robbert Krebbers committed Oct 25, 2016 241 242 243 ``````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. `````` Jacques-Henri Jourdan committed Aug 07, 2017 244 245 ``````Global Instance pure_flip_mono : Proper (flip impl ==> flip (⊢)) (@uPred_pure M). Proof. intros φ1 φ2; apply pure_mono. Qed. `````` Ralf Jung committed Nov 22, 2016 246 ``````Lemma pure_iff φ1 φ2 : (φ1 ↔ φ2) → ⌜φ1⌝ ⊣⊢ ⌜φ2⌝. `````` Robbert Krebbers committed Oct 25, 2016 247 ``````Proof. intros [??]; apply (anti_symm _); auto using pure_mono. Qed. `````` Ralf Jung committed Nov 22, 2016 248 ``````Lemma pure_intro_l φ Q R : φ → (⌜φ⌝ ∧ Q ⊢ R) → Q ⊢ R. `````` Robbert Krebbers committed Oct 25, 2016 249 ``````Proof. intros ? <-; auto using pure_intro. Qed. `````` Ralf Jung committed Nov 22, 2016 250 ``````Lemma pure_intro_r φ Q R : φ → (Q ∧ ⌜φ⌝ ⊢ R) → Q ⊢ R. `````` Robbert Krebbers committed Oct 25, 2016 251 ``````Proof. intros ? <-; auto. Qed. `````` Ralf Jung committed Nov 22, 2016 252 ``````Lemma pure_intro_impl φ Q R : φ → (Q ⊢ ⌜φ⌝ → R) → Q ⊢ R. `````` Robbert Krebbers committed Oct 25, 2016 253 ``````Proof. intros ? ->. eauto using pure_intro_l, impl_elim_r. Qed. `````` Ralf Jung committed Nov 22, 2016 254 ``````Lemma pure_elim_l φ Q R : (φ → Q ⊢ R) → ⌜φ⌝ ∧ Q ⊢ R. `````` Robbert Krebbers committed Oct 25, 2016 255 ``````Proof. intros; apply pure_elim with φ; eauto. Qed. `````` Ralf Jung committed Nov 22, 2016 256 ``````Lemma pure_elim_r φ Q R : (φ → Q ⊢ R) → Q ∧ ⌜φ⌝ ⊢ R. `````` Robbert Krebbers committed Oct 25, 2016 257 ``````Proof. intros; apply pure_elim with φ; eauto. Qed. `````` Robbert Krebbers committed Nov 21, 2016 258 `````` `````` Ralf Jung committed Nov 22, 2016 259 ``````Lemma pure_True (φ : Prop) : φ → ⌜φ⌝ ⊣⊢ True. `````` Robbert Krebbers committed Oct 25, 2016 260 ``````Proof. intros; apply (anti_symm _); auto. Qed. `````` Ralf Jung committed Nov 22, 2016 261 ``````Lemma pure_False (φ : Prop) : ¬φ → ⌜φ⌝ ⊣⊢ False. `````` Robbert Krebbers committed Nov 21, 2016 262 ``````Proof. intros; apply (anti_symm _); eauto using pure_elim. Qed. `````` Robbert Krebbers committed Oct 25, 2016 263 `````` `````` Ralf Jung committed Nov 22, 2016 264 ``````Lemma pure_and φ1 φ2 : ⌜φ1 ∧ φ2⌝ ⊣⊢ ⌜φ1⌝ ∧ ⌜φ2⌝. `````` Robbert Krebbers committed Oct 25, 2016 265 266 267 268 269 ``````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 270 ``````Lemma pure_or φ1 φ2 : ⌜φ1 ∨ φ2⌝ ⊣⊢ ⌜φ1⌝ ∨ ⌜φ2⌝. `````` Robbert Krebbers committed Oct 25, 2016 271 272 273 274 275 ``````Proof. apply (anti_symm _). - eapply pure_elim=> // -[?|?]; auto. - apply or_elim; eapply pure_elim; eauto. Qed. `````` Ralf Jung committed Nov 22, 2016 276 ``````Lemma pure_impl φ1 φ2 : ⌜φ1 → φ2⌝ ⊣⊢ (⌜φ1⌝ → ⌜φ2⌝). `````` Robbert Krebbers committed Oct 25, 2016 277 278 279 280 ``````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 281 `````` by rewrite -(left_id True uPred_and (_→_))%I (pure_True φ1) // impl_elim_r. `````` Robbert Krebbers committed Oct 25, 2016 282 ``````Qed. `````` Ralf Jung committed Nov 22, 2016 283 ``````Lemma pure_forall {A} (φ : A → Prop) : ⌜∀ x, φ x⌝ ⊣⊢ ∀ x, ⌜φ x⌝. `````` Robbert Krebbers committed Oct 25, 2016 284 285 286 287 ``````Proof. apply (anti_symm _); auto using pure_forall_2. apply forall_intro=> x. eauto using pure_mono. Qed. `````` Ralf Jung committed Nov 22, 2016 288 ``````Lemma pure_exist {A} (φ : A → Prop) : ⌜∃ x, φ x⌝ ⊣⊢ ∃ x, ⌜φ x⌝. `````` Robbert Krebbers committed Oct 25, 2016 289 290 291 292 293 294 ``````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 295 ``````Lemma internal_eq_refl' {A : ofeT} (a : A) P : P ⊢ a ≡ a. `````` Robbert Krebbers committed Oct 25, 2016 296 297 ``````Proof. rewrite (True_intro P). apply internal_eq_refl. Qed. Hint Resolve internal_eq_refl'. `````` Ralf Jung committed Nov 22, 2016 298 ``````Lemma equiv_internal_eq {A : ofeT} P (a b : A) : a ≡ b → P ⊢ a ≡ b. `````` Robbert Krebbers committed Oct 25, 2016 299 ``````Proof. by intros ->. Qed. `````` Ralf Jung committed Nov 22, 2016 300 ``````Lemma internal_eq_sym {A : ofeT} (a b : A) : a ≡ b ⊢ b ≡ a. `````` Ralf Jung committed Dec 05, 2016 301 ``````Proof. `````` Robbert Krebbers committed Oct 29, 2017 302 303 `````` rewrite (internal_eq_rewrite a b (λ b, b ≡ a)%I ltac:(solve_proper)). by rewrite -internal_eq_refl True_impl. `````` Ralf Jung committed Dec 05, 2016 304 ``````Qed. `````` Robbert Krebbers committed Oct 29, 2017 305 306 307 308 309 310 311 312 313 ``````Lemma f_equiv {A B : ofeT} (f : A → B) `{!NonExpansive f} x y : x ≡ y ⊢ f x ≡ f y. Proof. rewrite (internal_eq_rewrite x y (λ y, f x ≡ f y)%I ltac:(solve_proper)). by rewrite -internal_eq_refl True_impl. Qed. Lemma internal_eq_rewrite_contractive {A : ofeT} a b (Ψ : A → uPred M) {HΨ : Contractive Ψ} : ▷ (a ≡ b) ⊢ Ψ a → Ψ b. Proof. move: HΨ=> /contractiveI ->. by rewrite (internal_eq_rewrite _ _ id). Qed. `````` Robbert Krebbers committed Oct 25, 2016 314 `````` `````` Ralf Jung committed Nov 22, 2016 315 ``````Lemma pure_impl_forall φ P : (⌜φ⌝ → P) ⊣⊢ (∀ _ : φ, P). `````` Robbert Krebbers committed Nov 20, 2016 316 317 ``````Proof. apply (anti_symm _). `````` Robbert Krebbers committed Nov 21, 2016 318 `````` - apply forall_intro=> ?. by rewrite pure_True // left_id. `````` Robbert Krebbers committed Nov 20, 2016 319 320 `````` - apply impl_intro_l, pure_elim_l=> Hφ. by rewrite (forall_elim Hφ). Qed. `````` Ralf Jung committed Nov 22, 2016 321 ``````Lemma pure_alt φ : ⌜φ⌝ ⊣⊢ ∃ _ : φ, True. `````` Robbert Krebbers committed Oct 25, 2016 322 323 324 325 326 327 328 329 330 331 332 333 334 335 336 337 ``````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. `````` Ralf Jung committed Jan 27, 2017 338 ``````Global Instance iff_ne : NonExpansive2 (@uPred_iff M). `````` Robbert Krebbers committed Oct 25, 2016 339 340 341 342 343 344 ``````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. `````` 345 ``````Lemma iff_equiv P Q : (P ↔ Q)%I → (P ⊣⊢ Q). `````` Robbert Krebbers committed Oct 25, 2016 346 347 ``````Proof. intros HPQ; apply (anti_symm (⊢)); `````` 348 `````` apply impl_entails; rewrite /uPred_valid HPQ /uPred_iff; auto. `````` Robbert Krebbers committed Oct 25, 2016 349 ``````Qed. `````` 350 ``````Lemma equiv_iff P Q : (P ⊣⊢ Q) → (P ↔ Q)%I. `````` Robbert Krebbers committed Oct 25, 2016 351 ``````Proof. intros ->; apply iff_refl. Qed. `````` Robbert Krebbers committed Oct 25, 2016 352 ``````Lemma internal_eq_iff P Q : P ≡ Q ⊢ P ↔ Q. `````` Robbert Krebbers committed Oct 25, 2016 353 ``````Proof. `````` Robbert Krebbers committed Oct 29, 2017 354 355 `````` rewrite (internal_eq_rewrite P Q (λ Q, P ↔ Q)%I ltac:(solve_proper)). by rewrite -(iff_refl True) True_impl. `````` Robbert Krebbers committed Oct 25, 2016 356 357 358 359 ``````Qed. (* Derived BI Stuff *) Hint Resolve sep_mono. `````` Robbert Krebbers committed Nov 03, 2016 360 ``````Lemma sep_mono_l P P' Q : (P ⊢ Q) → P ∗ P' ⊢ Q ∗ P'. `````` Robbert Krebbers committed Oct 25, 2016 361 ``````Proof. by intros; apply sep_mono. Qed. `````` Robbert Krebbers committed Nov 03, 2016 362 ``````Lemma sep_mono_r P P' Q' : (P' ⊢ Q') → P ∗ P' ⊢ P ∗ Q'. `````` Robbert Krebbers committed Oct 25, 2016 363 364 365 366 367 368 ``````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 369 ``````Lemma wand_mono P P' Q Q' : (Q ⊢ P) → (P' ⊢ Q') → (P -∗ P') ⊢ Q -∗ Q'. `````` Robbert Krebbers committed Oct 25, 2016 370 371 372 373 374 ``````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 375 376 377 ``````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 378 379 380 381 382 383 384 385 386 387 388 389 `````` 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 390 ``````Lemma sep_elim_l P Q : P ∗ Q ⊢ P. `````` Robbert Krebbers committed Oct 25, 2016 391 ``````Proof. by rewrite (True_intro Q) right_id. Qed. `````` Robbert Krebbers committed Nov 03, 2016 392 393 394 ``````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 395 ``````Proof. intros ->; apply sep_elim_l. Qed. `````` Robbert Krebbers committed Nov 03, 2016 396 ``````Lemma sep_elim_r' P Q R : (Q ⊢ R) → P ∗ Q ⊢ R. `````` Robbert Krebbers committed Oct 25, 2016 397 398 ``````Proof. intros ->; apply sep_elim_r. Qed. Hint Resolve sep_elim_l' sep_elim_r'. `````` 399 ``````Lemma sep_intro_True_l P Q R : P%I → (R ⊢ Q) → R ⊢ P ∗ Q. `````` Robbert Krebbers committed Oct 25, 2016 400 ``````Proof. by intros; rewrite -(left_id True%I uPred_sep R); apply sep_mono. Qed. `````` 401 ``````Lemma sep_intro_True_r P Q R : (R ⊢ P) → Q%I → R ⊢ P ∗ Q. `````` Robbert Krebbers committed Oct 25, 2016 402 ``````Proof. by intros; rewrite -(right_id True%I uPred_sep R); apply sep_mono. Qed. `````` 403 ``````Lemma sep_elim_True_l P Q R : P → (P ∗ R ⊢ Q) → R ⊢ Q. `````` Robbert Krebbers committed Oct 25, 2016 404 ``````Proof. by intros HP; rewrite -HP left_id. Qed. `````` 405 ``````Lemma sep_elim_True_r P Q R : P → (R ∗ P ⊢ Q) → R ⊢ Q. `````` Robbert Krebbers committed Oct 25, 2016 406 ``````Proof. by intros HP; rewrite -HP right_id. Qed. `````` Robbert Krebbers committed Nov 03, 2016 407 ``````Lemma wand_intro_l P Q R : (Q ∗ P ⊢ R) → P ⊢ Q -∗ R. `````` Robbert Krebbers committed Oct 25, 2016 408 ``````Proof. rewrite comm; apply wand_intro_r. Qed. `````` Robbert Krebbers committed Nov 03, 2016 409 ``````Lemma wand_elim_l P Q : (P -∗ Q) ∗ P ⊢ Q. `````` Robbert Krebbers committed Oct 25, 2016 410 ``````Proof. by apply wand_elim_l'. Qed. `````` Robbert Krebbers committed Nov 03, 2016 411 ``````Lemma wand_elim_r P Q : P ∗ (P -∗ Q) ⊢ Q. `````` Robbert Krebbers committed Oct 25, 2016 412 ``````Proof. rewrite (comm _ P); apply wand_elim_l. Qed. `````` Robbert Krebbers committed Nov 03, 2016 413 ``````Lemma wand_elim_r' P Q R : (Q ⊢ P -∗ R) → P ∗ Q ⊢ R. `````` Robbert Krebbers committed Oct 25, 2016 414 ``````Proof. intros ->; apply wand_elim_r. Qed. `````` Robbert Krebbers committed Nov 03, 2016 415 ``````Lemma wand_apply P Q R S : (P ⊢ Q -∗ R) → (S ⊢ P ∗ Q) → S ⊢ R. `````` Ralf Jung committed Nov 01, 2016 416 ``````Proof. intros HR%wand_elim_l' HQ. by rewrite HQ. Qed. `````` Robbert Krebbers committed Nov 03, 2016 417 ``````Lemma wand_frame_l P Q R : (Q -∗ R) ⊢ P ∗ Q -∗ P ∗ R. `````` Robbert Krebbers committed Oct 25, 2016 418 ``````Proof. apply wand_intro_l. rewrite -assoc. apply sep_mono_r, wand_elim_r. Qed. `````` Robbert Krebbers committed Nov 03, 2016 419 ``````Lemma wand_frame_r P Q R : (Q -∗ R) ⊢ Q ∗ P -∗ R ∗ P. `````` Robbert Krebbers committed Oct 25, 2016 420 ``````Proof. `````` Robbert Krebbers committed Nov 03, 2016 421 `````` apply wand_intro_l. rewrite ![(_ ∗ P)%I]comm -assoc. `````` Robbert Krebbers committed Oct 25, 2016 422 423 `````` apply sep_mono_r, wand_elim_r. Qed. `````` Robbert Krebbers committed Nov 03, 2016 424 ``````Lemma wand_diag P : (P -∗ P) ⊣⊢ True. `````` Robbert Krebbers committed Oct 25, 2016 425 ``````Proof. apply (anti_symm _); auto. apply wand_intro_l; by rewrite right_id. Qed. `````` Robbert Krebbers committed Nov 03, 2016 426 ``````Lemma wand_True P : (True -∗ P) ⊣⊢ P. `````` Robbert Krebbers committed Oct 25, 2016 427 428 ``````Proof. apply (anti_symm _); last by auto using wand_intro_l. `````` 429 `````` eapply sep_elim_True_l; last by apply wand_elim_r. done. `````` Robbert Krebbers committed Oct 25, 2016 430 ``````Qed. `````` 431 ``````Lemma wand_entails P Q : (P -∗ Q)%I → P ⊢ Q. `````` Robbert Krebbers committed Oct 25, 2016 432 433 434 ``````Proof. intros HPQ. eapply sep_elim_True_r; first exact: HPQ. by rewrite wand_elim_r. Qed. `````` 435 436 ``````Lemma entails_wand P Q : (P ⊢ Q) → (P -∗ Q)%I. Proof. intro. apply wand_intro_l. auto. Qed. `````` Robbert Krebbers committed Nov 03, 2016 437 ``````Lemma wand_curry P Q R : (P -∗ Q -∗ R) ⊣⊢ (P ∗ Q -∗ R). `````` Robbert Krebbers committed Oct 25, 2016 438 439 440 441 442 443 ``````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 444 ``````Lemma sep_and P Q : (P ∗ Q) ⊢ (P ∧ Q). `````` Robbert Krebbers committed Oct 25, 2016 445 ``````Proof. auto. Qed. `````` 446 ``````Lemma impl_wand_1 P Q : (P → Q) ⊢ P -∗ Q. `````` Robbert Krebbers committed Oct 25, 2016 447 ``````Proof. apply wand_intro_r, impl_elim with P; auto. Qed. `````` Ralf Jung committed Nov 22, 2016 448 ``````Lemma pure_elim_sep_l φ Q R : (φ → Q ⊢ R) → ⌜φ⌝ ∗ Q ⊢ R. `````` Robbert Krebbers committed Oct 25, 2016 449 ``````Proof. intros; apply pure_elim with φ; eauto. Qed. `````` Ralf Jung committed Nov 22, 2016 450 ``````Lemma pure_elim_sep_r φ Q R : (φ → Q ⊢ R) → Q ∗ ⌜φ⌝ ⊢ R. `````` Robbert Krebbers committed Oct 25, 2016 451 452 453 454 455 456 457 ``````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 458 ``````Lemma entails_equiv_and P Q : (P ⊣⊢ Q ∧ P) ↔ (P ⊢ Q). `````` Robbert Krebbers committed Dec 27, 2016 459 ``````Proof. split. by intros ->; auto. intros; apply (anti_symm _); auto. Qed. `````` Robbert Krebbers committed Nov 03, 2016 460 ``````Lemma sep_and_l P Q R : P ∗ (Q ∧ R) ⊢ (P ∗ Q) ∧ (P ∗ R). `````` Robbert Krebbers committed Oct 25, 2016 461 ``````Proof. auto. Qed. `````` Robbert Krebbers committed Nov 03, 2016 462 ``````Lemma sep_and_r P Q R : (P ∧ Q) ∗ R ⊢ (P ∗ R) ∧ (Q ∗ R). `````` Robbert Krebbers committed Oct 25, 2016 463 ``````Proof. auto. Qed. `````` Robbert Krebbers committed Nov 03, 2016 464 ``````Lemma sep_or_l P Q R : P ∗ (Q ∨ R) ⊣⊢ (P ∗ Q) ∨ (P ∗ R). `````` Robbert Krebbers committed Oct 25, 2016 465 466 467 468 ``````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 469 ``````Lemma sep_or_r P Q R : (P ∨ Q) ∗ R ⊣⊢ (P ∗ R) ∨ (Q ∗ R). `````` Robbert Krebbers committed Oct 25, 2016 470 ``````Proof. by rewrite -!(comm _ R) sep_or_l. Qed. `````` Robbert Krebbers committed Nov 03, 2016 471 ``````Lemma sep_exist_l {A} P (Ψ : A → uPred M) : P ∗ (∃ a, Ψ a) ⊣⊢ ∃ a, P ∗ Ψ a. `````` Robbert Krebbers committed Oct 25, 2016 472 473 474 475 476 477 ``````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 478 ``````Lemma sep_exist_r {A} (Φ: A → uPred M) Q: (∃ a, Φ a) ∗ Q ⊣⊢ ∃ a, Φ a ∗ Q. `````` Robbert Krebbers committed Oct 25, 2016 479 ``````Proof. setoid_rewrite (comm _ _ Q); apply sep_exist_l. Qed. `````` Robbert Krebbers committed Nov 03, 2016 480 ``````Lemma sep_forall_l {A} P (Ψ : A → uPred M) : P ∗ (∀ a, Ψ a) ⊢ ∀ a, P ∗ Ψ a. `````` Robbert Krebbers committed Oct 25, 2016 481 ``````Proof. by apply forall_intro=> a; rewrite forall_elim. Qed. `````` Robbert Krebbers committed Nov 03, 2016 482 ``````Lemma sep_forall_r {A} (Φ : A → uPred M) Q : (∀ a, Φ a) ∗ Q ⊢ ∀ a, Φ a ∗ Q. `````` Robbert Krebbers committed Oct 25, 2016 483 484 ``````Proof. by apply forall_intro=> a; rewrite forall_elim. Qed. `````` Amin Timany committed Oct 26, 2017 485 486 487 488 489 490 491 492 493 494 495 496 497 498 499 500 501 502 503 504 505 506 507 508 509 510 511 512 513 514 515 516 517 518 519 520 521 522 523 524 525 526 527 528 529 530 531 532 533 534 535 536 537 538 539 ``````(* Plainness modality *) Global Instance plainly_mono' : Proper ((⊢) ==> (⊢)) (@uPred_plainly M). Proof. intros P Q; apply plainly_mono. Qed. Global Instance naugth_flip_mono' : Proper (flip (⊢) ==> flip (⊢)) (@uPred_plainly M). Proof. intros P Q; apply plainly_mono. Qed. Lemma plainly_elim P : ■ P ⊢ P. Proof. by rewrite plainly_elim' persistently_elim. Qed. Hint Resolve plainly_mono plainly_elim. Lemma plainly_intro' P Q : (■ P ⊢ Q) → ■ P ⊢ ■ Q. Proof. intros <-. apply plainly_idemp. Qed. Lemma plainly_idemp P : ■ ■ P ⊣⊢ ■ P. Proof. apply (anti_symm _); auto using plainly_idemp. Qed. Lemma persistently_plainly P : □ ■ P ⊣⊢ ■ P. Proof. apply (anti_symm _); auto using persistently_elim. by rewrite -plainly_elim' plainly_idemp. Qed. Lemma plainly_persistently P : ■ □ P ⊣⊢ ■ P. Proof. apply (anti_symm _); auto using plainly_mono, persistently_elim. by rewrite -plainly_elim' plainly_idemp. Qed. Lemma plainly_pure φ : ■ ⌜φ⌝ ⊣⊢ ⌜φ⌝. Proof. apply (anti_symm _); auto. apply pure_elim'=> Hφ. trans (∀ x : False, ■ True : uPred M)%I; [by apply forall_intro|]. rewrite plainly_forall_2. auto using plainly_mono, pure_intro. Qed. Lemma plainly_forall {A} (Ψ : A → uPred M) : (■ ∀ a, Ψ a) ⊣⊢ (∀ a, ■ Ψ a). Proof. apply (anti_symm _); auto using plainly_forall_2. apply forall_intro=> x. by rewrite (forall_elim x). Qed. Lemma plainly_exist {A} (Ψ : A → uPred M) : (■ ∃ a, Ψ a) ⊣⊢ (∃ a, ■ Ψ a). Proof. apply (anti_symm _); auto using plainly_exist_1. apply exist_elim=> x. by rewrite (exist_intro x). Qed. Lemma plainly_and P Q : ■ (P ∧ Q) ⊣⊢ ■ P ∧ ■ Q. Proof. rewrite !and_alt plainly_forall. by apply forall_proper=> -[]. Qed. Lemma plainly_or P Q : ■ (P ∨ Q) ⊣⊢ ■ P ∨ ■ Q. Proof. rewrite !or_alt plainly_exist. by apply exist_proper=> -[]. Qed. Lemma plainly_impl P Q : ■ (P → Q) ⊢ ■ P → ■ Q. Proof. apply impl_intro_l; rewrite -plainly_and. apply plainly_mono, impl_elim with P; auto. Qed. Lemma plainly_internal_eq {A:ofeT} (a b : A) : ■ (a ≡ b) ⊣⊢ a ≡ b. Proof. apply (anti_symm (⊢)); auto using persistently_elim. `````` Robbert Krebbers committed Oct 29, 2017 540 541 `````` rewrite {1}(internal_eq_rewrite a b (λ b, ■ (a ≡ b))%I ltac:(solve_proper)). by rewrite -internal_eq_refl plainly_pure True_impl. `````` Amin Timany committed Oct 26, 2017 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 572 573 574 575 576 577 578 579 580 581 ``````Qed. Lemma plainly_and_sep_l_1 P Q : ■ P ∧ Q ⊢ ■ P ∗ Q. Proof. by rewrite -persistently_plainly persistently_and_sep_l_1. Qed. Lemma plainly_and_sep_l' P Q : ■ P ∧ Q ⊣⊢ ■ P ∗ Q. Proof. apply (anti_symm (⊢)); auto using plainly_and_sep_l_1. Qed. Lemma plainly_and_sep_r' P Q : P ∧ ■ Q ⊣⊢ P ∗ ■ Q. Proof. by rewrite !(comm _ P) plainly_and_sep_l'. Qed. Lemma plainly_sep_dup' P : ■ P ⊣⊢ ■ P ∗ ■ P. Proof. by rewrite -plainly_and_sep_l' idemp. Qed. Lemma plainly_and_sep P Q : ■ (P ∧ Q) ⊣⊢ ■ (P ∗ Q). Proof. apply (anti_symm (⊢)); auto. rewrite -{1}plainly_idemp plainly_and plainly_and_sep_l'; auto. Qed. Lemma plainly_sep P Q : ■ (P ∗ Q) ⊣⊢ ■ P ∗ ■ Q. Proof. by rewrite -plainly_and_sep -plainly_and_sep_l' plainly_and. Qed. Lemma plainly_wand P Q : ■ (P -∗ Q) ⊢ ■ P -∗ ■ Q. Proof. by apply wand_intro_r; rewrite -plainly_sep wand_elim_l. Qed. Lemma plainly_impl_wand P Q : ■ (P → Q) ⊣⊢ ■ (P -∗ Q). Proof. apply (anti_symm (⊢)); [by rewrite -impl_wand_1|]. apply plainly_intro', impl_intro_r. by rewrite plainly_and_sep_l' plainly_elim wand_elim_l. Qed. Lemma wand_impl_plainly P Q : (■ P -∗ Q) ⊣⊢ (■ P → Q). Proof. apply (anti_symm (⊢)); [|by rewrite -impl_wand_1]. apply impl_intro_l. by rewrite plainly_and_sep_l' wand_elim_r. Qed. Lemma plainly_entails_l' P Q : (P ⊢ ■ Q) → P ⊢ ■ Q ∗ P. Proof. intros; rewrite -plainly_and_sep_l'; auto. Qed. Lemma plainly_entails_r' P Q : (P ⊢ ■ Q) → P ⊢ P ∗ ■ Q. Proof. intros; rewrite -plainly_and_sep_r'; auto. Qed. Lemma plainly_laterN n P : ■ ▷^n P ⊣⊢ ▷^n ■ P. Proof. induction n as [|n IH]; simpl; auto. by rewrite plainly_later IH. Qed. `````` Robbert Krebbers committed Oct 25, 2016 582 ``````(* Always derived *) `````` Robbert Krebbers committed Oct 25, 2017 583 584 585 586 587 588 ``````Hint Resolve persistently_mono persistently_elim. Global Instance persistently_mono' : Proper ((⊢) ==> (⊢)) (@uPred_persistently M). Proof. intros P Q; apply persistently_mono. Qed. Global Instance persistently_flip_mono' : Proper (flip (⊢) ==> flip (⊢)) (@uPred_persistently M). Proof. intros P Q; apply persistently_mono. Qed. `````` Robbert Krebbers committed Oct 25, 2016 589 `````` `````` Robbert Krebbers committed Oct 25, 2017 590 591 592 593 ``````Lemma persistently_intro' P Q : (□ P ⊢ Q) → □ P ⊢ □ Q. Proof. intros <-. apply persistently_idemp_2. Qed. Lemma persistently_idemp P : □ □ P ⊣⊢ □ P. Proof. apply (anti_symm _); auto using persistently_idemp_2. Qed. `````` Robbert Krebbers committed Oct 25, 2016 594 `````` `````` Robbert Krebbers committed Oct 25, 2017 595 ``````Lemma persistently_pure φ : □ ⌜φ⌝ ⊣⊢ ⌜φ⌝. `````` Amin Timany committed Oct 26, 2017 596 ``````Proof. by rewrite -plainly_pure persistently_plainly. Qed. `````` Robbert Krebbers committed Oct 25, 2017 597 ``````Lemma persistently_forall {A} (Ψ : A → uPred M) : (□ ∀ a, Ψ a) ⊣⊢ (∀ a, □ Ψ a). `````` Robbert Krebbers committed Oct 25, 2016 598 ``````Proof. `````` Robbert Krebbers committed Oct 25, 2017 599 `````` apply (anti_symm _); auto using persistently_forall_2. `````` Robbert Krebbers committed Oct 25, 2016 600 601 `````` apply forall_intro=> x. by rewrite (forall_elim x). Qed. `````` Robbert Krebbers committed Oct 25, 2017 602 ``````Lemma persistently_exist {A} (Ψ : A → uPred M) : (□ ∃ a, Ψ a) ⊣⊢ (∃ a, □ Ψ a). `````` Robbert Krebbers committed Oct 25, 2016 603 ``````Proof. `````` Robbert Krebbers committed Oct 25, 2017 604 `````` apply (anti_symm _); auto using persistently_exist_1. `````` Robbert Krebbers committed Oct 25, 2016 605 606 `````` apply exist_elim=> x. by rewrite (exist_intro x). Qed. `````` Robbert Krebbers committed Oct 25, 2017 607 608 609 610 611 ``````Lemma persistently_and P Q : □ (P ∧ Q) ⊣⊢ □ P ∧ □ Q. Proof. rewrite !and_alt persistently_forall. by apply forall_proper=> -[]. Qed. Lemma persistently_or P Q : □ (P ∨ Q) ⊣⊢ □ P ∨ □ Q. Proof. rewrite !or_alt persistently_exist. by apply exist_proper=> -[]. Qed. Lemma persistently_impl P Q : □ (P → Q) ⊢ □ P → □ Q. `````` Robbert Krebbers committed Oct 25, 2016 612 ``````Proof. `````` Robbert Krebbers committed Oct 25, 2017 613 614 `````` apply impl_intro_l; rewrite -persistently_and. apply persistently_mono, impl_elim with P; auto. `````` Robbert Krebbers committed Oct 25, 2016 615 ``````Qed. `````` Robbert Krebbers committed Oct 25, 2017 616 ``````Lemma persistently_internal_eq {A:ofeT} (a b : A) : □ (a ≡ b) ⊣⊢ a ≡ b. `````` Amin Timany committed Oct 26, 2017 617 ``````Proof. by rewrite -plainly_internal_eq persistently_plainly. Qed. `````` Robbert Krebbers committed Oct 25, 2016 618 `````` `````` 619 ``````Lemma persistently_and_sep_l P Q : □ P ∧ Q ⊣⊢ □ P ∗ Q. `````` Robbert Krebbers committed Oct 25, 2017 620 ``````Proof. apply (anti_symm (⊢)); auto using persistently_and_sep_l_1. Qed. `````` 621 622 623 624 ``````Lemma persistently_and_sep_r P Q : P ∧ □ Q ⊣⊢ P ∗ □ Q. Proof. by rewrite !(comm _ P) persistently_and_sep_l. Qed. Lemma persistently_sep_dup P : □ P ⊣⊢ □ P ∗ □ P. Proof. by rewrite -persistently_and_sep_l idemp. Qed. `````` Robbert Krebbers committed Jun 13, 2017 625 `````` `````` Robbert Krebbers committed Oct 25, 2017 626 ``````Lemma persistently_and_sep P Q : □ (P ∧ Q) ⊣⊢ □ (P ∗ Q). `````` Robbert Krebbers committed Jun 13, 2017 627 628 ``````Proof. apply (anti_symm (⊢)); auto. `````` 629 `````` rewrite -{1}persistently_idemp persistently_and persistently_and_sep_l; auto. `````` Robbert Krebbers committed Jun 13, 2017 630 ``````Qed. `````` Robbert Krebbers committed Oct 25, 2017 631 ``````Lemma persistently_sep P Q : □ (P ∗ Q) ⊣⊢ □ P ∗ □ Q. `````` 632 ``````Proof. by rewrite -persistently_and_sep -persistently_and_sep_l persistently_and. Qed. `````` Robbert Krebbers committed Oct 25, 2016 633 `````` `````` Robbert Krebbers committed Oct 25, 2017 634 635 ``````Lemma persistently_wand P Q : □ (P -∗ Q) ⊢ □ P -∗ □ Q. Proof. by apply wand_intro_r; rewrite -persistently_sep wand_elim_l. Qed. `````` 636 ``````Lemma persistently_impl_wand P Q : □ (P → Q) ⊣⊢ □ (P -∗ Q). `````` Robbert Krebbers committed Oct 25, 2016 637 ``````Proof. `````` 638 `````` apply (anti_symm (⊢)); [by rewrite -impl_wand_1|]. `````` Robbert Krebbers committed Oct 25, 2017 639 `````` apply persistently_intro', impl_intro_r. `````` 640 `````` by rewrite persistently_and_sep_l persistently_elim wand_elim_l. `````` Robbert Krebbers committed Oct 25, 2016 641 ``````Qed. `````` 642 ``````Lemma impl_wand_persistently P Q : (□ P → Q) ⊣⊢ (□ P -∗ Q). `````` Ralf Jung committed Aug 23, 2017 643 ``````Proof. `````` 644 645 `````` apply (anti_symm (⊢)); [by rewrite -impl_wand_1|]. apply impl_intro_l. by rewrite persistently_and_sep_l wand_elim_r. `````` Ralf Jung committed Aug 23, 2017 646 ``````Qed. `````` 647 648 649 650 ``````Lemma persistently_entails_l P Q : (P ⊢ □ Q) → P ⊢ □ Q ∗ P. Proof. intros; rewrite -persistently_and_sep_l; auto. Qed. Lemma persistently_entails_r P Q : (P ⊢ □ Q) → P ⊢ P ∗ □ Q. Proof. intros; rewrite -persistently_and_sep_r; auto. Qed. `````` Robbert Krebbers committed Oct 25, 2016 651 `````` `````` Robbert Krebbers committed Oct 25, 2017 652 653 ``````Lemma persistently_laterN n P : □ ▷^n P ⊣⊢ ▷^n □ P. Proof. induction n as [|n IH]; simpl; auto. by rewrite persistently_later IH. Qed. `````` Robbert Krebbers committed Nov 27, 2016 654 `````` `````` Robbert Krebbers committed May 12, 2017 655 656 657 658 ``````Lemma wand_alt P Q : (P -∗ Q) ⊣⊢ ∃ R, R ∗ □ (P ∗ R → Q). Proof. apply (anti_symm (⊢)). - rewrite -(right_id True%I uPred_sep (P -∗ Q)%I) -(exist_intro (P -∗ Q)%I). `````` Robbert Krebbers committed Oct 25, 2017 659 `````` apply sep_mono_r. rewrite -persistently_pure. apply persistently_mono, impl_intro_l. `````` Robbert Krebbers committed May 12, 2017 660 `````` by rewrite wand_elim_r right_id. `````` 661 `````` - apply exist_elim=> R. apply wand_intro_l. rewrite assoc -persistently_and_sep_r. `````` Robbert Krebbers committed Oct 25, 2017 662 `````` by rewrite persistently_elim impl_elim_r. `````` Robbert Krebbers committed May 12, 2017 663 664 665 666 667 ``````Qed. Lemma impl_alt P Q : (P → Q) ⊣⊢ ∃ R, R ∧ □ (P ∧ R -∗ Q). Proof. apply (anti_symm (⊢)). - rewrite -(right_id True%I uPred_and (P → Q)%I) -(exist_intro (P → Q)%I). `````` Robbert Krebbers committed Oct 25, 2017 668 `````` apply and_mono_r. rewrite -persistently_pure. apply persistently_mono, wand_intro_l. `````` Robbert Krebbers committed May 12, 2017 669 `````` by rewrite impl_elim_r right_id. `````` 670 `````` - apply exist_elim=> R. apply impl_intro_l. rewrite assoc persistently_and_sep_r. `````` Robbert Krebbers committed Oct 25, 2017 671 `````` by rewrite persistently_elim wand_elim_r. `````` Robbert Krebbers committed May 12, 2017 672 ``````Qed. `````` Robbert Krebbers committed Nov 27, 2016 673 `````` `````` Robbert Krebbers committed Oct 25, 2016 674 ``````(* Later derived *) `````` Ralf Jung committed Nov 11, 2017 675 ``````Lemma later_proper' P Q : (P ⊣⊢ Q) → ▷ P ⊣⊢ ▷ Q. `````` Robbert Krebbers committed Oct 25, 2016 676 ``````Proof. by intros ->. Qed. `````` Ralf Jung committed Nov 11, 2017 677 ``````Hint Resolve later_mono later_proper'. `````` Robbert Krebbers committed Oct 25, 2016 678 679 680 681 682 683 684 685 686 687 688 689 690 691 692 693 694 695 696 ``````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. `````` Robbert Krebbers committed Sep 27, 2017 697 698 ``````Lemma later_exist_2 {A} (Φ : A → uPred M) : (∃ a, ▷ Φ a) ⊢ ▷ (∃ a, Φ a). Proof. apply exist_elim; eauto using exist_intro. Qed. `````` Robbert Krebbers committed Oct 25, 2016 699 700 701 ``````Lemma later_exist `{Inhabited A} (Φ : A → uPred M) : ▷ (∃ a, Φ a) ⊣⊢ (∃ a, ▷ Φ a). Proof. `````` Robbert Krebbers committed Sep 27, 2017 702 `````` apply: anti_symm; [|apply later_exist_2]. `````` Robbert Krebbers committed Oct 25, 2016 703 704 705 706 707 708 709 710 711 `````` 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 712 ``````Lemma later_wand P Q : ▷ (P -∗ Q) ⊢ ▷ P -∗ ▷ Q. `````` Robbert Krebbers committed Oct 25, 2016 713 714 715 716 ``````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 717 ``````(* Iterated later modality *) `````` Ralf Jung committed Jan 27, 2017 718 ``````Global Instance laterN_ne m : NonExpansive (@uPred_laterN M m). `````` Robbert Krebbers committed Nov 27, 2016 719 720 721 722 723 724 725 726 727 728 729 730 731 732 733 734 735 736 737 738 739 740 741 742 743 744 745 746 747 748 ``````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. `````` Robbert Krebbers committed Sep 27, 2017 749 750 ``````Lemma laterN_exist_2 {A} n (Φ : A → uPred M) : (∃ a, ▷^n Φ a) ⊢ ▷^n (∃ a, Φ a). Proof. apply exist_elim; eauto using exist_intro, laterN_mono. Qed. `````` Robbert Krebbers committed Nov 27, 2016 751 752 753 754 755 756 757 758 759 760 761 762 763 764 765 766 767 768 769 770 ``````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, 2017 771 772 ``````(* Conditional persistently *) Global Instance persistently_if_ne p : NonExpansive (@uPred_persistently_if M p). `````` Robbert Krebbers committed Oct 25, 2016 773 ``````Proof. solve_proper. Qed. `````` Robbert Krebbers committed Oct 25, 2017 774 ``````Global Instance persistently_if_proper p : Proper ((⊣⊢) ==> (⊣⊢)) (@uPred_persistently_if M p). `````` Robbert Krebbers committed Oct 25, 2016 775 ``````Proof. solve_proper. Qed. `````` Robbert Krebbers committed Oct 25, 2017 776 ``````Global Instance persistently_if_mono p : Proper ((⊢) ==> (⊢)) (@uPred_persistently_if M p). `````` Robbert Krebbers committed Oct 25, 2016 777 778 ``````Proof. solve_proper. Qed. `````` Robbert Krebbers committed Oct 25, 2017 779 780 781 782 783 784 785 786 787 788 789 790 791 792 793 794 795 796 797 ``````Lemma persistently_if_elim p P : □?p P ⊢ P. Proof. destruct p; simpl; auto using persistently_elim. Qed. Lemma persistently_elim_if p P : □ P ⊢ □?p P. Proof. destruct p; simpl; auto using persistently_elim. Qed. Lemma persistently_if_pure p φ : □?p ⌜φ⌝ ⊣⊢ ⌜φ⌝. Proof. destruct p; simpl; auto using persistently_pure. Qed. Lemma persistently_if_and p P Q : □?p (P ∧ Q) ⊣⊢ □?p P ∧ □?p Q. Proof. destruct p; simpl; auto using persistently_and. Qed. Lemma persistently_if_or p P Q : □?p (P ∨ Q) ⊣⊢ □?p P ∨ □?p Q. Proof. destruct p; simpl; auto using persistently_or. Qed. Lemma persistently_if_exist {A} p (Ψ : A → uPred M) : (□?p ∃ a, Ψ a) ⊣⊢ ∃ a, □?p Ψ a. Proof. destruct p; simpl; auto using persistently_exist. Qed. Lemma persistently_if_sep p P Q : □?p (P ∗ Q) ⊣⊢ □?p P ∗ □?p Q. Proof. destruct p; simpl; auto using persistently_sep. Qed. Lemma persistently_if_later p P : □?p ▷ P ⊣⊢ ▷ □?p P. Proof. destruct p; simpl; auto using persistently_later. Qed. Lemma persistently_if_laterN p n P : □?p ▷^n P ⊣⊢ ▷^n □?p P. Proof. destruct p; simpl; auto using persistently_laterN. Qed. ``````