derived.v 39 KB
Newer Older
1 2 3 4 5 6 7
From iris.base_logic Require Export primitive.
Import uPred_entails uPred_primitive.

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's avatar
Robbert Krebbers committed
8 9 10 11 12 13 14 15 16 17
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.

18 19 20 21 22
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's avatar
Robbert Krebbers committed
23
  (at level 20, p at level 9, P at level 20, format "□? p  P").
24

25 26
Definition uPred_except_0 {M} (P : uPred M) : uPred M :=  False  P.
Notation "◇ P" := (uPred_except_0 P)
27
  (at level 20, right associativity) : uPred_scope.
28 29
Instance: Params (@uPred_except_0) 1.
Typeclasses Opaque uPred_except_0.
30 31 32 33 34 35 36 37 38 39 40 41 42 43 44 45 46 47

Class TimelessP {M} (P : uPred M) := timelessP :  P   P.
Arguments timelessP {_} _ {_}.

Class PersistentP {M} (P : uPred M) := persistentP : P   P.
Arguments persistentP {_} _ {_}.

Module uPred_derived.
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.
48
Proof. by apply (pure_elim' False). Qed.
49 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
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.
80
Lemma impl_entails P Q : (P  Q)%I  P  Q.
81
Proof. intros HPQ; apply impl_elim with P; rewrite -?HPQ; auto. Qed.
82 83
Lemma entails_impl P Q : (P  Q)  (P  Q)%I.
Proof. intro. apply impl_intro_l. auto. Qed.
84 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

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.
126 127 128
Global Instance impl_flip_mono' :
  Proper (() ==> flip () ==> flip ()) (@uPred_impl M).
Proof. by intros P P' HP Q Q' HQ; apply impl_mono. Qed.
129 130 131
Global Instance forall_mono' A :
  Proper (pointwise_relation _ () ==> ()) (@uPred_forall M A).
Proof. intros P1 P2; apply forall_mono. Qed.
132 133 134
Global Instance forall_flip_mono' A :
  Proper (pointwise_relation _ (flip ()) ==> flip ()) (@uPred_forall M A).
Proof. intros P1 P2; apply forall_mono. Qed.
135
Global Instance exist_mono' A :
136 137 138 139
  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).
140 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
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.
176 177 178 179 180
Lemma False_impl P : (False  P)  True.
Proof.
  apply (anti_symm ()); [by auto|].
  apply impl_intro_l. rewrite left_absorb. auto.
Qed.
181 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

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.
217 218 219 220 221 222 223
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.
224

225
Lemma pure_elim φ Q R : (Q  ⌜φ⌝)  (φ  Q  R)  Q  R.
226 227 228 229
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's avatar
Ralf Jung committed
230
Lemma pure_mono φ1 φ2 : (φ1  φ2)  ⌜φ1  ⌜φ2.
231 232 233
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's avatar
Ralf Jung committed
234
Lemma pure_iff φ1 φ2 : (φ1  φ2)  ⌜φ1  ⌜φ2.
235
Proof. intros [??]; apply (anti_symm _); auto using pure_mono. Qed.
Ralf Jung's avatar
Ralf Jung committed
236
Lemma pure_intro_l φ Q R : φ  (⌜φ⌝  Q  R)  Q  R.
237
Proof. intros ? <-; auto using pure_intro. Qed.
Ralf Jung's avatar
Ralf Jung committed
238
Lemma pure_intro_r φ Q R : φ  (Q  ⌜φ⌝  R)  Q  R.
239
Proof. intros ? <-; auto. Qed.
Ralf Jung's avatar
Ralf Jung committed
240
Lemma pure_intro_impl φ Q R : φ  (Q  ⌜φ⌝  R)  Q  R.
241
Proof. intros ? ->. eauto using pure_intro_l, impl_elim_r. Qed.
Ralf Jung's avatar
Ralf Jung committed
242
Lemma pure_elim_l φ Q R : (φ  Q  R)  ⌜φ⌝  Q  R.
243
Proof. intros; apply pure_elim with φ; eauto. Qed.
Ralf Jung's avatar
Ralf Jung committed
244
Lemma pure_elim_r φ Q R : (φ  Q  R)  Q  ⌜φ⌝  R.
245
Proof. intros; apply pure_elim with φ; eauto. Qed.
246

