class_instances.v 80.2 KB
Newer Older
1
From stdpp Require Import nat_cancel.
Robbert Krebbers's avatar
Robbert Krebbers committed
2
From iris.bi Require Import bi tactics.
3
From iris.proofmode Require Export classes.
4
Set Default Proof Using "Type".
Robbert Krebbers's avatar
Robbert Krebbers committed
5
6
Import bi.

Robbert Krebbers's avatar
Robbert Krebbers committed
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
Section always_modalities.
  Context {PROP : bi}.
  Lemma always_modality_persistently_mixin :
    always_modality_mixin (@bi_persistently PROP) AIEnvId AIEnvClear.
  Proof.
    split; eauto using equiv_entails_sym, persistently_intro, persistently_mono,
      persistently_and, persistently_sep_2 with typeclass_instances.
  Qed.
  Definition always_modality_persistently :=
    AlwaysModality _ always_modality_persistently_mixin.

  Lemma always_modality_affinely_mixin :
    always_modality_mixin (@bi_affinely PROP) AIEnvId (AIEnvForall Affine).
  Proof.
    split; eauto using equiv_entails_sym, affinely_intro, affinely_mono,
      affinely_and, affinely_sep_2 with typeclass_instances.
  Qed.
  Definition always_modality_affinely :=
    AlwaysModality _ always_modality_affinely_mixin.

  Lemma always_modality_affinely_persistently_mixin :
    always_modality_mixin (λ P : PROP,  P)%I AIEnvId AIEnvIsEmpty.
  Proof.
    split; eauto using equiv_entails_sym, affinely_persistently_emp,
      affinely_mono, persistently_mono, affinely_persistently_idemp,
      affinely_persistently_and, affinely_persistently_sep_2 with typeclass_instances.
  Qed.
  Definition always_modality_affinely_persistently :=
    AlwaysModality _ always_modality_affinely_persistently_mixin.

  Lemma always_modality_plainly_mixin :
    always_modality_mixin (@bi_plainly PROP) (AIEnvForall Plain) AIEnvClear.
  Proof.
    split; eauto using equiv_entails_sym, plainly_intro, plainly_mono,
      plainly_and, plainly_sep_2 with typeclass_instances.
  Qed.
  Definition always_modality_plainly :=
    AlwaysModality _ always_modality_plainly_mixin.

  Lemma always_modality_affinely_plainly_mixin :
    always_modality_mixin (λ P : PROP,  P)%I (AIEnvForall Plain) AIEnvIsEmpty.
  Proof.
    split; eauto using equiv_entails_sym, affinely_plainly_emp, affinely_intro,
      plainly_intro, affinely_mono, plainly_mono, affinely_plainly_idemp,
      affinely_plainly_and, affinely_plainly_sep_2 with typeclass_instances.
  Qed.
  Definition always_modality_affinely_plainly :=
    AlwaysModality _ always_modality_affinely_plainly_mixin.
End always_modalities.

Robbert Krebbers's avatar
Robbert Krebbers committed
57
58
59
60
Section bi_instances.
Context {PROP : bi}.
Implicit Types P Q R : PROP.

61
62
63
64
65
(* FromAffinely *)
Global Instance from_affinely_affine P : Affine P  FromAffinely P P.
Proof. intros. by rewrite /FromAffinely affinely_elim. Qed.
Global Instance from_affinely_default P : FromAffinely (bi_affinely P) P | 100.
Proof. by rewrite /FromAffinely. Qed.
66

67
68
69
70
71
(* IntoAbsorbingly *)
Global Instance into_absorbingly_True : @IntoAbsorbingly PROP True emp | 0.
Proof. by rewrite /IntoAbsorbingly -absorbingly_True_emp absorbingly_pure. Qed.
Global Instance into_absorbingly_absorbing P : Absorbing P  IntoAbsorbingly P P | 1.
Proof. intros. by rewrite /IntoAbsorbingly absorbing_absorbingly. Qed.
72
Global Instance into_absorbingly_default P : IntoAbsorbingly (bi_absorbingly P) P | 100.
73
Proof. by rewrite /IntoAbsorbingly. Qed.
74

75
(* FromAssumption *)
76
Global Instance from_assumption_exact p P : FromAssumption p P P | 0.
77
Proof. by rewrite /FromAssumption /= affinely_persistently_if_elim. Qed.
78

79
Global Instance from_assumption_persistently_r P Q :
80
  FromAssumption true P Q  FromAssumption true P (bi_persistently Q).
Robbert Krebbers's avatar
Robbert Krebbers committed
81
82
Proof.
  rewrite /FromAssumption /= =><-.
83
  by rewrite -{1}affinely_persistently_idemp affinely_elim.
Robbert Krebbers's avatar
Robbert Krebbers committed
84
Qed.
85
86
87
88
Global Instance from_assumption_affinely_r P Q :
  FromAssumption true P Q  FromAssumption true P (bi_affinely Q).
Proof. rewrite /FromAssumption /= =><-. by rewrite affinely_idemp. Qed.
Global Instance from_assumption_absorbingly_r p P Q :
89
  FromAssumption p P Q  FromAssumption p P (bi_absorbingly Q).
90
Proof. rewrite /FromAssumption /= =><-. apply absorbingly_intro. Qed.
91

92
93
94
95
96
97
98
99
100
101
102
103
Global Instance from_assumption_affinely_plainly_l p P Q :
  FromAssumption true P Q  FromAssumption p ( P) Q.
Proof.
  rewrite /FromAssumption /= =><-.
  by rewrite affinely_persistently_if_elim plainly_elim_persistently.
Qed.
Global Instance from_assumption_plainly_l_true P Q :
  FromAssumption true P Q  FromAssumption true (bi_plainly P) Q.
Proof.
  rewrite /FromAssumption /= =><-.
  by rewrite persistently_elim plainly_elim_persistently.
Qed.
104
Global Instance from_assumption_plainly_l_false `{BiAffine PROP} P Q :
105
106
107
108
109
  FromAssumption true P Q  FromAssumption false (bi_plainly P) Q.
Proof.
  rewrite /FromAssumption /= =><-.
  by rewrite affine_affinely plainly_elim_persistently.
Qed.
110
Global Instance from_assumption_affinely_persistently_l p P Q :
111
  FromAssumption true P Q  FromAssumption p ( P) Q.
112
Proof. rewrite /FromAssumption /= =><-. by rewrite affinely_persistently_if_elim. Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
113
Global Instance from_assumption_persistently_l_true P Q :
114
  FromAssumption true P Q  FromAssumption true (bi_persistently P) Q.
Robbert Krebbers's avatar
Robbert Krebbers committed
115
Proof. rewrite /FromAssumption /= =><-. by rewrite persistently_idemp. Qed.
116
Global Instance from_assumption_persistently_l_false `{BiAffine PROP} P Q :
117
  FromAssumption true P Q  FromAssumption false (bi_persistently P) Q.
