derived_laws.v 70.3 KB
Newer Older
Robbert Krebbers's avatar
Robbert Krebbers committed
1
From iris.algebra Require Import monoid.
2
From iris.bi Require Export extensions.
Ralf Jung's avatar
Ralf Jung committed
3
From iris.prelude Require Import options.
4

Ralf Jung's avatar
Ralf Jung committed
5
(* The sections add [BiAffine] and the like, which is only picked up with [Type*]. *)
6
Set Default Proof Using "Type*".
Robbert Krebbers's avatar
Robbert Krebbers committed
7

Ralf Jung's avatar
Ralf Jung committed
8
9
10
11
12
13
14
(** 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
15
16
Module bi.
Import interface.bi.
17
Section derived.
Robbert Krebbers's avatar
Robbert Krebbers committed
18
19
20
21
22
23
Context {PROP : bi}.
Implicit Types φ : Prop.
Implicit Types P Q R : PROP.
Implicit Types Ps : list PROP.
Implicit Types A : Type.

24
Local Hint Extern 100 (NonExpansive _) => solve_proper : core.
Robbert Krebbers's avatar
Robbert Krebbers committed
25
26

(* Force implicit argument PROP *)
27
28
Notation "P ⊢ Q" := (P @{PROP} Q).
Notation "P ⊣⊢ Q" := (P @{PROP} Q).
Robbert Krebbers's avatar
Robbert Krebbers committed
29
30
31

(* Derived stuff about the entailment *)
Global Instance entails_anti_sym : AntiSymm () (@bi_entails PROP).
32
33
34
35
36
37
38
39
Proof. intros P Q ??. by apply equiv_entails. Qed.
Lemma equiv_entails_1_1 P Q : (P  Q)  (P  Q).
Proof. apply equiv_entails. Qed.
Lemma equiv_entails_1_2 P Q : (P  Q)  (Q  P).
Proof. apply equiv_entails. Qed.
Lemma equiv_entails_2 P Q : (P  Q)  (Q  P)  (P  Q).
Proof. intros. by apply equiv_entails. Qed.

Robbert Krebbers's avatar
Robbert Krebbers committed
40
41
42
Global Instance entails_proper :
  Proper (() ==> () ==> iff) (() : relation PROP).
Proof.
43
  move => P1 P2 /equiv_entails [HP1 HP2] Q1 Q2 /equiv_entails [HQ1 HQ2]; split=>?.
Robbert Krebbers's avatar
Robbert Krebbers committed
44
45
46
47
48
49
50
  - 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
51
Global Instance bi_emp_valid_proper : Proper (() ==> iff) (@bi_emp_valid PROP).
Robbert Krebbers's avatar
Robbert Krebbers committed
52
Proof. solve_proper. Qed.
Ralf Jung's avatar
Ralf Jung committed
53
Global Instance bi_emp_valid_mono : Proper (() ==> impl) (@bi_emp_valid PROP).
Robbert Krebbers's avatar
Robbert Krebbers committed
54
Proof. solve_proper. Qed.
Ralf Jung's avatar
Ralf Jung committed
55
56
Global Instance bi_emp_valid_flip_mono :
  Proper (flip () ==> flip impl) (@bi_emp_valid PROP).
Robbert Krebbers's avatar
Robbert Krebbers committed
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
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.

101
102
103
Local Hint Resolve pure_intro forall_intro : core.
Local Hint Resolve or_elim or_intro_l' or_intro_r' : core.
Local Hint Resolve and_intro and_elim_l' and_elim_r' : core.
Robbert Krebbers's avatar
Robbert Krebbers committed
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119

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.
120
Local Hint Immediate False_elim : core.
Robbert Krebbers's avatar
Robbert Krebbers committed
121

122
123
124
Lemma entails_eq_True P Q : (P  Q)  ((P  Q)%I  True%I).
Proof.
  split=>EQ.
125
  - apply bi.equiv_entails; split; [by apply True_intro|].
126
127
128
129
130
    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.
131
Lemma entails_impl_True P Q : (P  Q)  (True  (P  Q)).
132
Proof. rewrite entails_eq_True equiv_entails; naive_solver. Qed.
133

Robbert Krebbers's avatar
Robbert Krebbers committed
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
226
227
228
229
230
231
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
232
Lemma exist_impl_forall {A} P (Ψ : A  PROP) :
Robbert Krebbers's avatar
Robbert Krebbers committed
233
234
  (( x : A, Ψ x)  P)   x : A, Ψ x  P.
Proof.
235
  apply equiv_entails; split.
Robbert Krebbers's avatar
Robbert Krebbers committed
236
237
238
239
  - 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.
240
241
242
243
244
245
246
247
248
249
250
251
252
253
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
254

255
256
257
258
259
260
261
262
263
264
265
266
267
268
269
270
271
272
273
Lemma exist_exist {A B} (Ψ : A  B  PROP) :
  ( x y, Ψ x y)  ( y x, Ψ x y).
Proof.
  apply (anti_symm ());
    do 2 (apply exist_elim=>?); rewrite -2!exist_intro; eauto.
Qed.
Lemma forall_forall {A B} (Ψ : A  B  PROP) :
  ( x y, Ψ x y)  ( y x, Ψ x y).
Proof.
  apply (anti_symm ());
    do 2 (apply forall_intro=>?); rewrite 2!forall_elim; eauto.
Qed.
Lemma exist_forall {A B} (Ψ : A  B  PROP) :
  ( x,  y, Ψ x y)  ( y,  x, Ψ x y).
Proof.
  apply forall_intro=>?. apply exist_elim=>?.
  rewrite -exist_intro forall_elim ; eauto.
Qed.

Dan Frumin's avatar
Dan Frumin committed
274
275
276
277
278
279
280
Lemma impl_curry P Q R : (P  Q  R)  (P  Q  R).
Proof.
  apply (anti_symm _).
  - apply impl_intro_l. by rewrite (comm _ P) -and_assoc !impl_elim_r.
  - do 2 apply impl_intro_l. by rewrite assoc (comm _ Q) impl_elim_r.
Qed.

Robbert Krebbers's avatar
Robbert Krebbers committed
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
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).
327
328
329
330
331
Proof.
  split.
  - intros ->; auto.
  - intros; apply (anti_symm _); auto.
Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
332
333
334
335
336
337
338
339

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.
340
341
342
343
344
Lemma iff_sym P Q : (P  Q)  (Q  P).
Proof.
  apply equiv_entails. split; apply and_intro;
    try apply and_elim_r; apply and_elim_l.
Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
345
346
347