Ralf Jung's avatar
Ralf Jung committed
247
Lemma pure_True (φ : Prop) : φ  ⌜φ⌝  True.
248
Proof. intros; apply (anti_symm _); auto. Qed.
Ralf Jung's avatar
Ralf Jung committed
249
Lemma pure_False (φ : Prop) : ¬φ  ⌜φ⌝  False.
250
Proof. intros; apply (anti_symm _); eauto using pure_elim. Qed.
251

Ralf Jung's avatar
Ralf Jung committed
252
Lemma pure_and φ1 φ2 : ⌜φ1  φ2  ⌜φ1  ⌜φ2.
253 254 255 256 257
Proof.
  apply (anti_symm _).
  - eapply pure_elim=> // -[??]; auto.
  - eapply (pure_elim φ1); [auto|]=> ?. eapply (pure_elim φ2); auto.
Qed.
Ralf Jung's avatar
Ralf Jung committed
258
Lemma pure_or φ1 φ2 : ⌜φ1  φ2  ⌜φ1  ⌜φ2.
259 260 261 262 263
Proof.
  apply (anti_symm _).
  - eapply pure_elim=> // -[?|?]; auto.
  - apply or_elim; eapply pure_elim; eauto.
Qed.
Ralf Jung's avatar
Ralf Jung committed
264
Lemma pure_impl φ1 φ2 : ⌜φ1  φ2  (⌜φ1  ⌜φ2).
265 266 267 268
Proof.
  apply (anti_symm _).
  - apply impl_intro_l. rewrite -pure_and. apply pure_mono. naive_solver.
  - rewrite -pure_forall_2. apply forall_intro=> ?.
269
    by rewrite -(left_id True uPred_and (_→_))%I (pure_True φ1) // impl_elim_r.
270
Qed.
Ralf Jung's avatar
Ralf Jung committed
271
Lemma pure_forall {A} (φ : A  Prop) :  x, φ x   x, ⌜φ x.
272 273 274 275
Proof.
  apply (anti_symm _); auto using pure_forall_2.
  apply forall_intro=> x. eauto using pure_mono.
Qed.
Ralf Jung's avatar
Ralf Jung committed
276
Lemma pure_exist {A} (φ : A  Prop) :  x, φ x   x, ⌜φ x.
277 278 279 280 281 282
Proof.
  apply (anti_symm _).
  - eapply pure_elim=> // -[x ?]. rewrite -(exist_intro x); auto.
  - apply exist_elim=> x. eauto using pure_mono.
Qed.

283
Lemma internal_eq_refl' {A : ofeT} (a : A) P : P  a  a.
284 285
Proof. rewrite (True_intro P). apply internal_eq_refl. Qed.
Hint Resolve internal_eq_refl'.
286
Lemma equiv_internal_eq {A : ofeT} P (a b : A) : a  b  P  a  b.
287
Proof. by intros ->. Qed.
288
Lemma internal_eq_sym {A : ofeT} (a b : A) : a  b  b  a.
289
Proof. apply (internal_eq_rewrite a b (λ b, b  a)%I); auto. solve_proper. Qed.
290 291 292
Lemma internal_eq_rewrite_contractive {A : ofeT} a b (Ψ : A  uPred M) P
  {HΨ : Contractive Ψ} : (P   (a  b))  (P  Ψ a)  P  Ψ b.
Proof.
293 294
  move: HΨ=> /contractiveI HΨ Heq ?.
  apply (internal_eq_rewrite (Ψ a) (Ψ b) id _)=>//=. by rewrite -HΨ.
295
Qed.
296

