derived.v 102 KB
Newer Older
Robbert Krebbers's avatar
Robbert Krebbers committed
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
From iris.bi Require Export interface.
From iris.algebra Require Import monoid.
From stdpp Require Import hlist.

Definition bi_iff {PROP : bi} (P Q : PROP) : PROP := ((P  Q)  (Q  P))%I.
Arguments bi_iff {_} _%I _%I : simpl never.
Instance: Params (@bi_iff) 1.
Infix "↔" := bi_iff : bi_scope.

Definition bi_wand_iff {PROP : bi} (P Q : PROP) : PROP :=
  ((P - Q)  (Q - P))%I.
Arguments bi_wand_iff {_} _%I _%I : simpl never.
Instance: Params (@bi_wand_iff) 1.
Infix "∗-∗" := bi_wand_iff (at level 95, no associativity) : bi_scope.

16
17
18
19
20
21
Class Plain {PROP : bi} (P : PROP) := plain : P  bi_plainly P.
Arguments Plain {_} _%I : simpl never.
Arguments plain {_} _%I {_}.
Hint Mode Plain + ! : typeclass_instances.
Instance: Params (@Plain) 1.

22
Class Persistent {PROP : bi} (P : PROP) := persistent : P  bi_persistently P.
Robbert Krebbers's avatar
Robbert Krebbers committed
23
24
25
26
27
Arguments Persistent {_} _%I : simpl never.
Arguments persistent {_} _%I {_}.
Hint Mode Persistent + ! : typeclass_instances.
Instance: Params (@Persistent) 1.

28
29
30
31
32
Definition bi_affinely {PROP : bi} (P : PROP) : PROP := (emp  P)%I.
Arguments bi_affinely {_} _%I : simpl never.
Instance: Params (@bi_affinely) 1.
Typeclasses Opaque bi_affinely.
Notation "□ P" := (bi_affinely (bi_persistently P))%I
33
  (at level 20, right associativity) : bi_scope.
34
35
Notation "■ P" := (bi_affinely (bi_plainly P))%I
  (at level 20, right associativity) : bi_scope.
Robbert Krebbers's avatar
Robbert Krebbers committed
36
37
38
39
40
41
42
43
44

Class Affine {PROP : bi} (Q : PROP) := affine : Q  emp.
Arguments Affine {_} _%I : simpl never.
Arguments affine {_} _%I {_}.
Hint Mode Affine + ! : typeclass_instances.

Class AffineBI (PROP : bi) := absorbing_bi (Q : PROP) : Affine Q.
Existing Instance absorbing_bi | 0.

45
Class PositiveBI (PROP : bi) :=
46
  positive_bi (P Q : PROP) : bi_affinely (P  Q)  bi_affinely P  Q.
47

48
49
50
51
Definition bi_absorbingly {PROP : bi} (P : PROP) : PROP := (True  P)%I.
Arguments bi_absorbingly {_} _%I : simpl never.
Instance: Params (@bi_absorbingly) 1.
Typeclasses Opaque bi_absorbingly.
Robbert Krebbers's avatar
Robbert Krebbers committed
52

53
Class Absorbing {PROP : bi} (P : PROP) := absorbing : bi_absorbingly P  P.
Robbert Krebbers's avatar
Robbert Krebbers committed
54
Arguments Absorbing {_} _%I : simpl never.
Robbert Krebbers's avatar
Robbert Krebbers committed
55
Arguments absorbing {_} _%I.
Robbert Krebbers's avatar
Robbert Krebbers committed
56

57
58
59
60
61
62
Definition bi_plainly_if {PROP : bi} (p : bool) (P : PROP) : PROP :=
  (if p then bi_plainly P else P)%I.
Arguments bi_plainly_if {_} !_ _%I /.
Instance: Params (@bi_plainly_if) 2.
Typeclasses Opaque bi_plainly_if.

Robbert Krebbers's avatar
Robbert Krebbers committed
63
Definition bi_persistently_if {PROP : bi} (p : bool) (P : PROP) : PROP :=
64
  (if p then bi_persistently P else P)%I.
Robbert Krebbers's avatar
Robbert Krebbers committed
65
66
67
68
Arguments bi_persistently_if {_} !_ _%I /.
Instance: Params (@bi_persistently_if) 2.
Typeclasses Opaque bi_persistently_if.

69
70
71
72
73
74
Definition bi_affinely_if {PROP : bi} (p : bool) (P : PROP) : PROP :=
  (if p then bi_affinely P else P)%I.