(* BI Stuff *)
348
Local Hint Resolve sep_mono : core.
Robbert Krebbers's avatar
Robbert Krebbers committed
349
350
351
352
353
354
355
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
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.

Gregory Malecha's avatar
Gregory Malecha committed
390
Lemma sep_intro_emp_valid_l P Q R : ( P)  (R  Q)  R  P  Q.
Robbert Krebbers's avatar
Robbert Krebbers committed
391
Proof. intros ? ->. rewrite -{1}(left_id emp%I _ Q). by apply sep_mono. Qed.
Gregory Malecha's avatar
Gregory Malecha committed
392
Lemma sep_intro_emp_valid_r P Q R : (R  P)  ( Q)  R  P  Q.
Ralf Jung's avatar
Ralf Jung committed
393
Proof. intros -> ?. rewrite comm. by apply sep_intro_emp_valid_l. Qed.
Gregory Malecha's avatar
Gregory Malecha committed
394
Lemma sep_elim_emp_valid_l P Q R : ( P)  (P  R  Q)  R  Q.
Robbert Krebbers's avatar
Robbert Krebbers committed
395
Proof. intros <- <-. by rewrite left_id. Qed.
Gregory Malecha's avatar
Gregory Malecha committed
396
Lemma sep_elim_emp_valid_r P Q R : (P)  (R  P  Q)  R  Q.
Robbert Krebbers's avatar
Robbert Krebbers committed
397
398
399
400
401
402
403
404
405
406
407
408
409
410
411
412
413
414
415
416
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.

417
Global Instance emp_wand : LeftId () emp%I (@bi_wand PROP).
Robbert Krebbers's avatar
Robbert Krebbers committed
418
Proof.
419
  intros P. apply (anti_symm _).