Ralf Jung's avatar
Ralf Jung committed
297
Lemma pure_impl_forall φ P : (⌜φ⌝  P)  ( _ : φ, P).
298 299
Proof.
  apply (anti_symm _).
300
  - apply forall_intro=> ?. by rewrite pure_True // left_id.
301 302
  - apply impl_intro_l, pure_elim_l=> Hφ. by rewrite (forall_elim Hφ).
Qed.
Ralf Jung's avatar
Ralf Jung committed
303
Lemma pure_alt φ : ⌜φ⌝   _ : φ, True.
304 305 306 307 308 309 310 311 312 313 314 315 316 317 318 319 320 321 322 323 324 325 326
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.
327
Lemma iff_equiv P Q : (P  Q)%I  (P  Q).
328 329
Proof.
  intros HPQ; apply (anti_symm ());
330
    apply impl_entails; rewrite /uPred_valid HPQ /uPred_iff; auto.
331
Qed.
332
Lemma equiv_iff P Q : (P  Q)  (P  Q)%I.
333
Proof. intros ->; apply iff_refl. Qed.
334
Lemma internal_eq_iff P Q : P  Q  P  Q.
335
Proof.
336 337
  apply (internal_eq_rewrite P Q (λ Q, P  Q))%I;
    first solve_proper; auto using iff_refl.
338 339 340 341
Qed.

