derived.v 35.3 KB
Newer Older
1 2 3 4 5 6 7 8 9 10 11 12 13 14
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.

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)
  (at level 20, p at level 0, P at level 20, format "□? p  P").

15 16
Definition uPred_except_0 {M} (P : uPred M) : uPred M :=  False  P.
Notation "◇ P" := (uPred_except_0 P)
17
  (at level 20, right associativity) : uPred_scope.
18 19
Instance: Params (@uPred_except_0) 1.
Typeclasses Opaque uPred_except_0.
20 21 22 23 24 25 26 27 28 29 30 31 32 33 34 35 36 37 38 39 40 41 42 43 44 45 46 47 48 49 50 51 52 53 54 55 56 57 58 59 60 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 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

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.
Proof. by apply (pure_elim False). Qed.
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.
Lemma impl_entails P Q : (True  P  Q)  P  Q.
Proof. intros HPQ; apply impl_elim with P; rewrite -?HPQ; auto. Qed.
Lemma entails_impl P Q : (P  Q)  True  P  Q.
Proof. auto using impl_intro_l. Qed.

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.
116 117 118
Global Instance impl_flip_mono' :
  Proper (() ==> flip () ==> flip ()) (@uPred_impl M).
Proof. by intros P P' HP Q Q' HQ; apply impl_mono. Qed.
119 120 121
Global Instance forall_mono' A :
  Proper (pointwise_relation _ () ==> ()) (@uPred_forall M A).
Proof. intros P1 P2; apply forall_mono. Qed.
122 123 124
Global Instance forall_flip_mono' A :
  Proper (pointwise_relation _ (flip ()) ==> flip ()) (@uPred_forall M A).
Proof. intros P1 P2; apply forall_mono. Qed.
125
Global Instance exist_mono' A :
126 127 128 129
  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).
130 131 132 133 134 135 136 137 138 139 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
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.
166 167 168 169 170
Lemma False_impl P : (False  P)  True.
Proof.
  apply (anti_symm ()); [by auto|].
  apply impl_intro_l. rewrite left_absorb. auto.
Qed.
171 172 173 174 175 176 177 178 179 180 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

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.
207 208 209 210 211 212 213
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.
214

Ralf Jung's avatar
Ralf Jung committed
215
Lemma pure_mono φ1 φ2 : (φ1  φ2)  ⌜φ1  ⌜φ2.
216 217 218
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
219
Lemma pure_iff φ1 φ2 : (φ1  φ2)  ⌜φ1  ⌜φ2.
220
Proof. intros [??]; apply (anti_symm _); auto using pure_mono. Qed.
Ralf Jung's avatar
Ralf Jung committed
221
Lemma pure_intro_l φ Q R : φ  (⌜φ⌝  Q  R)  Q  R.
222
Proof. intros ? <-; auto using pure_intro. Qed.
Ralf Jung's avatar
Ralf Jung committed
223
Lemma pure_intro_r φ Q R : φ  (Q  ⌜φ⌝  R)  Q  R.
224
Proof. intros ? <-; auto. Qed.
Ralf Jung's avatar
Ralf Jung committed
225
Lemma pure_intro_impl φ Q R : φ  (Q  ⌜φ⌝  R)  Q  R.
226
Proof. intros ? ->. eauto using pure_intro_l, impl_elim_r. Qed.
Ralf Jung's avatar
Ralf Jung committed
227
Lemma pure_elim_l φ Q R : (φ  Q  R)  ⌜φ⌝  Q  R.
228
Proof. intros; apply pure_elim with φ; eauto. Qed.
Ralf Jung's avatar
Ralf Jung committed
229
Lemma pure_elim_r φ Q R : (φ  Q  R)  Q  ⌜φ⌝  R.
230
Proof. intros; apply pure_elim with φ; eauto. Qed.
231

Ralf Jung's avatar
Ralf Jung committed
232
Lemma pure_True (φ : Prop) : φ  ⌜φ⌝  True.
233
Proof. intros; apply (anti_symm _); auto. Qed.
Ralf Jung's avatar
Ralf Jung committed
234
Lemma pure_False (φ : Prop) : ¬φ  ⌜φ⌝  False.
235
Proof. intros; apply (anti_symm _); eauto using pure_elim. Qed.
236