118
119
120
121
Proof. rewrite /FromAssumption /= =><-. by rewrite affine_affinely. Qed.
Global Instance from_assumption_affinely_l_true p P Q :
  FromAssumption p P Q  FromAssumption p (bi_affinely P) Q.
Proof. rewrite /FromAssumption /= =><-. by rewrite affinely_elim. Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
122
123

Global Instance from_assumption_forall {A} p (Φ : A  PROP) Q x :
124
125
  FromAssumption p (Φ x) Q  FromAssumption p ( x, Φ x) Q.
Proof. rewrite /FromAssumption=> <-. by rewrite forall_elim. Qed.
126
127

(* IntoPure *)
Robbert Krebbers's avatar
Robbert Krebbers committed
128
129
130
Global Instance into_pure_pure φ : @IntoPure PROP ⌜φ⌝ φ.
Proof. by rewrite /IntoPure. Qed.

Ralf Jung's avatar
Ralf Jung committed
131
Global Instance into_pure_pure_and (φ1 φ2 : Prop) P1 P2 :
Ralf Jung's avatar
Ralf Jung committed
132
  IntoPure P1 φ1  IntoPure P2 φ2  IntoPure (P1  P2) (φ1  φ2).
133
Proof. rewrite /IntoPure pure_and. by intros -> ->. Qed.
Ralf Jung's avatar
Ralf Jung committed
134
Global Instance into_pure_pure_or (φ1 φ2 : Prop) P1 P2 :
Ralf Jung's avatar
Ralf Jung committed
135
  IntoPure P1 φ1  IntoPure P2 φ2  IntoPure (P1  P2) (φ1  φ2).
136
Proof. rewrite /IntoPure pure_or. by intros -> ->. Qed.
Ralf Jung's avatar
Ralf Jung committed
137
Global Instance into_pure_pure_impl (φ1 φ2 : Prop) P1 P2 :
138
139
  FromPure false P1 φ1  IntoPure P2 φ2  IntoPure (P1  P2) (φ1  φ2).
Proof. rewrite /FromPure /IntoPure pure_impl=> <- -> //. Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
140
141
142
143
144
145
146
147
148
149
150

Global Instance into_pure_exist {A} (Φ : A  PROP) (φ : A  Prop) :
  ( x, IntoPure (Φ x) (φ x))  IntoPure ( x, Φ x) ( x, φ x).
Proof. rewrite /IntoPure=>Hx. rewrite pure_exist. by setoid_rewrite Hx. Qed.
Global Instance into_pure_forall {A} (Φ : A  PROP) (φ : A  Prop) :
  ( x, IntoPure (Φ x) (φ x))  IntoPure ( x, Φ x) ( x, φ x).
Proof. rewrite /IntoPure=>Hx. rewrite -pure_forall_2. by setoid_rewrite Hx. Qed.

Global Instance into_pure_pure_sep (φ1 φ2 : Prop) P1 P2 :
  IntoPure P1 φ1  IntoPure P2 φ2  IntoPure (P1  P2) (φ1  φ2).
Proof. rewrite /IntoPure=> -> ->. by rewrite sep_and pure_and. Qed.
Ralf Jung's avatar
Ralf Jung committed
151
Global Instance into_pure_pure_wand (φ1 φ2 : Prop) P1 P2 :
152
153
154
155
156
157
158
  FromPure true P1 φ1  IntoPure P2 φ2  IntoPure (P1 - P2) (φ1  φ2).
Proof.
  rewrite /FromPure /IntoPure=> <- -> /=.
  rewrite pure_impl -impl_wand_2. apply bi.wand_intro_l.
  rewrite {1}(persistent_absorbingly_affinely ⌜φ1%I) absorbingly_sep_l
          bi.wand_elim_r absorbing //.
Qed.
159

160
161
162
Global Instance into_pure_affinely P φ :
  IntoPure P φ  IntoPure (bi_affinely P) φ.
Proof. rewrite /IntoPure=> ->. apply affinely_elim. Qed.
163
Global Instance into_pure_absorbingly P φ : IntoPure P φ  IntoPure (bi_absorbingly P) φ.
164
Proof. rewrite /IntoPure=> ->. by rewrite absorbingly_pure. Qed.
165
166
Global Instance into_pure_plainly P φ : IntoPure P φ  IntoPure (bi_plainly P) φ.
Proof. rewrite /IntoPure=> ->. apply: plainly_elim. Qed.
167
168
Global Instance into_pure_persistently P φ :
  IntoPure P φ  IntoPure (bi_persistently P) φ.
169
Proof. rewrite /IntoPure=> ->. apply: persistently_elim. Qed.
170
Global Instance into_pure_embed `{BiEmbedding PROP PROP'} P φ :
171
  IntoPure P φ  IntoPure P φ.
172
Proof. rewrite /IntoPure=> ->. by rewrite bi_embed_pure. Qed.
173

174
(* FromPure *)
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
Global Instance from_pure_pure a φ : @FromPure PROP a ⌜φ⌝ φ.
Proof. rewrite /FromPure. apply affinely_if_elim. Qed.
Global Instance from_pure_pure_and a (φ1 φ2 : Prop) P1 P2 :
  FromPure a P1 φ1  FromPure a P2 φ2  FromPure a (P1  P2) (φ1  φ2).
Proof. rewrite /FromPure pure_and=> <- <- /=. by rewrite affinely_if_and. Qed.
Global Instance from_pure_pure_or a (φ1 φ2 : Prop) P1 P2 :
  FromPure a P1 φ1  FromPure a P2 φ2  FromPure a (P1  P2) (φ1  φ2).
Proof. by rewrite /FromPure pure_or affinely_if_or=><- <-. Qed.
Global Instance from_pure_pure_impl a (φ1 φ2 : Prop) P1 P2 :
  IntoPure P1 φ1  FromPure a P2 φ2  FromPure a (P1  P2) (φ1  φ2).
Proof.
  rewrite /FromPure /IntoPure pure_impl=> -> <-. destruct a=>//=.
  apply bi.impl_intro_l. by rewrite affinely_and_r bi.impl_elim_r.
Qed.

Global Instance from_pure_exist {A} a (Φ : A  PROP) (φ : A  Prop) :
  ( x, FromPure a (Φ x) (φ x))  FromPure a ( x, Φ x) ( x, φ x).
Proof.
  rewrite /FromPure=>Hx. rewrite pure_exist affinely_if_exist.
  by setoid_rewrite Hx.
Qed.
Global Instance from_pure_forall {A} a (Φ : A  PROP) (φ : A  Prop) :
  ( x, FromPure a (Φ x) (φ x))  FromPure a ( x, Φ x) ( x, φ x).
Proof.
  rewrite /FromPure=>Hx. rewrite pure_forall. setoid_rewrite <-Hx.
  destruct a=>//=. apply affinely_forall.
Qed.

Global Instance from_pure_pure_sep_true (φ1 φ2 : Prop) P1 P2 :
  FromPure true P1 φ1  FromPure true P2 φ2  FromPure true (P1  P2) (φ1  φ2).
Proof.
  rewrite /FromPure=> <- <- /=.
  by rewrite -persistent_and_affinely_sep_l affinely_and_r pure_and.
Qed.
Global Instance from_pure_pure_sep_false_l (φ1 φ2 : Prop) P1 P2 :
  FromPure false P1 φ1  FromPure true P2 φ2  FromPure false (P1  P2) (φ1  φ2).
Proof.
  rewrite /FromPure=> <- <- /=. by rewrite -persistent_and_affinely_sep_r pure_and.
Qed.
Global Instance from_pure_pure_sep_false_r (φ1 φ2 : Prop) P1 P2 :
  FromPure true P1 φ1  FromPure false P2 φ2  FromPure false (P1  P2) (φ1  φ2).
Proof.
  rewrite /FromPure=> <- <- /=. by rewrite -persistent_and_affinely_sep_l pure_and.
Qed.
Global Instance from_pure_pure_wand (φ1 φ2 : Prop) a P1 P2 :
  IntoPure P1 φ1  FromPure false P2 φ2  FromPure a (P1 - P2) (φ1  φ2).
Proof.
  rewrite /FromPure /IntoPure=> -> <- /=.
  by rewrite bi.affinely_if_elim pure_wand_forall pure_impl pure_impl_forall.
224
225
Qed.

226
Global Instance from_pure_plainly P φ :
227
  FromPure false P φ  FromPure false (bi_plainly P) φ.
228
Proof. rewrite /FromPure=> <-. by rewrite plainly_pure. Qed.
229
230
231
232
233
234
235
236
237
238
239
240
241
242
243
244
245
246
247
248
Global Instance from_pure_persistently P a φ :
  FromPure true P φ  FromPure a (bi_persistently P) φ.
Proof.
  rewrite /FromPure=> <- /=.
  by rewrite persistently_affinely affinely_if_elim persistently_pure.
Qed.
Global Instance from_pure_affinely_true P φ :
  FromPure true P φ  FromPure true (bi_affinely P) φ.
Proof. rewrite /FromPure=><- /=. by rewrite affinely_idemp. Qed.
Global Instance from_pure_affinely_false P φ `{!Affine P} :
  FromPure false P φ  FromPure false (bi_affinely P) φ.
