class_instances_bi.v 42.4 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 Import modality_instances classes ltac_tactics.
4
Set Default Proof Using "Type".
Robbert Krebbers's avatar
Robbert Krebbers committed
5
6
7
8
9
10
Import bi.

Section bi_instances.
Context {PROP : bi}.
Implicit Types P Q R : PROP.

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
(* AsEmpValid *)
Global Instance as_emp_valid_emp_valid {PROP : bi} (P : PROP) : AsEmpValid0 (bi_emp_valid P) P | 0.
Proof. by rewrite /AsEmpValid. Qed.
Global Instance as_emp_valid_entails {PROP : bi} (P Q : PROP) : AsEmpValid0 (P  Q) (P - Q).
Proof. split. apply bi.entails_wand. apply bi.wand_entails. Qed.
Global Instance as_emp_valid_equiv {PROP : bi} (P Q : PROP) : AsEmpValid0 (P  Q) (P - Q).
Proof. split. apply bi.equiv_wand_iff. apply bi.wand_iff_equiv. Qed.

Global Instance as_emp_valid_forall {A : Type} (φ : A  Prop) (P : A  PROP) :
  ( x, AsEmpValid (φ x) (P x))  AsEmpValid ( x, φ x) ( x, P x).
Proof.
  rewrite /AsEmpValid=>H1. split=>H2.
  - apply bi.forall_intro=>?. apply H1, H2.
  - intros x. apply H1. revert H2. by rewrite (bi.forall_elim x).
Qed.

