derived_laws_bi.v 63.1 KB
Newer Older
1
From iris.bi Require Export derived_connectives.
Robbert Krebbers's avatar
Robbert Krebbers committed
2
3
4
From iris.algebra Require Import monoid.
From stdpp Require Import hlist.

Ralf Jung's avatar
Ralf Jung committed
5
6
7
8
9
10
11
(** Naming schema for lemmas about modalities:
    M1_into_M2: M1 P ⊢ M2 P
    M1_M2_elim: M1 (M2 P) ⊣⊢ M1 P
    M1_elim_M2: M1 (M2 P) ⊣⊢ M2 P
    M1_M2: M1 (M2 P) ⊣⊢ M2 (M1 P)
*)

Robbert Krebbers's avatar
Robbert Krebbers committed
12
13
14
15
16
17
18
19
20
21
22
23
Module bi.
Import interface.bi.
Section bi_derived.
Context {PROP : bi}.
Implicit Types φ : Prop.
Implicit Types P Q R : PROP.
Implicit Types Ps : list PROP.
Implicit Types A : Type.

Hint Extern 100 (NonExpansive _) => solve_proper.

(* Force implicit argument PROP *)
24
25
Notation "P ⊢ Q" := (P @{PROP} Q).
Notation "P ⊣⊢ Q" := (P @{PROP} Q).
Robbert Krebbers's avatar
Robbert Krebbers committed
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44

(* Derived stuff about the entailment *)
Global Instance entails_anti_sym : AntiSymm () (@bi_entails PROP).
Proof. intros P Q ??. by apply equiv_spec. Qed.
Lemma equiv_entails P Q : (P  Q)  (P  Q).
Proof. apply equiv_spec. Qed.
Lemma equiv_entails_sym P Q : (Q  P)  (P  Q).
Proof. apply equiv_spec. Qed.
Global Instance entails_proper :
  Proper (() ==> () ==> iff) (() : relation PROP).
Proof.
  move => P1 P2 /equiv_spec [HP1 HP2] Q1 Q2 /equiv_spec [HQ1 HQ2]; split=>?.
  - by trans P1; [|trans Q1].
  - by trans P2; [|trans Q2].
Qed.
Lemma entails_equiv_l P Q R : (P  Q)  (Q  R)  (P  R).
Proof. by intros ->. Qed.
Lemma entails_equiv_r P Q R : (P  Q)  (Q  R)  (P  R).
Proof. by intros ? <-. Qed.
Ralf Jung's avatar
Ralf Jung committed
45
Global Instance bi_emp_valid_proper : Proper (() ==> iff) (@bi_emp_valid PROP).
Robbert Krebbers's avatar
Robbert Krebbers committed
46
Proof. solve_proper. Qed.
Ralf Jung's avatar
Ralf Jung committed
47
Global Instance bi_emp_valid_mono : Proper (() ==> impl) (@bi_emp_valid PROP).
Robbert Krebbers's avatar
Robbert Krebbers committed
48
Proof. solve_proper. Qed.
Ralf Jung's avatar
Ralf Jung committed
49
50
Global Instance bi_emp_valid_flip_mono :
  Proper (flip () ==> flip impl) (@bi_emp_valid PROP).
Robbert Krebbers's avatar
Robbert Krebbers committed
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
Proof. solve_proper. Qed.

(* Propers *)
Global Instance pure_proper : Proper (iff ==> ()) (@bi_pure PROP) | 0.
Proof. intros φ1 φ2 Hφ. apply equiv_dist=> n. by apply pure_ne. Qed.
Global Instance and_proper :
  Proper (() ==> () ==> ()) (@bi_and PROP) := ne_proper_2 _.
Global Instance or_proper :
  Proper (() ==> () ==> ()) (@bi_or PROP) := ne_proper_2 _.
Global Instance impl_proper :
  Proper (() ==> () ==> ()) (@bi_impl PROP) := ne_proper_2 _.
Global Instance sep_proper :
  Proper (() ==> () ==> ()) (@bi_sep PROP) := ne_proper_2 _.
Global Instance wand_proper :
  Proper (() ==> () ==> ()) (@bi_wand PROP) := ne_proper_2 _.
Global Instance forall_proper A :
  Proper (pointwise_relation _ () ==> ()) (@bi_forall PROP A).
Proof.
  intros Φ1 Φ2 HΦ. apply equiv_dist=> n.
  apply forall_ne=> x. apply equiv_dist, HΦ.
Qed.
Global Instance exist_proper A :
  Proper (pointwise_relation _ () ==> ()) (@bi_exist PROP A).
Proof.
  intros Φ1 Φ2 HΦ. apply equiv_dist=> n.
  apply exist_ne=> x. apply equiv_dist, HΦ.
Qed.
Global Instance persistently_proper :
  Proper (() ==> ()) (@bi_persistently PROP) := ne_proper _.

(* Derived logical stuff *)
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  PROP) a : (P  Ψ a)  P   a, Ψ a.
Proof. intros ->; apply exist_intro. Qed.
Lemma forall_elim' {A} P (Ψ : A  PROP) : (P   a, Ψ a)   a, P  Ψ a.
Proof. move=> HP a. by rewrite HP forall_elim. Qed.