Arguments bi_affinely_if {_} !_ _%I /.
Instance: Params (@bi_affinely_if) 2.
Typeclasses Opaque bi_affinely_if.
Notation "□? p P" := (bi_affinely_if p (bi_persistently_if p P))%I
Robbert Krebbers's avatar
Robbert Krebbers committed
75
  (at level 20, p at level 9, P at level 20,
76
   right associativity, format "□? p  P") : bi_scope.
77
78
79
Notation "■? p P" := (bi_affinely_if p (bi_plainly_if p P))%I
  (at level 20, p at level 9, P at level 20,
   right associativity, format "■? p  P") : bi_scope.
Robbert Krebbers's avatar
Robbert Krebbers committed
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
116
117
118
119
120
121
122
123
124
125
126
127
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

Fixpoint bi_hexist {PROP : bi} {As} : himpl As PROP  PROP :=
  match As return himpl As PROP  PROP with
  | tnil => id
  | tcons A As => λ Φ,  x, bi_hexist (Φ x)
  end%I.
Fixpoint bi_hforall {PROP : bi} {As} : himpl As PROP  PROP :=
  match As return himpl As PROP  PROP with
  | tnil => id
  | tcons A As => λ Φ,  x, bi_hforall (Φ x)
  end%I.

Definition bi_laterN {PROP : sbi} (n : nat) (P : PROP) : PROP :=
  Nat.iter n bi_later P.
Arguments bi_laterN {_} !_%nat_scope _%I.
Instance: Params (@bi_laterN) 2.
Notation "▷^ n P" := (bi_laterN n P)
  (at level 20, n at level 9, P at level 20, format "▷^ n  P") : bi_scope.
Notation "▷? p P" := (bi_laterN (Nat.b2n p) P)
  (at level 20, p at level 9, P at level 20, format "▷? p  P") : bi_scope.

Definition bi_except_0 {PROP : sbi} (P : PROP) : PROP := ( False  P)%I.
Arguments bi_except_0 {_} _%I : simpl never.
Notation "◇ P" := (bi_except_0 P) (at level 20, right associativity) : bi_scope.
Instance: Params (@bi_except_0) 1.
Typeclasses Opaque bi_except_0.

Class Timeless {PROP : sbi} (P : PROP) := timeless :  P   P.
Arguments Timeless {_} _%I : simpl never.
Arguments timeless {_} _%I {_}.
Hint Mode Timeless + ! : typeclass_instances.
Instance: Params (@Timeless) 1.

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 *)
Notation "P ⊢ Q" := (@bi_entails PROP P%I Q%I).
Notation "P ⊣⊢ Q" := (equiv (A:=bi_car PROP) P%I Q%I).