Robbert Krebbers's avatar
Robbert Krebbers committed
420
421
422
  - by rewrite -[(emp - P)%I]left_id wand_elim_r.
  - apply wand_intro_l. by rewrite left_id.
Qed.
423

Robbert Krebbers's avatar
Robbert Krebbers committed
424
425
426
427
428
429
Lemma False_wand P : (False - P)  True.
Proof.
  apply (anti_symm ()); [by auto|].
  apply wand_intro_l. rewrite left_absorb. auto.
Qed.

430
431
432
Lemma wand_trans P Q R : (P - Q)  (Q - R)  (P - R).
Proof. apply wand_intro_l. by rewrite assoc !wand_elim_r. Qed.

Robbert Krebbers's avatar
Robbert Krebbers committed
433
434
435
436
437
438
439
440
441
442
443
444
445
446
447
448
449
450
451
452
453
454
455
456
457
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.
458
Lemma sep_exist_r {A} (Φ: A  PROP) Q: ( a, Φ a)  Q   a, Φ a  Q.
Robbert Krebbers's avatar
Robbert Krebbers committed
459
460
461
462
463
464
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.

465
466
467
Lemma exist_wand_forall {A} P (Ψ : A  PROP) :
  (( x : A, Ψ x) - P)   x : A, Ψ x - P.
Proof.
468
  apply equiv_entails; split.
469
470
471
472
473
  - apply forall_intro=>x. by rewrite -exist_intro.
  - apply wand_intro_r, wand_elim_r', exist_elim=>x.
    apply wand_intro_r. by rewrite (forall_elim x) wand_elim_r.
Qed.

Robbert Krebbers's avatar
Robbert Krebbers committed
474
475
476
477
478
479
480
481
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.

Gregory Malecha's avatar
Gregory Malecha committed
482
Lemma wand_entails P Q : ( P - Q)  P  Q.
483
Proof. intros. rewrite -[P]emp_sep. by apply wand_elim_l'. Qed.
Gregory Malecha's avatar
Gregory Malecha committed
484
Lemma entails_wand P Q : (P  Q)   P - Q.
Robbert Krebbers's avatar
Robbert Krebbers committed
485
Proof. intros ->. apply wand_intro_r. by rewrite left_id. Qed.
486
487
488
(* A version that works with rewrite, in which bi_emp_valid is unfolded. *)
Lemma entails_wand' P Q : (P  Q)  emp  (P - Q).
Proof. apply entails_wand. Qed.
489
490
Lemma wand_entails' P Q : (emp  (P - Q))  P  Q.
Proof. apply wand_entails. Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
491

Gregory Malecha's avatar
Gregory Malecha committed
492
Lemma equiv_wand_iff P Q : (P  Q)   P - Q.
Robbert Krebbers's avatar
Robbert Krebbers committed
493
Proof. intros ->; apply wand_iff_refl. Qed.
Gregory Malecha's avatar
Gregory Malecha committed
494
Lemma wand_iff_equiv P Q : ( P - Q)  (P  Q).
Robbert Krebbers's avatar
Robbert Krebbers committed
495
496
Proof.
  intros HPQ; apply (anti_symm ());
Ralf Jung's avatar
Ralf Jung committed
497
    apply wand_entails; rewrite /bi_emp_valid HPQ /bi_wand_iff; auto.
Robbert Krebbers's avatar
Robbert Krebbers committed
498
Qed.
499
500
501
502
503
504
Lemma wand_iff_sym P Q :
  (P - Q)  (Q - P).
Proof.
  apply equiv_entails; split; apply and_intro;
    try apply and_elim_r; apply and_elim_l.
Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
505

