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

Robbert Krebbers's avatar
Robbert Krebbers committed
6
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
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
56
57
58
59
Section bi_instances.
Context {PROP : bi}.
Implicit Types P Q R : PROP.

60
61
62
63
64
(* 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.
65

66
67
68
69
70
(* 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.
71
Global Instance into_absorbingly_default P : IntoAbsorbingly (bi_absorbingly P) P | 100.
72
Proof. by rewrite /IntoAbsorbingly. Qed.
73

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

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

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

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

126
127
128
129
Global Instance from_assumption_bupd `{BUpdFacts PROP} p P Q :
  FromAssumption p P Q  FromAssumption p P (|==> Q).
Proof. rewrite /FromAssumption=>->. apply bupd_intro. Qed.

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

Ralf Jung's avatar
Ralf Jung committed
134
Global Instance into_pure_pure_and (φ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_and. by intros -> ->. Qed.
Ralf Jung's avatar
Ralf Jung committed
137
Global Instance into_pure_pure_or (φ1 φ2 : Prop) P1 P2 :
Ralf Jung's avatar
Ralf Jung committed
138
  IntoPure P1 φ1  IntoPure P2 φ2  IntoPure (P1  P2) (φ1  φ2).
139
Proof. rewrite /IntoPure pure_or. by intros -> ->. Qed.
Ralf Jung's avatar
Ralf Jung committed
140
Global Instance into_pure_pure_impl (φ1 φ2 : Prop) P1 P2 :
141
142
  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
143
144
145
146
147
148
149
150
151
152
153

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
154
Global Instance into_pure_pure_wand (φ1 φ2 : Prop) P1 P2 :
155
156
157
158
159
160
161
  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.
162

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

177
(* FromPure *)
178
179
180
181
182
183
184
185
186
187
188
189
190
191
192
193
194
195
196
197
198
199
200
201
202
203
204
205
206
207
208
209
210
211
212
213
214
215
216
217
218
219
220
221
222
223
224
225
226
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.
227
228
Qed.

229
Global Instance from_pure_plainly P φ :
230
  FromPure false P φ  FromPure false (bi_plainly P) φ.
231
Proof. rewrite /FromPure=> <-. by rewrite plainly_pure. Qed.
232
233
234
235
236
237
238
239
240
241
242
243
244
245
246
247
248
249
250
251
252
253
254
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.

Global Instance from_pure_bupd `{BUpdFacts PROP} a P φ :
  FromPure a P φ  FromPure a (|==> P) φ.
Proof. rewrite /FromPure=> <-. apply bupd_intro. Qed.
255

256
(* IntoPersistent *)
257
Global Instance into_persistent_persistently p P Q :
258
  IntoPersistent true P Q  IntoPersistent p (bi_persistently P) Q | 0.
Robbert Krebbers's avatar
Robbert Krebbers committed
259
260
261
262
Proof.
  rewrite /IntoPersistent /= => ->.
  destruct p; simpl; auto using persistently_idemp_1.
Qed.
263
264
265
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.
266
Global Instance into_persistent_embed `{BiEmbedding PROP PROP'} p P Q :
267
268
  IntoPersistent p P Q  IntoPersistent p P Q | 0.
Proof.
269
  rewrite /IntoPersistent -bi_embed_persistently -bi_embed_persistently_if=> -> //.
270
Qed.
271
Global Instance into_persistent_here P : IntoPersistent true P P | 1.
Robbert Krebbers's avatar
Robbert Krebbers committed
272
Proof. by rewrite /IntoPersistent. Qed.
273
274
Global Instance into_persistent_persistent P :
  Persistent P  IntoPersistent false P P | 100.
275
Proof. intros. by rewrite /IntoPersistent. Qed.
276

277
(* FromAlways *)
Robbert Krebbers's avatar
Robbert Krebbers committed
278
279
Global Instance from_always_affinely P :
  FromAlways always_modality_affinely (bi_affinely P) P | 2.
280
Proof. by rewrite /FromAlways. Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
281
282
283
284
285
286
287
288
289
290
291
292
293
294
295
296
297
298
299
300
301
302
303
304
305
306
307
308
309
310
311
312

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.
313
Proof.
Robbert Krebbers's avatar
Robbert Krebbers committed
314
  rewrite /FromAlways /= =><-. by rewrite bi_embed_affinely bi_embed_persistently.
315
Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
316
317
318
319
320
321
322
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.
323
Proof.
Robbert Krebbers's avatar
Robbert Krebbers committed
324
  rewrite /FromAlways /= =><-. by rewrite bi_embed_affinely bi_embed_plainly.
325
Qed.
326

Robbert Krebbers's avatar
Robbert Krebbers committed
327
328
329
(* IntoWand *)
Global Instance into_wand_wand p q P Q P' :
  FromAssumption q P P'  IntoWand p q (P' - Q) P Q.
330
Proof.
331
  rewrite /FromAssumption /IntoWand=> HP. by rewrite HP affinely_persistently_if_elim.
Robbert Krebbers's avatar
Robbert Krebbers committed
332
Qed.
333

334
335
Global Instance into_wand_impl_false_false P Q P' :
  Absorbing P'  Absorbing (P'  Q) 
Robbert Krebbers's avatar
Robbert Krebbers committed
336
337
  FromAssumption false P P'  IntoWand false false (P'  Q) P Q.
Proof.
338
  rewrite /FromAssumption /IntoWand /= => ?? ->. apply wand_intro_r.
Robbert Krebbers's avatar
Robbert Krebbers committed
339
340
  by rewrite sep_and impl_elim_l.
Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
341

Robbert Krebbers's avatar
Robbert Krebbers committed
342
Global Instance into_wand_impl_false_true P Q P' :
343
  Absorbing P'  FromAssumption true P P' 
Robbert Krebbers's avatar
Robbert Krebbers committed
344
  IntoWand false true (P'  Q) P Q.
345
Proof.
346
  rewrite /IntoWand /FromAssumption /= => ? HP. apply wand_intro_l.
347
348
  rewrite -(affinely_persistently_idemp P) HP.
  by rewrite -persistently_and_affinely_sep_l persistently_elim impl_elim_r.
349
350
Qed.

Robbert Krebbers's avatar
Robbert Krebbers committed
351
Global Instance into_wand_impl_true_false P Q P' :
352
  Affine P'  FromAssumption false P P' 
Robbert Krebbers's avatar
Robbert Krebbers committed
353
  IntoWand true false (P'  Q) P Q.
354
Proof.
355
  rewrite /FromAssumption /IntoWand /= => ? HP. apply wand_intro_r.
356
357
  rewrite -persistently_and_affinely_sep_l HP -{2}(affine_affinely P') -affinely_and_lr.
  by rewrite affinely_persistently_elim impl_elim_l.
358
Qed.
359

Robbert Krebbers's avatar
Robbert Krebbers committed
360
361
Global Instance into_wand_impl_true_true P Q P' :
  FromAssumption true P P'  IntoWand true true (P'  Q) P Q.
362
Proof.
Robbert Krebbers's avatar
Robbert Krebbers committed
363
  rewrite /FromAssumption /IntoWand /= => <-. apply wand_intro_l.
364
365
  rewrite -{1}(affinely_persistently_idemp P) -and_sep_affinely_persistently.
  by rewrite -affinely_persistently_and impl_elim_r affinely_persistently_elim.
366
Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
367
368
369
370
371
372
373
374

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.

375
376
377
378
379
380
381
382
383
384
385
386
387
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.
388

Robbert Krebbers's avatar
Robbert Krebbers committed
389
390
391
392
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.

393
394
395
396
397
398
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.
399
Global Instance into_wand_plainly_false `{!BiAffine PROP} q R P Q :
400
401
402
403
404
405
  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
406
Global Instance into_wand_persistently_true q R P Q :
407
  IntoWand true q R P Q  IntoWand true q (bi_persistently R) P Q.
Robbert Krebbers's avatar
Robbert Krebbers committed
408
Proof. by rewrite /IntoWand /= persistently_idemp. Qed.
409
Global Instance into_wand_persistently_false `{!BiAffine PROP} q R P Q :
410
  IntoWand false q R P Q  IntoWand false q (bi_persistently R) P Q.
411
Proof. by rewrite /IntoWand persistently_elim. Qed.
412
Global Instance into_wand_embed `{BiEmbedding PROP PROP'} p q R P Q :
413
414
  IntoWand p q R P Q  IntoWand p q R P Q.
Proof.
415
416
  rewrite /IntoWand -!bi_embed_persistently_if -!bi_embed_affinely_if
          -bi_embed_wand => -> //.
417
Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
418

419
420
421
422
423
424
425
426
427
428
429
430
431
432
433
434
435
436
437
438
439
Global Instance into_wand_bupd `{BUpdFacts PROP} p q R P Q :
  IntoWand false false R P Q  IntoWand p q (|==> R) (|==> P) (|==> Q).
Proof.
  rewrite /IntoWand /= => HR. rewrite !affinely_persistently_if_elim HR.
  apply wand_intro_l. by rewrite bupd_sep wand_elim_r.
Qed.

Global Instance into_wand_bupd_persistent `{BUpdFacts PROP} p q R P Q :
  IntoWand false q R P Q  IntoWand p q (|==> R) P (|==> Q).
Proof.
  rewrite /IntoWand /= => HR. rewrite affinely_persistently_if_elim HR.
  apply wand_intro_l. by rewrite bupd_frame_l wand_elim_r.
Qed.

Global Instance into_wand_bupd_args `{BUpdFacts PROP} p q R P Q :
  IntoWand p false R P Q  IntoWand' p q R (|==> P) (|==> Q).
Proof.
  rewrite /IntoWand' /IntoWand /= => ->.
  apply wand_intro_l. by rewrite affinely_persistently_if_elim bupd_wand_r.
Qed.

440
441
442
443
444
445
446
447
448
449
450
451
452
453
(* 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
454
455
456
457
(* 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 :
458
  FromAffinely P1 P1'  Persistent P1'  FromAnd (P1  P2) P1' P2 | 9.
459
Proof.
460
  rewrite /FromAffinely /FromAnd=> <- ?. by rewrite persistent_and_affinely_sep_l_1.
461
Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
462
Global Instance from_and_sep_persistent_r P1 P2 P2' :
463
  FromAffinely P2 P2'  Persistent P2'  FromAnd (P1  P2) P1 P2' | 10.
464
Proof.
465
  rewrite /FromAffinely /FromAnd=> <- ?. by rewrite persistent_and_affinely_sep_r_1.
466
Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
467
468
Global Instance from_and_sep_persistent P1 P2 :
  Persistent P1  Persistent P2  FromAnd (P1  P2) P1 P2 | 11.
469
Proof.
470
  rewrite /FromAffinely /FromAnd. intros ??. by rewrite -persistent_and_sep_1.
471
472
Qed.

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

476
477
478
479
480
481
482
483
484
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
485
Global Instance from_and_persistently P Q1 Q2 :
486
487
  FromAnd P Q1 Q2 
  FromAnd (bi_persistently P) (bi_persistently Q1) (bi_persistently Q2).
Robbert Krebbers's avatar
Robbert Krebbers committed
488
489
Proof. rewrite /FromAnd=> <-. by rewrite persistently_and. Qed.
Global Instance from_and_persistently_sep P Q1 Q2 :
490
491
  FromSep P Q1 Q2 
  FromAnd (bi_persistently P) (bi_persistently Q1) (bi_persistently Q2) | 11.
Robbert Krebbers's avatar
Robbert Krebbers committed
492
Proof. rewrite /FromAnd=> <-. by rewrite -persistently_and persistently_and_sep. Qed.
493

494
Global Instance from_and_embed `{BiEmbedding PROP PROP'} P Q1 Q2 :
495
  FromAnd P Q1 Q2  FromAnd P Q1 Q2.
496
Proof. by rewrite /FromAnd -bi_embed_and => <-. Qed.
497

Robbert Krebbers's avatar
Robbert Krebbers committed
498
499
500
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).
501
Proof. intros. by rewrite /FromAnd big_opL_cons persistent_and_sep_1. Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
502
503
504
505
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).
506
Proof. intros. by rewrite /FromAnd big_opL_app persistent_and_sep_1. Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
507
508
509
510
511

(* 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 :
512
  TCOr (TCAnd (Affine P1) (Affine P2)) (TCAnd (Absorbing P1) (Absorbing P2)) 
Robbert Krebbers's avatar
Robbert Krebbers committed
513
514
515
516
517
518
  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.

519
520
521
522
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 :
523
  FromSep P Q1 Q2  FromSep (bi_absorbingly P) (bi_absorbingly Q1) (bi_absorbingly Q2).
524
Proof. rewrite /FromSep=> <-. by rewrite absorbingly_sep. Qed.
525
526
527
528
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
529
Global Instance from_sep_persistently P Q1 Q2 :
530
531
  FromSep P Q1 Q2 
  FromSep (bi_persistently P) (bi_persistently Q1) (bi_persistently Q2).
532
Proof. rewrite /FromSep=> <-. by rewrite persistently_sep_2. Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
533

534
Global Instance from_sep_embed `{BiEmbedding PROP PROP'} P Q1 Q2 :
535
  FromSep P Q1 Q2  FromSep P Q1 Q2.
536
Proof. by rewrite /FromSep -bi_embed_sep => <-. Qed.
537

Robbert Krebbers's avatar
Robbert Krebbers committed
538
539
540
541
542
543
544
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.
545

546
547
548
549
Global Instance from_sep_bupd `{BUpdFacts PROP} P Q1 Q2 :
  FromSep P Q1 Q2  FromSep (|==> P) (|==> Q1) (|==> Q2).
Proof. rewrite /FromSep=><-. apply bupd_sep. Qed.

Robbert Krebbers's avatar
Robbert Krebbers committed
550
(* IntoAnd *)
551
Global Instance into_and_and p P Q : IntoAnd p (P  Q) P Q | 10.
552
Proof. by rewrite /IntoAnd affinely_persistently_if_and. Qed.
553
Global Instance into_and_and_affine_l P Q Q' :
554
  Affine P  FromAffinely Q' Q  IntoAnd false (P  Q) P Q'.
555
556
Proof.
  intros. rewrite /IntoAnd /=.
557
  by rewrite -(affine_affinely P) affinely_and_l affinely_and (from_affinely Q').
558
559
Qed.
Global Instance into_and_and_affine_r P P' Q :
560
  Affine Q  FromAffinely P' P  IntoAnd false (P  Q) P' Q.
561
562
Proof.
  intros. rewrite /IntoAnd /=.
563
  by rewrite -(affine_affinely Q) affinely_and_r affinely_and (from_affinely P').
564
565
Qed.

566
Global Instance into_and_sep `{BiPositive PROP} P Q : IntoAnd true (P  Q) P Q.
567
568
569
Proof.
  by rewrite /IntoAnd /= persistently_sep -and_sep_persistently persistently_and.
Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
570
571

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

574
575
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
576
Proof.
Robbert Krebbers's avatar
Robbert Krebbers committed
577
  rewrite /IntoAnd. destruct p; simpl.
578
579
  - by rewrite -affinely_and !persistently_affinely.
  - intros ->. by rewrite affinely_and.
Robbert Krebbers's avatar
Robbert Krebbers committed
580
Qed.
581
582
583
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).
584
Proof.
585
586
587
588
589
  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.
590
Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
591
Global Instance into_and_persistently p P Q1 Q2 :
592
593
  IntoAnd p P Q1 Q2 
  IntoAnd p (bi_persistently P) (bi_persistently Q1) (bi_persistently Q2).
Robbert Krebbers's avatar
Robbert Krebbers committed
594
Proof.
Robbert Krebbers's avatar
Robbert Krebbers committed
595
596
597
  rewrite /IntoAnd /=. destruct p; simpl.
  - by rewrite -persistently_and !persistently_idemp.
  - intros ->. by rewrite persistently_and.
Robbert Krebbers's avatar
Robbert Krebbers committed
598
Qed.
599
Global Instance into_and_embed `{BiEmbedding PROP PROP'} p P Q1 Q2 :
600
601
  IntoAnd p P Q1 Q2  IntoAnd p P Q1 Q2.
Proof.
602
603
  rewrite /IntoAnd -bi_embed_and -!bi_embed_persistently_if
          -!bi_embed_affinely_if=> -> //.
604
Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
605

Robbert Krebbers's avatar
Robbert Krebbers committed
606
(* IntoSep *)
607
608
Global Instance into_sep_sep P Q : IntoSep (P  Q) P Q.
Proof. by rewrite /IntoSep. Qed.
609

610
Inductive AndIntoSep : PROP  PROP  PROP  PROP  Prop :=
611
612
  | 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.
613
614
615
616
617
618
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'.
619
Proof.
620
  destruct 2 as [P Q Q'|P Q]; rewrite /IntoSep.
621
622
623
  - 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.
624
Qed.
625
626
Global Instance into_sep_and_persistent_r P P' Q Q' :
  Persistent Q  AndIntoSep Q Q' P P'  IntoSep (P  Q) P' Q'.
627
Proof.
628
  destruct 2 as [Q P P'|Q P]; rewrite /IntoSep.
629
630
631
  - 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.
632
Qed.
633
634


635
636
637
Global Instance into_sep_pure φ ψ : @IntoSep PROP ⌜φ  ψ⌝ ⌜φ⌝ ⌜ψ⌝.
Proof. by rewrite /IntoSep pure_and persistent_and_sep_1. Qed.

638
Global Instance into_sep_embed `{BiEmbedding PROP PROP'} P Q1 Q2 :
639
  IntoSep P Q1 Q2  IntoSep P Q1 Q2.
640
Proof. rewrite /IntoSep -bi_embed_sep=> -> //. Qed.
641

642
643
644
645
646
(* 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 P Q1 Q2 :
  IntoSep P Q1 Q2  IntoSep (bi_affinely P) Q1 Q2 | 20.
Proof. rewrite /IntoSep /= => ->. by rewrite affinely_elim. Qed.
647

648
Global Instance into_sep_plainly `{BiPositive PROP} P Q1 Q2 :
649
650
  IntoSep P Q1 Q2  IntoSep (bi_plainly P) (bi_plainly Q1) (bi_plainly Q2).
Proof. rewrite /IntoSep /= => ->. by rewrite plainly_sep. Qed.
651
Global Instance into_sep_persistently `{BiPositive PROP} P Q1 Q2 :
652
653
  IntoSep P Q1 Q2 
  IntoSep (bi_persistently P) (bi_persistently Q1) (bi_persistently Q2).
654
Proof. rewrite /IntoSep /= => ->. by rewrite persistently_sep. Qed.
655

656
657
658
(* 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. *)
659
Global Instance into_sep_big_sepL_cons {A} (Φ : nat  A  PROP) l x l' :
660
  IsCons l x l' 
661
  IntoSep ([ list] k  y  l, Φ k y)
662
    (Φ 0 x) ([ list] k  y  l', Φ (S k) y).
Robbert Krebbers's avatar
Robbert Krebbers committed
663
Proof. rewrite /IsCons=>->. by rewrite /IntoSep big_sepL_cons. Qed.
664
Global Instance into_sep_big_sepL_app {A} (Φ : nat  A  PROP) l l1 l2 :
665
  IsApp l l1 l2 
666
  IntoSep ([ list] k  y  l, Φ k y)
667
    ([ list] k  y  l1, Φ k y) ([ list] k  y  l2, Φ (length l1 + k) y).
Robbert Krebbers's avatar
Robbert Krebbers committed
668
669
670
671
672
673
674
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.
675
676
677
678
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 :
679
  FromOr P Q1 Q2  FromOr (bi_absorbingly P) (bi_absorbingly Q1) (bi_absorbingly Q2).
680
Proof. rewrite /FromOr=> <-. by rewrite absorbingly_or. Qed.
681
682
Global Instance from_or_plainly P Q1 Q2 :
  FromOr P Q1 Q2  FromOr (bi_plainly P) (bi_plainly Q1) (bi_plainly Q2).
683
Proof. rewrite /FromOr=> <-. by rewrite -plainly_or_2. Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
684
Global Instance from_or_persistently P Q1 Q2 :
685
686
  FromOr P Q1 Q2 
  FromOr (bi_persistently P) (bi_persistently Q1) (bi_persistently Q2).
Robbert Krebbers's avatar
Robbert Krebbers committed
687
Proof. rewrite /FromOr=> <-. by rewrite persistently_or. Qed.
688
Global Instance from_or_embed `{BiEmbedding PROP PROP'} P Q1 Q2 :
689
  FromOr P Q1 Q2  FromOr P Q1 Q2.
690
Proof. by rewrite /FromOr -bi_embed_or => <-. Qed.
691
692
693
694
695
696
Global Instance from_or_bupd `{BUpdFacts PROP} P Q1 Q2 :
  FromOr P Q1 Q2  FromOr (|==> P) (|==> Q1) (|==> Q2).
Proof.
  rewrite /FromOr=><-.
  apply or_elim; apply bupd_mono; auto using or_intro_l, or_intro_r.
Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
697
698
699
700
701
702

(* 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.
703
704
705
706
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 :
707
  IntoOr P Q1 Q2  IntoOr (bi_absorbingly P) (bi_absorbingly Q1) (bi_absorbingly Q2).
708
Proof. rewrite /IntoOr=>->. by rewrite absorbingly_or. Qed.
709
Global Instance into_or_plainly `{BiPlainlyExist PROP} P Q1 Q2 :
710
711
  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
712
Global Instance into_or_persistently P Q1 Q2 :
713
714
  IntoOr P Q1 Q2 
  IntoOr (bi_persistently P) (bi_persistently Q1) (bi_persistently Q2).
Robbert Krebbers's avatar
Robbert Krebbers committed
715
Proof. rewrite /IntoOr=>->. by rewrite persistently_or. Qed.
716
Global Instance into_or_embed `{BiEmbedding PROP PROP'} P Q1 Q2 :
717
  IntoOr P Q1 Q2  IntoOr P Q1 Q2.
718
Proof. by rewrite /IntoOr -bi_embed_or => <-. Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
719
720
721
722
723
724
725

(* 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.
726
727
728
729
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) :
730
  FromExist P Φ  FromExist (bi_absorbingly P) (λ a, bi_absorbingly (Φ a))%I.
731
Proof. rewrite /FromExist=> <-. by rewrite absorbingly_exist. Qed.
732
733
Global Instance from_exist_plainly {A} P (Φ : A  PROP) :
  FromExist P Φ  FromExist (bi_plainly P) (λ a, bi_plainly (Φ a))%I.
734
Proof. rewrite /FromExist=> <-. by rewrite -plainly_exist_2. Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
735
Global Instance from_exist_persistently {A} P (Φ : A  PROP) :
736
  FromExist P Φ  FromExist (bi_persistently P) (λ a, bi_persistently (Φ a))%I.
Robbert Krebbers's avatar
Robbert Krebbers committed
737
Proof. rewrite /FromExist=> <-. by rewrite persistently_exist. Qed.
738
Global Instance from_exist_embed `{BiEmbedding PROP PROP'} {A} P (Φ : A  PROP) :
739
  FromExist P Φ  FromExist P (λ a, ⎡Φ a%I).
740
Proof. by rewrite /FromExist -bi_embed_exist => <-. Qed.
741
742
743
744
745
Global Instance from_exist_bupd `{BUpdFacts PROP} {A} P (Φ : A  PROP) :
  FromExist P Φ  FromExist (|==> P) (λ a, |==> Φ a)%I.
Proof.
  rewrite /FromExist=><-. apply exist_elim=> a. by rewrite -(exist_intro a).
Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
746
747
748
749
750
751
752

(* 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.
753
754
755
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
756
757
758
759
760
761
762
763
764
765
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
766
  eapply (pure_elim φ'); [by rewrite (into_pure P); apply sep_elim_l, _|]=>?.
Robbert Krebbers's avatar
Robbert Krebbers committed
767
768
  rewrite -exist_intro //. apply sep_elim_r, _.
Qed.
769
Global Instance into_exist_absorbingly {A} P (Φ : A  PROP) :
770
  IntoExist P Φ  IntoExist (bi_absorbingly P) (λ a, bi_absorbingly (Φ a))%I.
771
Proof. rewrite /IntoExist=> HP. by rewrite HP absorbingly_exist. Qed.
772
Global Instance into_exist_plainly `{BiPlainlyExist PROP} {A} P (Φ : A  PROP) :
773
774
  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
775
Global Instance into_exist_persistently {A} P (Φ : A  PROP) :
776
  IntoExist P Φ  IntoExist (bi_persistently P) (λ a, bi_persistently (Φ a))%I.
Robbert Krebbers's avatar
Robbert Krebbers committed
777
Proof. rewrite /IntoExist=> HP. by rewrite HP persistently_exist. Qed.
778
Global Instance into_exist_embed `{BiEmbedding PROP PROP'} {A} P (Φ : A  PROP) :
779
  IntoExist P Φ  IntoExist P (λ a, ⎡Φ a%I).
780
Proof. by rewrite /IntoExist -bi_embed_exist => <-. Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
781
782
783
784

(* IntoForall *)
Global Instance into_forall_forall {A} (Φ : A  PROP) : IntoForall ( a, Φ a) Φ.
Proof. by rewrite /IntoForall. Qed.
785
786
787
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.
788
789
790
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
791
Global Instance into_forall_persistently {A} P (Φ : A  PROP) :
792
  IntoForall P Φ  IntoForall (bi_persistently P) (λ a, bi_persistently (Φ a))%I.
Robbert Krebbers's avatar
Robbert Krebbers committed
793
Proof. rewrite /IntoForall=> HP. by rewrite HP persistently_forall. Qed.
794
Global Instance into_forall_embed `{BiEmbedding PROP PROP'} {A} P (Φ : A