Hint Resolve pure_intro forall_intro.
Hint Resolve or_elim or_intro_l' or_intro_r'.
Hint Resolve and_intro and_elim_l' and_elim_r'.

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 P Q R : (P  Q  R)  (P  Q)  P  R.
Proof. intros. rewrite -(impl_elim_l' P Q R); 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_elim_l P Q : (P  Q)  P  Q.
Proof. by apply impl_elim_l'. Qed.
Lemma impl_elim_r P Q : P  (P  Q)  Q.
Proof. by apply impl_elim_r'. Qed.

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.
Hint Immediate False_elim.

116
117
118
119
120
121
122
123
124
Lemma entails_eq_True P Q : (P  Q)  ((P  Q)%I  True%I).
Proof.
  split=>EQ.
  - apply bi.equiv_spec; split; [by apply True_intro|].
    apply impl_intro_r. rewrite and_elim_r //.
  - trans (P  True)%I.
    + apply and_intro; first done. by apply pure_intro.
    + rewrite -EQ impl_elim_r. done.
Qed.
125
Lemma entails_impl_True P Q : (P  Q)  (True  (P  Q)).
Robbert Krebbers's avatar
Robbert Krebbers committed
126
Proof. rewrite entails_eq_True equiv_spec; naive_solver. Qed.
127

Robbert Krebbers's avatar
Robbert Krebbers committed
128
129
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
166
167
168
169
170
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
207
208
209
210
211
212
213
214
215
216
217
218
219
220
221
222
223
224
225
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  PROP) :
  ( 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  PROP) :
  ( 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 (() ==> () ==> ()) (@bi_and PROP).
Proof. by intros P P' HP Q Q' HQ; apply and_mono. Qed.
Global Instance and_flip_mono' :
  Proper (flip () ==> flip () ==> flip ()) (@bi_and PROP).
Proof. by intros P P' HP Q Q' HQ; apply and_mono. Qed.
Global Instance or_mono' : Proper (() ==> () ==> ()) (@bi_or PROP).
Proof. by intros P P' HP Q Q' HQ; apply or_mono. Qed.
Global Instance or_flip_mono' :
  Proper (flip () ==> flip () ==> flip ()) (@bi_or PROP).
Proof. by intros P P' HP Q Q' HQ; apply or_mono. Qed.
Global Instance impl_mono' :
  Proper (flip () ==> () ==> ()) (@bi_impl PROP).
Proof. by intros P P' HP Q Q' HQ; apply impl_mono. Qed.
Global Instance impl_flip_mono' :
  Proper (() ==> flip () ==> flip ()) (@bi_impl PROP).
Proof. by intros P P' HP Q Q' HQ; apply impl_mono. Qed.
Global Instance forall_mono' A :
  Proper (pointwise_relation _ () ==> ()) (@bi_forall PROP A).
Proof. intros P1 P2; apply forall_mono. Qed.
Global Instance forall_flip_mono' A :
  Proper (pointwise_relation _ (flip ()) ==> flip ()) (@bi_forall PROP A).
Proof. intros P1 P2; apply forall_mono. Qed.
Global Instance exist_mono' A :
  Proper (pointwise_relation _ (()) ==> ()) (@bi_exist PROP A).
Proof. intros P1 P2; apply exist_mono. Qed.
Global Instance exist_flip_mono' A :
  Proper (pointwise_relation _ (flip ()) ==> flip ()) (@bi_exist PROP A).
Proof. intros P1 P2; apply exist_mono. Qed.

Global Instance and_idem : IdemP () (@bi_and PROP).
Proof. intros P; apply (anti_symm ()); auto. Qed.
Global Instance or_idem : IdemP () (@bi_or PROP).
Proof. intros P; apply (anti_symm ()); auto. Qed.
Global Instance and_comm : Comm () (@bi_and PROP).
Proof. intros P Q; apply (anti_symm ()); auto. Qed.
Global Instance True_and : LeftId () True%I (@bi_and PROP).
Proof. intros P; apply (anti_symm ()); auto. Qed.
Global Instance and_True : RightId () True%I (@bi_and PROP).
Proof. intros P; apply (anti_symm ()); auto. Qed.
Global Instance False_and : LeftAbsorb () False%I (@bi_and PROP).
Proof. intros P; apply (anti_symm ()); auto. Qed.
Global Instance and_False : RightAbsorb () False%I (@bi_and PROP).
Proof. intros P; apply (anti_symm ()); auto. Qed.
Global Instance True_or : LeftAbsorb () True%I (@bi_or PROP).
Proof. intros P; apply (anti_symm ()); auto. Qed.
Global Instance or_True : RightAbsorb () True%I (@bi_or PROP).
Proof. intros P; apply (anti_symm ()); auto. Qed.
Global Instance False_or : LeftId () False%I (@bi_or PROP).
Proof. intros P; apply (anti_symm ()); auto. Qed.
Global Instance or_False : RightId () False%I (@bi_or PROP).
Proof. intros P; apply (anti_symm ()); auto. Qed.
Global Instance and_assoc : Assoc () (@bi_and PROP).
Proof. intros P Q R; apply (anti_symm ()); auto. Qed.
Global Instance or_comm : Comm () (@bi_or PROP).
Proof. intros P Q; apply (anti_symm ()); auto. Qed.
Global Instance or_assoc : Assoc () (@bi_or PROP).
Proof. intros P Q R; apply (anti_symm ()); auto. Qed.
Global Instance True_impl : LeftId () True%I (@bi_impl PROP).
Proof.
  intros P; apply (anti_symm ()).
  - by rewrite -(left_id True%I ()%I (_  _)%I) impl_elim_r.
  - by apply impl_intro_l; rewrite left_id.
Qed.

Lemma False_impl P : (False  P)  True.
Proof.
  apply (anti_symm ()); [by auto|].
  apply impl_intro_l. rewrite left_absorb. auto.
Qed.

Jacques-Henri Jourdan's avatar
Typo.    
Jacques-Henri Jourdan committed
226
Lemma exist_impl_forall {A} P (Ψ : A  PROP) :
Robbert Krebbers's avatar
Robbert Krebbers committed
227
228
229
230
231
232
233
  (( 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.
234
235
236
237
238
239
240
241
242
243
244
245
246
247
Lemma forall_unit (Ψ : unit  PROP) :
  ( x, Ψ x)  Ψ ().
Proof.
  apply (anti_symm ()).
  - rewrite (forall_elim ()) //.
  - apply forall_intro=>[[]]. done.
Qed.
Lemma exist_unit (Ψ : unit  PROP) :
  ( x, Ψ x)  Ψ ().
Proof.
  apply (anti_symm ()).
  - apply exist_elim=>[[]]. done.
  - rewrite -(exist_intro ()). done.
Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
248
249
250
251
252
253
254
255
256
257
258
259
260
261
262
263
264
265
266
267
268
269
270
271
272
273
274
275
276
277
278
279
280
281
282
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
313
314
315
316
317
318
319
320
321
322
323
324
325
326
327
328
329
330
331
332
333
334
335
336
337
338
339
340
341
342
343
344
345
346
347
348

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  PROP) : 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  PROP) : ( a, Φ a)  P   a, Φ a  P.
Proof.
  rewrite -(comm _ P) and_exist_l. apply exist_proper=>a. by rewrite comm.
Qed.
Lemma or_exist {A} (Φ Ψ : A  PROP) :
  ( 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.

Lemma and_alt P Q : P  Q   b : bool, if b then P else Q.
Proof.
   apply (anti_symm _); first apply forall_intro=> -[]; auto.
   by apply and_intro; [rewrite (forall_elim true)|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.
  by apply or_elim; [rewrite -(exist_intro true)|rewrite -(exist_intro false)].
Qed.

Lemma entails_equiv_and P Q : (P  Q  P)  (P  Q).
Proof. split. by intros ->; auto. intros; apply (anti_symm _); auto. Qed.

Global Instance iff_ne : NonExpansive2 (@bi_iff PROP).
Proof. unfold bi_iff; solve_proper. Qed.
Global Instance iff_proper :
  Proper (() ==> () ==> ()) (@bi_iff PROP) := ne_proper_2 _.

Lemma iff_refl Q P : Q  P  P.
Proof. rewrite /bi_iff; apply and_intro; apply impl_intro_l; auto. Qed.


(* BI Stuff *)
Hint Resolve sep_mono.
Lemma sep_mono_l P P' Q : (P  Q)  P  P'  Q  P'.
Proof. by intros; apply sep_mono. Qed.
Lemma sep_mono_r P P' Q' : (P'  Q')  P  P'  P  Q'.
Proof. by apply sep_mono. Qed.
Global Instance sep_mono' : Proper (() ==> () ==> ()) (@bi_sep PROP).
Proof. by intros P P' HP Q Q' HQ; apply sep_mono. Qed.
Global Instance sep_flip_mono' :
  Proper (flip () ==> flip () ==> flip ()) (@bi_sep PROP).
Proof. by intros P P' HP Q Q' HQ; apply sep_mono. Qed.
Lemma wand_mono P P' Q Q' : (Q  P)  (P'  Q')  (P - P')  Q - Q'.
Proof.
  intros HP HQ; apply wand_intro_r. rewrite HP -HQ. by apply wand_elim_l'.
Qed.
Global Instance wand_mono' : Proper (flip () ==> () ==> ()) (@bi_wand PROP).
Proof. by intros P P' HP Q Q' HQ; apply wand_mono. Qed.
Global Instance wand_flip_mono' :
  Proper (() ==> flip () ==> flip ()) (@bi_wand PROP).
Proof. by intros P P' HP Q Q' HQ; apply wand_mono. Qed.

Global Instance sep_comm : Comm () (@bi_sep PROP).
Proof. intros P Q; apply (anti_symm _); auto using sep_comm'. Qed.
Global Instance sep_assoc : Assoc () (@bi_sep PROP).
Proof.
  intros P Q R; apply (anti_symm _); auto using sep_assoc'.
  by rewrite !(comm _ P) !(comm _ _ R) sep_assoc'.
Qed.
Global Instance emp_sep : LeftId () emp%I (@bi_sep PROP).
Proof. intros P; apply (anti_symm _); auto using emp_sep_1, emp_sep_2. Qed.
Global Instance sep_emp : RightId () emp%I (@bi_sep PROP).
Proof. by intros P; rewrite comm left_id. Qed.

Global Instance sep_False : LeftAbsorb () False%I (@bi_sep PROP).
Proof. intros P; apply (anti_symm _); auto using wand_elim_l'. Qed.
Global Instance False_sep : RightAbsorb () False%I (@bi_sep PROP).
Proof. intros P. by rewrite comm left_absorb. Qed.

Lemma True_sep_2 P : P  True  P.
Proof. rewrite -{1}[P](left_id emp%I bi_sep). auto using sep_mono. Qed.
Lemma sep_True_2 P : P  P  True.
Proof. by rewrite comm -True_sep_2. Qed.

Ralf Jung's avatar
Ralf Jung committed
349
Lemma sep_intro_emp_valid_l P Q R : P  (R  Q)  R  P  Q.
Robbert Krebbers's avatar
Robbert Krebbers committed
350
Proof. intros ? ->. rewrite -{1}(left_id emp%I _ Q). by apply sep_mono. Qed.
Ralf Jung's avatar
Ralf Jung committed
351
352
353
Lemma sep_intro_emp_valid_r P Q R : (R  P)  Q  R  P  Q.
Proof. intros -> ?. rewrite comm. by apply sep_intro_emp_valid_l. Qed.
Lemma sep_elim_emp_valid_l P Q R : P  (P  R  Q)  R  Q.
Robbert Krebbers's avatar
Robbert Krebbers committed
354
Proof. intros <- <-. by rewrite left_id. Qed.
Ralf Jung's avatar
Ralf Jung committed
355
Lemma sep_elim_emp_valid_r P Q R : P  (R  P  Q)  R  Q.
Robbert Krebbers's avatar
Robbert Krebbers committed
356
357
358
359
360
361
362
363
364
365
366
367
368
369
370
371
372
373
374
375
376
377
378
379
380
381
382
383
384
385
386
387
388
389
390
391
392
393
394
395
396
397
398
399
400
401
402
403
404
405
406
407
408
409
410
411
412
413
414
415
416
417
418
419
420
421
422
423
424
425
426
427
428
429
430
431
432
433
434
435
436
437
Proof. intros <- <-. by rewrite right_id. Qed.

Lemma wand_intro_l P Q R : (Q  P  R)  P  Q - R.
Proof. rewrite comm; apply wand_intro_r. Qed.
Lemma wand_elim_l P Q : (P - Q)  P  Q.
Proof. by apply wand_elim_l'. Qed.
Lemma wand_elim_r P Q : P  (P - Q)  Q.
Proof. rewrite (comm _ P); apply wand_elim_l. Qed.
Lemma wand_elim_r' P Q R : (Q  P - R)  P  Q  R.
Proof. intros ->; apply wand_elim_r. Qed.
Lemma wand_apply P Q R S : (P  Q - R)  (S  P  Q)  S  R.
Proof. intros HR%wand_elim_l' HQ. by rewrite HQ. Qed.
Lemma wand_frame_l P Q R : (Q - R)  P  Q - P  R.
Proof. apply wand_intro_l. rewrite -assoc. apply sep_mono_r, wand_elim_r. Qed.
Lemma wand_frame_r P Q R : (Q - R)  Q  P - R  P.
Proof.
  apply wand_intro_l. rewrite ![(_  P)%I]comm -assoc.
  apply sep_mono_r, wand_elim_r.
Qed.

Lemma emp_wand P : (emp - P)  P.
Proof.
  apply (anti_symm _).
  - by rewrite -[(emp - P)%I]left_id wand_elim_r.
  - apply wand_intro_l. by rewrite left_id.
Qed.
Lemma False_wand P : (False - P)  True.
Proof.
  apply (anti_symm ()); [by auto|].
  apply wand_intro_l. rewrite left_absorb. auto.
Qed.

Lemma wand_curry P Q R : (P - Q - R)  (P  Q - R).
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.

Lemma sep_and_l P Q R : P  (Q  R)  (P  Q)  (P  R).
Proof. auto. Qed.
Lemma sep_and_r P Q R : (P  Q)  R  (P  R)  (Q  R).
Proof. auto. Qed.
Lemma sep_or_l P Q R : P  (Q  R)  (P  Q)  (P  R).
Proof.
  apply (anti_symm ()); last by eauto 8.
  apply wand_elim_r', or_elim; apply wand_intro_l; auto.
Qed.
Lemma sep_or_r P Q R : (P  Q)  R  (P  R)  (Q  R).
Proof. by rewrite -!(comm _ R) sep_or_l. Qed.
Lemma sep_exist_l {A} P (Ψ : A  PROP) : P  ( a, Ψ a)   a, P  Ψ a.
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.
Lemma sep_exist_r {A} (Φ: A  PROP) Q: ( a, Φ a)  Q   a, Φ a  Q.
Proof. setoid_rewrite (comm _ _ Q); apply sep_exist_l. Qed.
Lemma sep_forall_l {A} P (Ψ : A  PROP) : P  ( a, Ψ a)   a, P  Ψ a.
Proof. by apply forall_intro=> a; rewrite forall_elim. Qed.
Lemma sep_forall_r {A} (Φ : A  PROP) Q : ( a, Φ a)  Q   a, Φ a  Q.
Proof. by apply forall_intro=> a; rewrite forall_elim. Qed.

Global Instance wand_iff_ne : NonExpansive2 (@bi_wand_iff PROP).
Proof. solve_proper. Qed.
Global Instance wand_iff_proper :
  Proper (() ==> () ==> ()) (@bi_wand_iff PROP) := ne_proper_2 _.

Lemma wand_iff_refl P : emp  P - P.
Proof. apply and_intro; apply wand_intro_l; by rewrite right_id. Qed.

Lemma wand_entails P Q : (P - Q)%I  P  Q.
Proof. intros. rewrite -[P]left_id. by apply wand_elim_l'. Qed.
Lemma entails_wand P Q : (P  Q)  (P - Q)%I.
Proof. intros ->. apply wand_intro_r. by rewrite left_id. Qed.

Lemma equiv_wand_iff P Q : (P  Q)  (P - Q)%I.
Proof. intros ->; apply wand_iff_refl. Qed.
Lemma wand_iff_equiv P Q : (P - Q)%I  (P  Q).
Proof.
  intros HPQ; apply (anti_symm ());
Ralf Jung's avatar
Ralf Jung committed
438
    apply wand_entails; rewrite /bi_emp_valid HPQ /bi_wand_iff; auto.
Robbert Krebbers's avatar
Robbert Krebbers committed
439
440
441
442
443
444
445
446
447
448
449
450
Qed.

Lemma entails_impl P Q : (P  Q)  (P  Q)%I.
Proof. intros ->. apply impl_intro_l. auto. Qed.
Lemma impl_entails P Q `{!Affine P} : (P  Q)%I  P  Q.
Proof. intros HPQ. apply impl_elim with P=>//. by rewrite {1}(affine P). Qed.

Lemma equiv_iff P Q : (P  Q)  (P  Q)%I.
Proof. intros ->; apply iff_refl. Qed.
Lemma iff_equiv P Q `{!Affine P, !Affine Q} : (P  Q)%I  (P  Q).
Proof.
  intros HPQ; apply (anti_symm ());
Ralf Jung's avatar
Ralf Jung committed
451
    apply: impl_entails; rewrite /bi_emp_valid HPQ /bi_iff; auto.
Robbert Krebbers's avatar
Robbert Krebbers committed
452
453
Qed.

454
455
456
457
458
459
460
461
Lemma and_parallel P1 P2 Q1 Q2 :
  (P1  P2) - ((P1 - Q1)  (P2 - Q2)) - Q1  Q2.
Proof.
  apply wand_intro_r, and_intro.
  - rewrite !and_elim_l wand_elim_r. done.
  - rewrite !and_elim_r wand_elim_r. done.
Qed.

Robbert Krebbers's avatar
Robbert Krebbers committed
462
463
464
465
466
467
468
469
470
471
472
473
474
475
476
477
478
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
(* Pure stuff *)
Lemma pure_elim φ Q R : (Q  ⌜φ⌝)  (φ  Q  R)  Q  R.
Proof.
  intros HQ HQR. rewrite -(idemp ()%I Q) {1}HQ.
  apply impl_elim_l', pure_elim'=> ?. apply impl_intro_l.
  rewrite and_elim_l; auto.
Qed.
Lemma pure_mono φ1 φ2 : (φ1  φ2)  ⌜φ1  ⌜φ2.
Proof. auto using pure_elim', pure_intro. Qed.
Global Instance pure_mono' : Proper (impl ==> ()) (@bi_pure PROP).
Proof. intros φ1 φ2; apply pure_mono. Qed.
Global Instance pure_flip_mono : Proper (flip impl ==> flip ()) (@bi_pure PROP).
Proof. intros φ1 φ2; apply pure_mono. Qed.
Lemma pure_iff φ1 φ2 : (φ1  φ2)  ⌜φ1  ⌜φ2.
Proof. intros [??]; apply (anti_symm _); auto using pure_mono. Qed.
Lemma pure_elim_l φ Q R : (φ  Q  R)  ⌜φ⌝  Q  R.
Proof. intros; apply pure_elim with φ; eauto. Qed.
Lemma pure_elim_r φ Q R : (φ  Q  R)  Q  ⌜φ⌝  R.
Proof. intros; apply pure_elim with φ; eauto. Qed.

Lemma pure_True (φ : Prop) : φ  ⌜φ⌝  True.
Proof. intros; apply (anti_symm _); auto. Qed.
Lemma pure_False (φ : Prop) : ¬φ  ⌜φ⌝  False.
Proof. intros; apply (anti_symm _); eauto using pure_mono. Qed.

Lemma pure_and φ1 φ2 : ⌜φ1  φ2  ⌜φ1  ⌜φ2.
Proof.
  apply (anti_symm _).
  - apply and_intro; apply pure_mono; tauto.
  - eapply (pure_elim φ1); [auto|]=> ?. rewrite and_elim_r. auto using pure_mono.
Qed.
Lemma pure_or φ1 φ2 : ⌜φ1  φ2  ⌜φ1  ⌜φ2.
Proof.
  apply (anti_symm _).
  - eapply pure_elim=> // -[?|?]; auto using pure_mono.
  - apply or_elim; eauto using pure_mono.
Qed.
Lemma pure_impl φ1 φ2 : ⌜φ1  φ2  (⌜φ1  ⌜φ2).
Proof.
  apply (anti_symm _).
  - apply impl_intro_l. rewrite -pure_and. apply pure_mono. naive_solver.
  - rewrite -pure_forall_2. apply forall_intro=> ?.
    by rewrite -(left_id True bi_and (_→_))%I (pure_True φ1) // impl_elim_r.
Qed.
Lemma pure_forall {A} (φ : A  Prop) :  x, φ x   x, ⌜φ x.
Proof.
  apply (anti_symm _); auto using pure_forall_2.
  apply forall_intro=> x. eauto using pure_mono.
Qed.
Lemma pure_exist {A} (φ : A  Prop) :  x, φ x   x, ⌜φ x.
Proof.
  apply (anti_symm _).
  - eapply pure_elim=> // -[x ?]. rewrite -(exist_intro x); auto using pure_mono.
  - apply exist_elim=> x. eauto using pure_mono.
Qed.

Lemma pure_impl_forall φ P : (⌜φ⌝  P)  ( _ : φ, P).
Proof.
  apply (anti_symm _).
  - apply forall_intro=> ?. by rewrite pure_True // left_id.
  - apply impl_intro_l, pure_elim_l=> Hφ. by rewrite (forall_elim Hφ).
Qed.
Lemma pure_alt φ : ⌜φ⌝   _ : φ, True.
Proof.
  apply (anti_symm _).
  - eapply pure_elim; eauto=> H. rewrite -(exist_intro H); auto.
  - by apply exist_elim, pure_intro.
Qed.
Lemma pure_wand_forall φ P `{!Absorbing P} : (⌜φ⌝ - P)  ( _ : φ, P).
Proof.
  apply (anti_symm _).
  - apply forall_intro=> Hφ.
534
    by rewrite -(left_id emp%I _ (_ - _)%I) (pure_intro φ emp%I) // wand_elim_r.
Robbert Krebbers's avatar
Robbert Krebbers committed
535
  - apply wand_intro_l, wand_elim_l', pure_elim'=> Hφ.
Robbert Krebbers's avatar
Robbert Krebbers committed
536
    apply wand_intro_l. rewrite (forall_elim Hφ) comm. by apply absorbing.
Robbert Krebbers's avatar
Robbert Krebbers committed
537
538
Qed.

539
540
(* Properties of the affinely modality *)
Global Instance affinely_ne : NonExpansive (@bi_affinely PROP).
Robbert Krebbers's avatar
Robbert Krebbers committed
541
Proof. solve_proper. Qed.
542
Global Instance affinely_proper : Proper (() ==> ()) (@bi_affinely PROP).
Robbert Krebbers's avatar
Robbert Krebbers committed
543
Proof. solve_proper. Qed.
544
Global Instance affinely_mono' : Proper (() ==> ()) (@bi_affinely PROP).
Robbert Krebbers's avatar
Robbert Krebbers committed
545
Proof. solve_proper. Qed.
546
547
Global Instance affinely_flip_mono' :
  Proper (flip () ==> flip ()) (@bi_affinely PROP).
Robbert Krebbers's avatar
Robbert Krebbers committed
548
549
Proof. solve_proper. Qed.

550
Lemma affinely_elim_emp P : <affine> P  emp.
551
Proof. rewrite /bi_affinely; auto. Qed.
552
Lemma affinely_elim P : <affine> P  P.
553
Proof. rewrite /bi_affinely; auto. Qed.
554
Lemma affinely_mono P Q : (P  Q)  <affine> P  <affine> Q.
Robbert Krebbers's avatar
Robbert Krebbers committed
555
Proof. by intros ->. Qed.
556
Lemma affinely_idemp P : <affine> <affine> P  <affine> P.
557
Proof. by rewrite /bi_affinely assoc idemp. Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
558

559
Lemma affinely_intro' P Q : (<affine> P  Q)  <affine> P  <affine> Q.
560
Proof. intros <-. by rewrite affinely_idemp. Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
561

562
Lemma affinely_False : <affine> False  False.
563
Proof. by rewrite /bi_affinely right_absorb. Qed.
564
Lemma affinely_emp : <affine> emp  emp.
565
Proof. by rewrite /bi_affinely (idemp bi_and). Qed.
566
Lemma affinely_or P Q : <affine> (P  Q)  <affine> P  <affine> Q.
567
Proof. by rewrite /bi_affinely and_or_l. Qed.
568
Lemma affinely_and P Q : <affine> (P  Q)  <affine> P  <affine> Q.
Robbert Krebbers's avatar
Robbert Krebbers committed
569
Proof.
570
  rewrite /bi_affinely -(comm _ P) (assoc _ (_  _)%I) -!(assoc _ P).
Robbert Krebbers's avatar
Robbert Krebbers committed
571
572
  by rewrite idemp !assoc (comm _ P).
Qed.
573
Lemma affinely_sep_2 P Q : <affine> P  <affine> Q  <affine> (P  Q).
Robbert Krebbers's avatar
Robbert Krebbers committed
574
Proof.
575
  rewrite /bi_affinely. apply and_intro.
576
577
578
  - by rewrite !and_elim_l right_id.
  - by rewrite !and_elim_r.
Qed.
579
Lemma affinely_sep `{BiPositive PROP} P Q :
580
  <affine> (P  Q)  <affine> P  <affine> Q.
581
Proof.
582
  apply (anti_symm _), affinely_sep_2.
583
  by rewrite -{1}affinely_idemp bi_positive !(comm _ (<affine> P)%I) bi_positive.
Robbert Krebbers's avatar
Robbert Krebbers committed
584
Qed.
585
Lemma affinely_forall {A} (Φ : A  PROP) : <affine> ( a, Φ a)   a, <affine> (Φ a).
Robbert Krebbers's avatar
Robbert Krebbers committed
586
Proof. apply forall_intro=> a. by rewrite (forall_elim a). Qed.
587
Lemma affinely_exist {A} (Φ : A  PROP) : <affine> ( a, Φ a)   a, <affine> (Φ a).
588
589
Proof. by rewrite /bi_affinely and_exist_l. Qed.

590
Lemma affinely_True_emp : <affine> True  <affine> emp.
591
592
Proof. apply (anti_symm _); rewrite /bi_affinely; auto. Qed.

593
Lemma affinely_and_l P Q : <affine> P  Q  <affine> (P  Q).
594
Proof. by rewrite /bi_affinely assoc. Qed.
595
Lemma affinely_and_r P Q : P  <affine> Q  <affine> (P  Q).
596
Proof. by rewrite /bi_affinely !assoc (comm _ P). Qed.
597
Lemma affinely_and_lr P Q : <affine> P  Q  P  <affine> Q.
598
599
600
601
Proof. by rewrite affinely_and_l affinely_and_r. Qed.

(* Properties of the absorbingly modality *)
Global Instance absorbingly_ne : NonExpansive (@bi_absorbingly PROP).
Robbert Krebbers's avatar
Robbert Krebbers committed
602
Proof. solve_proper. Qed.
603
Global Instance absorbingly_proper : Proper (() ==> ()) (@bi_absorbingly PROP).
Robbert Krebbers's avatar
Robbert Krebbers committed
604
Proof. solve_proper. Qed.
605
Global Instance absorbingly_mono' : Proper (() ==> ()) (@bi_absorbingly PROP).
Robbert Krebbers's avatar
Robbert Krebbers committed
606
Proof. solve_proper. Qed.
607
608
Global Instance absorbingly_flip_mono' :
  Proper (flip () ==> flip ()) (@bi_absorbingly PROP).
Robbert Krebbers's avatar
Robbert Krebbers committed
609
610
Proof. solve_proper. Qed.

611
Lemma absorbingly_intro P : P  <absorb> P.
612
Proof. by rewrite /bi_absorbingly -True_sep_2. Qed.
613
Lemma absorbingly_mono P Q : (P  Q)  <absorb> P  <absorb> Q.
Robbert Krebbers's avatar
Robbert Krebbers committed
614
Proof. by intros ->. Qed.
615
Lemma absorbingly_idemp P : <absorb> <absorb> P  <absorb> P.
Robbert Krebbers's avatar
Robbert Krebbers committed
616
Proof.
617
618
  apply (anti_symm _), absorbingly_intro.
  rewrite /bi_absorbingly assoc. apply sep_mono; auto.
Robbert Krebbers's avatar
Robbert Krebbers committed
619
620
Qed.

621
Lemma absorbingly_pure φ : <absorb>  φ    φ .
Robbert Krebbers's avatar
Robbert Krebbers committed
622
Proof.
623
  apply (anti_symm _), absorbingly_intro.
Robbert Krebbers's avatar
Robbert Krebbers committed
624
625
  apply wand_elim_r', pure_elim'=> ?. apply wand_intro_l; auto.
Qed.
626
Lemma absorbingly_or P Q : <absorb> (P  Q)  <absorb> P  <absorb> Q.
627
Proof. by rewrite /bi_absorbingly sep_or_l. Qed.
628
Lemma absorbingly_and_1 P Q : <absorb> (P  Q)  <absorb> P  <absorb> Q.
629
Proof. apply and_intro; apply absorbingly_mono; auto. Qed.
630
Lemma absorbingly_forall {A} (Φ : A  PROP) : <absorb> ( a, Φ a)   a, <absorb> (Φ a).
Robbert Krebbers's avatar
Robbert Krebbers committed
631
Proof. apply forall_intro=> a. by rewrite (forall_elim a). Qed.
632
Lemma absorbingly_exist {A} (Φ : A  PROP) : <absorb> ( a, Φ a)   a, <absorb> (Φ a).
633
Proof. by rewrite /bi_absorbingly sep_exist_l. Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
634

635
Lemma absorbingly_sep P Q : <absorb> (P  Q)  <absorb> P  <absorb> Q.
636
Proof. by rewrite -{1}absorbingly_idemp /bi_absorbingly !assoc -!(comm _ P) !assoc. Qed.
637
Lemma absorbingly_True_emp : <absorb> True  <absorb> emp.
638
Proof. by rewrite absorbingly_pure /bi_absorbingly right_id. Qed.
639
Lemma absorbingly_wand P Q : <absorb> (P - Q)  <absorb> P - <absorb> Q.
640
Proof. apply wand_intro_l. by rewrite -absorbingly_sep wand_elim_r. Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
641

642
Lemma absorbingly_sep_l P Q : <absorb> P  Q  <absorb> (P  Q).
643
Proof. by rewrite /bi_absorbingly assoc. Qed.
644
Lemma absorbingly_sep_r P Q : P  <absorb> Q  <absorb> (P  Q).
645
Proof. by rewrite /bi_absorbingly !assoc (comm _ P). Qed.
646
Lemma absorbingly_sep_lr P Q : <absorb> P  Q  P  <absorb> Q.
647
Proof. by rewrite absorbingly_sep_l absorbingly_sep_r. Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
648

Ralf Jung's avatar
Ralf Jung committed
649
Lemma affinely_absorbingly_elim `{!BiPositive PROP} P : <affine> <absorb> P  <affine> P.
Robbert Krebbers's avatar
Robbert Krebbers committed
650
Proof.
651
652
  apply (anti_symm _), affinely_mono, absorbingly_intro.
  by rewrite /bi_absorbingly affinely_sep affinely_True_emp affinely_emp left_id.
Robbert Krebbers's avatar
Robbert Krebbers committed
653
654
Qed.

655
(* Affine and absorbing propositions *)
Robbert Krebbers's avatar
Robbert Krebbers committed
656
Global Instance Affine_proper : Proper (() ==> iff) (@Affine PROP).
Robbert Krebbers's avatar
Robbert Krebbers committed
657
Proof. solve_proper. Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
658
659
Global Instance Absorbing_proper : Proper (() ==> iff) (@Absorbing PROP).
Proof. solve_proper. Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
660

661
Lemma affine_affinely P `{!Affine P} : <affine> P  P.
662
Proof. rewrite /bi_affinely. apply (anti_symm _); auto. Qed.
663
Lemma absorbing_absorbingly P `{!Absorbing P} : <absorb> P  P.
664
Proof. by apply (anti_symm _), absorbingly_intro. Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
665

666
Lemma True_affine_all_affine P : Affine (PROP:=PROP) True  Affine P.
Robbert Krebbers's avatar
Robbert Krebbers committed
667
Proof. rewrite /Affine=> <-; auto. Qed.
668
Lemma emp_absorbing_all_absorbing P : Absorbing (PROP:=PROP) emp  Absorbing P.
Robbert Krebbers's avatar
Robbert Krebbers committed
669
670
Proof.
  intros. rewrite /Absorbing -{2}(left_id emp%I _ P).
671
  by rewrite -(absorbing emp) absorbingly_sep_l left_id.
Robbert Krebbers's avatar
Robbert Krebbers committed
672
Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
673
674

Lemma sep_elim_l P Q `{H : TCOr (Affine Q) (Absorbing P)} : P  Q  P.
Robbert Krebbers's avatar
Robbert Krebbers committed
675
676
677
678
679
Proof.
  destruct H.
  - by rewrite (affine Q) right_id.
  - by rewrite (True_intro Q) comm.
Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
680
681
682
Lemma sep_elim_r P Q `{H : TCOr (Affine P) (Absorbing Q)} : P  Q  Q.
Proof. by rewrite comm sep_elim_l. Qed.

Ralf Jung's avatar
Ralf Jung committed
683
684
Lemma sep_and P Q :
  TCOr (Affine P) (Absorbing Q)  TCOr (Absorbing P) (Affine Q) 
Robbert Krebbers's avatar
Robbert Krebbers committed
685
  P  Q  P  Q.
686
Proof.
Ralf Jung's avatar
Ralf Jung committed
687
  intros [?|?] [?|?];
688
689
    apply and_intro; apply: sep_elim_l || apply: sep_elim_r.
Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
690

691
Lemma affinely_intro P Q `{!Affine P} : (P  Q)  P  <affine> Q.
692
Proof. intros <-. by rewrite affine_affinely. Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
693
694
695
696
697
698
699
700
701
702
703

Lemma emp_and P `{!Affine P} : emp  P  P.
Proof. apply (anti_symm _); auto. Qed.
Lemma and_emp P `{!Affine P} : P  emp  P.
Proof. apply (anti_symm _); auto. Qed.
Lemma emp_or P `{!Affine P} : emp  P  emp.
Proof. apply (anti_symm _); auto. Qed.
Lemma or_emp P `{!Affine P} : P  emp  emp.
Proof. apply (anti_symm _); auto. Qed.

Lemma True_sep P `{!Absorbing P} : True  P  P.
Robbert Krebbers's avatar
Robbert Krebbers committed
704
Proof. apply (anti_symm _); auto using True_sep_2. Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
705
Lemma sep_True P `{!Absorbing P} : P  True  P.
Robbert Krebbers's avatar
Robbert Krebbers committed
706
Proof. by rewrite comm True_sep. Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
707

Ralf Jung's avatar
Ralf Jung committed
708
709
710
711
712
713
714
715
716
Lemma True_emp_iff_BiAffine :
  BiAffine PROP  (True  emp).
Proof.
  split.
  - intros ?. exact: affine.
  - rewrite /BiAffine /Affine=>Hemp ?. rewrite -Hemp.
    exact: True_intro.
Qed.

717
718
Section bi_affine.
  Context `{BiAffine PROP}.
Robbert Krebbers's avatar
Robbert Krebbers committed
719

720
  Global Instance bi_affine_absorbing P : Absorbing P | 0.
721
  Proof. by rewrite /Absorbing /bi_absorbingly (affine True%I) left_id. Qed.
722
  Global Instance bi_affine_positive : BiPositive PROP.
723
  Proof. intros P Q. by rewrite !affine_affinely. Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
724
725
726
727
728
729
730
731
732
733
734
735
736
737
738
739
740
741
742
743
744
745
746
747

  Lemma True_emp : True  emp.
  Proof. apply (anti_symm _); auto using affine. Qed.

  Global Instance emp_and' : LeftId () emp%I (@bi_and PROP).
  Proof. intros P. by rewrite -True_emp left_id. Qed.
  Global Instance and_emp' : RightId () emp%I (@bi_and PROP).
  Proof. intros P. by rewrite -True_emp right_id. Qed.

  Global Instance True_sep' : LeftId () True%I (@bi_sep PROP).
  Proof. intros P. by rewrite True_emp left_id. Qed.
  Global Instance sep_True' : RightId () True%I (@bi_sep PROP).
  Proof. intros P. by rewrite True_emp right_id. Qed.

  Lemma impl_wand_1 P Q : (P  Q)  P - Q.
  Proof. apply wand_intro_l. by rewrite sep_and impl_elim_r. Qed.

  Lemma decide_emp φ `{!Decision φ} (P : PROP) :
    (if decide φ then P else emp)  (⌜φ⌝  P).
  Proof.
    destruct (decide _).
    - by rewrite pure_True // True_impl.
    - by rewrite pure_False // False_impl True_emp.
  Qed.
748
End bi_affine.
Robbert Krebbers's avatar
Robbert Krebbers committed
749

750
(* Properties of the persistence modality *)
Robbert Krebbers's avatar
Robbert Krebbers committed
751
752
753
754
755
756
Hint Resolve persistently_mono.
Global Instance persistently_mono' : Proper (() ==> ()) (@bi_persistently PROP).
Proof. intros P Q; apply persistently_mono. Qed.
Global Instance persistently_flip_mono' :
  Proper (flip () ==> flip ()) (@bi_persistently PROP).
Proof. intros P Q; apply persistently_mono. Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
757

Ralf Jung's avatar
Ralf Jung committed
758
Lemma absorbingly_elim_persistently P : <absorb> <pers> P  <pers> P.
Robbert Krebbers's avatar
Robbert Krebbers committed
759
Proof.
760
761
  apply (anti_symm _), absorbingly_intro.
  by rewrite /bi_absorbingly comm persistently_absorbing.
Robbert Krebbers's avatar
Robbert Krebbers committed
762
Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
763

764
Lemma persistently_forall {A} (Ψ : A  PROP) :
765
  <pers> ( a, Ψ a)   a, <pers> (Ψ a).
766
767
768
769
770
Proof.
  apply (anti_symm _); auto using persistently_forall_2.
  apply forall_intro=> x. by rewrite (forall_elim x).
Qed.
Lemma persistently_exist {A} (Ψ : A  PROP) :
771
  <pers> ( a, Ψ a)   a, <pers> (Ψ a).
772
773
774
775
Proof.
  apply (anti_symm _); auto using persistently_exist_1.
  apply exist_elim=> x. by rewrite (exist_intro x).
Qed.
776
Lemma persistently_and P Q : <pers> (P  Q)  <pers> P  <pers> Q.
777
Proof. rewrite !and_alt persistently_forall. by apply forall_proper=> -[]. Qed.
778
Lemma persistently_or P Q : <pers> (P  Q)  <pers> P  <pers> Q.
779
Proof. rewrite !or_alt persistently_exist. by apply exist_proper=> -[]. Qed.
780
Lemma persistently_impl P Q : <pers> (P  Q)  <pers> P  <pers> Q.
781
782
783
784
785
Proof.
  apply impl_intro_l; rewrite -persistently_and.
  apply persistently_mono, impl_elim with P; auto.
Qed.

786
787
788
789
790
Lemma persistently_emp_intro P : P  <pers> emp.
Proof.
  by rewrite -(left_id emp%I bi_sep P) {1}persistently_emp_2 persistently_absorbing.
Qed.

791
Lemma persistently_True_emp : <pers> True  <pers> emp.
792
793
Proof. apply (anti_symm _); auto using persistently_emp_intro. Qed.

794
Lemma persistently_and_emp P : <pers> P  <pers> (emp  P).
795
796
797
798
799
800
Proof.
  apply (anti_symm ()); last by rewrite and_elim_r.
  rewrite persistently_and. apply and_intro; last done.
  apply persistently_emp_intro.
Qed.

801
Lemma persistently_and_sep_elim_emp P Q : <pers> P  Q  (emp  P)  Q.
802
803
804
805
806
Proof.
  rewrite persistently_and_emp.
  apply persistently_and_sep_elim.
Qed.

807
Lemma persistently_and_sep_assoc P Q R : <pers> P  (Q  R)  (<pers> P  Q)  R.
Robbert Krebbers's avatar
Robbert Krebbers committed
808
Proof.
809
  apply (anti_symm ()).
810
  - rewrite {1}persistently_idemp_2 persistently_and_sep_elim_emp assoc.
811
    apply sep_mono_l, and_intro.
812
    + by rewrite and_elim_r persistently_absorbing.
813
814
    + by rewrite and_elim_l left_id.
  - apply and_intro.
815
    + by rewrite and_elim_l persistently_absorbing.
816
    + by rewrite and_elim_r.
Robbert Krebbers's avatar
Robbert Krebbers committed
817
Qed.
818
Lemma persistently_and_emp_elim P : emp  <pers> P  P.
819
Proof. by rewrite comm persistently_and_sep_elim_emp right_id and_elim_r. Qed.
Ralf Jung's avatar
Ralf Jung committed
820
Lemma persistently_into_absorbingly P : <pers> P  <absorb> P.
Robbert Krebbers's avatar
Robbert Krebbers committed
821
Proof.
822
  rewrite -(right_id True%I _ (<pers> _)%I) -{1}(left_id emp%I _ True%I).
Robbert Krebbers's avatar
Robbert Krebbers committed
823
  by rewrite persistently_and_sep_assoc (comm bi_and) persistently_and_emp_elim comm.
Robbert Krebbers's avatar
Robbert Krebbers committed
824
Qed.
825
Lemma persistently_elim P `{!Absorbing P} : <pers> P  P.
Ralf Jung's avatar
Ralf Jung committed
826
Proof. by rewrite persistently_into_absorbingly absorbing_absorbingly. Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
827

828
Lemma persistently_idemp_1 P : <pers> <pers> P  <pers> P.
Ralf Jung's avatar
Ralf Jung committed
829
Proof. by rewrite persistently_into_absorbingly absorbingly_elim_persistently. Qed.
830
Lemma persistently_idemp P : <pers> <pers> P  <pers> P.
831
Proof. apply (anti_symm _); auto using persistently_idemp_1, persistently_idemp_2. Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
832

833
Lemma persistently_intro' P Q : (<pers> P  Q)  <pers> P  <pers> Q.
Robbert Krebbers's avatar
Robbert Krebbers committed
834
835
Proof. intros <-. apply persistently_idemp_2. Qed.

836
Lemma persistently_pure φ : <pers> ⌜φ⌝  ⌜φ⌝.
Robbert Krebbers's avatar
Robbert Krebbers committed
837
Proof.
838
  apply (anti_symm _).
Ralf Jung's avatar
Ralf Jung committed
839
  { by rewrite persistently_into_absorbingly absorbingly_pure. }
840
  apply pure_elim'=> Hφ.
841
  trans ( x : False, <pers> True : PROP)%I; [by apply forall_intro|].
842
  rewrite persistently_forall_2. auto using persistently_mono, pure_intro.
Robbert Krebbers's avatar
Robbert Krebbers committed
843
844
Qed.

845
Lemma persistently_sep_dup P : <pers> P  <pers> P  <pers> P.
Robbert Krebbers's avatar
Robbert Krebbers committed
846
Proof.
847
  apply (anti_symm _).
848
849
  - rewrite -{1}(idemp bi_and (<pers> _)%I).
    by rewrite -{2}(left_id emp%I _ (<pers> _)%I)
850
851
      persistently_and_sep_assoc and_elim_l.
  - by rewrite persistently_absorbing.
Robbert Krebbers's avatar
Robbert Krebbers committed
852
853
Qed.

854
Lemma persistently_and_sep_l_1 P Q : <pers> P  Q  <pers> P  Q.
Robbert Krebbers's avatar
Robbert Krebbers committed
855
856
857
Proof.
  by rewrite -{1}(left_id emp%I _ Q%I) persistently_and_sep_assoc and_elim_l.
Qed.
858
Lemma persistently_and_sep_r_1 P Q : P  <pers> Q  P  <pers> Q.
Robbert Krebbers's avatar
Robbert Krebbers committed
859
860
Proof. by rewrite !(comm _ P) persistently_and_sep_l_1. Qed.

861
Lemma persistently_and_sep P Q : <pers> (P  Q)  <pers> (P  Q).
Robbert Krebbers's avatar
Robbert Krebbers committed
862
Proof.
863
864
865
866
867
  rewrite persistently_and.
  rewrite -{1}persistently_idemp -persistently_and -{1}(left_id emp%I _ Q%I).
  by rewrite persistently_and_sep_assoc (comm bi_and) persistently_and_emp_elim.
Qed.

Ralf Jung's avatar
Ralf Jung committed
868
Lemma persistently_affinely_elim P : <pers> <affine> P  <pers> P.
869
Proof.
870
  by rewrite /bi_affinely persistently_and -persistently_True_emp
871
             persistently_pure left_id.
Robbert Krebbers's avatar
Robbert Krebbers committed
872
873
Qed.

874
Lemma and_sep_persistently P Q : <pers> P  <pers> Q  <pers> P  <pers> Q.
Robbert Krebbers's avatar
Robbert Krebbers committed
875
Proof.
876
877
878
879
  apply (anti_symm _); auto using persistently_and_sep_l_1.
  apply and_intro.
  - by rewrite persistently_absorbing.
  - by rewrite comm persistently_absorbing.
Robbert Krebbers's avatar
Robbert Krebbers committed
880
Qed.
881
Lemma persistently_sep_2 P Q : <pers> P  <pers> Q  <pers> (P  Q).
Robbert Krebbers's avatar
Robbert Krebbers committed
882
Proof. by rewrite -persistently_and_sep persistently_and -and_sep_persistently. Qed.
883
Lemma persistently_sep `{BiPositive PROP} P Q : <pers> (P  Q)  <pers> P  <pers> Q.
884
885
Proof.
  apply (anti_symm _); auto using persistently_sep_2.
Ralf Jung's avatar
Ralf Jung committed
886
  rewrite -persistently_affinely_elim affinely_sep -and_sep_persistently. apply and_intro.
887
888
  - by rewrite (affinely_elim_emp Q) right_id affinely_elim.
  - by rewrite (affinely_elim_emp P) left_id affinely_elim.
889
Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
890

891
892
893
894
895
896
897
898
Lemma persistently_alt_fixpoint P :
  <pers> P  P  <pers> P.
Proof.
  apply (anti_symm _).
  - rewrite -persistently_and_sep_elim. apply and_intro; done.
  - rewrite comm persistently_absorbing. done.
Qed.

899
900
901
Lemma persistently_alt_fixpoint' P :
  <pers> P  <affine> P  <pers> P.
Proof.
Ralf Jung's avatar
Ralf Jung committed
902
903
  rewrite -{1}persistently_affinely_elim {1}persistently_alt_fixpoint
          persistently_affinely_elim //.
904
905
Qed.

906
Lemma persistently_wand P Q : <pers> (P - Q)  <pers> P - <pers> Q.
907
Proof. apply wand_intro_r. by rewrite persistently_sep_2 wand_elim_l. Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
908

909
Lemma persistently_entails_l P Q : (P  <pers> Q)  P  <pers> Q  P.
Robbert Krebbers's avatar
Robbert Krebbers committed
910
Proof. intros; rewrite -persistently_and_sep_l_1; auto. Qed.
911
Lemma persistently_entails_r P Q : (P  <pers> Q)  P  P  <pers> Q.
Robbert Krebbers's avatar
Robbert Krebbers committed