Gregory Malecha's avatar
Gregory Malecha committed
506
Lemma entails_impl P Q : (P  Q)  ( P  Q).
Robbert Krebbers's avatar
Robbert Krebbers committed
507
Proof. intros ->. apply impl_intro_l. auto. Qed.
Gregory Malecha's avatar
Gregory Malecha committed
508
Lemma impl_entails P Q `{!Affine P} : ( P  Q)  P  Q.
Robbert Krebbers's avatar
Robbert Krebbers committed
509
510
Proof. intros HPQ. apply impl_elim with P=>//. by rewrite {1}(affine P). Qed.

Gregory Malecha's avatar
Gregory Malecha committed
511
Lemma equiv_iff P Q : (P  Q)  ( P  Q).
Robbert Krebbers's avatar
Robbert Krebbers committed
512
Proof. intros ->; apply iff_refl. Qed.
Gregory Malecha's avatar
Gregory Malecha committed
513
Lemma iff_equiv P Q `{!Affine P, !Affine Q} : ( P  Q)%I  (P  Q).
Robbert Krebbers's avatar
Robbert Krebbers committed
514
515
Proof.
  intros HPQ; apply (anti_symm ());
Ralf Jung's avatar
Ralf Jung committed
516
    apply: impl_entails; rewrite /bi_emp_valid HPQ /bi_iff; auto.
Robbert Krebbers's avatar
Robbert Krebbers committed
517
518
Qed.

519
520
521
522
523
524
525
526
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.

527
528
529
530
Lemma wandM_sound (mP : option PROP) Q :
  (mP -? Q)  (default emp mP - Q).
Proof. destruct mP; simpl; first done. rewrite emp_wand //. Qed.