(* 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.
 Global Instance bi_valid_proper : Proper (() ==> iff) (@bi_valid PROP).
Proof. solve_proper. Qed.
Global Instance bi_valid_mono : Proper (() ==> impl) (@bi_valid PROP).
Proof. solve_proper. Qed.
Global Instance bi_valid_flip_mono :
  Proper (flip () ==> flip impl) (@bi_valid PROP).
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 internal_eq_proper (A : ofeT) :
  Proper (() ==> () ==> ()) (@bi_internal_eq PROP A) := ne_proper_2 _.
181
182
Global Instance plainly_proper :
  Proper (() ==> ()) (@bi_plainly PROP) := ne_proper _.
Robbert Krebbers's avatar
Robbert Krebbers committed
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
232
233
234
235
236
237
238
239
240
241
242
243
244
245
246
247
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
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
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
438
439
440
441
442
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.

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.

Lemma exists_impl_forall {A} P (Ψ : A  PROP) :
  (( 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  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.

(* Equality stuff *)
Hint Resolve internal_eq_refl.
Lemma equiv_internal_eq {A : ofeT} P (a b : A) : a  b  P  a  b.
Proof. intros ->. auto. Qed.
Lemma internal_eq_rewrite' {A : ofeT} a b (Ψ : A  PROP) P
  {HΨ : NonExpansive Ψ} : (P  a  b)  (P  Ψ a)  P  Ψ b.
Proof.
  intros Heq HΨa. rewrite -(idemp bi_and P) {1}Heq HΨa.
  apply impl_elim_l'. by apply internal_eq_rewrite.
Qed.

Lemma internal_eq_sym {A : ofeT} (a b : A) : a  b  b  a.
Proof. apply (internal_eq_rewrite' a b (λ b, b  a)%I); auto. Qed.
Lemma internal_eq_iff P Q : P  Q  P  Q.
Proof. apply (internal_eq_rewrite' P Q (λ Q, P  Q))%I; auto using iff_refl. Qed.

Lemma f_equiv {A B : ofeT} (f : A  B) `{!NonExpansive f} x y :
  x  y  f x  f y.
Proof. apply (internal_eq_rewrite' x y (λ y, f x  f y)%I); auto. Qed.

Lemma prod_equivI {A B : ofeT} (x y : A * B) : x  y  x.1  y.1  x.2  y.2.
Proof.
  apply (anti_symm _).
  - apply and_intro; apply f_equiv; apply _.
  - rewrite {3}(surjective_pairing x) {3}(surjective_pairing y).
    apply (internal_eq_rewrite' (x.1) (y.1) (λ a, (x.1,x.2)  (a,y.2))%I); auto.
    apply (internal_eq_rewrite' (x.2) (y.2) (λ b, (x.1,x.2)  (x.1,b))%I); auto.
Qed.
Lemma sum_equivI {A B : ofeT} (x y : A + B) :
  x  y 
    match x, y with
    | inl a, inl a' => a  a' | inr b, inr b' => b  b' | _, _ => False
    end.
Proof.
  apply (anti_symm _).
  - apply (internal_eq_rewrite' x y (λ y,
             match x, y with
             | inl a, inl a' => a  a' | inr b, inr b' => b  b' | _, _ => False
             end)%I); auto.
    destruct x; auto.
  - destruct x as [a|b], y as [a'|b']; auto; apply f_equiv, _.
Qed.
Lemma option_equivI {A : ofeT} (x y : option A) :
  x  y  match x, y with
           | Some a, Some a' => a  a' | None, None => True | _, _ => False
           end.
Proof.
  apply (anti_symm _).
  - apply (internal_eq_rewrite' x y (λ y,
             match x, y with
             | Some a, Some a' => a  a' | None, None => True | _, _ => False
             end)%I); auto.
    destruct x; auto.
  - destruct x as [a|], y as [a'|]; auto. apply f_equiv, _.
Qed.

Lemma sig_equivI {A : ofeT} (P : A  Prop) (x y : sig P) : `x  `y  x  y.
Proof. apply (anti_symm _). apply sig_eq. apply f_equiv, _. Qed.

443
Lemma ofe_fun_equivI {A} {B : A  ofeT} (f g : ofe_fun B) : f  g   x, f x  g x.
Robbert Krebbers's avatar
Robbert Krebbers committed
444
445
446
447
448
449
450
451
452
Proof.
  apply (anti_symm _); auto using fun_ext.
  apply (internal_eq_rewrite' f g (λ g,  x : A, f x  g x)%I); auto.
  intros n h h' Hh; apply forall_ne=> x; apply internal_eq_ne; auto.
Qed.
Lemma ofe_morC_equivI {A B : ofeT} (f g : A -n> B) : f  g   x, f x  g x.
Proof.
  apply (anti_symm _).
  - apply (internal_eq_rewrite' f g (λ g,  x : A, f x  g x)%I); auto.
453
  - rewrite -(ofe_fun_equivI (ofe_mor_car _ _ f) (ofe_mor_car _ _ g)).
Robbert Krebbers's avatar
Robbert Krebbers committed
454
    set (h1 (f : A -n> B) :=
455
456
      exist (λ f : A -c> B, NonExpansive (f : A  B)) f (ofe_mor_ne A B f)).
    set (h2 (f : sigC (λ f : A -c> B, NonExpansive (f : A  B))) :=
Robbert Krebbers's avatar
Robbert Krebbers committed
457
458
459
460
461
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
534
535
536
537
538
539
540
541
542
543
544
545
546
547
548
549
550
551
552
553
554
555
556
557
558
559
560
561
562
563
564
565
566
567
568
569
570
571
572
573
574
575
576
577
578
579
580
581
582
583
584
585
586
587
588
589
590
591
592
593
594
595
596
597
598
599
600
601
602
603
604
605
606
607
608
609
610
611
612
613
614
615
616
617
618
619
620
621
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
652
653
654
655
656
657
658
659
660
661
662
663
664
665
666
667
668
669
670
671
672
673
674
675
676
677
678
679
680
681
682
683
684
      @CofeMor A B (`f) (proj2_sig f)).
    assert ( f, h2 (h1 f) = f) as Hh by (by intros []).
    assert (NonExpansive h2) by (intros ??? EQ; apply EQ).
    by rewrite -{2}[f]Hh -{2}[g]Hh -f_equiv -sig_equivI.
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.

Lemma sep_intro_valid_l P Q R : P  (R  Q)  R  P  Q.
Proof. intros ? ->. rewrite -{1}(left_id emp%I _ Q). by apply sep_mono. Qed.
Lemma sep_intro_valid_r P Q R : (R  P)  Q  R  P  Q.
Proof. intros -> ?. rewrite comm. by apply sep_intro_valid_l. Qed.
Lemma sep_elim_valid_l P Q R : P  (P  R  Q)  R  Q.
Proof. intros <- <-. by rewrite left_id. Qed.
Lemma sep_elim_valid_r P Q R : P  (R  P  Q)  R  Q.
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 ());
    apply wand_entails; rewrite /bi_valid HPQ /bi_wand_iff; auto.
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 ());
    apply: impl_entails; rewrite /bi_valid HPQ /bi_iff; auto.
Qed.

(* 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φ.
    by rewrite -(left_id emp%I _ (_ - _)%I) (pure_intro emp%I φ) // wand_elim_r.
  - apply wand_intro_l, wand_elim_l', pure_elim'=> Hφ.
Robbert Krebbers's avatar
Robbert Krebbers committed
685
    apply wand_intro_l. rewrite (forall_elim Hφ) comm. by apply absorbing.
Robbert Krebbers's avatar
Robbert Krebbers committed
686
687
688
689
690
691
692
693
694
Qed.

Lemma pure_internal_eq {A : ofeT} (x y : A) : x  y  x  y.
Proof. apply pure_elim'=> ->. apply internal_eq_refl. Qed.
Lemma discrete_eq {A : ofeT} (a b : A) : Discrete a  a  b  a  b.
Proof.
  intros. apply (anti_symm _); auto using discrete_eq_1, pure_internal_eq.
Qed.

695
696
(* Properties of the affinely modality *)
Global Instance affinely_ne : NonExpansive (@bi_affinely PROP).
Robbert Krebbers's avatar
Robbert Krebbers committed
697
Proof. solve_proper. Qed.
698
Global Instance affinely_proper : Proper (() ==> ()) (@bi_affinely PROP).
Robbert Krebbers's avatar
Robbert Krebbers committed
699
Proof. solve_proper. Qed.
700
Global Instance affinely_mono' : Proper (() ==> ()) (@bi_affinely PROP).
Robbert Krebbers's avatar
Robbert Krebbers committed
701
Proof. solve_proper. Qed.
702
703
Global Instance affinely_flip_mono' :
  Proper (flip () ==> flip ()) (@bi_affinely PROP).
Robbert Krebbers's avatar
Robbert Krebbers committed
704
705
Proof. solve_proper. Qed.

706
707
708
709
710
Lemma affinely_elim_emp P : bi_affinely P  emp.
Proof. rewrite /bi_affinely; auto. Qed.
Lemma affinely_elim P : bi_affinely P  P.
Proof. rewrite /bi_affinely; auto. Qed.
Lemma affinely_mono P Q : (P  Q)  bi_affinely P  bi_affinely Q.
Robbert Krebbers's avatar
Robbert Krebbers committed
711
Proof. by intros ->. Qed.
712
713
Lemma affinely_idemp P : bi_affinely (bi_affinely P)  bi_affinely P.
Proof. by rewrite /bi_affinely assoc idemp. Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
714

715
716
Lemma affinely_intro' P Q : (bi_affinely P  Q)  bi_affinely P  bi_affinely Q.
Proof. intros <-. by rewrite affinely_idemp. Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
717

718
719
720
721
722
723
724
Lemma affinely_False : bi_affinely False  False.
Proof. by rewrite /bi_affinely right_absorb. Qed.
Lemma affinely_emp : bi_affinely emp  emp.
Proof. by rewrite /bi_affinely (idemp bi_and). Qed.
Lemma affinely_or P Q : bi_affinely (P  Q)  bi_affinely P  bi_affinely Q.
Proof. by rewrite /bi_affinely and_or_l. Qed.
Lemma affinely_and P Q : bi_affinely (P  Q)  bi_affinely P  bi_affinely Q.
Robbert Krebbers's avatar
Robbert Krebbers committed
725
Proof.
726
  rewrite /bi_affinely -(comm _ P) (assoc _ (_  _)%I) -!(assoc _ P).
Robbert Krebbers's avatar
Robbert Krebbers committed
727
728
  by rewrite idemp !assoc (comm _ P).
Qed.
729
Lemma affinely_sep_2 P Q : bi_affinely P  bi_affinely Q  bi_affinely (P  Q).
Robbert Krebbers's avatar
Robbert Krebbers committed
730
Proof.
731
  rewrite /bi_affinely. apply and_intro.
732
733
734
  - by rewrite !and_elim_l right_id.
  - by rewrite !and_elim_r.
Qed.
735
736
Lemma affinely_sep `{PositiveBI PROP} P Q :
  bi_affinely (P  Q)  bi_affinely P  bi_affinely Q.
737
Proof.
738
739
  apply (anti_symm _), affinely_sep_2.
  by rewrite -{1}affinely_idemp positive_bi !(comm _ (bi_affinely P)%I) positive_bi.
Robbert Krebbers's avatar
Robbert Krebbers committed
740
Qed.
741
742
Lemma affinely_forall {A} (Φ : A  PROP) :
  bi_affinely ( a, Φ a)   a, bi_affinely (Φ a).
Robbert Krebbers's avatar
Robbert Krebbers committed
743
Proof. apply forall_intro=> a. by rewrite (forall_elim a). Qed.
744
745
746
747
748
749
750
751
752
753
754
755
756
757
758
759
Lemma affinely_exist {A} (Φ : A  PROP) :
  bi_affinely ( a, Φ a)   a, bi_affinely (Φ a).
Proof. by rewrite /bi_affinely and_exist_l. Qed.

Lemma affinely_True_emp : bi_affinely True  bi_affinely emp.
Proof. apply (anti_symm _); rewrite /bi_affinely; auto. Qed.

Lemma affinely_and_l P Q : bi_affinely P  Q  bi_affinely (P  Q).
Proof. by rewrite /bi_affinely assoc. Qed.
Lemma affinely_and_r P Q : P  bi_affinely Q  bi_affinely (P  Q).
Proof. by rewrite /bi_affinely !assoc (comm _ P). Qed.
Lemma affinely_and_lr P Q : bi_affinely P  Q  P  bi_affinely Q.
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
760
Proof. solve_proper. Qed.
761
Global Instance absorbingly_proper : Proper (() ==> ()) (@bi_absorbingly PROP).
Robbert Krebbers's avatar
Robbert Krebbers committed
762
Proof. solve_proper. Qed.
763
Global Instance absorbingly_mono' : Proper (() ==> ()) (@bi_absorbingly PROP).
Robbert Krebbers's avatar
Robbert Krebbers committed
764
Proof. solve_proper. Qed.
765
766
Global Instance absorbingly_flip_mono' :
  Proper (flip () ==> flip ()) (@bi_absorbingly PROP).
Robbert Krebbers's avatar
Robbert Krebbers committed
767
768
Proof. solve_proper. Qed.

769
Lemma absorbingly_intro P : P  bi_absorbingly P.
770
Proof. by rewrite /bi_absorbingly -True_sep_2. Qed.
771
Lemma absorbingly_mono P Q : (P  Q)  bi_absorbingly P  bi_absorbingly Q.
Robbert Krebbers's avatar
Robbert Krebbers committed
772
Proof. by intros ->. Qed.
773
Lemma absorbingly_idemp P : bi_absorbingly (bi_absorbingly P)  bi_absorbingly P.
Robbert Krebbers's avatar
Robbert Krebbers committed
774
Proof.
775
776
  apply (anti_symm _), absorbingly_intro.
  rewrite /bi_absorbingly assoc. apply sep_mono; auto.
Robbert Krebbers's avatar
Robbert Krebbers committed
777
778
Qed.

779
Lemma absorbingly_pure φ : bi_absorbingly  φ    φ .
Robbert Krebbers's avatar
Robbert Krebbers committed
780
Proof.
781
  apply (anti_symm _), absorbingly_intro.
Robbert Krebbers's avatar
Robbert Krebbers committed
782
783
  apply wand_elim_r', pure_elim'=> ?. apply wand_intro_l; auto.
Qed.
784
785
Lemma absorbingly_or P Q :
  bi_absorbingly (P  Q)  bi_absorbingly P  bi_absorbingly Q.
786
Proof. by rewrite /bi_absorbingly sep_or_l. Qed.
787
788
Lemma absorbingly_and P Q :
  bi_absorbingly (P  Q)  bi_absorbingly P  bi_absorbingly Q.
789
Proof. apply and_intro; apply absorbingly_mono; auto. Qed.
790
791
Lemma absorbingly_forall {A} (Φ : A  PROP) :
  bi_absorbingly ( a, Φ a)   a, bi_absorbingly (Φ a).
Robbert Krebbers's avatar
Robbert Krebbers committed
792
Proof. apply forall_intro=> a. by rewrite (forall_elim a). Qed.
793
794
Lemma absorbingly_exist {A} (Φ : A  PROP) :
  bi_absorbingly ( a, Φ a)   a, bi_absorbingly (Φ a).
795
Proof. by rewrite /bi_absorbingly sep_exist_l. Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
796

797
Lemma absorbingly_internal_eq {A : ofeT} (x y : A) : bi_absorbingly (x  y)  x  y.
Robbert Krebbers's avatar
Robbert Krebbers committed
798
Proof.
799
  apply (anti_symm _), absorbingly_intro.
Robbert Krebbers's avatar
Robbert Krebbers committed
800
801
802
803
  apply wand_elim_r', (internal_eq_rewrite' x y (λ y, True - x  y)%I); auto.
  apply wand_intro_l, internal_eq_refl.
Qed.

804
Lemma absorbingly_sep P Q : bi_absorbingly (P  Q)  bi_absorbingly P  bi_absorbingly Q.
805
Proof. by rewrite -{1}absorbingly_idemp /bi_absorbingly !assoc -!(comm _ P) !assoc. Qed.
806
Lemma absorbingly_True_emp : bi_absorbingly True  bi_absorbingly emp.
807
Proof. by rewrite absorbingly_pure /bi_absorbingly right_id. Qed.
808
Lemma absorbingly_wand P Q : bi_absorbingly (P - Q)  bi_absorbingly P - bi_absorbingly Q.
809
Proof. apply wand_intro_l. by rewrite -absorbingly_sep wand_elim_r. Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
810

811
Lemma absorbingly_sep_l P Q : bi_absorbingly P  Q  bi_absorbingly (P  Q).
812
Proof. by rewrite /bi_absorbingly assoc. Qed.
813
Lemma absorbingly_sep_r P Q : P  bi_absorbingly Q  bi_absorbingly (P  Q).
814
Proof. by rewrite /bi_absorbingly !assoc (comm _ P). Qed.
815
Lemma absorbingly_sep_lr P Q : bi_absorbingly P  Q  P  bi_absorbingly Q.
816
Proof. by rewrite absorbingly_sep_l absorbingly_sep_r. Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
817

818
Lemma affinely_absorbingly `{!PositiveBI PROP} P :
819
  bi_affinely (bi_absorbingly P)  bi_affinely P.
Robbert Krebbers's avatar
Robbert Krebbers committed
820
Proof.
821
822
  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
823
824
Qed.

Robbert Krebbers's avatar
Robbert Krebbers committed
825
(* Affine propositions *)
Robbert Krebbers's avatar
Robbert Krebbers committed
826
Global Instance Affine_proper : Proper (() ==> iff) (@Affine PROP).
Robbert Krebbers's avatar
Robbert Krebbers committed
827
828
829
830
831
832
833
834
835
836
837
838
839
840
841
842
Proof. solve_proper. Qed.

Global Instance emp_affine_l : Affine (emp%I : PROP).
Proof. by rewrite /Affine. Qed.
Global Instance and_affine_l P Q : Affine P  Affine (P  Q).
Proof. rewrite /Affine=> ->; auto. Qed.
Global Instance and_affine_r P Q : Affine Q  Affine (P  Q).
Proof. rewrite /Affine=> ->; auto. Qed.
Global Instance or_affine P Q : Affine P  Affine Q  Affine (P  Q).
Proof.  rewrite /Affine=> -> ->; auto. Qed.
Global Instance forall_affine `{Inhabited A} (Φ : A  PROP) :
  ( x, Affine (Φ x))  Affine ( x, Φ x).
Proof. intros. rewrite /Affine (forall_elim inhabitant). apply: affine. Qed.
Global Instance exist_affine {A} (Φ : A  PROP) :
  ( x, Affine (Φ x))  Affine ( x, Φ x).
Proof. rewrite /Affine=> H. apply exist_elim=> a. by rewrite H. Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
843

Robbert Krebbers's avatar
Robbert Krebbers committed
844
845
Global Instance sep_affine P Q : Affine P  Affine Q  Affine (P  Q).
Proof. rewrite /Affine=>-> ->. by rewrite left_id. Qed.
846
847
Global Instance affinely_affine P : Affine (bi_affinely P).
Proof. rewrite /bi_affinely. apply _. Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
848
849

(* Absorbing propositions *)
Robbert Krebbers's avatar
Robbert Krebbers committed
850
851
Global Instance Absorbing_proper : Proper (() ==> iff) (@Absorbing PROP).
Proof. solve_proper. Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
852
853

Global Instance pure_absorbing φ : Absorbing (⌜φ⌝%I : PROP).
854
Proof. by rewrite /Absorbing absorbingly_pure. Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
855
Global Instance and_absorbing P Q : Absorbing P  Absorbing Q  Absorbing (P  Q).
856
Proof. intros. by rewrite /Absorbing absorbingly_and !absorbing. Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
857
Global Instance or_absorbing P Q : Absorbing P  Absorbing Q  Absorbing (P  Q).
858
Proof. intros. by rewrite /Absorbing absorbingly_or !absorbing. Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
859
860
Global Instance forall_absorbing {A} (Φ : A  PROP) :
  ( x, Absorbing (Φ x))  Absorbing ( x, Φ x).
861
Proof. rewrite /Absorbing=> ?. rewrite absorbingly_forall. auto using forall_mono. Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
862
863
Global Instance exist_absorbing {A} (Φ : A  PROP) :
  ( x, Absorbing (Φ x))  Absorbing ( x, Φ x).
864
Proof. rewrite /Absorbing=> ?. rewrite absorbingly_exist. auto using exist_mono. Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
865

Robbert Krebbers's avatar
Robbert Krebbers committed
866
867
Global Instance internal_eq_absorbing {A : ofeT} (x y : A) :
  Absorbing (x  y : PROP)%I.
868
Proof. by rewrite /Absorbing absorbingly_internal_eq. Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
869
870

Global Instance sep_absorbing_l P Q : Absorbing P  Absorbing (P  Q).
871
Proof. intros. by rewrite /Absorbing -absorbingly_sep_l absorbing. Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
872
Global Instance sep_absorbing_r P Q : Absorbing Q  Absorbing (P  Q).
873
Proof. intros. by rewrite /Absorbing -absorbingly_sep_r absorbing. Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
874
875

Global Instance wand_absorbing P Q : Absorbing Q  Absorbing (P - Q).
876
Proof. intros. by rewrite /Absorbing absorbingly_wand !absorbing -absorbingly_intro. Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
877

878
Global Instance absorbingly_absorbing P : Absorbing (bi_absorbingly P).
879
Proof. rewrite /bi_absorbingly. apply _. Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
880
881

(* Properties of affine and absorbing propositions *)
882
883
Lemma affine_affinely P `{!Affine P} : bi_affinely P  P.
Proof. rewrite /bi_affinely. apply (anti_symm _); auto. Qed.
884
Lemma absorbing_absorbingly P `{!Absorbing P} : bi_absorbingly P  P.
885
Proof. by apply (anti_symm _), absorbingly_intro. Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
886

Robbert Krebbers's avatar
Robbert Krebbers committed
887
888
889
Lemma True_affine_all_affine P : Affine (True%I : PROP)  Affine P.
Proof. rewrite /Affine=> <-; auto. Qed.
Lemma emp_absorbing_all_absorbing P : Absorbing (emp%I : PROP)  Absorbing P.
Robbert Krebbers's avatar
Robbert Krebbers committed
890
891
Proof.
  intros. rewrite /Absorbing -{2}(left_id emp%I _ P).
892
  by rewrite -(absorbing emp) absorbingly_sep_l left_id.
Robbert Krebbers's avatar
Robbert Krebbers committed
893
Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
894
895

Lemma sep_elim_l P Q `{H : TCOr (Affine Q) (Absorbing P)} : P  Q  P.
Robbert Krebbers's avatar
Robbert Krebbers committed
896
897
898
899
900
Proof.
  destruct H.
  - by rewrite (affine Q) right_id.
  - by rewrite (True_intro Q) comm.
Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
901
902
903
Lemma sep_elim_r P Q `{H : TCOr (Affine P) (Absorbing Q)} : P  Q  Q.
Proof. by rewrite comm sep_elim_l. Qed.

904
905
Lemma sep_and P Q
    `{HPQ : TCOr (TCAnd (Affine P) (Affine Q)) (TCAnd (Absorbing P) (Absorbing Q))} :
Robbert Krebbers's avatar
Robbert Krebbers committed
906
  P  Q  P  Q.
907
908
909
910
Proof.
  destruct HPQ as [[??]|[??]];
    apply and_intro; apply: sep_elim_l || apply: sep_elim_r.
Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
911

Robbert Krebbers's avatar
Robbert Krebbers committed
912

913
914
Lemma affinely_intro P Q `{!Affine P} : (P  Q)  P  bi_affinely Q.
Proof. intros <-. by rewrite affine_affinely. Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
915
916
917
918
919
920
921
922
923
924
925

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
926
Proof. apply (anti_symm _); auto using True_sep_2. Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
927
Lemma sep_True P `{!Absorbing P} : P  True  P.
Robbert Krebbers's avatar
Robbert Krebbers committed
928
Proof. by rewrite comm True_sep. Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
929
930
931
932

Section affine_bi.
  Context `{AffineBI PROP}.

933
  Global Instance affine_bi_absorbing P : Absorbing P | 0.
934
  Proof. by rewrite /Absorbing /bi_absorbingly (affine True%I) left_id. Qed.
935
  Global Instance affine_bi_positive : PositiveBI PROP.
936
  Proof. intros P Q. by rewrite !affine_affinely. Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
937
938
939
940
941
942
943
944
945
946
947
948
949
950
951
952
953
954
955
956
957
958
959
960
961
962

  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.
End affine_bi.

963
(* Properties of the persistence modality *)
Robbert Krebbers's avatar
Robbert Krebbers committed
964
965
966
967
968
969
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
970

971
972
Lemma absorbingly_persistently P :
  bi_absorbingly (bi_persistently P)  bi_persistently P.
Robbert Krebbers's avatar
Robbert Krebbers committed
973
Proof.
974
975
  apply (anti_symm _), absorbingly_intro.
  by rewrite /bi_absorbingly comm persistently_absorbing.
Robbert Krebbers's avatar
Robbert Krebbers committed
976
Qed.
977
Global Instance persistently_absorbing P : Absorbing (bi_persistently P).
978
Proof. by rewrite /Absorbing absorbingly_persistently. Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
979

980
981
Lemma persistently_and_sep_assoc P Q R :
  bi_persistently P  (Q  R)  (bi_persistently P  Q)  R.
Robbert Krebbers's avatar
Robbert Krebbers committed
982
Proof.
983
984
985
  apply (anti_symm ()).
  - rewrite {1}persistently_idemp_2 persistently_and_sep_elim assoc.
    apply sep_mono_l, and_intro.
Robbert Krebbers's avatar
Robbert Krebbers committed
986
    + by rewrite and_elim_r sep_elim_l.
987
988
989
990
    + by rewrite and_elim_l left_id.
  - apply and_intro.
    + by rewrite and_elim_l sep_elim_l.
    + by rewrite and_elim_r.
Robbert Krebbers's avatar
Robbert Krebbers committed
991
Qed.
992
Lemma persistently_and_emp_elim P : emp  bi_persistently P  P.
Robbert Krebbers's avatar
Robbert Krebbers committed
993
Proof. by rewrite comm persistently_and_sep_elim right_id and_elim_r. Qed.
994
Lemma persistently_elim_absorbingly P : bi_persistently P  bi_absorbingly P.
Robbert Krebbers's avatar
Robbert Krebbers committed
995
Proof.
996
  rewrite -(right_id True%I _ (bi_persistently _)%I) -{1}(left_id emp%I _ True%I).
Robbert Krebbers's avatar
Robbert Krebbers committed
997
  by rewrite persistently_and_sep_assoc (comm bi_and) persistently_and_emp_elim comm.
Robbert Krebbers's avatar
Robbert Krebbers committed
998
Qed.
999
Lemma persistently_elim P `{!Absorbing P} : bi_persistently P  P.
1000
Proof. by rewrite persistently_elim_absorbingly absorbing_absorbingly. Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
1001

1002
1003
Lemma persistently_idemp_1 P :
  bi_persistently (bi_persistently P)  bi_persistently P.
1004
Proof. by rewrite persistently_elim_absorbingly absorbingly_persistently. Qed.
1005
1006
Lemma persistently_idemp P :
  bi_persistently (bi_persistently P)  bi_persistently P.
1007
Proof. apply (anti_symm _); auto using persistently_idemp_1, persistently_idemp_2. Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
1008

1009
1010
Lemma persistently_intro' P Q :
  (bi_persistently P  Q)  bi_persistently P  bi_persistently Q.
Robbert Krebbers's avatar
Robbert Krebbers committed
1011
1012
Proof. intros <-. apply persistently_idemp_2. Qed.

1013
Lemma persistently_pure φ : bi_persistently ⌜φ⌝  ⌜φ⌝.
Robbert Krebbers's avatar
Robbert Krebbers committed
1014
Proof.
1015
1016
  apply (anti_symm _); first by rewrite persistently_elim.
  apply pure_elim'=> Hφ.
1017
  trans ( x : False, bi_persistently True : PROP)%I; [by apply forall_intro|].
1018
  rewrite persistently_forall_2. auto using persistently_mono, pure_intro.
Robbert Krebbers's avatar
Robbert Krebbers committed
1019
Qed.
1020
1021
Lemma persistently_forall {A} (Ψ : A  PROP) :
  bi_persistently ( a, Ψ a)   a, bi_persistently (Ψ a).
Robbert Krebbers's avatar
Robbert Krebbers committed
1022
1023
1024
1025
Proof.
  apply (anti_symm _); auto using persistently_forall_2.
  apply forall_intro=> x. by rewrite (forall_elim x).
Qed.
1026
1027
Lemma persistently_exist {A} (Ψ : A  PROP) :
  bi_persistently ( a, Ψ a)   a, bi_persistently (