class_instances.v 81 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 modality_instances classes.
4
Set Default Proof Using "Type".
Robbert Krebbers's avatar
Robbert Krebbers committed
5
6
Import bi.

7
Section bi_modalities.
Robbert Krebbers's avatar
Robbert Krebbers committed
8
  Context {PROP : bi}.
9

10
11
  Lemma modality_persistently_mixin :
    modality_mixin (@bi_persistently PROP) MIEnvId MIEnvClear.
Robbert Krebbers's avatar
Robbert Krebbers committed
12
  Proof.
13
14
    split; simpl; eauto using equiv_entails_sym, persistently_intro,
      persistently_mono, persistently_sep_2 with typeclass_instances.
Robbert Krebbers's avatar
Robbert Krebbers committed
15
  Qed.
16
17
  Definition modality_persistently :=
    Modality _ modality_persistently_mixin.
Robbert Krebbers's avatar
Robbert Krebbers committed
18

19
20
  Lemma modality_affinely_mixin :
    modality_mixin (@bi_affinely PROP) MIEnvId (MIEnvForall Affine).
Robbert Krebbers's avatar
Robbert Krebbers committed
21
  Proof.
22
    split; simpl; eauto using equiv_entails_sym, affinely_intro, affinely_mono,
23
      affinely_sep_2 with typeclass_instances.
Robbert Krebbers's avatar
Robbert Krebbers committed
24
  Qed.
25
26
  Definition modality_affinely :=
    Modality _ modality_affinely_mixin.
Robbert Krebbers's avatar
Robbert Krebbers committed
27

28
29
  Lemma modality_affinely_persistently_mixin :
    modality_mixin (λ P : PROP,  P)%I MIEnvId MIEnvIsEmpty.
Robbert Krebbers's avatar
Robbert Krebbers committed
30
  Proof.
31
    split; simpl; eauto using equiv_entails_sym, affinely_persistently_emp,
Robbert Krebbers's avatar
Robbert Krebbers committed
32
      affinely_mono, persistently_mono, affinely_persistently_idemp,
33
      affinely_persistently_sep_2 with typeclass_instances.
Robbert Krebbers's avatar
Robbert Krebbers committed
34
  Qed.
35
36
  Definition modality_affinely_persistently :=
    Modality _ modality_affinely_persistently_mixin.
Robbert Krebbers's avatar
Robbert Krebbers committed
37

38
39
  Lemma modality_plainly_mixin :
    modality_mixin (@bi_plainly PROP) (MIEnvForall Plain) MIEnvClear.
Robbert Krebbers's avatar
Robbert Krebbers committed
40
  Proof.
41
42
    split; simpl; split_and?; eauto using equiv_entails_sym, plainly_intro,
      plainly_mono, plainly_and, plainly_sep_2 with typeclass_instances.
Robbert Krebbers's avatar
Robbert Krebbers committed
43
  Qed.
44
45
  Definition modality_plainly :=
    Modality _ modality_plainly_mixin.
Robbert Krebbers's avatar
Robbert Krebbers committed
46

47
48
  Lemma modality_affinely_plainly_mixin :
    modality_mixin (λ P : PROP,  P)%I (MIEnvForall Plain) MIEnvIsEmpty.
Robbert Krebbers's avatar
Robbert Krebbers committed
49
  Proof.
50
51
    split; simpl; split_and?; eauto using equiv_entails_sym,
      affinely_plainly_emp, affinely_intro,
Robbert Krebbers's avatar
Robbert Krebbers committed
52
53
54
      plainly_intro, affinely_mono, plainly_mono, affinely_plainly_idemp,
      affinely_plainly_and, affinely_plainly_sep_2 with typeclass_instances.
  Qed.
55
56
57
  Definition modality_affinely_plainly :=
    Modality _ modality_affinely_plainly_mixin.

