derived.v 55.1 KB
Newer Older
1
From iris.base_logic Require Export primitive.
2
Set Default Proof Using "Type".
3
Import upred.uPred primitive.uPred.
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's avatar
Robbert Krebbers committed
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.

19
Definition uPred_persistently_if {M} (p : bool) (P : uPred M) : uPred M :=
20
  (if p then  P else P)%I.
21 22 23
Instance: Params (@uPred_persistently_if) 2.
Arguments uPred_persistently_if _ !_ _/.
Notation "□? p P" := (uPred_persistently_if p P)
Robbert Krebbers's avatar
Robbert Krebbers committed
24
  (at level 20, p at level 9, P at level 20, format "□? p  P").
25

26 27
Definition uPred_except_0 {M} (P : uPred M) : uPred M :=  False  P.
Notation "◇ P" := (uPred_except_0 P)
28
  (at level 20, right associativity) : uPred_scope.
29 30
Instance: Params (@uPred_except_0) 1.
Typeclasses Opaque uPred_except_0.
31

32
Class Timeless {M} (P : uPred M) := timelessP :  P   P.
33
Arguments timelessP {_} _ {_}.
34 35
Hint Mode Timeless + ! : typeclass_instances.
Instance: Params (@Timeless) 1.
36

37 38 39 40
Class Persistent {M} (P : uPred M) := persistent : P   P.
Arguments persistent {_} _ {_}.
Hint Mode Persistent + ! : typeclass_instances.
Instance: Params (@Persistent) 1.
41

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.

47
Module uPred.
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.
58
Proof. by apply (pure_elim' False). Qed.
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.
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.
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.
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.
139 140 141
Global Instance forall_mono' A :
  Proper (pointwise_relation _ () ==> ()) (@uPred_forall M A).
Proof. intros P1 P2; apply forall_mono. Qed.
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.
145
Global Instance exist_mono' A :
Jacques-Henri Jourdan's avatar
Jacques-Henri Jourdan committed
146
  Proper (pointwise_relation _ () ==> ()) (@uPred_exist M A).
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).
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.
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.
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.
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.
234

235
Lemma pure_elim φ Q R : (Q  ⌜φ⌝)  (φ  Q  R)  Q  R.
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's avatar
Ralf Jung committed
240
Lemma pure_mono φ1 φ2 : (φ1  φ2)  ⌜φ1  ⌜φ2.
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's avatar
Jacques-Henri Jourdan committed
244 245
Global Instance pure_flip_mono : Proper (flip impl ==> flip ()) (@uPred_pure M).
Proof. intros φ1 φ2; apply pure_mono. Qed.
Ralf Jung's avatar
Ralf Jung committed
246
Lemma pure_iff φ1 φ2 : (φ1  φ2)  ⌜φ1  ⌜φ2.
247
Proof. intros [??]; apply (anti_symm _); auto using pure_mono. Qed.
Ralf Jung's avatar
Ralf Jung committed
248
Lemma pure_intro_l φ Q R : φ  (⌜φ⌝  Q  R)  Q  R.
249
Proof. intros ? <-; auto using pure_intro. Qed.
Ralf Jung's avatar
Ralf Jung committed
250
Lemma pure_intro_r φ Q R : φ  (Q  ⌜φ⌝  R)  Q  R.
251
Proof. intros ? <-; auto. Qed.
Ralf Jung's avatar
Ralf Jung committed
252
Lemma pure_intro_impl φ Q R : φ  (Q  ⌜φ⌝  R)  Q  R.
253
Proof. intros ? ->. eauto using pure_intro_l, impl_elim_r. Qed.
Ralf Jung's avatar
Ralf Jung committed
254
Lemma pure_elim_l φ Q R : (φ  Q  R)  ⌜φ⌝  Q  R.
255
Proof. intros; apply pure_elim with φ; eauto. Qed.
Ralf Jung's avatar
Ralf Jung committed
256
Lemma pure_elim_r φ Q R : (φ  Q  R)  Q  ⌜φ⌝  R.
257
Proof. intros; apply pure_elim with φ; eauto. Qed.
258

Ralf Jung's avatar
Ralf Jung committed
259
Lemma pure_True (φ : Prop) : φ  ⌜φ⌝  True.
260
Proof. intros; apply (anti_symm _); auto. Qed.
Ralf Jung's avatar
Ralf Jung committed
261
Lemma pure_False (φ : Prop) : ¬φ  ⌜φ⌝  False.
262
Proof. intros; apply (anti_symm _); eauto using pure_elim. Qed.
263