Ralf Jung's avatar
Ralf Jung committed
237
Lemma pure_and φ1 φ2 : ⌜φ1  φ2  ⌜φ1  ⌜φ2.
238 239 240 241 242
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
243
Lemma pure_or φ1 φ2 : ⌜φ1  φ2  ⌜φ1  ⌜φ2.
244 245 246 247 248
Proof.
  apply (anti_symm _).
  - eapply pure_elim=> // -[?|?]; auto.
  - apply or_elim; eapply pure_elim; eauto.
Qed.
Ralf Jung's avatar
Ralf Jung committed
249
Lemma pure_impl φ1 φ2 : ⌜φ1  φ2  (⌜φ1  ⌜φ2).
250 251 252 253
Proof.
  apply (anti_symm _).
  - apply impl_intro_l. rewrite -pure_and. apply pure_mono. naive_solver.
  - rewrite -pure_forall_2. apply forall_intro=> ?.
254
    by rewrite -(left_id True uPred_and (_→_))%I (pure_True φ1) // impl_elim_r.
255
Qed.
Ralf Jung's avatar
Ralf Jung committed
256
Lemma pure_forall {A} (φ : A  Prop) :  x, φ x   x, ⌜φ x.
257 258 259 260
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
261
Lemma pure_exist {A} (φ : A  Prop) :  x, φ x   x, ⌜φ x.
262 263 264 265 266 267
Proof.
  apply (anti_symm _).
  - eapply pure_elim=> // -[x ?]. rewrite -(exist_intro x); auto.
  - apply exist_elim=> x. eauto using pure_mono.
Qed.

268
Lemma internal_eq_refl' {A : ofeT} (a : A) P : P  a  a.
269 270
Proof. rewrite (True_intro P). apply internal_eq_refl. Qed.
Hint Resolve internal_eq_refl'.
271
Lemma equiv_internal_eq {A : ofeT} P (a b : A) : a  b  P  a  b.
272
Proof. by intros ->. Qed.
273
Lemma internal_eq_sym {A : ofeT} (a b : A) : a  b  b  a.
274
Proof. apply (internal_eq_rewrite a b (λ b, b  a)%I); auto. solve_proper. Qed.
275

Ralf Jung's avatar
Ralf Jung committed
276
Lemma pure_impl_forall φ P : (⌜φ⌝  P)  ( _ : φ, P).
277 278
Proof.
  apply (anti_symm _).
279
  - apply forall_intro=> ?. by rewrite pure_True // left_id.
280 281
  - apply impl_intro_l, pure_elim_l=> Hφ. by rewrite (forall_elim Hφ).
Qed.
Ralf Jung's avatar
Ralf Jung committed
282
Lemma pure_alt φ : ⌜φ⌝   _ : φ, True.
283 284 285 286 287 288 289 290 291 292 293 294 295 296 297 298 299 300 301 302 303 304 305 306 307 308 309 310 311 312
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.
Lemma iff_equiv P Q : (True  P  Q)  (P  Q).
Proof.
  intros HPQ; apply (anti_symm ());
    apply impl_entails; rewrite HPQ /uPred_iff; auto.
Qed.
Lemma equiv_iff P Q : (P  Q)  True  P  Q.
Proof. intros ->; apply iff_refl. Qed.
313
Lemma internal_eq_iff P Q : P  Q  P  Q.
314
Proof.
315 316
  apply (internal_eq_rewrite P Q (λ Q, P  Q))%I;
    first solve_proper; auto using iff_refl.
317 318 319 320
Qed.