Robbert Krebbers's avatar
Robbert Krebbers committed
531
532
533
534
535
536
537
538
539
540
541
542
543
544
545
546
547
548
549
550
551
552
553
554
555
556
557
558
559
560
561
562
563
564
565
566
567
(* 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.
568
569
570
571
572
573
574
575
576
577
578
579
580
581
Lemma pure_impl_1 φ1 φ2 : ⌜φ1  φ2  (⌜φ1  ⌜φ2).
Proof. apply impl_intro_l. rewrite -pure_and. apply pure_mono. naive_solver. Qed.
Lemma pure_impl_2 `{!BiPureForall PROP} φ1 φ2 : (⌜φ1  ⌜φ2)  ⌜φ1  φ2.
Proof.
  rewrite -pure_forall_2. apply forall_intro=> ?.
  by rewrite -(left_id True bi_and (_→_))%I (pure_True φ1) // impl_elim_r.
Qed.
Lemma pure_impl `{!BiPureForall PROP} φ1 φ2 : ⌜φ1  φ2  (⌜φ1  ⌜φ2).
Proof. apply (anti_symm _); auto using pure_impl_1, pure_impl_2. Qed.
Lemma pure_forall_1 {A} (φ : A  Prop) :  x, φ x   x, ⌜φ x.
Proof. apply forall_intro=> x. eauto using pure_mono. Qed.
Lemma pure_forall `{!BiPureForall PROP} {A} (φ : A  Prop) :
   x, φ x   x, ⌜φ x.
Proof. apply (anti_symm _); auto using pure_forall_1, pure_forall_2. Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
582
583
584
585
586
587
588
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.

589
590
591
592
593
594
595
Lemma bi_pure_forall_em : ( φ : Prop, φ  ¬φ)  BiPureForall PROP.
Proof.
  intros Hem A φ. destruct (Hem ( a, ¬φ a)) as [[a Hφ]|Hφ].
  { rewrite (forall_elim a). by apply pure_elim'. }
  apply pure_intro=> a. destruct (Hem (φ a)); naive_solver.
Qed.

Robbert Krebbers's avatar
Robbert Krebbers committed
596
597
598
599
600
601
602
603
604
605
606
607
608
609
610
611
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φ.
612
    rewrite -(pure_intro φ emp) // emp_wand //.
Robbert Krebbers's avatar
Robbert Krebbers committed
613
  - apply wand_intro_l, wand_elim_l', pure_elim'=> Hφ.
Robbert Krebbers's avatar
Robbert Krebbers committed
614
    apply wand_intro_l. rewrite (forall_elim Hφ) comm. by apply absorbing.
Robbert Krebbers's avatar
Robbert Krebbers committed
615
Qed.
Michael Sammler's avatar
Michael Sammler committed
616
617
618
619
620
621
622
Lemma decide_bi_True φ `{!Decision φ} (P : PROP) :
  (if decide φ then P else True)  (⌜φ⌝  P).
Proof.
  destruct (decide _).
  - by rewrite pure_True // True_impl.
  - by rewrite (pure_False φ) // False_impl.
Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
623

624
625
(* Properties of the affinely modality *)
Global Instance affinely_ne : NonExpansive (@bi_affinely PROP).
Robbert Krebbers's avatar
Robbert Krebbers committed
626
Proof. solve_proper. Qed.
627
Global Instance affinely_proper : Proper (() ==> ()) (@bi_affinely PROP).
Robbert Krebbers's avatar
Robbert Krebbers committed
628
Proof. solve_proper. Qed.
629
Global Instance affinely_mono' : Proper (() ==> ()) (@bi_affinely PROP).
Robbert Krebbers's avatar
Robbert Krebbers committed
630
Proof. solve_proper. Qed.
631
632
Global Instance affinely_flip_mono' :
  Proper (flip () ==> flip ()) (@bi_affinely PROP).
Robbert Krebbers's avatar
Robbert Krebbers committed
633
634
Proof. solve_proper. Qed.

635
Lemma affinely_elim_emp P : <affine> P  emp.
636
Proof. rewrite /bi_affinely; auto. Qed.
637
Lemma affinely_elim P : <affine> P  P.
638
Proof. rewrite /bi_affinely; auto. Qed.
639
Lemma affinely_mono P Q : (P  Q)  <affine> P  <affine> Q.
Robbert Krebbers's avatar
Robbert Krebbers committed
640
Proof. by intros ->. Qed.
641
Lemma affinely_idemp P : <affine> <affine> P  <affine> P.
642
Proof. by rewrite /bi_affinely assoc idemp. Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
643

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

647
Lemma affinely_False : <affine> False  False.
648
Proof. by rewrite /bi_affinely right_absorb. Qed.
649
Lemma affinely_emp : <affine> emp  emp.
650
Proof. by rewrite /bi_affinely (idemp bi_and). Qed.
651
Lemma affinely_or P Q : <affine> (P  Q)  <affine> P  <affine> Q.
652
Proof. by rewrite /bi_affinely and_or_l. Qed.
653
Lemma affinely_and P Q : <affine> (P  Q)  <affine> P  <affine> Q.
Robbert Krebbers's avatar
Robbert Krebbers committed
654
Proof.
655
  rewrite /bi_affinely -(comm _ P) (assoc _ (_  _)%I) -!(assoc _ P).
Robbert Krebbers's avatar
Robbert Krebbers committed
656
657
  by rewrite idemp !assoc (comm _ P).
Qed.
658
Lemma affinely_sep_2 P Q : <affine> P  <affine> Q  <affine> (P  Q).
Robbert Krebbers's avatar
Robbert Krebbers committed
659
Proof.
660
  rewrite /bi_affinely. apply and_intro.
661
662
663
  - by rewrite !and_elim_l right_id.
  - by rewrite !and_elim_r.
Qed.
664
Lemma affinely_sep `{BiPositive PROP} P Q :
665
  <affine> (P  Q)  <affine> P  <affine> Q.
666
Proof.
667
  apply (anti_symm _), affinely_sep_2.
668
  by rewrite -{1}affinely_idemp bi_positive !(comm _ (<affine> P)%I) bi_positive.
Robbert Krebbers's avatar
Robbert Krebbers committed
669
Qed.
670
Lemma affinely_forall {A} (Φ : A  PROP) : <affine> ( a, Φ a)   a, <affine> (Φ a).
Robbert Krebbers's avatar
Robbert Krebbers committed
671
Proof. apply forall_intro=> a. by rewrite (forall_elim a). Qed.
672
Lemma affinely_exist {A} (Φ : A  PROP) : <affine> ( a, Φ a)   a, <affine> (Φ a).
673
674
Proof. by rewrite /bi_affinely and_exist_l. Qed.

675
Lemma affinely_True_emp : <affine> True  emp.
676
677
Proof. apply (anti_symm _); rewrite /bi_affinely; auto. Qed.

678
Lemma affinely_and_l P Q : <affine> P  Q  <affine> (P  Q).
679
Proof. by rewrite /bi_affinely assoc. Qed.
680
Lemma affinely_and_r P Q : P  <affine> Q  <affine> (P  Q).
681
Proof. by rewrite /bi_affinely !assoc (comm _ P). Qed.
682
Lemma affinely_and_lr P Q : <affine> P  Q  P  <affine> Q.
683
684
685
686
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
687
Proof. solve_proper. Qed.
688
Global Instance absorbingly_proper : Proper (() ==> ()) (@bi_absorbingly PROP).
Robbert Krebbers's avatar
Robbert Krebbers committed
689
Proof. solve_proper. Qed.
690
Global Instance absorbingly_mono' : Proper (() ==> ()) (@bi_absorbingly PROP).
Robbert Krebbers's avatar
Robbert Krebbers committed
691
Proof. solve_proper. Qed.
692
693
Global Instance absorbingly_flip_mono' :
  Proper (flip () ==> flip ()) (@bi_absorbingly PROP).
Robbert Krebbers's avatar
Robbert Krebbers committed
694
695
Proof. solve_proper. Qed.

696
Lemma absorbingly_intro P : P  <absorb> P.
697
Proof. by rewrite /bi_absorbingly -True_sep_2. Qed.
698
Lemma absorbingly_mono P Q : (P  Q)  <absorb> P  <absorb> Q.
Robbert Krebbers's avatar
Robbert Krebbers committed
699
Proof. by intros ->. Qed.
700
Lemma absorbingly_idemp P : <absorb> <absorb> P  <absorb> P.
Robbert Krebbers's avatar
Robbert Krebbers committed
701
Proof.
702
703
  apply (anti_symm _), absorbingly_intro.
  rewrite /bi_absorbingly assoc. apply sep_mono; auto.
Robbert Krebbers's avatar
Robbert Krebbers committed
704
705
Qed.

706
Lemma absorbingly_pure φ : <absorb>  φ    φ .
Robbert Krebbers's avatar
Robbert Krebbers committed
707
Proof.
708
  apply (anti_symm _), absorbingly_intro.
Robbert Krebbers's avatar
Robbert Krebbers committed
709
710
  apply wand_elim_r', pure_elim'=> ?. apply wand_intro_l; auto.
Qed.
711
712
Lemma absorbingly_True : <absorb> True  True.
Proof. apply absorbingly_pure. Qed.
713
Lemma absorbingly_or P Q : <absorb> (P  Q)  <absorb> P  <absorb> Q.
714
Proof. by rewrite /bi_absorbingly sep_or_l. Qed.
715
Lemma absorbingly_and_1 P Q : <absorb> (P  Q)  <absorb> P  <absorb> Q.
716
Proof. apply and_intro; apply absorbingly_mono; auto. Qed.
717
Lemma absorbingly_forall {A} (Φ : A  PROP) : <absorb> ( a, Φ a)   a, <absorb> (Φ a).
Robbert Krebbers's avatar
Robbert Krebbers committed
718
Proof. apply forall_intro=> a. by rewrite (forall_elim a). Qed.
719
Lemma absorbingly_exist {A} (Φ : A  PROP) : <absorb> ( a, Φ a)   a, <absorb> (Φ a).
720
Proof. by rewrite /bi_absorbingly sep_exist_l. Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
721

722
Lemma absorbingly_sep P Q : <absorb> (P  Q)  <absorb> P  <absorb> Q.
723
Proof. by rewrite -{1}absorbingly_idemp /bi_absorbingly !assoc -!(comm _ P) !assoc. Qed.
724
725
Lemma absorbingly_emp_True : <absorb> emp  True.
Proof. rewrite /bi_absorbingly right_id //. Qed.
726
Lemma absorbingly_wand P Q : <absorb> (P - Q)  <absorb> P - <absorb> Q.
727
Proof. apply wand_intro_l. by rewrite -absorbingly_sep wand_elim_r. Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
728

729
Lemma absorbingly_sep_l P Q : <absorb> P  Q  <absorb> (P  Q).
730
Proof. by rewrite /bi_absorbingly assoc. Qed.
731
Lemma absorbingly_sep_r P Q : P  <absorb> Q  <absorb> (P  Q).
732
Proof. by rewrite /bi_absorbingly !assoc (comm _ P). Qed.
733
Lemma absorbingly_sep_lr P Q : <absorb> P  Q  P  <absorb> Q.
734
Proof. by rewrite absorbingly_sep_l absorbingly_sep_r. Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
735

Ralf Jung's avatar
Ralf Jung committed
736
Lemma affinely_absorbingly_elim `{!BiPositive PROP} P : <affine> <absorb> P  <affine> P.
Robbert Krebbers's avatar
Robbert Krebbers committed
737
Proof.
738
  apply (anti_symm _), affinely_mono, absorbingly_intro.
739
  by rewrite /bi_absorbingly affinely_sep affinely_True_emp left_id.
Robbert Krebbers's avatar
Robbert Krebbers committed
740
741
Qed.

742
(* Affine and absorbing propositions *)
Robbert Krebbers's avatar
Robbert Krebbers committed
743
Global Instance Affine_proper : Proper (() ==> iff) (@Affine PROP).
Robbert Krebbers's avatar
Robbert Krebbers committed
744
Proof. solve_proper. Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
745
746
Global Instance Absorbing_proper : Proper (() ==> iff) (@Absorbing PROP).
Proof. solve_proper. Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
747

748
Lemma affine_affinely P `{!Affine P} : <affine> P  P.
749
Proof. rewrite /bi_affinely. apply (anti_symm _); auto. Qed.
750
Lemma absorbing_absorbingly P `{!Absorbing P} : <absorb> P  P.
751
Proof. by apply (anti_symm _), absorbingly_intro. Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
752

753
Lemma True_affine_all_affine P : Affine (PROP:=PROP) True  Affine P.
Robbert Krebbers's avatar
Robbert Krebbers committed
754
Proof. rewrite /Affine=> <-; auto. Qed.
755
Lemma emp_absorbing_all_absorbing P : Absorbing (PROP:=PROP) emp  Absorbing P.
Robbert Krebbers's avatar
Robbert Krebbers committed
756
Proof.
757
758
  intros. rewrite /Absorbing -{2}(emp_sep P).
  rewrite -(absorbing emp) absorbingly_sep_l left_id //.
Robbert Krebbers's avatar
Robbert Krebbers committed
759
Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
760

761
Lemma sep_elim_l P Q `{HQP : TCOr (Affine Q) (Absorbing P)} : P  Q  P.
Robbert Krebbers's avatar
Robbert Krebbers committed
762
Proof.
763
  destruct HQP.
Robbert Krebbers's avatar
Robbert Krebbers committed
764
765
766
  - by rewrite (affine Q) right_id.
  - by rewrite (True_intro Q) comm.
Qed.
767
Lemma sep_elim_r P Q `{TCOr (Affine P) (Absorbing Q)} : P  Q  Q.
Robbert Krebbers's avatar
Robbert Krebbers committed
768
769
Proof. by rewrite comm sep_elim_l. Qed.

Ralf Jung's avatar
Ralf Jung committed
770
771
Lemma sep_and P Q :
  TCOr (Affine P) (Absorbing Q)  TCOr (Absorbing P) (Affine Q) 
Robbert Krebbers's avatar
Robbert Krebbers committed
772
  P  Q  P  Q.
773
Proof.
Ralf Jung's avatar
Ralf Jung committed
774
  intros [?|?] [?|?];
775
776
    apply and_intro; apply: sep_elim_l || apply: sep_elim_r.
Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
777

778
Lemma affinely_intro P Q `{!Affine P} : (P  Q)  P  <affine> Q.
779
Proof. intros <-. by rewrite affine_affinely. Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
780
781
782
783
784
785
786
787
788
789
790

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
791
Proof. apply (anti_symm _); auto using True_sep_2. Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
792
Lemma sep_True P `{!Absorbing P} : P  True  P.
Robbert Krebbers's avatar
Robbert Krebbers committed
793
Proof. by rewrite comm True_sep. Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
794

Ralf Jung's avatar
Ralf Jung committed
795
796
797
798
799
800
801
802
803
Lemma True_emp_iff_BiAffine :
  BiAffine PROP  (True  emp).
Proof.
  split.
  - intros ?. exact: affine.
  - rewrite /BiAffine /Affine=>Hemp ?. rewrite -Hemp.
    exact: True_intro.
Qed.

804
805
Section bi_affine.
  Context `{BiAffine PROP}.
Robbert Krebbers's avatar
Robbert Krebbers committed
806

807
  Global Instance bi_affine_absorbing P : Absorbing P | 0.
808
  Proof. by rewrite /Absorbing /bi_absorbingly (affine True) left_id. Qed.
809
  Global Instance bi_affine_positive : BiPositive PROP.
810
  Proof. intros P Q. by rewrite !affine_affinely. Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
811
812
813
814
815
816
817
818
819
820
821
822
823
824
825
826
827
828
829
830
831
832
833
834

  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.
835
End bi_affine.
Robbert Krebbers's avatar
Robbert Krebbers committed
836

837
(* Properties of the persistence modality *)
838
Local Hint Resolve persistently_mono : core.
Robbert Krebbers's avatar
Robbert Krebbers committed
839
840
841
842
843
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
844

Ralf Jung's avatar
Ralf Jung committed
845
Lemma absorbingly_elim_persistently P : <absorb> <pers> P  <pers> P.
Robbert Krebbers's avatar
Robbert Krebbers committed
846
Proof.
847
848
  apply (anti_symm _), absorbingly_intro.
  by rewrite /bi_absorbingly comm persistently_absorbing.
Robbert Krebbers's avatar
Robbert Krebbers committed
849
Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
850

851
852
853
854
Lemma persistently_forall_1 {A} (Ψ : A  PROP) :
  <pers> ( a, Ψ a)   a, <pers> (Ψ a).
Proof. apply forall_intro=> x. by rewrite (forall_elim x). Qed.
Lemma persistently_forall `{!BiPersistentlyForall PROP} {A} (Ψ : A  PROP) :
855
  <pers> ( a, Ψ a)   a, <pers> (Ψ a).
856
Proof. apply (anti_symm _); auto using persistently_forall_1, persistently_forall_2. Qed.
857
Lemma persistently_exist {A} (Ψ : A  PROP) :
858
  <pers> ( a, Ψ a)   a, <pers> (Ψ a).
859
Proof.
860
  apply (anti_symm _); first by auto using persistently_exist_1.
861
862
  apply exist_elim=> x. by rewrite (exist_intro x).
Qed.
863
Lemma persistently_and P Q : <pers> (P  Q)  <pers> P  <pers> Q.
864
Proof. apply (anti_symm _); by auto using persistently_and_2. Qed.
865
Lemma persistently_or P Q : <pers> (P  Q)  <pers> P  <pers> Q.
866
Proof. rewrite !or_alt persistently_exist. by apply exist_proper=> -[]. Qed.
Ralf Jung's avatar
Ralf Jung committed
867
Lemma persistently_impl P Q : <pers> (P  Q)  <pers> P  <pers> Q.
868
869
870
871
872
Proof.
  apply impl_intro_l; rewrite -persistently_and.
  apply persistently_mono, impl_elim with P; auto.
Qed.

873
874
875
876
877
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.

878
Lemma persistently_True_emp : <pers> True  <pers> emp.
879
Proof. apply (anti_symm _); auto using persistently_emp_intro. Qed.
880
881
Lemma persistently_True : True  <pers> True.
Proof. rewrite persistently_True_emp. apply persistently_emp_intro. Qed.
882

883
Lemma persistently_and_emp P : <pers> P  <pers> (emp  P).
884
885
886
887
888
889
Proof.
  apply (anti_symm ()); last by rewrite and_elim_r.
  rewrite persistently_and. apply and_intro; last done.
  apply persistently_emp_intro.
Qed.

890
Lemma persistently_and_sep_elim_emp P Q : <pers> P  Q  (emp  P)  Q.
891
892
893
894
895
Proof.
  rewrite persistently_and_emp.
  apply persistently_and_sep_elim.
Qed.