Ralf Jung's avatar
Ralf Jung committed
264
Lemma pure_and φ1 φ2 : ⌜φ1  φ2  ⌜φ1  ⌜φ2.
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's avatar
Ralf Jung committed
270
Lemma pure_or φ1 φ2 : ⌜φ1  φ2  ⌜φ1  ⌜φ2.
271 272 273 274 275
Proof.
  apply (anti_symm _).
  - eapply pure_elim=> // -[?|?]; auto.
  - apply or_elim; eapply pure_elim; eauto.
Qed.
Ralf Jung's avatar
Ralf Jung committed
276
Lemma pure_impl φ1 φ2 : ⌜φ1  φ2  (⌜φ1  ⌜φ2).
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=> ?.
281
    by rewrite -(left_id True uPred_and (_→_))%I (pure_True φ1) // impl_elim_r.
282
Qed.
Ralf Jung's avatar
Ralf Jung committed
283
Lemma pure_forall {A} (φ : A  Prop) :  x, φ x   x, ⌜φ x.
284 285 286 287
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
288
Lemma pure_exist {A} (φ : A  Prop) :  x, φ x   x, ⌜φ x.
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.

295
Lemma internal_eq_refl' {A : ofeT} (a : A) P : P  a  a.
296 297
Proof. rewrite (True_intro P). apply internal_eq_refl. Qed.
Hint Resolve internal_eq_refl'.
298
Lemma equiv_internal_eq {A : ofeT} P (a b : A) : a  b  P  a  b.
299
Proof. by intros ->. Qed.
300
Lemma internal_eq_sym {A : ofeT} (a b : A) : a  b  b  a.
301
Proof. apply (internal_eq_rewrite a b (λ b, b  a)%I); auto. solve_proper. Qed.
302 303 304
Lemma internal_eq_rewrite_contractive {A : ofeT} a b (Ψ : A  uPred M) P
  {HΨ : Contractive Ψ} : (P   (a  b))  (P  Ψ a)  P  Ψ b.
Proof.
305 306
  move: HΨ=> /contractiveI HΨ Heq ?.
  apply (internal_eq_rewrite (Ψ a) (Ψ b) id _)=>//=. by rewrite -HΨ.
307
Qed.
308

Ralf Jung's avatar
Ralf Jung committed
309
Lemma pure_impl_forall φ P : (⌜φ⌝  P)  ( _ : φ, P).
310 311
Proof.
  apply (anti_symm _).
312
  - apply forall_intro=> ?. by rewrite pure_True // left_id.
313 314
  - apply impl_intro_l, pure_elim_l=> Hφ. by rewrite (forall_elim Hφ).
Qed.
Ralf Jung's avatar
Ralf Jung committed
315
Lemma pure_alt φ : ⌜φ⌝   _ : φ, True.
316 317 318 319 320 321 322 323 324 325 326 327 328 329 330 331
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.

332
Global Instance iff_ne : NonExpansive2 (@uPred_iff M).
333 334 335 336 337 338
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.
339
Lemma iff_equiv P Q : (P  Q)%I  (P  Q).
340 341
Proof.
  intros HPQ; apply (anti_symm ());
342
    apply impl_entails; rewrite /uPred_valid HPQ /uPred_iff; auto.
343
Qed.
344
Lemma equiv_iff P Q : (P  Q)  (P  Q)%I.
345
Proof. intros ->; apply iff_refl. Qed.
346
Lemma internal_eq_iff P Q : P  Q  P  Q.
347
Proof.
348 349
  apply (internal_eq_rewrite P Q (λ Q, P  Q))%I;
    first solve_proper; auto using iff_refl.
350 351 352 353
Qed.