(* Derived BI Stuff *)
Hint Resolve sep_mono.
321
Lemma sep_mono_l P P' Q : (P  Q)  P  P'  Q  P'.
322
Proof. by intros; apply sep_mono. Qed.
323
Lemma sep_mono_r P P' Q' : (P'  Q')  P  P'  P  Q'.
324 325 326 327 328 329
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.
330
Lemma wand_mono P P' Q Q' : (Q  P)  (P'  Q')  (P - P')  Q - Q'.
331 332 333 334 335
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.
336 337 338
Global Instance wand_flip_mono' :
  Proper (() ==> flip () ==> flip ()) (@uPred_wand M).
Proof. by intros P P' HP Q Q' HQ; apply wand_mono. Qed.
339 340 341 342 343 344 345 346 347 348 349 350

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.
351
Lemma sep_elim_l P Q : P  Q  P.
352
Proof. by rewrite (True_intro Q) right_id. Qed.
353 354 355
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.
356
Proof. intros ->; apply sep_elim_l. Qed.
357
Lemma sep_elim_r' P Q R : (Q  R)  P  Q  R.
358 359
Proof. intros ->; apply sep_elim_r. Qed.
Hint Resolve sep_elim_l' sep_elim_r'.
360
Lemma sep_intro_True_l P Q R : (True  P)  (R  Q)  R  P  Q.
361
Proof. by intros; rewrite -(left_id True%I uPred_sep R); apply sep_mono. Qed.
362
Lemma sep_intro_True_r P Q R : (R  P)  (True  Q)  R  P  Q.
363
Proof. by intros; rewrite -(right_id True%I uPred_sep R); apply sep_mono. Qed.
364
Lemma sep_elim_True_l P Q R : (True  P)  (P  R  Q)  R  Q.
365
Proof. by intros HP; rewrite -HP left_id. Qed.
366
Lemma sep_elim_True_r P Q R : (True  P)  (R  P  Q)  R  Q.
367
Proof. by intros HP; rewrite -HP right_id. Qed.
368
Lemma wand_intro_l P Q R : (Q  P  R)  P  Q - R.
369
Proof. rewrite comm; apply wand_intro_r. Qed.
370
Lemma wand_elim_l P Q : (P - Q)  P  Q.
371
Proof. by apply wand_elim_l'. Qed.
372
Lemma wand_elim_r P Q : P  (P - Q)  Q.
373
Proof. rewrite (comm _ P); apply wand_elim_l. Qed.
374
Lemma wand_elim_r' P Q R : (Q  P - R)  P  Q  R.
375
Proof. intros ->; apply wand_elim_r. Qed.
376
Lemma wand_apply P Q R S : (P  Q - R)  (S  P  Q)  S  R.
Ralf Jung's avatar
Ralf Jung committed
377
Proof. intros HR%wand_elim_l' HQ. by rewrite HQ. Qed.
378
Lemma wand_frame_l P Q R : (Q - R)  P  Q - P  R.
379
Proof. apply wand_intro_l. rewrite -assoc. apply sep_mono_r, wand_elim_r. Qed.
380
Lemma wand_frame_r P Q R : (Q - R)  Q  P - R  P.
381
Proof.
382
  apply wand_intro_l. rewrite ![(_  P)%I]comm -assoc.
383 384
  apply sep_mono_r, wand_elim_r.
Qed.
385
Lemma wand_diag P : (P - P)  True.
386
Proof. apply (anti_symm _); auto. apply wand_intro_l; by rewrite right_id. Qed.
387
Lemma wand_True P : (True - P)  P.
388 389 390 391
Proof.
  apply (anti_symm _); last by auto using wand_intro_l.
  eapply sep_elim_True_l; first reflexivity. by rewrite wand_elim_r.
Qed.
392
Lemma wand_entails P Q : (True  P - Q)  P  Q.
393 394 395
Proof.
  intros HPQ. eapply sep_elim_True_r; first exact: HPQ. by rewrite wand_elim_r.
Qed.
396
Lemma entails_wand P Q : (P  Q)  True  P - Q.
397
Proof. auto using wand_intro_l. Qed.
398
Lemma wand_curry P Q R : (P - Q - R)  (P  Q - R).
399 400 401 402 403 404
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.

405
Lemma sep_and P Q : (P  Q)  (P  Q).
406
Proof. auto. Qed.
407
Lemma impl_wand P Q : (P  Q)  P - Q.
408
Proof. apply wand_intro_r, impl_elim with P; auto. Qed.
Ralf Jung's avatar
Ralf Jung committed
409
Lemma pure_elim_sep_l φ Q R : (φ  Q  R)  ⌜φ⌝  Q  R.
410
Proof. intros; apply pure_elim with φ; eauto. Qed.
Ralf Jung's avatar
Ralf Jung committed
411
Lemma pure_elim_sep_r φ Q R : (φ  Q  R)  Q  ⌜φ⌝  R.
412 413 414 415 416 417 418
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.

419
Lemma sep_and_l P Q R : P  (Q  R)  (P  Q)  (P  R).
420
Proof. auto. Qed.
421
Lemma sep_and_r P Q R : (P  Q)  R  (P  R)  (Q  R).
422
Proof. auto. Qed.
423
Lemma sep_or_l P Q R : P  (Q  R)  (P  Q)  (P  R).
424 425 426 427
Proof.
  apply (anti_symm ()); last by eauto 8.
  apply wand_elim_r', or_elim; apply wand_intro_l; auto.
Qed.
428
Lemma sep_or_r P Q R : (P  Q)  R  (P  R)  (Q  R).
429
Proof. by rewrite -!(comm _ R) sep_or_l. Qed.
430
Lemma sep_exist_l {A} P (Ψ : A  uPred M) : P  ( a, Ψ a)   a, P  Ψ a.
431 432 433 434 435 436
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.
437
Lemma sep_exist_r {A} (Φ: A  uPred M) Q: ( a, Φ a)  Q   a, Φ a  Q.
438
Proof. setoid_rewrite (comm _ _ Q); apply sep_exist_l. Qed.
439
Lemma sep_forall_l {A} P (Ψ : A  uPred M) : P  ( a, Ψ a)   a, P  Ψ a.
440
Proof. by apply forall_intro=> a; rewrite forall_elim. Qed.
441
Lemma sep_forall_r {A} (Φ : A  uPred M) Q : ( a, Φ a)  Q   a, Φ a  Q.
442 443 444 445 446 447 448 449 450 451 452 453 454
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
455
Lemma always_pure φ :  ⌜φ⌝  ⌜φ⌝.
456 457 458 459 460 461 462 463 464 465 466 467 468 469 470 471 472 473 474 475
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.
476
Lemma always_internal_eq {A:ofeT} (a b : A) :  (a  b)  a  b.
477 478
Proof.
  apply (anti_symm ()); auto using always_elim.
479
  apply (internal_eq_rewrite a b (λ b,  (a  b))%I); auto.
480
  { intros n; solve_proper. }
481
  rewrite -(internal_eq_refl a) always_pure; auto.
482 483
Qed.

484
Lemma always_and_sep P Q :  (P  Q)   (P  Q).
485
Proof. apply (anti_symm ()); auto using always_and_sep_1. Qed.
486
Lemma always_and_sep_l' P Q :  P  Q   P  Q.
487
Proof. apply (anti_symm ()); auto using always_and_sep_l_1. Qed.
488
Lemma always_and_sep_r' P Q : P   Q  P   Q.
489
Proof. by rewrite !(comm _ P) always_and_sep_l'. Qed.
490
Lemma always_sep P Q :  (P  Q)   P   Q.
491
Proof. by rewrite -always_and_sep -always_and_sep_l' always_and. Qed.
492
Lemma always_sep_dup' P :  P   P   P.
493 494
Proof. by rewrite -always_sep -always_and_sep (idemp _). Qed.

495
Lemma always_wand P Q :  (P - Q)   P -  Q.
496
Proof. by apply wand_intro_r; rewrite -always_sep wand_elim_l. Qed.
497
Lemma always_wand_impl P Q :  (P - Q)   (P  Q).
498 499 500 501 502
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.
503
Lemma always_entails_l' P Q : (P   Q)  P   Q  P.
504
Proof. intros; rewrite -always_and_sep_l'; auto. Qed.
505
Lemma always_entails_r' P Q : (P   Q)  P  P   Q.
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
Proof. intros; rewrite -always_and_sep_r'; auto. Qed.

(* 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.
544
Lemma later_wand P Q :  (P - Q)   P -  Q.
545 546 547 548 549 550 551 552 553 554 555 556 557 558 559 560 561 562
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.


(* 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
563
Lemma always_if_pure p φ : ?p ⌜φ⌝  ⌜φ⌝.
564 565 566 567 568 569 570
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.
571
Lemma always_if_sep p P Q : ?p (P  Q)  ?p P  ?p Q.
572 573 574 575 576 577
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 *)
578
Global Instance except_0_ne n : Proper (dist n ==> dist n) (@uPred_except_0 M).
579
Proof. solve_proper. Qed.
580
Global Instance except_0_proper : Proper (() ==> ()) (@uPred_except_0 M).
581
Proof. solve_proper. Qed.
582
Global Instance except_0_mono' : Proper (() ==> ()) (@uPred_except_0 M).
583
Proof. solve_proper. Qed.
584 585
Global Instance except_0_flip_mono' :
  Proper (flip () ==> flip ()) (@uPred_except_0 M).
586 587
Proof. solve_proper. Qed.

588 589 590
Lemma except_0_intro P : P   P.
Proof. rewrite /uPred_except_0; auto. Qed.
Lemma except_0_mono P Q : (P  Q)   P   Q.
591
Proof. by intros ->. Qed.
592 593 594 595 596 597 598 599 600
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.
601
Lemma except_0_sep P Q :  (P  Q)   P   Q.
602 603
Proof.
  rewrite /uPred_except_0. apply (anti_symm _).
604 605 606 607
  - 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.
608
Lemma except_0_forall {A} (Φ : A  uPred M) :  ( a, Φ a)   a,  Φ a.
609
Proof. apply forall_intro=> a. by rewrite (forall_elim a). Qed.
610
Lemma except_0_exist {A} (Φ : A  uPred M) : ( a,  Φ a)    a, Φ a.
611
Proof. apply exist_elim=> a. by rewrite (exist_intro a). Qed.
612 613 614 615 616 617
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.
618
Lemma except_0_frame_l P Q : P   Q   (P  Q).
619
Proof. by rewrite {1}(except_0_intro P) except_0_sep. Qed.
620
Lemma except_0_frame_r P Q :  P  Q   (P  Q).
621
Proof. by rewrite {1}(except_0_intro Q) except_0_sep. Qed.
622 623 624 625 626 627 628 629 630 631 632 633 634 635 636 637 638 639 640 641 642 643 644 645

(* 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.
Proof. apply (anti_symm _); auto using ownM_empty. Qed.
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.
646
Lemma bupd_frame_l R Q : (R  |==> Q) == R  Q.
647
Proof. rewrite !(comm _ R); apply bupd_frame_r. Qed.
648
Lemma bupd_wand_l P Q : (P - Q)  (|==> P) == Q.
649
Proof. by rewrite bupd_frame_l wand_elim_l. Qed.
650
Lemma bupd_wand_r P Q : (|==> P)  (P - Q) == Q.
651
Proof. by rewrite bupd_frame_r wand_elim_r. Qed.
652
Lemma bupd_sep P Q : (|==> P)  (|==> Q) == P  Q.
653 654 655 656 657 658
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.
659
Lemma except_0_bupd P :  (|==> P)  (|==>  P).
660
Proof.
661
  rewrite /uPred_except_0. apply or_elim; auto using bupd_mono.
662 663 664 665
  by rewrite -bupd_intro -or_intro_l.
Qed.

(* Timeless instances *)
Ralf Jung's avatar
Ralf Jung committed
666
Global Instance pure_timeless φ : TimelessP (⌜φ⌝ : uPred M)%I.
667 668 669 670 671 672 673
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).
674
Proof. intros; rewrite /TimelessP except_0_and later_and; auto. Qed.
675
Global Instance or_timeless P Q : TimelessP P  TimelessP Q  TimelessP (P  Q).
676
Proof. intros; rewrite /TimelessP except_0_or later_or; auto. Qed.
677 678 679 680 681
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.
682
  rewrite HQ /uPred_except_0 !and_or_r. apply or_elim; last auto.
683 684
  by rewrite assoc (comm _ _ P) -assoc !impl_elim_r.
Qed.
685
Global Instance sep_timeless P Q: TimelessP P  TimelessP Q  TimelessP (P  Q).
686
Proof. intros; rewrite /TimelessP except_0_sep later_sep; auto. Qed.
687
Global Instance wand_timeless P Q : TimelessP Q  TimelessP (P - Q).
688 689 690 691
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.
692
  rewrite HQ /uPred_except_0 !and_or_r. apply or_elim; last auto.
693 694 695 696 697 698 699 700 701
  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.
702
  rewrite HQ /uPred_except_0 !and_or_r. apply or_elim; last auto.
703 704 705 706 707 708
  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.
709
  - rewrite /uPred_except_0; auto.
710 711 712
  - apply exist_elim=> x. rewrite -(exist_intro x); auto.
Qed.
Global Instance always_timeless P : TimelessP P  TimelessP ( P).
713
Proof. intros; rewrite /TimelessP except_0_always -always_later; auto. Qed.
714 715
Global Instance always_if_timeless p P : TimelessP P  TimelessP (?p P).
Proof. destruct p; apply _. Qed.
716
Global Instance eq_timeless {A : ofeT} (a b : A) :
717 718 719 720 721
  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.
722
  rewrite (timelessP (ab)) (except_0_intro (uPred_ownM b)) -except_0_and.
723 724
  apply except_0_mono. rewrite internal_eq_sym.
  apply (internal_eq_rewrite b a (uPred_ownM)); first apply _; auto.
725 726 727
Qed.

(* Persistence *)
Ralf Jung's avatar
Ralf Jung committed
728
Global Instance pure_persistent φ : PersistentP (⌜φ⌝ : uPred M)%I.
729 730 731 732 733 734 735 736 737 738
Proof. by rewrite /PersistentP always_pure. Qed.
Global Instance always_persistent P : PersistentP ( P).
Proof. by intros; apply always_intro'. Qed.
Global Instance and_persistent P Q :
  PersistentP P  PersistentP Q  PersistentP (P  Q).
Proof. by intros; rewrite /PersistentP always_and; apply and_mono. Qed.
Global Instance or_persistent P Q :
  PersistentP P  PersistentP Q  PersistentP (P  Q).
Proof. by intros; rewrite /PersistentP always_or; apply or_mono. Qed.
Global Instance sep_persistent P Q :
739
  PersistentP P  PersistentP Q  PersistentP (P  Q).
740 741 742 743 744 745 746
Proof. by intros; rewrite /PersistentP always_sep; apply sep_mono. Qed.
Global Instance forall_persistent {A} (Ψ : A  uPred M) :
  ( x, PersistentP (Ψ x))  PersistentP ( x, Ψ x).
Proof. by intros; rewrite /PersistentP always_forall; apply forall_mono. Qed.
Global Instance exist_persistent {A} (Ψ : A  uPred M) :
  ( x, PersistentP (Ψ x))  PersistentP ( x, Ψ x).
Proof. by intros; rewrite /PersistentP always_exist; apply exist_mono. Qed.
747
Global Instance internal_eq_persistent {A : ofeT} (a b : A) :
748
  PersistentP (a  b : uPred M)%I.
749
Proof. by intros; rewrite /PersistentP always_internal_eq. Qed.
750 751 752 753 754 755 756 757 758 759 760 761 762 763 764 765 766 767
Global Instance cmra_valid_persistent {A : cmraT} (a : A) :
  PersistentP ( a : uPred M)%I.
Proof. by intros; rewrite /PersistentP always_cmra_valid. Qed.
Global Instance later_persistent P : PersistentP P  PersistentP ( P).
Proof. by intros; rewrite /PersistentP always_later; apply later_mono. Qed.
Global Instance ownM_persistent : Persistent a  PersistentP (@uPred_ownM M a).
Proof. intros. by rewrite /PersistentP always_ownM. Qed.
Global Instance from_option_persistent {A} P (Ψ : A  uPred M) (mx : option A) :
  ( x, PersistentP (Ψ x))  PersistentP P  PersistentP (from_option Ψ P mx).
Proof. destruct mx; apply _. Qed.

(* Derived lemmas for persistence *)
Lemma always_always P `{!PersistentP P} :  P  P.
Proof. apply (anti_symm ()); auto using always_elim. Qed.
Lemma always_if_always p P `{!PersistentP P} : ?p P  P.
Proof. destruct p; simpl; auto using always_always. Qed.
Lemma always_intro P Q `{!PersistentP P} : (P  Q)  P   Q.
Proof. rewrite -(always_always P); apply always_intro'. Qed.
768
Lemma always_and_sep_l P Q `{!PersistentP P} : P  Q  P  Q.
769
Proof. by rewrite -(always_always P) always_and_sep_l'. Qed.
770
Lemma always_and_sep_r P Q `{!PersistentP Q} : P  Q  P  Q.
771
Proof. by rewrite -(always_always Q) always_and_sep_r'. Qed.
772
Lemma always_sep_dup P `{!PersistentP P} : P  P  P.
773
Proof. by rewrite -(always_always P) -always_sep_dup'. Qed.
774
Lemma always_entails_l P Q `{!PersistentP Q} : (P  Q)  P  Q  P.
775
Proof. by rewrite -(always_always Q); apply always_entails_l'. Qed.
776
Lemma always_entails_r P Q `{!PersistentP Q} : (P  Q)  P  P  Q.
777 778 779
Proof. by rewrite -(always_always Q); apply always_entails_r'. Qed.
End derived.
End uPred_derived.