Proof. rewrite /FromPure /= affine_affinely //. Qed.

Global Instance from_pure_absorbingly P φ :
  FromPure true P φ  FromPure false (bi_absorbingly P) φ.
Proof. rewrite /FromPure=> <- /=. apply persistent_absorbingly_affinely, _. Qed.
Global Instance from_pure_embed `{BiEmbedding PROP PROP'} a P φ :
  FromPure a P φ  FromPure a P φ.
Proof. rewrite /FromPure=> <-. by rewrite bi_embed_affinely_if bi_embed_pure. Qed.

249
(* IntoPersistent *)
250
Global Instance into_persistent_persistently p P Q :
251
  IntoPersistent true P Q  IntoPersistent p (bi_persistently P) Q | 0.
Robbert Krebbers's avatar
Robbert Krebbers committed
252
253
254
255
Proof.
  rewrite /IntoPersistent /= => ->.
  destruct p; simpl; auto using persistently_idemp_1.
Qed.
256
257
258
Global Instance into_persistent_affinely p P Q :
  IntoPersistent p P Q  IntoPersistent p (bi_affinely P) Q | 0.
Proof. rewrite /IntoPersistent /= => <-. by rewrite affinely_elim. Qed.
259
Global Instance into_persistent_embed `{BiEmbedding PROP PROP'} p P Q :
260
261
  IntoPersistent p P Q  IntoPersistent p P Q | 0.
Proof.
262
  rewrite /IntoPersistent -bi_embed_persistently -bi_embed_persistently_if=> -> //.
263
Qed.
264
Global Instance into_persistent_here P : IntoPersistent true P P | 1.
Robbert Krebbers's avatar
Robbert Krebbers committed
265
Proof. by rewrite /IntoPersistent. Qed.
266
267
Global Instance into_persistent_persistent P :
  Persistent P  IntoPersistent false P P | 100.
268
Proof. intros. by rewrite /IntoPersistent. Qed.
269

270
(* FromAlways *)
Robbert Krebbers's avatar
Robbert Krebbers committed
271
272
Global Instance from_always_affinely P :
  FromAlways always_modality_affinely (bi_affinely P) P | 2.
273
Proof. by rewrite /FromAlways. Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
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

Global Instance from_always_persistently P :
  FromAlways always_modality_persistently (bi_persistently P) P | 2.
Proof. by rewrite /FromAlways. Qed.
Global Instance from_always_affinely_persistently P :
  FromAlways always_modality_affinely_persistently ( P) P | 1.
Proof. by rewrite /FromAlways. Qed.
Global Instance from_always_affinely_persistently_affine_bi P :
  BiAffine PROP  FromAlways always_modality_persistently ( P) P | 0.
Proof. intros. by rewrite /FromAlways /= affine_affinely. Qed.

Global Instance from_always_plainly P :
  FromAlways always_modality_plainly (bi_plainly P) P | 2.
Proof. by rewrite /FromAlways. Qed.
Global Instance from_always_affinely_plainly P :
  FromAlways always_modality_affinely_plainly ( P) P | 1.
Proof. by rewrite /FromAlways. Qed.
Global Instance from_always_affinely_plainly_affine_bi P :
  BiAffine PROP  FromAlways always_modality_plainly ( P) P | 0.
Proof. intros. by rewrite /FromAlways /= affine_affinely. Qed.

Global Instance from_always_affinely_embed `{BiEmbedding PROP PROP'} P Q :
  FromAlways always_modality_affinely P Q 
  FromAlways always_modality_affinely P Q.
Proof. rewrite /FromAlways /= =><-. by rewrite bi_embed_affinely. Qed.
Global Instance from_always_persistently_embed `{BiEmbedding PROP PROP'} P Q :
  FromAlways always_modality_persistently P Q 
  FromAlways always_modality_persistently P Q.
Proof. rewrite /FromAlways /= =><-. by rewrite bi_embed_persistently. Qed.
Global Instance from_always_affinely_persistently_embed `{BiEmbedding PROP PROP'} P Q :
  FromAlways always_modality_affinely_persistently P Q 
  FromAlways always_modality_affinely_persistently P Q.
306
Proof.
Robbert Krebbers's avatar
Robbert Krebbers committed
307
  rewrite /FromAlways /= =><-. by rewrite bi_embed_affinely bi_embed_persistently.
308
Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
309
310
311
312
313
314
315
Global Instance from_always_plainly_embed `{BiEmbedding PROP PROP'} P Q :
  FromAlways always_modality_plainly P Q 
  FromAlways always_modality_plainly P Q.
Proof. rewrite /FromAlways /= =><-. by rewrite bi_embed_plainly. Qed.
Global Instance from_always_affinely_plainly_embed `{BiEmbedding PROP PROP'} P Q :
  FromAlways always_modality_affinely_plainly P Q 
  FromAlways always_modality_affinely_plainly P Q.
316
Proof.
Robbert Krebbers's avatar
Robbert Krebbers committed
317
  rewrite /FromAlways /= =><-. by rewrite bi_embed_affinely bi_embed_plainly.
318
Qed.
319

Robbert Krebbers's avatar
Robbert Krebbers committed
320
321
322
(* IntoWand *)
Global Instance into_wand_wand p q P Q P' :
  FromAssumption q P P'  IntoWand p q (P' - Q) P Q.
323
Proof.
324
  rewrite /FromAssumption /IntoWand=> HP. by rewrite HP affinely_persistently_if_elim.
Robbert Krebbers's avatar
Robbert Krebbers committed
325
Qed.
326
327
Global Instance into_wand_impl_false_false P Q P' :
  Absorbing P'  Absorbing (P'  Q) 
Robbert Krebbers's avatar
Robbert Krebbers committed
328
329
  FromAssumption false P P'  IntoWand false false (P'  Q) P Q.
Proof.
330
  rewrite /FromAssumption /IntoWand /= => ?? ->. apply wand_intro_r.
Robbert Krebbers's avatar
Robbert Krebbers committed
331
332
333
  by rewrite sep_and impl_elim_l.
Qed.
Global Instance into_wand_impl_false_true P Q P' :
334
  Absorbing P'  FromAssumption true P P' 
Robbert Krebbers's avatar
Robbert Krebbers committed
335
  IntoWand false true (P'  Q) P Q.
336
Proof.
337
  rewrite /IntoWand /FromAssumption /= => ? HP. apply wand_intro_l.
338
339
  rewrite -(affinely_persistently_idemp P) HP.
  by rewrite -persistently_and_affinely_sep_l persistently_elim impl_elim_r.
340
Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
341
Global Instance into_wand_impl_true_false P Q P' :
342
  Affine P'  FromAssumption false P P' 
Robbert Krebbers's avatar
Robbert Krebbers committed
343
  IntoWand true false (P'  Q) P Q.
344
Proof.
345
  rewrite /FromAssumption /IntoWand /= => ? HP. apply wand_intro_r.
346
347
  rewrite -persistently_and_affinely_sep_l HP -{2}(affine_affinely P') -affinely_and_lr.
  by rewrite affinely_persistently_elim impl_elim_l.
348
Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
349
350
Global Instance into_wand_impl_true_true P Q P' :
  FromAssumption true P P'  IntoWand true true (P'  Q) P Q.
351
Proof.
Robbert Krebbers's avatar
Robbert Krebbers committed
352
  rewrite /FromAssumption /IntoWand /= => <-. apply wand_intro_l.
353
354
  rewrite -{1}(affinely_persistently_idemp P) -and_sep_affinely_persistently.
  by rewrite -affinely_persistently_and impl_elim_r affinely_persistently_elim.
355
Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
356
357
358
359
360
361
362
363

Global Instance into_wand_and_l p q R1 R2 P' Q' :
  IntoWand p q R1 P' Q'  IntoWand p q (R1  R2) P' Q'.
Proof. rewrite /IntoWand=> ?. by rewrite /bi_wand_iff and_elim_l. Qed.
Global Instance into_wand_and_r p q R1 R2 P' Q' :
  IntoWand p q R2 Q' P'  IntoWand p q (R1  R2) Q' P'.
Proof. rewrite /IntoWand=> ?. by rewrite /bi_wand_iff and_elim_r. Qed.

364
365
366
367
368
369
370
371
372
373
374
375
376
Global Instance into_wand_forall_prop_true p (φ : Prop) P :
  IntoWand p true ( _ : φ, P)  φ  P.
Proof.
  rewrite /IntoWand (affinely_persistently_if_elim p) /=
          -impl_wand_affinely_persistently -pure_impl_forall
          bi.persistently_elim //.
Qed.
Global Instance into_wand_forall_prop_false p (φ : Prop) P :
  Absorbing P  IntoWand p false ( _ : φ, P)  φ  P.
Proof.
  intros ?.
  rewrite /IntoWand (affinely_persistently_if_elim p) /= pure_wand_forall //.
Qed.
377

Robbert Krebbers's avatar
Robbert Krebbers committed
378
379
380
381
Global Instance into_wand_forall {A} p q (Φ : A  PROP) P Q x :
  IntoWand p q (Φ x) P Q  IntoWand p q ( x, Φ x) P Q.
Proof. rewrite /IntoWand=> <-. by rewrite (forall_elim x). Qed.

382
383
384
385
386
387
Global Instance into_wand_affinely_plainly p q R P Q :
  IntoWand p q R P Q  IntoWand p q ( R) P Q.
Proof. by rewrite /IntoWand affinely_plainly_elim. Qed.
Global Instance into_wand_plainly_true q R P Q :
  IntoWand true q R P Q  IntoWand true q (bi_plainly R) P Q.
Proof. by rewrite /IntoWand /= persistently_plainly plainly_elim_persistently. Qed.
388
Global Instance into_wand_plainly_false `{!BiAffine PROP} q R P Q :
389
390
391
392
393
394
  IntoWand false q R P Q  IntoWand false q (bi_plainly R) P Q.
Proof. by rewrite /IntoWand plainly_elim. Qed.

Global Instance into_wand_affinely_persistently p q R P Q :
  IntoWand p q R P Q  IntoWand p q ( R) P Q.
Proof. by rewrite /IntoWand affinely_persistently_elim. Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
395
Global Instance into_wand_persistently_true q R P Q :
396
  IntoWand true q R P Q  IntoWand true q (bi_persistently R) P Q.
Robbert Krebbers's avatar
Robbert Krebbers committed
397
Proof. by rewrite /IntoWand /= persistently_idemp. Qed.
398
Global Instance into_wand_persistently_false `{!BiAffine PROP} q R P Q :
399
  IntoWand false q R P Q  IntoWand false q (bi_persistently R) P Q.
400
Proof. by rewrite /IntoWand persistently_elim. Qed.
401
Global Instance into_wand_embed `{BiEmbedding PROP PROP'} p q R P Q :
402
403
  IntoWand p q R P Q  IntoWand p q R P Q.
Proof.
404
405
  rewrite /IntoWand -!bi_embed_persistently_if -!bi_embed_affinely_if
          -bi_embed_wand => -> //.
406
Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
407

408
409
410
411
412
413
414
415
416
417
418
419
420
421
(* FromWand *)
Global Instance from_wand_wand P1 P2 : FromWand (P1 - P2) P1 P2.
Proof. by rewrite /FromWand. Qed.
Global Instance from_wand_embed `{BiEmbedding PROP PROP'} P Q1 Q2 :
  FromWand P Q1 Q2  FromWand P Q1 Q2.
Proof. by rewrite /FromWand -bi_embed_wand => <-. Qed.

(* FromImpl *)
Global Instance from_impl_impl P1 P2 : FromImpl (P1  P2) P1 P2.
Proof. by rewrite /FromImpl. Qed.
Global Instance from_impl_embed `{BiEmbedding PROP PROP'} P Q1 Q2 :
  FromImpl P Q1 Q2  FromImpl P Q1 Q2.
Proof. by rewrite /FromImpl -bi_embed_impl => <-. Qed.

Robbert Krebbers's avatar
Robbert Krebbers committed
422
423
424
425
(* FromAnd *)
Global Instance from_and_and P1 P2 : FromAnd (P1  P2) P1 P2 | 100.
Proof. by rewrite /FromAnd. Qed.
Global Instance from_and_sep_persistent_l P1 P1' P2 :
426
  FromAffinely P1 P1'  Persistent P1'  FromAnd (P1  P2) P1' P2 | 9.
427
Proof.
428
  rewrite /FromAffinely /FromAnd=> <- ?. by rewrite persistent_and_affinely_sep_l_1.
429
Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
430
Global Instance from_and_sep_persistent_r P1 P2 P2' :
431
  FromAffinely P2 P2'  Persistent P2'  FromAnd (P1  P2) P1 P2' | 10.
432
Proof.
433
  rewrite /FromAffinely /FromAnd=> <- ?. by rewrite persistent_and_affinely_sep_r_1.
434
Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
435
436
Global Instance from_and_sep_persistent P1 P2 :
  Persistent P1  Persistent P2  FromAnd (P1  P2) P1 P2 | 11.
437
Proof.
438
  rewrite /FromAffinely /FromAnd. intros ??. by rewrite -persistent_and_sep_1.
439
440
Qed.

Robbert Krebbers's avatar
Robbert Krebbers committed
441
442
Global Instance from_and_pure φ ψ : @FromAnd PROP ⌜φ  ψ⌝ ⌜φ⌝ ⌜ψ⌝.
Proof. by rewrite /FromAnd pure_and. Qed.
443

444
445
446
447
448
449
450
451
452
Global Instance from_and_plainly P Q1 Q2 :
  FromAnd P Q1 Q2 
  FromAnd (bi_plainly P) (bi_plainly Q1) (bi_plainly Q2).
Proof. rewrite /FromAnd=> <-. by rewrite plainly_and. Qed.
Global Instance from_and_plainly_sep P Q1 Q2 :
  FromSep P Q1 Q2 
  FromAnd (bi_plainly P) (bi_plainly Q1) (bi_plainly Q2) | 11.
Proof. rewrite /FromAnd=> <-. by rewrite -plainly_and plainly_and_sep. Qed.

Robbert Krebbers's avatar
Robbert Krebbers committed
453
Global Instance from_and_persistently P Q1 Q2 :
454
455
  FromAnd P Q1 Q2 
  FromAnd (bi_persistently P) (bi_persistently Q1) (bi_persistently Q2).
Robbert Krebbers's avatar
Robbert Krebbers committed
456
457
Proof. rewrite /FromAnd=> <-. by rewrite persistently_and. Qed.
Global Instance from_and_persistently_sep P Q1 Q2 :
458
459
  FromSep P Q1 Q2 
  FromAnd (bi_persistently P) (bi_persistently Q1) (bi_persistently Q2) | 11.
Robbert Krebbers's avatar
Robbert Krebbers committed
460
Proof. rewrite /FromAnd=> <-. by rewrite -persistently_and persistently_and_sep. Qed.
461

462
Global Instance from_and_embed `{BiEmbedding PROP PROP'} P Q1 Q2 :
463
  FromAnd P Q1 Q2  FromAnd P Q1 Q2.
464
Proof. by rewrite /FromAnd -bi_embed_and => <-. Qed.
465

Robbert Krebbers's avatar
Robbert Krebbers committed
466
467
468
Global Instance from_and_big_sepL_cons_persistent {A} (Φ : nat  A  PROP) x l :
  Persistent (Φ 0 x) 
  FromAnd ([ list] k  y  x :: l, Φ k y) (Φ 0 x) ([ list] k  y  l, Φ (S k) y).
469
Proof. intros. by rewrite /FromAnd big_opL_cons persistent_and_sep_1. Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
470
471
472
473
Global Instance from_and_big_sepL_app_persistent {A} (Φ : nat  A  PROP) l1 l2 :
  ( k y, Persistent (Φ k y)) 
  FromAnd ([ list] k  y  l1 ++ l2, Φ k y)
    ([ list] k  y  l1, Φ k y) ([ list] k  y  l2, Φ (length l1 + k) y).
474
Proof. intros. by rewrite /FromAnd big_opL_app persistent_and_sep_1. Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
475
476
477
478
479

(* FromSep *)
Global Instance from_sep_sep P1 P2 : FromSep (P1  P2) P1 P2 | 100.
Proof. by rewrite /FromSep. Qed.
Global Instance from_sep_and P1 P2 :
480
  TCOr (TCAnd (Affine P1) (Affine P2)) (TCAnd (Absorbing P1) (Absorbing P2)) 
Robbert Krebbers's avatar
Robbert Krebbers committed
481
482
483
484
485
486
  FromSep (P1  P2) P1 P2 | 101.
Proof. intros. by rewrite /FromSep sep_and. Qed.

Global Instance from_sep_pure φ ψ : @FromSep PROP ⌜φ  ψ⌝ ⌜φ⌝ ⌜ψ⌝.
Proof. by rewrite /FromSep pure_and sep_and. Qed.

487
488
489
490
Global Instance from_sep_affinely P Q1 Q2 :
  FromSep P Q1 Q2  FromSep (bi_affinely P) (bi_affinely Q1) (bi_affinely Q2).
Proof. rewrite /FromSep=> <-. by rewrite affinely_sep_2. Qed.
Global Instance from_sep_absorbingly P Q1 Q2 :
491
  FromSep P Q1 Q2  FromSep (bi_absorbingly P) (bi_absorbingly Q1) (bi_absorbingly Q2).
492
Proof. rewrite /FromSep=> <-. by rewrite absorbingly_sep. Qed.
493
494
495
496
Global Instance from_sep_plainly P Q1 Q2 :
  FromSep P Q1 Q2 
  FromSep (bi_plainly P) (bi_plainly Q1) (bi_plainly Q2).
Proof. rewrite /FromSep=> <-. by rewrite plainly_sep_2. Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
497
Global Instance from_sep_persistently P Q1 Q2 :
498
499
  FromSep P Q1 Q2 
  FromSep (bi_persistently P) (bi_persistently Q1) (bi_persistently Q2).
500
Proof. rewrite /FromSep=> <-. by rewrite persistently_sep_2. Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
501

502
Global Instance from_sep_embed `{BiEmbedding PROP PROP'} P Q1 Q2 :
503
  FromSep P Q1 Q2  FromSep P Q1 Q2.
504
Proof. by rewrite /FromSep -bi_embed_sep => <-. Qed.
505

Robbert Krebbers's avatar
Robbert Krebbers committed
506
507
508
509
510
511
512
Global Instance from_sep_big_sepL_cons {A} (Φ : nat  A  PROP) x l :
  FromSep ([ list] k  y  x :: l, Φ k y) (Φ 0 x) ([ list] k  y  l, Φ (S k) y).
Proof. by rewrite /FromSep big_sepL_cons. Qed.
Global Instance from_sep_big_sepL_app {A} (Φ : nat  A  PROP) l1 l2 :
  FromSep ([ list] k  y  l1 ++ l2, Φ k y)
    ([ list] k  y  l1, Φ k y) ([ list] k  y  l2, Φ (length l1 + k) y).
Proof. by rewrite /FromSep big_opL_app. Qed.
513

Robbert Krebbers's avatar
Robbert Krebbers committed
514
(* IntoAnd *)
515
Global Instance into_and_and p P Q : IntoAnd p (P  Q) P Q | 10.
516
Proof. by rewrite /IntoAnd affinely_persistently_if_and. Qed.
517
Global Instance into_and_and_affine_l P Q Q' :
518
  Affine P  FromAffinely Q' Q  IntoAnd false (P  Q) P Q'.
519
520
Proof.
  intros. rewrite /IntoAnd /=.
521
  by rewrite -(affine_affinely P) affinely_and_l affinely_and (from_affinely Q').
522
523
Qed.
Global Instance into_and_and_affine_r P P' Q :
524
  Affine Q  FromAffinely P' P  IntoAnd false (P  Q) P' Q.
525
526
Proof.
  intros. rewrite /IntoAnd /=.
527
  by rewrite -(affine_affinely Q) affinely_and_r affinely_and (from_affinely P').
528
529
Qed.

530
Global Instance into_and_sep `{BiPositive PROP} P Q : IntoAnd true (P  Q) P Q.
531
532
533
Proof.
  by rewrite /IntoAnd /= persistently_sep -and_sep_persistently persistently_and.
Qed.
534
535
536
537
Global Instance into_and_sep_affine P Q :
  TCOr (TCAnd (Affine P) (Affine Q)) (TCAnd (Absorbing P) (Absorbing Q)) 
  IntoAnd true (P  Q) P Q.
Proof. intros. by rewrite /IntoAnd /= sep_and. Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
538
539

Global Instance into_and_pure p φ ψ : @IntoAnd PROP p ⌜φ  ψ⌝ ⌜φ⌝ ⌜ψ⌝.
540
Proof. by rewrite /IntoAnd pure_and affinely_persistently_if_and. Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
541

542
543
Global Instance into_and_affinely p P Q1 Q2 :
  IntoAnd p P Q1 Q2  IntoAnd p (bi_affinely P) (bi_affinely Q1) (bi_affinely Q2).
Robbert Krebbers's avatar
Robbert Krebbers committed
544
Proof.
Robbert Krebbers's avatar
Robbert Krebbers committed
545
  rewrite /IntoAnd. destruct p; simpl.
546
547
  - by rewrite -affinely_and !persistently_affinely.
  - intros ->. by rewrite affinely_and.
Robbert Krebbers's avatar
Robbert Krebbers committed
548
Qed.
549
550
551
Global Instance into_and_plainly p P Q1 Q2 :
  IntoAnd p P Q1 Q2 
  IntoAnd p (bi_plainly P) (bi_plainly Q1) (bi_plainly Q2).
552
Proof.
553
554
555
556
557
  rewrite /IntoAnd /=. destruct p; simpl.
  - rewrite -plainly_and persistently_plainly -plainly_persistently
            -plainly_affinely => ->.
    by rewrite plainly_affinely plainly_persistently persistently_plainly.
  - intros ->. by rewrite plainly_and.
558
Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
559
Global Instance into_and_persistently p P Q1 Q2 :
560
561
  IntoAnd p P Q1 Q2 
  IntoAnd p (bi_persistently P) (bi_persistently Q1) (bi_persistently Q2).
Robbert Krebbers's avatar
Robbert Krebbers committed
562
Proof.
Robbert Krebbers's avatar
Robbert Krebbers committed
563
564
565
  rewrite /IntoAnd /=. destruct p; simpl.
  - by rewrite -persistently_and !persistently_idemp.
  - intros ->. by rewrite persistently_and.
Robbert Krebbers's avatar
Robbert Krebbers committed
566
Qed.
567
Global Instance into_and_embed `{BiEmbedding PROP PROP'} p P Q1 Q2 :
568
569
  IntoAnd p P Q1 Q2  IntoAnd p P Q1 Q2.
Proof.
570
571
  rewrite /IntoAnd -bi_embed_and -!bi_embed_persistently_if
          -!bi_embed_affinely_if=> -> //.
572
Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
573

Robbert Krebbers's avatar
Robbert Krebbers committed
574
(* IntoSep *)
575
576
Global Instance into_sep_sep P Q : IntoSep (P  Q) P Q.
Proof. by rewrite /IntoSep. Qed.
577

578
Inductive AndIntoSep : PROP  PROP  PROP  PROP  Prop :=
579
580
  | and_into_sep_affine P Q Q' : Affine P  FromAffinely Q' Q  AndIntoSep P P Q Q'
  | and_into_sep P Q : AndIntoSep P (bi_affinely P)%I Q Q.
581
582
583
584
585
586
Existing Class AndIntoSep.
Global Existing Instance and_into_sep_affine | 0.
Global Existing Instance and_into_sep | 2.

Global Instance into_sep_and_persistent_l P P' Q Q' :
  Persistent P  AndIntoSep P P' Q Q'  IntoSep (P  Q) P' Q'.
587
Proof.
588
  destruct 2 as [P Q Q'|P Q]; rewrite /IntoSep.
589
590
591
  - rewrite -(from_affinely Q') -(affine_affinely P) affinely_and_lr.
    by rewrite persistent_and_affinely_sep_l_1.
  - by rewrite persistent_and_affinely_sep_l_1.
592
Qed.
593
594
Global Instance into_sep_and_persistent_r P P' Q Q' :
  Persistent Q  AndIntoSep Q Q' P P'  IntoSep (P  Q) P' Q'.
595
Proof.
596
  destruct 2 as [Q P P'|Q P]; rewrite /IntoSep.
597
598
599
  - rewrite -(from_affinely P') -(affine_affinely Q) -affinely_and_lr.
    by rewrite persistent_and_affinely_sep_r_1.
  - by rewrite persistent_and_affinely_sep_r_1.
600
Qed.
601

602
603
604
Global Instance into_sep_pure φ ψ : @IntoSep PROP ⌜φ  ψ⌝ ⌜φ⌝ ⌜ψ⌝.
Proof. by rewrite /IntoSep pure_and persistent_and_sep_1. Qed.

605
Global Instance into_sep_embed `{BiEmbedding PROP PROP'} P Q1 Q2 :
606
  IntoSep P Q1 Q2  IntoSep P Q1 Q2.
607
Proof. rewrite /IntoSep -bi_embed_sep=> -> //. Qed.
608

609
610
611
612
613
614
615
Global Instance into_sep_affinely `{BiPositive PROP} P Q1 Q2 :
  IntoSep P Q1 Q2  IntoSep (bi_affinely P) (bi_affinely Q1) (bi_affinely Q2) | 0.
Proof. rewrite /IntoSep /= => ->. by rewrite affinely_sep. Qed.
(* FIXME: This instance is kind of strange, it just gets rid of the bi_affinely.
Also, it overlaps with `into_sep_affinely_later`, and hence has lower
precedence. *)
Global Instance into_sep_affinely_trim P Q1 Q2 :
616
617
  IntoSep P Q1 Q2  IntoSep (bi_affinely P) Q1 Q2 | 20.
Proof. rewrite /IntoSep /= => ->. by rewrite affinely_elim. Qed.
618

619
Global Instance into_sep_plainly `{BiPositive PROP} P Q1 Q2 :
620
621
  IntoSep P Q1 Q2  IntoSep (bi_plainly P) (bi_plainly Q1) (bi_plainly Q2).
Proof. rewrite /IntoSep /= => ->. by rewrite plainly_sep. Qed.
622
623
624
625
626
627
628
629
Global Instance into_sep_plainly_affine P Q1 Q2 :
  IntoSep P Q1 Q2 
  TCOr (TCAnd (Affine Q1) (Affine Q2)) (TCAnd (Absorbing Q1) (Absorbing Q2)) 
  IntoSep (bi_plainly P) (bi_plainly Q1) (bi_plainly Q2).
Proof.
  rewrite /IntoSep /= => -> ?. by rewrite sep_and plainly_and plainly_and_sep_l_1.
Qed.

630
Global Instance into_sep_persistently `{BiPositive PROP} P Q1 Q2 :
631
632
  IntoSep P Q1 Q2 
  IntoSep (bi_persistently P) (bi_persistently Q1) (bi_persistently Q2).
633
Proof. rewrite /IntoSep /= => ->. by rewrite persistently_sep. Qed.
634
635
636
637
638
639
640
641
642
643
644
645
646
647
648
649
Global Instance into_sep_persistently_affine P Q1 Q2 :
  IntoSep P Q1 Q2 
  TCOr (TCAnd (Affine Q1) (Affine Q2)) (TCAnd (Absorbing Q1) (Absorbing Q2)) 
  IntoSep (bi_persistently P) (bi_persistently Q1) (bi_persistently Q2).
Proof.
  rewrite /IntoSep /= => -> ?.
  by rewrite sep_and persistently_and persistently_and_sep_l_1.
Qed.
Global Instance into_sep_affinely_persistently_affine P Q1 Q2 :
  IntoSep P Q1 Q2 
  TCOr (TCAnd (Affine Q1) (Affine Q2)) (TCAnd (Absorbing Q1) (Absorbing Q2)) 
  IntoSep ( P) ( Q1) ( Q2).
Proof.
  rewrite /IntoSep /= => -> ?.
  by rewrite sep_and affinely_persistently_and and_sep_affinely_persistently.
Qed.
650

651
652
653
(* We use [IsCons] and [IsApp] to make sure that [frame_big_sepL_cons] and
[frame_big_sepL_app] cannot be applied repeatedly often when having
[ [∗ list] k ↦ x ∈ ?e, Φ k x] with [?e] an evar. *)
654
Global Instance into_sep_big_sepL_cons {A} (Φ : nat  A  PROP) l x l' :
655
  IsCons l x l' 
656
  IntoSep ([ list] k  y  l, Φ k y)
657
    (Φ 0 x) ([ list] k  y  l', Φ (S k) y).
Robbert Krebbers's avatar
Robbert Krebbers committed
658
Proof. rewrite /IsCons=>->. by rewrite /IntoSep big_sepL_cons. Qed.
659
Global Instance into_sep_big_sepL_app {A} (Φ : nat  A  PROP) l l1 l2 :
660
  IsApp l l1 l2 
661
  IntoSep ([ list] k  y  l, Φ k y)
662
    ([ list] k  y  l1, Φ k y) ([ list] k  y  l2, Φ (length l1 + k) y).
Robbert Krebbers's avatar
Robbert Krebbers committed
663
664
665
666
667
668
669
Proof. rewrite /IsApp=>->. by rewrite /IntoSep big_sepL_app. Qed.

(* FromOr *)
Global Instance from_or_or P1 P2 : FromOr (P1  P2) P1 P2.
Proof. by rewrite /FromOr. Qed.
Global Instance from_or_pure φ ψ : @FromOr PROP ⌜φ  ψ⌝ ⌜φ⌝ ⌜ψ⌝.
Proof. by rewrite /FromOr pure_or. Qed.
670
671
672
673
Global Instance from_or_affinely P Q1 Q2 :
  FromOr P Q1 Q2  FromOr (bi_affinely P) (bi_affinely Q1) (bi_affinely Q2).
Proof. rewrite /FromOr=> <-. by rewrite affinely_or. Qed.
Global Instance from_or_absorbingly P Q1 Q2 :
674
  FromOr P Q1 Q2  FromOr (bi_absorbingly P) (bi_absorbingly Q1) (bi_absorbingly Q2).
675
Proof. rewrite /FromOr=> <-. by rewrite absorbingly_or. Qed.
676
677
Global Instance from_or_plainly P Q1 Q2 :
  FromOr P Q1 Q2  FromOr (bi_plainly P) (bi_plainly Q1) (bi_plainly Q2).
678
Proof. rewrite /FromOr=> <-. by rewrite -plainly_or_2. Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
679
Global Instance from_or_persistently P Q1 Q2 :
680
681
  FromOr P Q1 Q2 
  FromOr (bi_persistently P) (bi_persistently Q1) (bi_persistently Q2).
Robbert Krebbers's avatar
Robbert Krebbers committed
682
Proof. rewrite /FromOr=> <-. by rewrite persistently_or. Qed.
683
Global Instance from_or_embed `{BiEmbedding PROP PROP'} P Q1 Q2 :
684
  FromOr P Q1 Q2  FromOr P Q1 Q2.
685
Proof. by rewrite /FromOr -bi_embed_or => <-. Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
686
687
688
689
690
691

(* IntoOr *)
Global Instance into_or_or P Q : IntoOr (P  Q) P Q.
Proof. by rewrite /IntoOr. Qed.
Global Instance into_or_pure φ ψ : @IntoOr PROP ⌜φ  ψ⌝ ⌜φ⌝ ⌜ψ⌝.
Proof. by rewrite /IntoOr pure_or. Qed.
692
693
694
695
Global Instance into_or_affinely P Q1 Q2 :
  IntoOr P Q1 Q2  IntoOr (bi_affinely P) (bi_affinely Q1) (bi_affinely Q2).
Proof. rewrite /IntoOr=>->. by rewrite affinely_or. Qed.
Global Instance into_or_absorbingly P Q1 Q2 :
696
  IntoOr P Q1 Q2  IntoOr (bi_absorbingly P) (bi_absorbingly Q1) (bi_absorbingly Q2).
697
Proof. rewrite /IntoOr=>->. by rewrite absorbingly_or. Qed.
698
Global Instance into_or_plainly `{BiPlainlyExist PROP} P Q1 Q2 :
699
700
  IntoOr P Q1 Q2  IntoOr (bi_plainly P) (bi_plainly Q1) (bi_plainly Q2).
Proof. rewrite /IntoOr=>->. by rewrite plainly_or. Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
701
Global Instance into_or_persistently P Q1 Q2 :
702
703
  IntoOr P Q1 Q2 
  IntoOr (bi_persistently P) (bi_persistently Q1) (bi_persistently Q2).
Robbert Krebbers's avatar
Robbert Krebbers committed
704
Proof. rewrite /IntoOr=>->. by rewrite persistently_or. Qed.
705
Global Instance into_or_embed `{BiEmbedding PROP PROP'} P Q1 Q2 :
706
  IntoOr P Q1 Q2  IntoOr P Q1 Q2.
707
Proof. by rewrite /IntoOr -bi_embed_or => <-. Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
708
709
710
711
712
713
714

(* FromExist *)
Global Instance from_exist_exist {A} (Φ : A  PROP): FromExist ( a, Φ a) Φ.
Proof. by rewrite /FromExist. Qed.
Global Instance from_exist_pure {A} (φ : A  Prop) :
  @FromExist PROP A  x, φ x (λ a, ⌜φ a)%I.
Proof. by rewrite /FromExist pure_exist. Qed.
715
716
717
718
Global Instance from_exist_affinely {A} P (Φ : A  PROP) :
  FromExist P Φ  FromExist (bi_affinely P) (λ a, bi_affinely (Φ a))%I.
Proof. rewrite /FromExist=> <-. by rewrite affinely_exist. Qed.
Global Instance from_exist_absorbingly {A} P (Φ : A  PROP) :
719
  FromExist P Φ  FromExist (bi_absorbingly P) (λ a, bi_absorbingly (Φ a))%I.
720
Proof. rewrite /FromExist=> <-. by rewrite absorbingly_exist. Qed.
721
722
Global Instance from_exist_plainly {A} P (Φ : A  PROP) :
  FromExist P Φ  FromExist (bi_plainly P) (λ a, bi_plainly (Φ a))%I.
723
Proof. rewrite /FromExist=> <-. by rewrite -plainly_exist_2. Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
724
Global Instance from_exist_persistently {A} P (Φ : A  PROP) :
725
  FromExist P Φ  FromExist (bi_persistently P) (λ a, bi_persistently (Φ a))%I.
Robbert Krebbers's avatar
Robbert Krebbers committed
726
Proof. rewrite /FromExist=> <-. by rewrite persistently_exist. Qed.
727
Global Instance from_exist_embed `{BiEmbedding PROP PROP'} {A} P (Φ : A  PROP) :
728
  FromExist P Φ  FromExist P (λ a, ⎡Φ a%I).
729
Proof. by rewrite /FromExist -bi_embed_exist => <-. Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
730
731
732
733
734
735
736

(* IntoExist *)
Global Instance into_exist_exist {A} (Φ : A  PROP) : IntoExist ( a, Φ a) Φ.
Proof. by rewrite /IntoExist. Qed.
Global Instance into_exist_pure {A} (φ : A  Prop) :
  @IntoExist PROP A  x, φ x (λ a, ⌜φ a)%I.
Proof. by rewrite /IntoExist pure_exist. Qed.
737
738
739
Global Instance into_exist_affinely {A} P (Φ : A  PROP) :
  IntoExist P Φ  IntoExist (bi_affinely P) (λ a, bi_affinely (Φ a))%I.
Proof. rewrite /IntoExist=> HP. by rewrite HP affinely_exist. Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
740
741
742
743
744
745
746
747
748
749
Global Instance into_exist_and_pure P Q φ :
  IntoPureT P φ  IntoExist (P  Q) (λ _ : φ, Q).
Proof.
  intros (φ'&->&?). rewrite /IntoExist (into_pure P).
  apply pure_elim_l=> Hφ. by rewrite -(exist_intro Hφ).
Qed.
Global Instance into_exist_sep_pure P Q φ :
  TCOr (Affine P) (Absorbing Q)  IntoPureT P φ  IntoExist (P  Q) (λ _ : φ, Q).
Proof.
  intros ? (φ'&->&?). rewrite /IntoExist.
Robbert Krebbers's avatar
Robbert Krebbers committed
750
  eapply (pure_elim φ'); [by rewrite (into_pure P); apply sep_elim_l, _|]=>?.
Robbert Krebbers's avatar
Robbert Krebbers committed
751
752
  rewrite -exist_intro //. apply sep_elim_r, _.
Qed.
753
Global Instance into_exist_absorbingly {A} P (Φ : A  PROP) :
754
  IntoExist P Φ  IntoExist (bi_absorbingly P) (λ a, bi_absorbingly (Φ a))%I.
755
Proof. rewrite /IntoExist=> HP. by rewrite HP absorbingly_exist. Qed.
756
Global Instance into_exist_plainly `{BiPlainlyExist PROP} {A} P (Φ : A  PROP) :
757
758
  IntoExist P Φ  IntoExist (bi_plainly P) (λ a, bi_plainly (Φ a))%I.
Proof. rewrite /IntoExist=> HP. by rewrite HP plainly_exist. Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
759
Global Instance into_exist_persistently {A} P (Φ : A  PROP) :
760
  IntoExist P Φ  IntoExist (bi_persistently P) (λ a, bi_persistently (Φ a))%I.
Robbert Krebbers's avatar
Robbert Krebbers committed
761
Proof. rewrite /IntoExist=> HP. by rewrite HP persistently_exist. Qed.
762
Global Instance into_exist_embed `{BiEmbedding PROP PROP'} {A} P (Φ : A  PROP) :
763
  IntoExist P Φ  IntoExist P (λ a, ⎡Φ a%I).
764
Proof. by rewrite /IntoExist -bi_embed_exist => <-. Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
765
766
767
768

(* IntoForall *)
Global Instance into_forall_forall {A} (Φ : A  PROP) : IntoForall ( a, Φ a) Φ.
Proof. by rewrite /IntoForall. Qed.
769
770
771
Global Instance into_forall_affinely {A} P (Φ : A  PROP) :
  IntoForall P Φ  IntoForall (bi_affinely P) (λ a, bi_affinely (Φ a))%I.
Proof. rewrite /IntoForall=> HP. by rewrite HP affinely_forall. Qed.
772
773
774
Global Instance into_forall_plainly {A} P (Φ : A  PROP) :
  IntoForall P Φ  IntoForall (bi_plainly P) (λ a, bi_plainly (Φ a))%I.
Proof. rewrite /IntoForall=> HP. by rewrite HP plainly_forall. Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
775
Global Instance into_forall_persistently {A} P (Φ : A  PROP) :
776