(* Derived BI Stuff *)
Hint Resolve sep_mono.
354
Lemma sep_mono_l P P' Q : (P  Q)  P  P'  Q  P'.
355
Proof. by intros; apply sep_mono. Qed.
356
Lemma sep_mono_r P P' Q' : (P'  Q')  P  P'  P  Q'.
357 358 359 360 361 362
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.
363
Lemma wand_mono P P' Q Q' : (Q  P)  (P'  Q')  (P - P')  Q - Q'.
364 365 366 367 368
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.
369 370 371
Global Instance wand_flip_mono' :
  Proper (() ==> flip () ==> flip ()) (@uPred_wand M).
Proof. by intros P P' HP Q Q' HQ; apply wand_mono. Qed.
372 373 374 375 376 377 378 379 380 381 382 383

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

438
Lemma sep_and P Q : (P  Q)  (P  Q).
439
Proof. auto. Qed.
440
Lemma impl_wand_1 P Q : (P  Q)  P - Q.
441
Proof. apply wand_intro_r, impl_elim with P; auto. Qed.
Ralf Jung's avatar
Ralf Jung committed
442
Lemma pure_elim_sep_l φ Q R : (φ  Q  R)  ⌜φ⌝  Q  R.
443
Proof. intros; apply pure_elim with φ; eauto. Qed.
Ralf Jung's avatar
Ralf Jung committed
444
Lemma pure_elim_sep_r φ Q R : (φ  Q  R)  Q  ⌜φ⌝  R.
445 446 447 448 449 450 451
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.

452
Lemma entails_equiv_and P Q : (P  Q  P)  (P  Q).
Robbert Krebbers's avatar
Robbert Krebbers committed
453
Proof. split. by intros ->; auto. intros; apply (anti_symm _); auto. Qed.
454
Lemma sep_and_l P Q R : P  (Q  R)  (P  Q)  (P  R).
455
Proof. auto. Qed.
456
Lemma sep_and_r P Q R : (P  Q)  R  (P  R)  (Q  R).
457
Proof. auto. Qed.
458
Lemma sep_or_l P Q R : P  (Q  R)  (P  Q)  (P  R).
459 460 461 462
Proof.
  apply (anti_symm ()); last by eauto 8.
  apply wand_elim_r', or_elim; apply wand_intro_l; auto.
Qed.
463
Lemma sep_or_r P Q R : (P  Q)  R  (P  R)  (Q  R).
464
Proof. by rewrite -!(comm _ R) sep_or_l. Qed.
465
Lemma sep_exist_l {A} P (Ψ : A  uPred M) : P  ( a, Ψ a)   a, P  Ψ a.
466 467 468 469 470 471
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.
472
Lemma sep_exist_r {A} (Φ: A  uPred M) Q: ( a, Φ a)  Q   a, Φ a  Q.
473
Proof. setoid_rewrite (comm _ _ Q); apply sep_exist_l. Qed.
474
Lemma sep_forall_l {A} P (Ψ : A  uPred M) : P  ( a, Ψ a)   a, P  Ψ a.
475
Proof. by apply forall_intro=> a; rewrite forall_elim. Qed.
476
Lemma sep_forall_r {A} (Φ : A  uPred M) Q : ( a, Φ a)  Q   a, Φ a  Q.
477 478
Proof. by apply forall_intro=> a; rewrite forall_elim. Qed.

479 480 481 482 483 484 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 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 572 573 574 575 576
(* 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.
  apply (internal_eq_rewrite a b (λ b,  (a  b))%I); auto.
  { intros n; solve_proper. }
  rewrite -(internal_eq_refl a) plainly_pure; auto.
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.

577
(* Always derived *)
578 579 580 581 582 583
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.
584

585 586 587 588
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.
589

590
Lemma persistently_pure φ :  ⌜φ⌝  ⌜φ⌝.
591
Proof. by rewrite -plainly_pure persistently_plainly. Qed.
592
Lemma persistently_forall {A} (Ψ : A  uPred M) : (  a, Ψ a)  ( a,  Ψ a).
593
Proof.
594
  apply (anti_symm _); auto using persistently_forall_2.
595 596
  apply forall_intro=> x. by rewrite (forall_elim x).
Qed.
597
Lemma persistently_exist {A} (Ψ : A  uPred M) : (  a, Ψ a)  ( a,  Ψ a).
598
Proof.
599
  apply (anti_symm _); auto using persistently_exist_1.
600 601
  apply exist_elim=> x. by rewrite (exist_intro x).
Qed.
602 603 604 605 606
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.
607
Proof.
608 609
  apply impl_intro_l; rewrite -persistently_and.
  apply persistently_mono, impl_elim with P; auto.
610
Qed.
611
Lemma persistently_internal_eq {A:ofeT} (a b : A) :  (a  b)  a  b.
612
Proof. by rewrite -plainly_internal_eq persistently_plainly. Qed.
613

614
Lemma persistently_and_sep_l P Q :  P  Q   P  Q.
615
Proof. apply (anti_symm ()); auto using persistently_and_sep_l_1. Qed.
616 617 618 619
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.
620

621
Lemma persistently_and_sep P Q :  (P  Q)   (P  Q).
622 623
Proof.
  apply (anti_symm ()); auto.
624
  rewrite -{1}persistently_idemp persistently_and persistently_and_sep_l; auto.
625
Qed.
626
Lemma persistently_sep P Q :  (P  Q)   P   Q.
627
Proof. by rewrite -persistently_and_sep -persistently_and_sep_l persistently_and. Qed.
628

629 630
Lemma persistently_wand P Q :  (P - Q)   P -  Q.
Proof. by apply wand_intro_r; rewrite -persistently_sep wand_elim_l. Qed.
631
Lemma persistently_impl_wand P Q :  (P  Q)   (P - Q).
632
Proof.
633
  apply (anti_symm ()); [by rewrite -impl_wand_1|].
634
  apply persistently_intro', impl_intro_r.
635
  by rewrite persistently_and_sep_l persistently_elim wand_elim_l.
636
Qed.
637
Lemma impl_wand_persistently P Q : ( P  Q)  ( P - Q).
Ralf Jung's avatar
Ralf Jung committed
638
Proof.
639 640
  apply (anti_symm ()); [by rewrite -impl_wand_1|].
  apply impl_intro_l. by rewrite persistently_and_sep_l wand_elim_r.
Ralf Jung's avatar
Ralf Jung committed
641
Qed.
642 643 644 645
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.
646

647 648
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's avatar
Robbert Krebbers committed
649

650 651 652 653
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).
654
    apply sep_mono_r. rewrite -persistently_pure. apply persistently_mono, impl_intro_l.
655
    by rewrite wand_elim_r right_id.
656
  - apply exist_elim=> R. apply wand_intro_l. rewrite assoc -persistently_and_sep_r.
657
    by rewrite persistently_elim impl_elim_r.
658 659 660 661 662
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).
663
    apply and_mono_r. rewrite -persistently_pure. apply persistently_mono, wand_intro_l.
