derived.v 46.5 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
Module uPred.
43 44 45 46 47 48 49 50 51 52
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.
53
Proof. by apply (pure_elim' False). Qed.
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
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.
85
Lemma impl_entails P Q : (P  Q)%I  P  Q.
86
Proof. intros HPQ; apply impl_elim with P; rewrite -?HPQ; auto. Qed.
87 88
Lemma entails_impl P Q : (P  Q)  (P  Q)%I.
Proof. intro. apply impl_intro_l. auto. Qed.
89 90 91 92 93 94 95 96 97 98 99 100 101 102 103 104 105 106 107 108 109 110 111 112 113 114 115 116 117 118 119 120 121 122 123 124 125 126 127 128 129 130

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.
131 132 133
Global Instance impl_flip_mono' :
  Proper (() ==> flip () ==> flip ()) (@uPred_impl M).
Proof. by intros P P' HP Q Q' HQ; apply impl_mono. Qed.
134 135 136
Global Instance forall_mono' A :
  Proper (pointwise_relation _ () ==> ()) (@uPred_forall M A).
Proof. intros P1 P2; apply forall_mono. Qed.
137 138 139
Global Instance forall_flip_mono' A :
  Proper (pointwise_relation _ (flip ()) ==> flip ()) (@uPred_forall M A).
Proof. intros P1 P2; apply forall_mono. Qed.
140
Global Instance exist_mono' A :
Jacques-Henri Jourdan's avatar
Jacques-Henri Jourdan committed
141
  Proper (pointwise_relation _ () ==> ()) (@uPred_exist M A).
142 143 144
Proof. intros P1 P2; apply exist_mono. Qed.
Global Instance exist_flip_mono' A :
  Proper (pointwise_relation _ (flip ()) ==> flip ()) (@uPred_exist M A).
145 146 147 148 149 150 151 152 153 154 155 156 157 158 159 160 161 162 163 164 165 166 167 168 169 170 171 172 173 174 175 176 177 178 179 180
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.
181 182 183 184 185
Lemma False_impl P : (False  P)  True.
Proof.
  apply (anti_symm ()); [by auto|].
  apply impl_intro_l. rewrite left_absorb. auto.
Qed.
186 187 188 189 190 191 192 193 194 195 196 197 198 199 200 201 202 203 204 205 206 207 208 209 210 211 212 213 214 215 216 217 218 219 220 221

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.
222 223 224 225 226 227 228
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.
229

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

Ralf Jung's avatar
Ralf Jung committed
254
Lemma pure_True (φ : Prop) : φ  ⌜φ⌝  True.
255
Proof. intros; apply (anti_symm _); auto. Qed.
Ralf Jung's avatar
Ralf Jung committed
256
Lemma pure_False (φ : Prop) : ¬φ  ⌜φ⌝  False.
257
Proof. intros; apply (anti_symm _); eauto using pure_elim. Qed.
258

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

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

Ralf Jung's avatar
Ralf Jung committed
304
Lemma pure_impl_forall φ P : (⌜φ⌝  P)  ( _ : φ, P).
305 306
Proof.
  apply (anti_symm _).
307
  - apply forall_intro=> ?. by rewrite pure_True // left_id.
308 309
  - apply impl_intro_l, pure_elim_l=> Hφ. by rewrite (forall_elim Hφ).
Qed.
Ralf Jung's avatar
Ralf Jung committed
310
Lemma pure_alt φ : ⌜φ⌝   _ : φ, True.
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.

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

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

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

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

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

(* Always derived *)
475 476 477 478 479 480
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.
481

482 483 484 485
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.
486

487
Lemma persistently_pure φ :  ⌜φ⌝  ⌜φ⌝.
488 489 490 491
Proof.
  apply (anti_symm _); auto.
  apply pure_elim'=> Hφ.
  trans ( x : False,  True : uPred M)%I; [by apply forall_intro|].
492
  rewrite persistently_forall_2. auto using persistently_mono, pure_intro.
493
Qed.
494
Lemma persistently_forall {A} (Ψ : A  uPred M) : (  a, Ψ a)  ( a,  Ψ a).
495
Proof.
496
  apply (anti_symm _); auto using persistently_forall_2.
497 498
  apply forall_intro=> x. by rewrite (forall_elim x).
Qed.
499
Lemma persistently_exist {A} (Ψ : A  uPred M) : (  a, Ψ a)  ( a,  Ψ a).
500
Proof.
501
  apply (anti_symm _); auto using persistently_exist_1.
502 503
  apply exist_elim=> x. by rewrite (exist_intro x).
Qed.
504 505 506 507 508
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.
509
Proof.
510 511
  apply impl_intro_l; rewrite -persistently_and.
  apply persistently_mono, impl_elim with P; auto.
512
Qed.
513
Lemma persistently_internal_eq {A:ofeT} (a b : A) :  (a  b)  a  b.
514
Proof.
515
  apply (anti_symm ()); auto using persistently_elim.
516
  apply (internal_eq_rewrite a b (λ b,  (a  b))%I); auto.
517
  { intros n; solve_proper. }
518
  rewrite -(internal_eq_refl a) persistently_pure; auto.
519 520
Qed.

521
Lemma persistently_and_sep_l P Q :  P  Q   P  Q.
522
Proof. apply (anti_symm ()); auto using persistently_and_sep_l_1. Qed.
523 524 525 526
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.
527

528
Lemma persistently_and_sep P Q :  (P  Q)   (P  Q).
529 530
Proof.
  apply (anti_symm ()); auto.
531
  rewrite -{1}persistently_idemp persistently_and persistently_and_sep_l; auto.
532
Qed.
533
Lemma persistently_sep P Q :  (P  Q)   P   Q.
534
Proof. by rewrite -persistently_and_sep -persistently_and_sep_l persistently_and. Qed.
535

536 537
Lemma persistently_wand P Q :  (P - Q)   P -  Q.
Proof. by apply wand_intro_r; rewrite -persistently_sep wand_elim_l. Qed.
538
Lemma persistently_impl_wand P Q :  (P  Q)   (P - Q).
539
Proof.
540
  apply (anti_symm ()); [by rewrite -impl_wand_1|].
541
  apply persistently_intro', impl_intro_r.
542
  by rewrite persistently_and_sep_l persistently_elim wand_elim_l.
543
Qed.
544
Lemma impl_wand_persistently P Q : ( P  Q)  ( P - Q).
Ralf Jung's avatar
Ralf Jung committed
545
Proof.
546 547
  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
548
Qed.
549 550 551 552
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.
553

554 555
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
556

557 558 559 560
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).
561
    apply sep_mono_r. rewrite -persistently_pure. apply persistently_mono, impl_intro_l.