58
59
60
61
62
63
64
65
66
67
68
69
  Lemma modality_embed_mixin `{BiEmbedding PROP PROP'} :
    modality_mixin (@bi_embed PROP PROP' _)
      (MIEnvTransform IntoEmbed) (MIEnvTransform IntoEmbed).
  Proof.
    split; simpl; split_and?;
      eauto using equiv_entails_sym, bi_embed_emp, bi_embed_sep, bi_embed_and.
    - intros P Q. rewrite /IntoEmbed=> ->.
      by rewrite bi_embed_affinely bi_embed_persistently.
    - by intros P Q ->.
  Qed.
  Definition modality_embed `{BiEmbedding PROP PROP'} :=
    Modality _ modality_embed_mixin.
70
71
72
73
74
75
76
77
78
End bi_modalities.

Section sbi_modalities.
  Context {PROP : sbi}.

  Lemma modality_laterN_mixin n :
    modality_mixin (@sbi_laterN PROP n)
      (MIEnvTransform (MaybeIntoLaterN false n)) (MIEnvTransform (MaybeIntoLaterN false n)).
  Proof.
79
80
    split; simpl; split_and?; eauto using equiv_entails_sym, laterN_intro,
      laterN_mono, laterN_and, laterN_sep with typeclass_instances.
81
82
83
84
85
    rewrite /MaybeIntoLaterN=> P Q ->. by rewrite laterN_affinely_persistently_2.
  Qed.
  Definition modality_laterN n :=
    Modality _ (modality_laterN_mixin n).
End sbi_modalities.
Robbert Krebbers's avatar
Robbert Krebbers committed
86

Robbert Krebbers's avatar
Robbert Krebbers committed
87
88
89
90
Section bi_instances.
Context {PROP : bi}.
Implicit Types P Q R : PROP.

91
92
93
94
95
(* 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.
96

97
98
99
100
101
(* 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.
102
Global Instance into_absorbingly_default P : IntoAbsorbingly (bi_absorbingly P) P | 100.
103
Proof. by rewrite /IntoAbsorbingly. Qed.
104

105
(* FromAssumption *)
106
Global Instance from_assumption_exact p P : FromAssumption p P P | 0.
107
Proof. by rewrite /FromAssumption /= affinely_persistently_if_elim. Qed.
108

109
Global Instance from_assumption_persistently_r P Q :
110
  FromAssumption true P Q  FromAssumption true P (bi_persistently Q).
Robbert Krebbers's avatar
Robbert Krebbers committed
111
112
Proof.
  rewrite /FromAssumption /= =><-.
113
  by rewrite -{1}affinely_persistently_idemp affinely_elim.
Robbert Krebbers's avatar
Robbert Krebbers committed
114
Qed.
115
116
117
118
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 :
119
  FromAssumption p P Q  FromAssumption p P (bi_absorbingly Q).
120
Proof. rewrite /FromAssumption /= =><-. apply absorbingly_intro. Qed.
121

122
123
124
125
126
127
128
129
130
131
132
133
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.
134
Global Instance from_assumption_plainly_l_false `{BiAffine PROP} P Q :
135
136
137
138
139
  FromAssumption true P Q  FromAssumption false (bi_plainly P) Q.
Proof.
  rewrite /FromAssumption /= =><-.
  by rewrite affine_affinely plainly_elim_persistently.
Qed.
140
Global Instance from_assumption_affinely_persistently_l p P Q :
141
  FromAssumption true P Q  FromAssumption p ( P) Q.
142
Proof. rewrite /FromAssumption /= =><-. by rewrite affinely_persistently_if_elim. Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
143
Global Instance from_assumption_persistently_l_true P Q :
144
  FromAssumption true P Q  FromAssumption true (bi_persistently P) Q.
Robbert Krebbers's avatar
Robbert Krebbers committed
145
Proof. rewrite /FromAssumption /= =><-. by rewrite persistently_idemp. Qed.
146
Global Instance from_assumption_persistently_l_false `{BiAffine PROP} P Q :
147
  FromAssumption true P Q  FromAssumption false (bi_persistently P) Q.
148
149
150
151
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
152
153

Global Instance from_assumption_forall {A} p (Φ : A  PROP) Q x :
154
155
  FromAssumption p (Φ x) Q  FromAssumption p ( x, Φ x) Q.
Proof. rewrite /FromAssumption=> <-. by rewrite forall_elim. Qed.
156
157

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

Ralf Jung's avatar
Ralf Jung committed
161
Global Instance into_pure_pure_and (φ1 φ2 : Prop) P1 P2 :
Ralf Jung's avatar
Ralf Jung committed
162
  IntoPure P1 φ1  IntoPure P2 φ2  IntoPure (P1  P2) (φ1  φ2).
163
Proof. rewrite /IntoPure pure_and. by intros -> ->. Qed.
Ralf Jung's avatar
Ralf Jung committed
164
Global Instance into_pure_pure_or (φ1 φ2 : Prop) P1 P2 :
Ralf Jung's avatar
Ralf Jung committed
165
  IntoPure P1 φ1  IntoPure P2 φ2  IntoPure (P1  P2) (φ1  φ2).
166
Proof. rewrite /IntoPure pure_or. by intros -> ->. Qed.
Ralf Jung's avatar
Ralf Jung committed
167
Global Instance into_pure_pure_impl (φ1 φ2 : Prop) P1 P2 :
168
169
  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
170
171
172
173
174
175
176
177
178
179
180

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
181
Global Instance into_pure_pure_wand (φ1 φ2 : Prop) P1 P2 :
182
183
184
185
186
187
188
  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.
189

190
191
192
Global Instance into_pure_affinely P φ :
  IntoPure P φ  IntoPure (bi_affinely P) φ.
Proof. rewrite /IntoPure=> ->. apply affinely_elim. Qed.
193
Global Instance into_pure_absorbingly P φ : IntoPure P φ  IntoPure (bi_absorbingly P) φ.
194
Proof. rewrite /IntoPure=> ->. by rewrite absorbingly_pure. Qed.
195
196
Global Instance into_pure_plainly P φ : IntoPure P φ  IntoPure (bi_plainly P) φ.
Proof. rewrite /IntoPure=> ->. apply: plainly_elim. Qed.
197
198
Global Instance into_pure_persistently P φ :
  IntoPure P φ  IntoPure (bi_persistently P) φ.
199
Proof. rewrite /IntoPure=> ->. apply: persistently_elim. Qed.
200
Global Instance into_pure_embed `{BiEmbedding PROP PROP'} P φ :
201
  IntoPure P φ  IntoPure P φ.
202
Proof. rewrite /IntoPure=> ->. by rewrite bi_embed_pure. Qed.
203

204
(* FromPure *)
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
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.
254
255
Qed.

256
Global Instance from_pure_plainly P φ :
257
  FromPure false P φ  FromPure false (bi_plainly P) φ.
258
Proof. rewrite /FromPure=> <-. by rewrite plainly_pure. Qed.
259
260
261
262
263
264
265
266
267
268
269
270
271
272
273
274
275
276
277
278
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.

279
(* IntoPersistent *)
280
Global Instance into_persistent_persistently p P Q :
281
  IntoPersistent true P Q  IntoPersistent p (bi_persistently P) Q | 0.
Robbert Krebbers's avatar
Robbert Krebbers committed
282
283
284
285
Proof.
  rewrite /IntoPersistent /= => ->.
  destruct p; simpl; auto using persistently_idemp_1.
Qed.
286
287
288
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.
289
Global Instance into_persistent_embed `{BiEmbedding PROP PROP'} p P Q :
290
291
  IntoPersistent p P Q  IntoPersistent p P Q | 0.
Proof.
292
  rewrite /IntoPersistent -bi_embed_persistently -bi_embed_persistently_if=> -> //.
293
Qed.
294
Global Instance into_persistent_here P : IntoPersistent true P P | 1.
Robbert Krebbers's avatar
Robbert Krebbers committed
295
Proof. by rewrite /IntoPersistent. Qed.
296
297
Global Instance into_persistent_persistent P :
  Persistent P  IntoPersistent false P P | 100.
298
Proof. intros. by rewrite /IntoPersistent. Qed.
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
(* FromModal *)
Global Instance from_modal_affinely P :
  FromModal modality_affinely (bi_affinely P) P | 2.
Proof. by rewrite /FromModal. Qed.

Global Instance from_modal_persistently P :
  FromModal modality_persistently (bi_persistently P) P | 2.
Proof. by rewrite /FromModal. Qed.
Global Instance from_modal_affinely_persistently P :
  FromModal modality_affinely_persistently ( P) P | 1.
Proof. by rewrite /FromModal. Qed.
Global Instance from_modal_affinely_persistently_affine_bi P :
  BiAffine PROP  FromModal modality_persistently ( P) P | 0.
Proof. intros. by rewrite /FromModal /= affine_affinely. Qed.

Global Instance from_modal_plainly P :
  FromModal modality_plainly (bi_plainly P) P | 2.
Proof. by rewrite /FromModal. Qed.
Global Instance from_modal_affinely_plainly P :
  FromModal modality_affinely_plainly ( P) P | 1.
Proof. by rewrite /FromModal. Qed.
Global Instance from_modal_affinely_plainly_affine_bi P :
  BiAffine PROP  FromModal modality_plainly ( P) P | 0.
Proof. intros. by rewrite /FromModal /= affine_affinely. Qed.

Global Instance from_modal_affinely_embed `{BiEmbedding PROP PROP'} P Q :
  FromModal modality_affinely P Q 
  FromModal modality_affinely P Q.
Proof. rewrite /FromModal /= =><-. by rewrite bi_embed_affinely. Qed.
Global Instance from_modal_persistently_embed `{BiEmbedding PROP PROP'} P Q :
  FromModal modality_persistently P Q 
  FromModal modality_persistently P Q.
Proof. rewrite /FromModal /= =><-. by rewrite bi_embed_persistently. Qed.
Global Instance from_modal_affinely_persistently_embed `{BiEmbedding PROP PROP'} P Q :
  FromModal modality_affinely_persistently P Q 
  FromModal modality_affinely_persistently P Q.
Proof.
  rewrite /FromModal /= =><-. by rewrite bi_embed_affinely bi_embed_persistently.
Qed.
Global Instance from_modal_plainly_embed `{BiEmbedding PROP PROP'} P Q :
  FromModal modality_plainly P Q 
  FromModal modality_plainly P Q.
Proof. rewrite /FromModal /= =><-. by rewrite bi_embed_plainly. Qed.
Global Instance from_modal_affinely_plainly_embed `{BiEmbedding PROP PROP'} P Q :
  FromModal modality_affinely_plainly P Q 
  FromModal modality_affinely_plainly P Q.
Proof.
  rewrite /FromModal /= =><-. by rewrite bi_embed_affinely bi_embed_plainly.
348
Qed.
349

Robbert Krebbers's avatar
Robbert Krebbers committed
350
351
352
(* IntoWand *)
Global Instance into_wand_wand p q P Q P' :
  FromAssumption q P P'  IntoWand p q (P' - Q) P Q.
353
Proof.
354
  rewrite /FromAssumption /IntoWand=> HP. by rewrite HP affinely_persistently_if_elim.
Robbert Krebbers's avatar
Robbert Krebbers committed
355
Qed.
356
357
Global Instance into_wand_impl_false_false P Q P' :
  Absorbing P'  Absorbing (P'  Q) 
Robbert Krebbers's avatar
Robbert Krebbers committed
358
359
  FromAssumption false P P'  IntoWand false false (P'  Q) P Q.
Proof.
360
  rewrite /FromAssumption /IntoWand /= => ?? ->. apply wand_intro_r.
Robbert Krebbers's avatar
Robbert Krebbers committed
361
362
363
  by rewrite sep_and impl_elim_l.
Qed.
Global Instance into_wand_impl_false_true P Q P' :
364
  Absorbing P'  FromAssumption true P P' 
Robbert Krebbers's avatar
Robbert Krebbers committed
365
  IntoWand false true (P'  Q) P Q.
366
Proof.
367
  rewrite /IntoWand /FromAssumption /= => ? HP. apply wand_intro_l.
368
369
  rewrite -(affinely_persistently_idemp P) HP.
  by rewrite -persistently_and_affinely_sep_l persistently_elim impl_elim_r.
370
Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
371
Global Instance into_wand_impl_true_false P Q P' :
372
  Affine P'  FromAssumption false P P' 
Robbert Krebbers's avatar
Robbert Krebbers committed
373
  IntoWand true false (P'  Q) P Q.
374
Proof.
375
  rewrite /FromAssumption /IntoWand /= => ? HP. apply wand_intro_r.
376
377
  rewrite -persistently_and_affinely_sep_l HP -{2}(affine_affinely P') -affinely_and_lr.
  by rewrite affinely_persistently_elim impl_elim_l.
378
Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
379
380
Global Instance into_wand_impl_true_true P Q P' :
  FromAssumption true P P'  IntoWand true true (P'  Q) P Q.
381
Proof.
Robbert Krebbers's avatar
Robbert Krebbers committed
382
  rewrite /FromAssumption /IntoWand /= => <-. apply wand_intro_l.
383
384
  rewrite -{1}(affinely_persistently_idemp P) -and_sep_affinely_persistently.
  by rewrite -affinely_persistently_and impl_elim_r affinely_persistently_elim.
385
Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
386
387
388
389
390
391
392
393

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.

394
395
396
397
398
399
400
401
402
403
404
405
406
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.
407

Robbert Krebbers's avatar
Robbert Krebbers committed
408
409
410
411
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.

412
413
414
415
416
417
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.
418
Global Instance into_wand_plainly_false `{!BiAffine PROP} q R P Q :
419
420
421
422
423
424
  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
425
Global Instance into_wand_persistently_true q R P Q :
426
  IntoWand true q R P Q  IntoWand true q (bi_persistently R) P Q.
Robbert Krebbers's avatar
Robbert Krebbers committed
427
Proof. by rewrite /IntoWand /= persistently_idemp. Qed.
428
Global Instance into_wand_persistently_false `{!BiAffine PROP} q R P Q :
429
  IntoWand false q R P Q  IntoWand false q (bi_persistently R) P Q.
430
Proof. by rewrite /IntoWand persistently_elim. Qed.
431
Global Instance into_wand_embed `{BiEmbedding PROP PROP'} p q R P Q :
432
433
  IntoWand p q R P Q  IntoWand p q R P Q.
Proof.
434
435
  rewrite /IntoWand -!bi_embed_persistently_if -!bi_embed_affinely_if
          -bi_embed_wand => -> //.
436
Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
437

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

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

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

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

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

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

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

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

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

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

560
Global Instance into_and_sep `{BiPositive PROP} P Q : IntoAnd true (P  Q) P Q.
561
562
563
Proof.
  by rewrite /IntoAnd /= persistently_sep -and_sep_persistently persistently_and.
Qed.
564
Global Instance into_and_sep_affine P Q :
Ralf Jung's avatar
Ralf Jung committed
565
  TCOr (Affine P) (Absorbing Q)  TCOr (Absorbing P) (Affine Q) 
566
567
  IntoAnd true (P  Q) P Q.
Proof. intros. by rewrite /IntoAnd /= sep_and. Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
568
569

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

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

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

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

632
633
634
Global Instance into_sep_pure φ ψ : @IntoSep PROP ⌜φ  ψ⌝ ⌜φ⌝ ⌜ψ⌝.
Proof. by rewrite /IntoSep pure_and persistent_and_sep_1. Qed.

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

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

649
Global Instance into_sep_plainly `{BiPositive PROP} P Q1 Q2 :
650
651
  IntoSep P Q1 Q2  IntoSep (bi_plainly P) (bi_plainly Q1) (bi_plainly Q2).
Proof. rewrite /IntoSep /= => ->. by rewrite plainly_sep. Qed.
652
653
Global Instance into_sep_plainly_affine P Q1 Q2 :
  IntoSep P Q1 Q2 
Ralf Jung's avatar
Ralf Jung committed
654
  TCOr (Affine Q1) (Absorbing Q2)  TCOr (Absorbing Q1) (Affine Q2) 
655
656
  IntoSep (bi_plainly P) (bi_plainly Q1) (bi_plainly Q2).
Proof.
Ralf Jung's avatar
Ralf Jung committed
657
  rewrite /IntoSep /= => -> ??. by rewrite sep_and plainly_and plainly_and_sep_l_1.
658
659
Qed.

660
Global Instance into_sep_persistently `{BiPositive PROP} P Q1 Q2 :
661
662
  IntoSep P Q1 Q2 
  IntoSep (bi_persistently P) (bi_persistently Q1) (bi_persistently Q2).
663
Proof. rewrite /IntoSep /= => ->. by rewrite persistently_sep. Qed.
664
665
Global Instance into_sep_persistently_affine P Q1 Q2 :
  IntoSep P Q1 Q2 
Ralf Jung's avatar
Ralf Jung committed
666
  TCOr (Affine Q1) (Absorbing Q2)  TCOr (Absorbing Q1) (Affine Q2) 
667
668
  IntoSep (bi_persistently P) (bi_persistently Q1) (bi_persistently Q2).
Proof.
Ralf Jung's avatar
Ralf Jung committed
669
  rewrite /IntoSep /= => -> ??.
670
671
672
673
  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 
Ralf Jung's avatar
Ralf Jung committed
674
  TCOr (Affine Q1) (Absorbing Q2)  TCOr (Absorbing Q1) (Affine Q2) 
675
676
  IntoSep ( P) ( Q1) ( Q2).
Proof.
Ralf Jung's avatar
Ralf Jung committed
677
  rewrite /IntoSep /= => -> ??.
678
679
  by rewrite sep_and affinely_persistently_and and_sep_affinely_persistently.
Qed.
680

681
682
683
(* 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. *)
684
Global Instance into_sep_big_sepL_cons {A} (Φ : nat  A  PROP) l x l' :
685
  IsCons l x l' 
686
  IntoSep ([ list] k  y  l, Φ k y)
687
    (Φ 0 x) ([ list] k  y  l', Φ (S k) y).
Robbert Krebbers's avatar
Robbert Krebbers committed
688
Proof. rewrite /IsCons=>->. by rewrite /IntoSep big_sepL_cons. Qed.
689
Global Instance into_sep_big_sepL_app {A} (Φ : nat  A  PROP) l l1 l2 :
690
  IsApp l l1 l2 
691
  IntoSep ([ list] k  y  l, Φ k y)
692
    ([ list] k  y  l1, Φ k y) ([ list] k  y  l2, Φ (length l1 + k) y).
Robbert Krebbers's avatar
Robbert Krebbers committed
693
694
695
696
697
698
699
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.
700
701
702
703
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 :
704
  FromOr P Q1 Q2  FromOr (bi_absorbingly P) (bi_absorbingly Q1) (bi_absorbingly Q2).
705
Proof. rewrite /FromOr=> <-. by rewrite absorbingly_or. Qed.
706
707
Global Instance from_or_plainly P Q1 Q2 :
  FromOr P Q1 Q2  FromOr (bi_plainly P) (bi_plainly Q1) (bi_plainly Q2).
708
Proof. rewrite /FromOr=> <-. by rewrite -plainly_or_2. Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
709
Global Instance from_or_persistently P Q1 Q2 :
710
711
  FromOr P Q1 Q2 
  FromOr (bi_persistently P) (bi_persistently Q1) (bi_persistently Q2).
Robbert Krebbers's avatar
Robbert Krebbers committed
712
Proof. rewrite /FromOr=> <-. by rewrite persistently_or. Qed.
713
Global Instance from_or_embed `{BiEmbedding PROP PROP'} P Q1 Q2 :
714
  FromOr P Q1 Q2  FromOr P Q1 Q2.
715
Proof. by rewrite /FromOr -bi_embed_or => <-. Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
716
717
718
719
720
721

(* 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.
722
723
724
725
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 :
726
  IntoOr P Q1 Q2  IntoOr (bi_absorbingly P) (bi_absorbingly Q1) (bi_absorbingly Q2).
727
Proof. rewrite /IntoOr=>->. by rewrite absorbingly_or. Qed.
728
Global Instance into_or_plainly `{BiPlainlyExist PROP} P Q1 Q2 :
729
730
  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
731
Global Instance into_or_persistently P Q1 Q2 :
732
733
  IntoOr P Q1 Q2 
  IntoOr (bi_persistently P) (bi_persistently Q1) (bi_persistently Q2).
Robbert Krebbers's avatar
Robbert Krebbers committed
734
Proof. rewrite /IntoOr=>->. by rewrite persistently_or. Qed.
735
Global Instance into_or_embed `{BiEmbedding PROP PROP'} P Q1 Q2 :
736
  IntoOr P Q1 Q2  IntoOr P Q1 Q2.
737
Proof. by rewrite /IntoOr -bi_embed_or => <-. Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
738
739
740
741
742
743
744

(* 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.
745
746
747
748
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) :
749
  FromExist P Φ  FromExist (bi_absorbingly P) (λ a, bi_absorbingly (Φ a))%I.
750
Proof. rewrite /FromExist=> <-. by rewrite absorbingly_exist. Qed.
751
752
Global Instance from_exist_plainly {A} P (Φ : A  PROP) :
  FromExist P Φ  FromExist (bi_plainly P) (λ a, bi_plainly (Φ a))%I.