(* We add a useless hypothesis [BiEmbed PROP PROP'] in order to make
   sure this instance is not used when there is no embedding between
   PROP and PROP'.
   The first [`{BiEmbed PROP PROP'}] is not considered as a premise by
   Coq TC search mechanism because the rest of the hypothesis is dependent
   on it. *)
Global Instance as_emp_valid_embed `{BiEmbed PROP PROP'} (φ : Prop) (P : PROP) :
  BiEmbed PROP PROP' 
  AsEmpValid0 φ P  AsEmpValid φ P.
Proof. rewrite /AsEmpValid0 /AsEmpValid=> _ ->. rewrite embed_emp_valid //. Qed.

38
39
40
(* FromAffinely *)
Global Instance from_affinely_affine P : Affine P  FromAffinely P P.
Proof. intros. by rewrite /FromAffinely affinely_elim. Qed.
41
Global Instance from_affinely_default P : FromAffinely (<affine> P) P | 100.
42
Proof. by rewrite /FromAffinely. Qed.
43
44
45
Global Instance from_affinely_intuitionistically P :
  FromAffinely ( P) (<pers> P) | 100.
Proof. by rewrite /FromAffinely. Qed.
46

47
48
49
50
51
(* 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.
52
Global Instance into_absorbingly_intuitionistically P :
53
  IntoAbsorbingly (<pers> P) ( P) | 2.
54
55
56
Proof.
  by rewrite /IntoAbsorbingly -absorbingly_intuitionistically_into_persistently.
Qed.
57
Global Instance into_absorbingly_default P : IntoAbsorbingly (<absorb> P) P | 100.
58
Proof. by rewrite /IntoAbsorbingly. Qed.
59

60
(* FromAssumption *)
61
Global Instance from_assumption_exact p P : FromAssumption p P P | 0.
62
Proof. by rewrite /FromAssumption /= intuitionistically_if_elim. Qed.
63

64
Global Instance from_assumption_persistently_r P Q :
65
  FromAssumption true P Q  KnownRFromAssumption true P (<pers> Q).
Robbert Krebbers's avatar
Robbert Krebbers committed
66
Proof.
67
  rewrite /KnownRFromAssumption /FromAssumption /= =><-.
68
  apply intuitionistically_persistent.
Robbert Krebbers's avatar
Robbert Krebbers committed
69
Qed.
70
Global Instance from_assumption_affinely_r P Q :
71
  FromAssumption true P Q  KnownRFromAssumption true P (<affine> Q).
72
73
74
75
Proof.
  rewrite /KnownRFromAssumption /FromAssumption /= =><-.
  by rewrite affinely_idemp.
Qed.
76
77
78
79
80
81
Global Instance from_assumption_intuitionistically_r P Q :
  FromAssumption true P Q  KnownRFromAssumption true P ( Q).
Proof.
  rewrite /KnownRFromAssumption /FromAssumption /= =><-.
  by rewrite intuitionistically_idemp.
Qed.
82
Global Instance from_assumption_absorbingly_r p P Q :
83
  FromAssumption p P Q  KnownRFromAssumption p P (<absorb> Q).
84
85
86
87
Proof.
  rewrite /KnownRFromAssumption /FromAssumption /= =><-.
  apply absorbingly_intro.
Qed.
88

89
Global Instance from_assumption_intuitionistically_l p P Q :
90
91
92
  FromAssumption true P Q  KnownLFromAssumption p ( P) Q.
Proof.
  rewrite /KnownLFromAssumption /FromAssumption /= =><-.
93
  by rewrite intuitionistically_if_elim.
94
Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
95
Global Instance from_assumption_persistently_l_true P Q :
96
  FromAssumption true P Q  KnownLFromAssumption true (<pers> P) Q.
97
98
Proof.
  rewrite /KnownLFromAssumption /FromAssumption /= =><-.
Ralf Jung's avatar
Ralf Jung committed
99
  rewrite intuitionistically_persistently_elim //.
100
Qed.
101
Global Instance from_assumption_persistently_l_false `{BiAffine PROP} P Q :
102
  FromAssumption true P Q  KnownLFromAssumption false (<pers> P) Q.
103
104
Proof.
  rewrite /KnownLFromAssumption /FromAssumption /= =><-.
Ralf Jung's avatar
Ralf Jung committed
105
  by rewrite intuitionistically_into_persistently.
106
Qed.
107
Global Instance from_assumption_affinely_l_true p P Q :
108
  FromAssumption p P Q  KnownLFromAssumption p (<affine> P) Q.
109
110
111
112
Proof.
  rewrite /KnownLFromAssumption /FromAssumption /= =><-.
  by rewrite affinely_elim.
Qed.
113
114
115
116
117
118
Global Instance from_assumption_intuitionistically_l_true p P Q :
  FromAssumption p P Q  KnownLFromAssumption p ( P) Q.
Proof.
  rewrite /KnownLFromAssumption /FromAssumption /= =><-.
  by rewrite intuitionistically_elim.
Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
119
120

Global Instance from_assumption_forall {A} p (Φ : A  PROP) Q x :
121
122
123
124
125
  FromAssumption p (Φ x) Q  KnownLFromAssumption p ( x, Φ x) Q.
Proof.
  rewrite /KnownLFromAssumption /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
  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.
156
  rewrite -{1}(persistent_absorbingly_affinely ⌜φ1%I) absorbingly_sep_l
157
158
          bi.wand_elim_r absorbing //.
Qed.
159

160
Global Instance into_pure_affinely P φ : IntoPure P φ  IntoPure (<affine> P) φ.
161
Proof. rewrite /IntoPure=> ->. apply affinely_elim. Qed.
162
163
164
Global Instance into_pure_intuitionistically P φ :
  IntoPure P φ  IntoPure ( P) φ.
Proof. rewrite /IntoPure=> ->. apply intuitionistically_elim. Qed.
165
Global Instance into_pure_absorbingly P φ : IntoPure P φ  IntoPure (<absorb> P) φ.
166
167
Proof. rewrite /IntoPure=> ->. by rewrite absorbingly_pure. Qed.
Global Instance into_pure_persistently P φ :
168
  IntoPure P φ  IntoPure (<pers> P) φ.
169
Proof. rewrite /IntoPure=> ->. apply: persistently_elim. Qed.
170
Global Instance into_pure_embed `{BiEmbed PROP PROP'} P φ :
171
  IntoPure P φ  IntoPure P φ.
172
Proof. rewrite /IntoPure=> ->. by rewrite 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_persistently P a φ :
227
  FromPure true P φ  FromPure a (<pers> P) φ.
228
229
Proof.
  rewrite /FromPure=> <- /=.
Ralf Jung's avatar
Ralf Jung committed
230
  by rewrite persistently_affinely_elim affinely_if_elim persistently_pure.
231
232
Qed.
Global Instance from_pure_affinely_true P φ :
233
  FromPure true P φ  FromPure true (<affine> P) φ.
234
235
Proof. rewrite /FromPure=><- /=. by rewrite affinely_idemp. Qed.
Global Instance from_pure_affinely_false P φ `{!Affine P} :
236
  FromPure false P φ  FromPure false (<affine> P) φ.
237
Proof. rewrite /FromPure /= affine_affinely //. Qed.
238
239
240
Global Instance from_pure_intuitionistically_true P φ :
  FromPure true P φ  FromPure true ( P) φ.
Proof.
Ralf Jung's avatar
Ralf Jung committed
241
  rewrite /FromPure=><- /=. rewrite intuitionistically_affinely_elim.
242
243
  rewrite {1}(persistent ⌜φ⌝%I) //.
Qed.
244

245
246
247
248
249
250
Global Instance from_pure_absorbingly P φ p :
  FromPure true P φ  FromPure p (<absorb> P) φ.
Proof.
  rewrite /FromPure=> <- /=.
  rewrite persistent_absorbingly_affinely affinely_if_elim //.
Qed.
251
Global Instance from_pure_embed `{BiEmbed PROP PROP'} a P φ :
252
  FromPure a P φ  FromPure a P φ.
Robbert Krebbers's avatar
Robbert Krebbers committed
253
Proof. rewrite /FromPure=> <-. by rewrite -embed_pure embed_affinely_if_2. Qed.
254

255
(* IntoPersistent *)
256
Global Instance into_persistent_persistently p P Q :
257
  IntoPersistent true P Q  IntoPersistent p (<pers> P) Q | 0.
Robbert Krebbers's avatar
Robbert Krebbers committed
258
259
260
261
Proof.
  rewrite /IntoPersistent /= => ->.
  destruct p; simpl; auto using persistently_idemp_1.
Qed.
262
Global Instance into_persistent_affinely p P Q :
263
  IntoPersistent p P Q  IntoPersistent p (<affine> P) Q | 0.
264
Proof. rewrite /IntoPersistent /= => <-. by rewrite affinely_elim. Qed.
265
Global Instance into_persistent_intuitionistically p P Q :
266
267
268
269
270
  IntoPersistent true P Q  IntoPersistent p ( P) Q | 0.
Proof.
  rewrite /IntoPersistent /= =><-.
  destruct p; simpl;
    eauto using persistently_mono, intuitionistically_elim,
Ralf Jung's avatar
Ralf Jung committed
271
    intuitionistically_into_persistently_1.
272
Qed.
273
Global Instance into_persistent_embed `{BiEmbed PROP PROP'} p P Q :
274
275
  IntoPersistent p P Q  IntoPersistent p P Q | 0.
Proof.
276
  rewrite /IntoPersistent -embed_persistently -embed_persistently_if=> -> //.
277
Qed.
278
Global Instance into_persistent_here P : IntoPersistent true P P | 1.
Robbert Krebbers's avatar
Robbert Krebbers committed
279
Proof. by rewrite /IntoPersistent. Qed.
280
281
Global Instance into_persistent_persistent P :
  Persistent P  IntoPersistent false P P | 100.
282
Proof. intros. by rewrite /IntoPersistent. Qed.
283

284
285
(* FromModal *)
Global Instance from_modal_affinely P :
286
  FromModal modality_affinely (<affine> P) (<affine> P) P | 2.
287
288
289
Proof. by rewrite /FromModal. Qed.

Global Instance from_modal_persistently P :
290
  FromModal modality_persistently (<pers> P) (<pers> P) P | 2.
291
Proof. by rewrite /FromModal. Qed.
292
293
Global Instance from_modal_intuitionistically P :
  FromModal modality_intuitionistically ( P) ( P) P | 1.
294
Proof. by rewrite /FromModal. Qed.
295
Global Instance from_modal_intuitionistically_affine_bi P :
296
  BiAffine PROP  FromModal modality_persistently ( P) ( P) P | 0.
Ralf Jung's avatar
Ralf Jung committed
297
298
299
Proof.
  intros. by rewrite /FromModal /= intuitionistically_into_persistently.
Qed.
300

301
Global Instance from_modal_absorbingly P :
302
  FromModal modality_id (<absorb> P) (<absorb> P) P.
303
304
305
Proof. by rewrite /FromModal /= -absorbingly_intro. Qed.

(* When having a modality nested in an embedding, e.g. [ ⎡|==> P⎤ ], we prefer
306
the embedding over the modality. *)
307
308
Global Instance from_modal_embed `{BiEmbed PROP PROP'} (P : PROP) :
  FromModal (@modality_embed PROP PROP' _) P P P.
309
310
Proof. by rewrite /FromModal. Qed.

311
Global Instance from_modal_id_embed `{BiEmbed PROP PROP'} `(sel : A) P Q :
312
  FromModal modality_id sel P Q 
313
  FromModal modality_id sel P Q | 100.
314
315
Proof. by rewrite /FromModal /= =><-. Qed.

316
Global Instance from_modal_affinely_embed `{BiEmbed PROP PROP'} `(sel : A) P Q :
317
  FromModal modality_affinely sel P Q 
318
  FromModal modality_affinely sel P Q | 100.
Robbert Krebbers's avatar
Robbert Krebbers committed
319
Proof. rewrite /FromModal /= =><-. by rewrite embed_affinely_2. Qed.
320
Global Instance from_modal_persistently_embed `{BiEmbed PROP PROP'} `(sel : A) P Q :
321
  FromModal modality_persistently sel P Q 
322
  FromModal modality_persistently sel P Q | 100.
323
Proof. rewrite /FromModal /= =><-. by rewrite embed_persistently. Qed.
324
325
326
Global Instance from_modal_intuitionistically_embed `{BiEmbed PROP PROP'} `(sel : A) P Q :
  FromModal modality_intuitionistically sel P Q 
  FromModal modality_intuitionistically sel P Q | 100.
Robbert Krebbers's avatar
Robbert Krebbers committed
327
Proof. rewrite /FromModal /= =><-. by rewrite embed_intuitionistically_2. Qed.
328

Robbert Krebbers's avatar
Robbert Krebbers committed
329
330
331
(* IntoWand *)
Global Instance into_wand_wand p q P Q P' :
  FromAssumption q P P'  IntoWand p q (P' - Q) P Q.
332
Proof.
333
  rewrite /FromAssumption /IntoWand=> HP. by rewrite HP intuitionistically_if_elim.
Robbert Krebbers's avatar
Robbert Krebbers committed
334
Qed.
335
336
Global Instance into_wand_impl_false_false P Q P' :
  Absorbing P'  Absorbing (P'  Q) 
Robbert Krebbers's avatar
Robbert Krebbers committed
337
338
  FromAssumption false P P'  IntoWand false false (P'  Q) P Q.
Proof.
339
  rewrite /FromAssumption /IntoWand /= => ?? ->. apply wand_intro_r.
Robbert Krebbers's avatar
Robbert Krebbers committed
340
341
342
  by rewrite sep_and impl_elim_l.
Qed.
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 -(intuitionistically_idemp P) HP.
  by rewrite -persistently_and_intuitionistically_sep_l persistently_elim impl_elim_r.
349
Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
350
Global Instance into_wand_impl_true_false P Q P' :
351
  Affine P'  FromAssumption false P P' 
Robbert Krebbers's avatar
Robbert Krebbers committed
352
  IntoWand true false (P'  Q) P Q.
353
Proof.
354
  rewrite /FromAssumption /IntoWand /= => ? HP. apply wand_intro_r.
355
  rewrite HP sep_and intuitionistically_elim impl_elim_l //.
356
Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
357
358
Global Instance into_wand_impl_true_true P Q P' :
  FromAssumption true P P'  IntoWand true true (P'  Q) P Q.
359
Proof.
Robbert Krebbers's avatar
Robbert Krebbers committed
360
  rewrite /FromAssumption /IntoWand /= => <-. apply wand_intro_l.
361
  rewrite sep_and [( (_  _))%I]intuitionistically_elim impl_elim_r //.
362
Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
363
364
365
366
367
368
369
370

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.

371
372
373
Global Instance into_wand_forall_prop_true p (φ : Prop) P :
  IntoWand p true ( _ : φ, P)  φ  P.
Proof.
374
375
  rewrite /IntoWand (intuitionistically_if_elim p) /=
          -impl_wand_intuitionistically -pure_impl_forall
376
377
378
379
380
381
          bi.persistently_elim //.
Qed.
Global Instance into_wand_forall_prop_false p (φ : Prop) P :
  Absorbing P  IntoWand p false ( _ : φ, P)  φ  P.
Proof.
  intros ?.
382
  rewrite /IntoWand (intuitionistically_if_elim p) /= pure_wand_forall //.
383
Qed.
384

Robbert Krebbers's avatar
Robbert Krebbers committed
385
386
387
388
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.

389
390
391
392
393
394
395
396
397
398
399
400
401
402
403
404
405
406
407
408
409
410
411
412
413
414
415
416
417
418
419
420
Global Instance into_wand_affine p q R P Q :
  IntoWand p q R P Q  IntoWand p q (<affine> R) (<affine> P) (<affine> Q).
Proof.
  rewrite /IntoWand /= => HR. apply wand_intro_r. destruct p; simpl in *.
  - rewrite (affinely_elim R) -(affine_affinely ( R)%I) HR. destruct q; simpl in *.
    + rewrite (affinely_elim P) -{2}(affine_affinely ( P)%I).
      by rewrite affinely_sep_2 wand_elim_l.
    + by rewrite affinely_sep_2 wand_elim_l.
  - rewrite HR. destruct q; simpl in *.
    + rewrite (affinely_elim P) -{2}(affine_affinely ( P)%I).
      by rewrite affinely_sep_2 wand_elim_l.
    + by rewrite affinely_sep_2 wand_elim_l.
Qed.
(* In case the argument is affine, but the wand resides in the spatial context,
we can only eliminate the affine modality in the argument. This would lead to
the following instance:

  IntoWand false q R P Q → IntoWand' false q R (<affine> P) Q.

This instance is redundant, however, since the elimination of the affine
modality is already covered by the [IntoAssumption] instances that are used at
the leaves of the instance search for [IntoWand]. *)
Global Instance into_wand_affine_args q R P Q :
  IntoWand true q R P Q  IntoWand' true q R (<affine> P) (<affine> Q).
Proof.
  rewrite /IntoWand' /IntoWand /= => HR. apply wand_intro_r.
  rewrite -(affine_affinely ( R)%I) HR. destruct q; simpl.
  - rewrite (affinely_elim P) -{2}(affine_affinely ( P)%I).
    by rewrite affinely_sep_2 wand_elim_l.
  - by rewrite affinely_sep_2 wand_elim_l.
Qed.

421
Global Instance into_wand_intuitionistically p q R P Q :
422
423
  IntoWand true q R P Q  IntoWand p q ( R) P Q.
Proof. rewrite /IntoWand /= => ->. by rewrite {1}intuitionistically_if_elim. Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
424
Global Instance into_wand_persistently_true q R P Q :
425
  IntoWand true q R P Q  IntoWand true q (<pers> R) P Q.
Ralf Jung's avatar
Ralf Jung committed
426
Proof. by rewrite /IntoWand /= intuitionistically_persistently_elim. Qed.
427
428
429
Global Instance into_wand_persistently_false q R P Q :
  Absorbing R  IntoWand false q R P Q  IntoWand false q (<pers> R) P Q.
Proof. intros ?. by rewrite /IntoWand persistently_elim. Qed.
430

431
432
433
Global Instance into_wand_embed `{BiEmbed PROP PROP'} p q R P Q :
  IntoWand p q R P Q  IntoWand p q R P Q.
Proof. by rewrite /IntoWand !embed_intuitionistically_if_2 -embed_wand=> ->. Qed.
434
435
436
437
438
439
440
441
442
443
444
445
446
447
448
449
450
451
452
453
454
455
456

(* There are two versions for [IntoWand ⎡RR⎤ ...] with the argument being
[<affine> ⎡PP⎤]. When the wand [⎡RR⎤] resides in the intuitionistic context
the result of wand elimination will have the affine modality. Otherwise, it
won't. Note that when the wand [⎡RR⎤] is under an affine modality, the instance
[into_wand_affine] would already have been used. *)
Global Instance into_wand_affine_embed_true `{BiEmbed PROP PROP'} q (PP QQ RR : PROP) :
  IntoWand true q RR PP QQ  IntoWand true q RR (<affine> PP) (<affine> QQ) | 100.
Proof.
  rewrite /IntoWand /=.
  rewrite -(intuitionistically_idemp  _ %I) embed_intuitionistically_2=> ->.
  apply bi.wand_intro_l. destruct q; simpl.
  - rewrite affinely_elim  -(intuitionistically_idemp  _ %I).
    rewrite embed_intuitionistically_2 intuitionistically_sep_2 -embed_sep.
    by rewrite wand_elim_r intuitionistically_affinely.
  - by rewrite intuitionistically_affinely affinely_sep_2 -embed_sep wand_elim_r.
Qed.
Global Instance into_wand_affine_embed_false `{BiEmbed PROP PROP'} q (PP QQ RR : PROP) :
  IntoWand false q RR (<affine> PP) QQ  IntoWand false q RR (<affine> PP) QQ | 100.
Proof.
  rewrite /IntoWand /= => ->.
  by rewrite embed_affinely_2 embed_intuitionistically_if_2 embed_wand.
Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
457

458
459
460
(* FromWand *)
Global Instance from_wand_wand P1 P2 : FromWand (P1 - P2) P1 P2.
Proof. by rewrite /FromWand. Qed.
461
Global Instance from_wand_embed `{BiEmbed PROP PROP'} P Q1 Q2 :
462
  FromWand P Q1 Q2  FromWand P Q1 Q2.
463
Proof. by rewrite /FromWand -embed_wand => <-. Qed.
464
465
466
467

(* FromImpl *)
Global Instance from_impl_impl P1 P2 : FromImpl (P1  P2) P1 P2.
Proof. by rewrite /FromImpl. Qed.
468
Global Instance from_impl_embed `{BiEmbed PROP PROP'} P Q1 Q2 :
469
  FromImpl P Q1 Q2  FromImpl P Q1 Q2.
470
Proof. by rewrite /FromImpl -embed_impl => <-. Qed.
471

Robbert Krebbers's avatar
Robbert Krebbers committed
472
473
474
475
(* 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 :
476
  Persistent P1  IntoAbsorbingly P1' P1  FromAnd (P1  P2) P1' P2 | 9.
477
Proof.
478
479
480
  rewrite /IntoAbsorbingly /FromAnd=> ? ->.
  rewrite persistent_and_affinely_sep_l_1 {1}(persistent_persistently_2 P1).
  by rewrite absorbingly_elim_persistently -{2}(intuitionistically_elim P1).
481
Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
482
Global Instance from_and_sep_persistent_r P1 P2 P2' :
483
  Persistent P2  IntoAbsorbingly P2' P2  FromAnd (P1  P2) P1 P2' | 10.
484
Proof.
485
486
487
  rewrite /IntoAbsorbingly /FromAnd=> ? ->.
  rewrite persistent_and_affinely_sep_r_1 {1}(persistent_persistently_2 P2).
  by rewrite absorbingly_elim_persistently -{2}(intuitionistically_elim P2).
488
489
Qed.

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

Robbert Krebbers's avatar
Robbert Krebbers committed
493
Global Instance from_and_persistently P Q1 Q2 :
494
  FromAnd P Q1 Q2 
495
  FromAnd (<pers> P) (<pers> Q1) (<pers> Q2).
Robbert Krebbers's avatar
Robbert Krebbers committed
496
497
Proof. rewrite /FromAnd=> <-. by rewrite persistently_and. Qed.
Global Instance from_and_persistently_sep P Q1 Q2 :
498
  FromSep P Q1 Q2 
499
  FromAnd (<pers> P) (<pers> Q1) (<pers> Q2) | 11.
Robbert Krebbers's avatar
Robbert Krebbers committed
500
Proof. rewrite /FromAnd=> <-. by rewrite -persistently_and persistently_and_sep. Qed.
501

502
Global Instance from_and_embed `{BiEmbed PROP PROP'} P Q1 Q2 :
503
  FromAnd P Q1 Q2  FromAnd P Q1 Q2.
504
Proof. by rewrite /FromAnd -embed_and => <-. Qed.
505

Robbert Krebbers's avatar
Robbert Krebbers committed
506
507
508
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).
509
Proof. intros. by rewrite /FromAnd big_opL_cons persistent_and_sep_1. Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
510
511
512
513
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).
514
Proof. intros. by rewrite /FromAnd big_opL_app persistent_and_sep_1. Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
515
516
517
518
519

(* 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
520
  TCOr (Affine P1) (Absorbing P2)  TCOr (Absorbing P1) (Affine P2) 
Robbert Krebbers's avatar
Robbert Krebbers committed
521
522
523
524
525
526
  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.

527
Global Instance from_sep_affinely P Q1 Q2 :
528
  FromSep P Q1 Q2  FromSep (<affine> P) (<affine> Q1) (<affine> Q2).
529
Proof. rewrite /FromSep=> <-. by rewrite affinely_sep_2. Qed.
530
531
532
Global Instance from_sep_intuitionistically P Q1 Q2 :
  FromSep P Q1 Q2  FromSep ( P) ( Q1) ( Q2).
Proof. rewrite /FromSep=> <-. by rewrite intuitionistically_sep_2. Qed.
533
Global Instance from_sep_absorbingly P Q1 Q2 :
534
  FromSep P Q1 Q2  FromSep (<absorb> P) (<absorb> Q1) (<absorb> Q2).
535
Proof. rewrite /FromSep=> <-. by rewrite absorbingly_sep. Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
536
Global Instance from_sep_persistently P Q1 Q2 :
537
  FromSep P Q1 Q2 
538
  FromSep (<pers> P) (<pers> Q1) (<pers> Q2).
539
Proof. rewrite /FromSep=> <-. by rewrite persistently_sep_2. Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
540

541
Global Instance from_sep_embed `{BiEmbed PROP PROP'} P Q1 Q2 :
542
  FromSep P Q1 Q2  FromSep P Q1 Q2.
543
Proof. by rewrite /FromSep -embed_sep => <-. Qed.
544

Robbert Krebbers's avatar
Robbert Krebbers committed
545
546
547
548
549
550
551
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.
552

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

569
Global Instance into_and_sep `{BiPositive PROP} P Q : IntoAnd true (P  Q) P Q.
570
Proof.
571
  rewrite /IntoAnd /= intuitionistically_sep -and_sep_intuitionistically intuitionistically_and //.
572
Qed.
573
Global Instance into_and_sep_affine P Q :
Ralf Jung's avatar
Ralf Jung committed
574
  TCOr (Affine P) (Absorbing Q)  TCOr (Absorbing P) (Affine Q) 
575
576
  IntoAnd true (P  Q) P Q.
Proof. intros. by rewrite /IntoAnd /= sep_and. Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
577
578

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

581
Global Instance into_and_affinely p P Q1 Q2 :
582
  IntoAnd p P Q1 Q2  IntoAnd p (<affine> P) (<affine> Q1) (<affine> Q2).
Robbert Krebbers's avatar
Robbert Krebbers committed
583
Proof.
Robbert Krebbers's avatar
Robbert Krebbers committed
584
  rewrite /IntoAnd. destruct p; simpl.
Ralf Jung's avatar
Ralf Jung committed
585
  - rewrite -affinely_and !intuitionistically_affinely_elim //.
586
  - intros ->. by rewrite affinely_and.
Robbert Krebbers's avatar
Robbert Krebbers committed
587
Qed.
588
589
590
591
592
593
594
Global Instance into_and_intuitionistically p P Q1 Q2 :
  IntoAnd p P Q1 Q2  IntoAnd p ( P) ( Q1) ( Q2).
Proof.
  rewrite /IntoAnd. destruct p; simpl.
  - rewrite -intuitionistically_and !intuitionistically_idemp //.
  - intros ->. by rewrite intuitionistically_and.
Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
595
Global Instance into_and_persistently p P Q1 Q2 :
596
  IntoAnd p P Q1 Q2 
597
  IntoAnd p (<pers> P) (<pers> Q1) (<pers> Q2).
Robbert Krebbers's avatar
Robbert Krebbers committed
598
Proof.
Robbert Krebbers's avatar
Robbert Krebbers committed
599
  rewrite /IntoAnd /=. destruct p; simpl.
Ralf Jung's avatar
Ralf Jung committed
600
  - rewrite -persistently_and !intuitionistically_persistently_elim //.
Robbert Krebbers's avatar
Robbert Krebbers committed
601
  - intros ->. by rewrite persistently_and.
Robbert Krebbers's avatar
Robbert Krebbers committed
602
Qed.
603
Global Instance into_and_embed `{BiEmbed PROP PROP'} p P Q1 Q2 :
604
605
  IntoAnd p P Q1 Q2  IntoAnd p P Q1 Q2.
Proof.
Robbert Krebbers's avatar
Robbert Krebbers committed
606
607
  rewrite /IntoAnd -embed_and=> HP. apply intuitionistically_if_intro'.
  by rewrite embed_intuitionistically_if_2 HP intuitionistically_if_elim.
608
Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
609

Robbert Krebbers's avatar
Robbert Krebbers committed
610
(* IntoSep *)
611
612
Global Instance into_sep_sep P Q : IntoSep (P  Q) P Q.
Proof. by rewrite /IntoSep. Qed.
613

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

638
639
640
Global Instance into_sep_pure φ ψ : @IntoSep PROP ⌜φ  ψ⌝ ⌜φ⌝ ⌜ψ⌝.
Proof. by rewrite /IntoSep pure_and persistent_and_sep_1. Qed.

641
Global Instance into_sep_embed `{BiEmbed PROP PROP'} P Q1 Q2 :
642
  IntoSep P Q1 Q2  IntoSep P Q1 Q2.
643
Proof. rewrite /IntoSep -embed_sep=> -> //. Qed.
644

645
Global Instance into_sep_affinely `{BiPositive PROP} P Q1 Q2 :
646
  IntoSep P Q1 Q2  IntoSep (<affine> P) (<affine> Q1) (<affine> Q2) | 0.
647
Proof. rewrite /IntoSep /= => ->. by rewrite affinely_sep. Qed.
648
649
650
Global Instance into_sep_intuitionistically `{BiPositive PROP} P Q1 Q2 :
  IntoSep P Q1 Q2  IntoSep ( P) ( Q1) ( Q2) | 0.
Proof. rewrite /IntoSep /= => ->. by rewrite intuitionistically_sep. Qed.
651
652
653
654
(* 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 :
655
  IntoSep P Q1 Q2  IntoSep (<affine> P) Q1 Q2 | 20.
656
Proof. rewrite /IntoSep /= => ->. by rewrite affinely_elim. Qed.
657

658
Global Instance into_sep_persistently `{BiPositive PROP} P Q1 Q2 :
659
  IntoSep P Q1 Q2 
660
  IntoSep (<pers> P) (<pers> Q1) (<pers> Q2).
661
Proof. rewrite /IntoSep /= => ->. by rewrite persistently_sep. Qed.
662
663
Global Instance into_sep_persistently_affine P Q1 Q2 :
  IntoSep P Q1 Q2 
Ralf Jung's avatar
Ralf Jung committed
664
  TCOr (Affine Q1) (Absorbing Q2)  TCOr (Absorbing Q1) (Affine Q2) 
665
  IntoSep (<pers> P) (<pers> Q1) (<pers> Q2).
666
Proof.
Ralf Jung's avatar
Ralf Jung committed
667
  rewrite /IntoSep /= => -> ??.
668
669
  by rewrite sep_and persistently_and persistently_and_sep_l_1.
Qed.
670
Global Instance into_sep_intuitionistically_affine P Q1 Q2 :
671
  IntoSep P Q1 Q2 
Ralf Jung's avatar
Ralf Jung committed
672
  TCOr (Affine Q1) (Absorbing Q2)  TCOr (Absorbing Q1) (Affine Q2) 
673
674
  IntoSep ( P) ( Q1) ( Q2).
Proof.
Ralf Jung's avatar
Ralf Jung committed
675
  rewrite /IntoSep /= => -> ??.
676
  by rewrite sep_and intuitionistically_and and_sep_intuitionistically.
677
Qed.
678

679
680
681
(* 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. *)
682
Global Instance into_sep_big_sepL_cons {A} (Φ : nat  A  PROP) l x l' :
683
  IsCons l x l' 
684
  IntoSep ([ list] k  y  l, Φ k y)
685
    (Φ 0 x) ([ list] k  y  l', Φ (S k) y).
Robbert Krebbers's avatar
Robbert Krebbers committed
686
Proof. rewrite /IsCons=>->. by rewrite /IntoSep big_sepL_cons. Qed.
687
Global Instance into_sep_big_sepL_app {A} (Φ : nat  A  PROP) l l1 l2 :
688
  IsApp l l1 l2 
689
  IntoSep ([ list] k  y  l, Φ k y)
690
    ([ list] k  y  l1, Φ k y) ([ list] k  y  l2, Φ (length l1 + k) y).
Robbert Krebbers's avatar
Robbert Krebbers committed
691
692
693
694
695
696
697
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.
698
Global Instance from_or_affinely P Q1 Q2 :
699
  FromOr P Q1 Q2  FromOr (<affine> P) (<affine> Q1) (<affine> Q2).
700
Proof. rewrite /FromOr=> <-. by rewrite affinely_or. Qed.
701
702
703
Global Instance from_or_intuitionistically P Q1 Q2 :
  FromOr P Q1 Q2  FromOr ( P) ( Q1) ( Q2).
Proof. rewrite /FromOr=> <-. by rewrite intuitionistically_or. Qed.
704
Global Instance from_or_absorbingly P Q1 Q2 :
705
  FromOr P Q1 Q2  FromOr (<absorb> P) (<absorb> Q1) (<absorb> Q2).
706
Proof. rewrite /FromOr=> <-. by rewrite absorbingly_or. Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
707
Global Instance from_or_persistently P Q1 Q2 :
708
  FromOr P Q1 Q2 
709
  FromOr (<pers> P) (<pers> Q1) (<pers> Q2).
Robbert Krebbers's avatar
Robbert Krebbers committed
710
Proof. rewrite /FromOr=> <-. by rewrite persistently_or. Qed.
711
Global Instance from_or_embed `{BiEmbed PROP PROP'} P Q1 Q2 :
712
  FromOr P Q1 Q2  FromOr P Q1 Q2.
713
Proof. by rewrite /FromOr -embed_or => <-. Qed.