562
    by rewrite wand_elim_r right_id.
563
  - apply exist_elim=> R. apply wand_intro_l. rewrite assoc -persistently_and_sep_r.
564
    by rewrite persistently_elim impl_elim_r.
565 566 567 568 569
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).
570
    apply and_mono_r. rewrite -persistently_pure. apply persistently_mono, wand_intro_l.
571
    by rewrite impl_elim_r right_id.
572
  - apply exist_elim=> R. apply impl_intro_l. rewrite assoc persistently_and_sep_r.
573
    by rewrite persistently_elim wand_elim_r.
574
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
(* 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
599 600
Lemma later_exist_2 {A} (Φ : A  uPred M) : ( a,  Φ a)   ( a, Φ a).
Proof. apply exist_elim; eauto using exist_intro. Qed.
601 602 603
Lemma later_exist `{Inhabited A} (Φ : A  uPred M) :
   ( a, Φ a)  ( a,  Φ a).
Proof.
Robbert Krebbers's avatar
Robbert Krebbers committed
604
  apply: anti_symm; [|apply later_exist_2].
605 606 607 608 609 610 611 612 613
  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.
614
Lemma later_wand P Q :  (P - Q)   P -  Q.
615 616 617 618 619
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
620
(* Iterated later modality *)
621
Global Instance laterN_ne m : NonExpansive (@uPred_laterN M m).
Robbert Krebbers's avatar
Robbert Krebbers committed
622 623 624 625 626 627 628 629 630 631 632 633 634 635 636 637 638 639 640 641 642 643 644 645 646 647 648 649 650 651
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
652 653
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
654 655 656 657 658 659 660 661 662 663 664 665 666 667 668 669 670 671 672 673
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.

674 675
(* Conditional persistently *)
Global Instance persistently_if_ne p : NonExpansive (@uPred_persistently_if M p).
676
Proof. solve_proper. Qed.
677
Global Instance persistently_if_proper p : Proper (() ==> ()) (@uPred_persistently_if M p).
678
Proof. solve_proper. Qed.
679
Global Instance persistently_if_mono p : Proper (() ==> ()) (@uPred_persistently_if M p).
680 681
Proof. solve_proper. Qed.

682 683 684 685 686 687 688 689 690 691 692 693 694 695 696 697 698 699 700
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.
701 702

(* True now *)
703
Global Instance except_0_ne : NonExpansive (@uPred_except_0 M).
704
Proof. solve_proper. Qed.
705
Global Instance except_0_proper : Proper (() ==> ()) (@uPred_except_0 M).
706
Proof. solve_proper. Qed.
707
Global Instance except_0_mono' : Proper (() ==> ()) (@uPred_except_0 M).
708
Proof. solve_proper. Qed.
709 710
Global Instance except_0_flip_mono' :
  Proper (flip () ==> flip ()) (@uPred_except_0 M).
711 712
Proof. solve_proper. Qed.

713 714 715
Lemma except_0_intro P : P   P.
Proof. rewrite /uPred_except_0; auto. Qed.
Lemma except_0_mono P Q : (P  Q)   P   Q.
716
Proof. by intros ->. Qed.
717 718 719 720 721 722 723 724 725
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.
726
Lemma except_0_sep P Q :  (P  Q)   P   Q.
727 728
Proof.
  rewrite /uPred_except_0. apply (anti_symm _).
729
  - apply or_elim; last by auto.
730
    by rewrite -!or_intro_l -persistently_pure -persistently_later -persistently_sep_dup.
731 732
  - rewrite sep_or_r sep_elim_l sep_or_l; auto.
Qed.
733
Lemma except_0_forall {A} (Φ : A  uPred M) :  ( a, Φ a)   a,  Φ a.
734
Proof. apply forall_intro=> a. by rewrite (forall_elim a). Qed.
735
Lemma except_0_exist_2 {A} (Φ : A  uPred M) : ( a,  Φ a)    a, Φ a.
736
Proof. apply exist_elim=> a. by rewrite (exist_intro a). Qed.
737 738 739 740 741 742 743
Lemma except_0_exist `{Inhabited A} (Φ : A  uPred M) :
   ( a, Φ a)  ( a,  Φ a).
Proof.
  apply (anti_symm _); [|by apply except_0_exist_2]. apply or_elim.
  - rewrite -(exist_intro inhabitant). by apply or_intro_l.
  - apply exist_mono=> a. apply except_0_intro.
Qed.
744 745
Lemma except_0_later P :   P   P.
Proof. by rewrite /uPred_except_0 -later_or False_or. Qed.
746 747 748 749
Lemma except_0_persistently P :   P    P.
Proof. by rewrite /uPred_except_0 persistently_or persistently_later persistently_pure. Qed.
Lemma except_0_persistently_if p P :  ?p P  ?p  P.
Proof. destruct p; simpl; auto using except_0_persistently. Qed.