(* Derived BI Stuff *)
Hint Resolve sep_mono.
342
Lemma sep_mono_l P P' Q : (P  Q)  P  P'  Q  P'.
343
Proof. by intros; apply sep_mono. Qed.
344
Lemma sep_mono_r P P' Q' : (P'  Q')  P  P'  P  Q'.
345 346 347 348 349 350
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.
351
Lemma wand_mono P P' Q Q' : (Q  P)  (P'  Q')  (P - P')  Q - Q'.
352 353 354 355 356
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.
357 358 359
Global Instance wand_flip_mono' :
  Proper (() ==> flip () ==> flip ()) (@uPred_wand M).
Proof. by intros P P' HP Q Q' HQ; apply wand_mono. Qed.
360 361 362 363 364 365 366 367 368 369 370 371

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.
372
Lemma sep_elim_l P Q : P  Q  P.
373
Proof. by rewrite (True_intro Q) right_id. Qed.
374 375 376
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.
377
Proof. intros ->; apply sep_elim_l. Qed.
378
Lemma sep_elim_r' P Q R : (Q  R)  P  Q  R.
379 380
Proof. intros ->; apply sep_elim_r. Qed.
Hint Resolve sep_elim_l' sep_elim_r'.
381
Lemma sep_intro_True_l P Q R : P%I  (R  Q)  R  P  Q.
382
Proof. by intros; rewrite -(left_id True%I uPred_sep R); apply sep_mono. Qed.
383
Lemma sep_intro_True_r P Q R : (R  P)  Q%I  R  P  Q.
384
Proof. by intros; rewrite -(right_id True%I uPred_sep R); apply sep_mono. Qed.
385
Lemma sep_elim_True_l P Q R : P  (P  R  Q)  R  Q.
386
Proof. by intros HP; rewrite -HP left_id. Qed.
387
Lemma sep_elim_True_r P Q R : P  (R  P  Q)  R  Q.
388
Proof. by intros HP; rewrite -HP right_id. Qed.
389
Lemma wand_intro_l P Q R : (Q  P  R)  P  Q - R.
390
Proof. rewrite comm; apply wand_intro_r. Qed.
391
Lemma wand_elim_l P Q : (P - Q)  P  Q.
392
Proof. by apply wand_elim_l'. Qed.
393
Lemma wand_elim_r P Q : P  (P - Q)  Q.
394
Proof. rewrite (comm _ P); apply wand_elim_l. Qed.
395
Lemma wand_elim_r' P Q R : (Q  P - R)  P  Q  R.
396
Proof. intros ->; apply wand_elim_r. Qed.
397
Lemma wand_apply P Q R S : (P  Q - R)  (S  P  Q)  S  R.
Ralf Jung's avatar
Ralf Jung committed
398
Proof. intros HR%wand_elim_l' HQ. by rewrite HQ. Qed.
399
Lemma wand_frame_l P Q R : (Q - R)  P  Q - P  R.
400
Proof. apply wand_intro_l. rewrite -assoc. apply sep_mono_r, wand_elim_r. Qed.
401
Lemma wand_frame_r P Q R : (Q - R)  Q  P - R  P.
402
Proof.
403
  apply wand_intro_l. rewrite ![(_  P)%I]comm -assoc.
404 405
  apply sep_mono_r, wand_elim_r.
Qed.
406
Lemma wand_diag P : (P - P)  True.
407
Proof. apply (anti_symm _); auto. apply wand_intro_l; by rewrite right_id. Qed.
408
Lemma wand_True P : (True - P)  P.
409 410
Proof.
  apply (anti_symm _); last by auto using wand_intro_l.
411
  eapply sep_elim_True_l; last by apply wand_elim_r. done.
412
Qed.
413
Lemma wand_entails P Q : (P - Q)%I  P  Q.
414 415 416
Proof.
  intros HPQ. eapply sep_elim_True_r; first exact: HPQ. by rewrite wand_elim_r.
Qed.
417 418
Lemma entails_wand P Q : (P  Q)  (P - Q)%I.
Proof. intro. apply wand_intro_l. auto. Qed.
419
Lemma wand_curry P Q R : (P - Q - R)  (P  Q - R).
420 421 422 423 424 425
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.

426
Lemma sep_and P Q : (P  Q)  (P  Q).
427
Proof. auto. Qed.
428
Lemma impl_wand P Q : (P  Q)  P - Q.
429
Proof. apply wand_intro_r, impl_elim with P; auto. Qed.
Ralf Jung's avatar
Ralf Jung committed
430
Lemma pure_elim_sep_l φ Q R : (φ  Q  R)  ⌜φ⌝  Q  R.
431
Proof. intros; apply pure_elim with φ; eauto. Qed.
Ralf Jung's avatar
Ralf Jung committed
432
Lemma pure_elim_sep_r φ Q R : (φ  Q  R)  Q  ⌜φ⌝  R.
433 434 435 436 437 438 439
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.

440
Lemma sep_and_l P Q R : P  (Q  R)  (P  Q)  (P  R).
441
Proof. auto. Qed.
442
Lemma sep_and_r P Q R : (P  Q)  R  (P  R)  (Q  R).
443
Proof. auto. Qed.
444
Lemma sep_or_l P Q R : P  (Q  R)  (P  Q)  (P  R).
445 446 447 448
Proof.
  apply (anti_symm ()); last by eauto 8.
  apply wand_elim_r', or_elim; apply wand_intro_l; auto.
Qed.
449
Lemma sep_or_r P Q R : (P  Q)  R  (P  R)  (Q  R).
450
Proof. by rewrite -!(comm _ R) sep_or_l. Qed.
451
Lemma sep_exist_l {A} P (Ψ : A  uPred M) : P  ( a, Ψ a)   a, P  Ψ a.
452 453 454 455 456 457
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.
458
Lemma sep_exist_r {A} (Φ: A  uPred M) Q: ( a, Φ a)  Q   a, Φ a  Q.
459
Proof. setoid_rewrite (comm _ _ Q); apply sep_exist_l. Qed.
460
Lemma sep_forall_l {A} P (Ψ : A  uPred M) : P  ( a, Ψ a)   a, P  Ψ a.
461
Proof. by apply forall_intro=> a; rewrite forall_elim. Qed.
462
Lemma sep_forall_r {A} (Φ : A  uPred M) Q : ( a, Φ a)  Q   a, Φ a  Q.
463 464 465 466 467 468 469 470 471 472 473 474 475
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's avatar
Ralf Jung committed
476
Lemma always_pure φ :  ⌜φ⌝  ⌜φ⌝.
477 478 479 480 481 482 483 484 485 486 487 488 489 490 491 492 493 494 495 496
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.
497
Lemma always_internal_eq {A:ofeT} (a b : A) :  (a  b)  a  b.
498 499
Proof.
  apply (anti_symm ()); auto using always_elim.
500
  apply (internal_eq_rewrite a b (λ b,  (a  b))%I); auto.
501
  { intros n; solve_proper. }
502
  rewrite -(internal_eq_refl a) always_pure; auto.
503 504
Qed.

505
Lemma always_and_sep P Q :  (P  Q)   (P  Q).
506
Proof. apply (anti_symm ()); auto using always_and_sep_1. Qed.
507
Lemma always_and_sep_l' P Q :  P  Q   P  Q.
508
Proof. apply (anti_symm ()); auto using always_and_sep_l_1. Qed.
509
Lemma always_and_sep_r' P Q : P   Q  P   Q.
510
Proof. by rewrite !(comm _ P) always_and_sep_l'. Qed.
511
Lemma always_sep P Q :  (P  Q)   P   Q.
512
Proof. by rewrite -always_and_sep -always_and_sep_l' always_and. Qed.
513
Lemma always_sep_dup' P :  P   P   P.
514 515
Proof. by rewrite -always_sep -always_and_sep (idemp _). Qed.

516
Lemma always_wand P Q :  (P - Q)   P -  Q.
517
Proof. by apply wand_intro_r; rewrite -always_sep wand_elim_l. Qed.
518
Lemma always_wand_impl P Q :  (P - Q)   (P  Q).
519 520 521 522 523
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.
524
Lemma always_entails_l' P Q : (P   Q)  P   Q  P.
525
Proof. intros; rewrite -always_and_sep_l'; auto. Qed.
526
Lemma always_entails_r' P Q : (P   Q)  P  P   Q.
527 528
Proof. intros; rewrite -always_and_sep_r'; auto. Qed.

Robbert Krebbers's avatar
Robbert Krebbers committed
529 530 531 532
Lemma always_laterN n P :  ^n P  ^n  P.
Proof. induction n as [|n IH]; simpl; auto. by rewrite always_later IH. Qed.


533 534 535 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
(* 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.
569
Lemma later_wand P Q :  (P - Q)   P -  Q.
570 571 572 573 574
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's avatar
Robbert Krebbers committed
575 576 577 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
(* 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.

627 628 629 630 631 632 633 634 635 636 637 638 639
(* 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's avatar
Ralf Jung committed
640
Lemma always_if_pure p φ : ?p ⌜φ⌝  ⌜φ⌝.
641 642 643 644 645 646 647
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.
648
Lemma always_if_sep p P Q : ?p (P  Q)  ?p P  ?p Q.
649 650 651 652 653 654
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 *)
655
Global Instance except_0_ne n : Proper (dist n ==> dist n) (@uPred_except_0 M).
656
Proof. solve_proper. Qed.
657
Global Instance except_0_proper : Proper (() ==> ()) (@uPred_except_0 M).
658
Proof. solve_proper. Qed.
659
Global Instance except_0_mono' : Proper (() ==> ()) (@uPred_except_0 M).
660
Proof. solve_proper. Qed.
661 662
Global Instance except_0_flip_mono' :
  Proper (flip () ==> flip ()) (@uPred_except_0 M).
663 664
Proof. solve_proper. Qed.

665 666 667
Lemma except_0_intro P : P   P.
Proof. rewrite /uPred_except_0; auto. Qed.
Lemma except_0_mono P Q : (P  Q)   P   Q.
668
Proof. by intros ->. Qed.
669 670 671 672 673 674 675 676 677
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.
678
Lemma except_0_sep P Q :  (P  Q)   P   Q.
679 680
Proof.
  rewrite /uPred_except_0. apply (anti_symm _).
681 682 683 684
  - 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.
685
Lemma except_0_forall {A} (Φ : A  uPred M) :  ( a, Φ a)   a,  Φ a.
686
Proof. apply forall_intro=> a. by rewrite (forall_elim a). Qed.
687
Lemma except_0_exist {A} (Φ : A  uPred M) : ( a,  Φ a)    a, Φ a.
688
Proof. apply exist_elim=> a. by rewrite (exist_intro a). Qed.
689 690 691 692 693 694
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.
695
Lemma except_0_frame_l P Q : P   Q   (P  Q).
696
Proof. by rewrite {1}(except_0_intro P) except_0_sep. Qed.
697
Lemma except_0_frame_r P Q :  P  Q   (P  Q).
698
Proof. by rewrite {1}(except_0_intro Q) except_0_sep. Qed.
699 700 701 702 703 704 705 706 707 708 709 710

(* 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.
711
Proof. apply (anti_symm _); first by auto. apply ownM_empty. Qed.
712 713 714 715 716 717 718 719 720 721 722
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.
723
Lemma bupd_frame_l R Q : (R  |==> Q) == R  Q.
724
Proof. rewrite !(comm _ R); apply bupd_frame_r. Qed.
725
Lemma bupd_wand_l P Q : (P - Q)  (|==> P) == Q.
726
Proof. by rewrite bupd_frame_l wand_elim_l. Qed.
727
Lemma bupd_wand_r P Q : (|==> P)  (P - Q) == Q.
728
Proof. by rewrite bupd_frame_r wand_elim_r. Qed.
729
Lemma bupd_sep P Q : (|==> P)  (|==> Q) == P  Q.
730 731 732 733 734 735
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.
736
Lemma except_0_bupd P :  (|==> P)  (|==>  P).
737
Proof.
738
  rewrite /uPred_except_0. apply or_elim; auto using bupd_mono.
739 740 741 742
  by rewrite -bupd_intro -or_intro_l.
Qed.

(* Timeless instances *)
Ralf Jung's avatar
Ralf Jung committed
743
Global Instance pure_timeless φ : TimelessP (⌜φ⌝ : uPred M)%I.
744 745 746 747 748 749 750
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).
751
Proof. intros; rewrite /TimelessP except_0_and later_and; auto. Qed.
752
Global Instance or_timeless P Q : TimelessP P  TimelessP Q  TimelessP (P  Q).
753
Proof. intros; rewrite /TimelessP except_0_or later_or; auto. Qed.
754 755 756 757 758
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.
759
  rewrite HQ /uPred_except_0 !and_or_r. apply or_elim; last auto.
760 761
  by rewrite assoc (comm _ _ P) -assoc !impl_elim_r.
Qed.
762
Global Instance sep_timeless P Q: TimelessP P  TimelessP Q  TimelessP (P  Q).
763
Proof. intros; rewrite /TimelessP except_0_sep later_sep; auto. Qed.
764
Global Instance wand_timeless P Q : TimelessP Q  TimelessP (P - Q).
765 766 767 768
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.
769
  rewrite HQ /uPred_except_0 !and_or_r. apply or_elim; last auto.
770 771 772 773 774 775 776 777 778
  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.
779
  rewrite HQ /uPred_except_0 !and_or_r. apply or_elim; last auto.
780 781 782 783 784 785
  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.
786
  - rewrite /uPred_except_0; auto.
787 788 789
  - apply exist_elim=> x. rewrite -(exist_intro x); auto.
Qed.
Global Instance always_timeless P : TimelessP P  TimelessP ( P).
790
Proof. intros; rewrite /TimelessP except_0_always -always_later; auto. Qed.
791 792
Global Instance always_if_timeless p P : TimelessP P  TimelessP (?p P).
Proof. destruct p; apply _. Qed.
793
Global Instance eq_timeless {A : ofeT} (a b : A) :
794 795 796 797 798
  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.
799
  rewrite (timelessP (ab)) (except_0_intro (uPred_ownM b)) -except_0_and.
800 801
  apply except_0_mono. rewrite internal_eq_sym.
  apply (internal_eq_rewrite b a (uPred_ownM)); first apply _; auto.
802
Qed.
803 804 805
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.