664
    by rewrite impl_elim_r right_id.
665
  - apply exist_elim=> R. apply impl_intro_l. rewrite assoc persistently_and_sep_r.
666
    by rewrite persistently_elim wand_elim_r.
667
Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
668

669 670 671 672 673 674 675 676 677 678 679 680 681 682 683 684 685 686 687 688 689 690 691
(* 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.
Robbert Krebbers's avatar
Robbert Krebbers committed
692 693
Lemma later_exist_2 {A} (Φ : A  uPred M) : ( a,  Φ a)   ( a, Φ a).
Proof. apply exist_elim; eauto using exist_intro. Qed.
694 695 696
Lemma later_exist `{Inhabited A} (Φ : A  uPred M) :
   ( a, Φ a)  ( a,  Φ a).
Proof.
Robbert Krebbers's avatar
Robbert Krebbers committed
697
  apply: anti_symm; [|apply later_exist_2].
698 699 700 701 702 703 704 705 706
  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.
707
Lemma later_wand P Q :  (P - Q)   P -  Q.
708 709 710 711
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
712
(* Iterated later modality *)
713
Global Instance laterN_ne m : NonExpansive (@uPred_laterN M m).
Robbert Krebbers's avatar
Robbert Krebbers committed
714 715 716 717 718 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
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's avatar
Robbert Krebbers committed
744 745
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's avatar
Robbert Krebbers committed
746 747 748 749 750 751 752 753 754 755 756 757 758 759 760 761 762 763 764 765
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.

766 767
(* Conditional persistently *)
Global Instance persistently_if_ne p : NonExpansive (@uPred_persistently_if M p).
768
Proof. solve_proper. Qed.
769
Global Instance persistently_if_proper p : Proper (() ==> ()) (@uPred_persistently_if M p).
770
Proof. solve_proper. Qed.
771
Global Instance persistently_if_mono p : Proper (() ==> ()) (@uPred_persistently_if M p).
772 773
Proof. solve_proper. Qed.

774 775 776 777 778 779 780 781 782 783 784 785 786 787 788 789 790 791 792
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.
793 794

(* True now *)
795
Global Instance except_0_ne : NonExpansive (@uPred_except_0 M).
796
Proof. solve_proper. Qed.
797
Global Instance except_0_proper : Proper (() ==> ()) (@uPred_except_0 M).
798
Proof. solve_proper. Qed.
799
Global Instance except_0_mono' :</