class_instances.v 76.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 Export modality_instances classes.
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
(* 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.
16

17
18
19
20
21
(* 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.
22
Global Instance into_absorbingly_default P : IntoAbsorbingly (bi_absorbingly P) P | 100.
23
Proof. by rewrite /IntoAbsorbingly. Qed.
24

25
(* FromAssumption *)
26
Global Instance from_assumption_exact p P : FromAssumption p P P | 0.
27
Proof. by rewrite /FromAssumption /= affinely_persistently_if_elim. Qed.
28

29
Global Instance from_assumption_persistently_r P Q :
30
  FromAssumption true P Q  FromAssumption true P (bi_persistently Q).
Robbert Krebbers's avatar
Robbert Krebbers committed
31
32
Proof.
  rewrite /FromAssumption /= =><-.
33
  by rewrite -{1}affinely_persistently_idemp affinely_elim.
Robbert Krebbers's avatar
Robbert Krebbers committed
34
Qed.
35
36
37
38
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 :
39
  FromAssumption p P Q  FromAssumption p P (bi_absorbingly Q).
40
Proof. rewrite /FromAssumption /= =><-. apply absorbingly_intro. Qed.
41

42
Global Instance from_assumption_affinely_persistently_l p P Q :
43
  FromAssumption true P Q  FromAssumption p ( P) Q.
44
Proof. rewrite /FromAssumption /= =><-. by rewrite affinely_persistently_if_elim. Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
45
Global Instance from_assumption_persistently_l_true P Q :
46
  FromAssumption true P Q  FromAssumption true (bi_persistently P) Q.
Robbert Krebbers's avatar
Robbert Krebbers committed
47
Proof. rewrite /FromAssumption /= =><-. by rewrite persistently_idemp. Qed.
48
Global Instance from_assumption_persistently_l_false `{BiAffine PROP} P Q :
49
  FromAssumption true P Q  FromAssumption false (bi_persistently P) Q.
50
51
52
53
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
54
55

Global Instance from_assumption_forall {A} p (Φ : A  PROP) Q x :
56
57
  FromAssumption p (Φ x) Q  FromAssumption p ( x, Φ x) Q.
Proof. rewrite /FromAssumption=> <-. by rewrite forall_elim. Qed.
58
59

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

Ralf Jung's avatar
Ralf Jung committed
63
Global Instance into_pure_pure_and (φ1 φ2 : Prop) P1 P2 :
Ralf Jung's avatar
Ralf Jung committed
64
  IntoPure P1 φ1  IntoPure P2 φ2  IntoPure (P1  P2) (φ1  φ2).
65
Proof. rewrite /IntoPure pure_and. by intros -> ->. Qed.
Ralf Jung's avatar
Ralf Jung committed
66
Global Instance into_pure_pure_or (φ1 φ2 : Prop) P1 P2 :
Ralf Jung's avatar
Ralf Jung committed
67
  IntoPure P1 φ1  IntoPure P2 φ2  IntoPure (P1  P2) (φ1  φ2).
68
Proof. rewrite /IntoPure pure_or. by intros -> ->. Qed.
Ralf Jung's avatar
Ralf Jung committed
69
Global Instance into_pure_pure_impl (φ1 φ2 : Prop) P1 P2 :
70
71
  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
72
73
74
75
76
77
78
79
80
81
82

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
83
Global Instance into_pure_pure_wand (φ1 φ2 : Prop) P1 P2 :
84
85
86
87
88
89
90
  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.
91

92
93
94
Global Instance into_pure_affinely P φ :
  IntoPure P φ  IntoPure (bi_affinely P) φ.
Proof. rewrite /IntoPure=> ->. apply affinely_elim. Qed.
95
Global Instance into_pure_absorbingly P φ : IntoPure P φ  IntoPure (bi_absorbingly P) φ.
96
97
98
Proof. rewrite /IntoPure=> ->. by rewrite absorbingly_pure. Qed.
Global Instance into_pure_persistently P φ :
  IntoPure P φ  IntoPure (bi_persistently P) φ.
99
Proof. rewrite /IntoPure=> ->. apply: persistently_elim. Qed.
100
Global Instance into_pure_embed `{BiEmbed PROP PROP'} P φ :
101
  IntoPure P φ  IntoPure P φ.
102
Proof. rewrite /IntoPure=> ->. by rewrite embed_pure. Qed.
103

104
(* FromPure *)
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
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.
154
155
Qed.

156
157
158
159
160
161
162
163
164
165
166
167
168
169
170
171
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.
172
Global Instance from_pure_embed `{BiEmbed PROP PROP'} a P φ :
173
  FromPure a P φ  FromPure a P φ.
174
Proof. rewrite /FromPure=> <-. by rewrite embed_affinely_if embed_pure. Qed.
175

176
(* IntoPersistent *)
177
Global Instance into_persistent_persistently p P Q :
178
  IntoPersistent true P Q  IntoPersistent p (bi_persistently P) Q | 0.
Robbert Krebbers's avatar
Robbert Krebbers committed
179
180
181
182
Proof.
  rewrite /IntoPersistent /= => ->.
  destruct p; simpl; auto using persistently_idemp_1.
Qed.
183
184
185
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.
186
Global Instance into_persistent_embed `{BiEmbed PROP PROP'} p P Q :
187
188
  IntoPersistent p P Q  IntoPersistent p P Q | 0.
Proof.
189
  rewrite /IntoPersistent -embed_persistently -embed_persistently_if=> -> //.
190
Qed.
191
Global Instance into_persistent_here P : IntoPersistent true P P | 1.
Robbert Krebbers's avatar
Robbert Krebbers committed
192
Proof. by rewrite /IntoPersistent. Qed.
193
194
Global Instance into_persistent_persistent P :
  Persistent P  IntoPersistent false P P | 100.
195
Proof. intros. by rewrite /IntoPersistent. Qed.
196

197
198
(* FromModal *)
Global Instance from_modal_affinely P :
199
  FromModal modality_affinely (bi_affinely P) (bi_affinely P) P | 2.
200
201
202
Proof. by rewrite /FromModal. Qed.

Global Instance from_modal_persistently P :
203
  FromModal modality_persistently (bi_persistently P) (bi_persistently P) P | 2.
204
205
Proof. by rewrite /FromModal. Qed.
Global Instance from_modal_affinely_persistently P :
206
  FromModal modality_affinely_persistently ( P) ( P) P | 1.
207
208
Proof. by rewrite /FromModal. Qed.
Global Instance from_modal_affinely_persistently_affine_bi P :
209
  BiAffine PROP  FromModal modality_persistently ( P) ( P) P | 0.
210
211
Proof. intros. by rewrite /FromModal /= affine_affinely. Qed.

212
213
214
215
216
Global Instance from_modal_absorbingly P :
  FromModal modality_id (bi_absorbingly P) (bi_absorbingly P) P.
Proof. by rewrite /FromModal /= -absorbingly_intro. Qed.

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

222
Global Instance from_modal_id_embed `{BiEmbed PROP PROP'} `(sel : A) P Q :
223
  FromModal modality_id sel P Q 
224
  FromModal modality_id sel P Q | 100.
225
226
Proof. by rewrite /FromModal /= =><-. Qed.

227
Global Instance from_modal_affinely_embed `{BiEmbed PROP PROP'} `(sel : A) P Q :
228
  FromModal modality_affinely sel P Q 
229
  FromModal modality_affinely sel P Q | 100.
230
231
Proof. rewrite /FromModal /= =><-. by rewrite embed_affinely. Qed.
Global Instance from_modal_persistently_embed `{BiEmbed PROP PROP'} `(sel : A) P Q :
232
  FromModal modality_persistently sel P Q 
233
  FromModal modality_persistently sel P Q | 100.
234
235
Proof. rewrite /FromModal /= =><-. by rewrite embed_persistently. Qed.
Global Instance from_modal_affinely_persistently_embed `{BiEmbed PROP PROP'} `(sel : A) P Q :
236
  FromModal modality_affinely_persistently sel P Q 
237
  FromModal modality_affinely_persistently sel P Q | 100.
238
Proof.
239
  rewrite /FromModal /= =><-. by rewrite embed_affinely embed_persistently.
240
Qed.
241

Robbert Krebbers's avatar
Robbert Krebbers committed
242
243
244
(* IntoWand *)
Global Instance into_wand_wand p q P Q P' :
  FromAssumption q P P'  IntoWand p q (P' - Q) P Q.
245
Proof.
246
  rewrite /FromAssumption /IntoWand=> HP. by rewrite HP affinely_persistently_if_elim.
Robbert Krebbers's avatar
Robbert Krebbers committed
247
Qed.
248
249
Global Instance into_wand_impl_false_false P Q P' :
  Absorbing P'  Absorbing (P'  Q) 
Robbert Krebbers's avatar
Robbert Krebbers committed
250
251
  FromAssumption false P P'  IntoWand false false (P'  Q) P Q.
Proof.
252
  rewrite /FromAssumption /IntoWand /= => ?? ->. apply wand_intro_r.
Robbert Krebbers's avatar
Robbert Krebbers committed
253
254
255
  by rewrite sep_and impl_elim_l.
Qed.
Global Instance into_wand_impl_false_true P Q P' :
256
  Absorbing P'  FromAssumption true P P' 
Robbert Krebbers's avatar
Robbert Krebbers committed
257
  IntoWand false true (P'  Q) P Q.
258
Proof.
259
  rewrite /IntoWand /FromAssumption /= => ? HP. apply wand_intro_l.
260
261
  rewrite -(affinely_persistently_idemp P) HP.
  by rewrite -persistently_and_affinely_sep_l persistently_elim impl_elim_r.
262
Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
263
Global Instance into_wand_impl_true_false P Q P' :
264
  Affine P'  FromAssumption false P P' 
Robbert Krebbers's avatar
Robbert Krebbers committed
265
  IntoWand true false (P'  Q) P Q.
266
Proof.
267
  rewrite /FromAssumption /IntoWand /= => ? HP. apply wand_intro_r.
268
269
  rewrite -persistently_and_affinely_sep_l HP -{2}(affine_affinely P') -affinely_and_lr.
  by rewrite affinely_persistently_elim impl_elim_l.
270
Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
271
272
Global Instance into_wand_impl_true_true P Q P' :
  FromAssumption true P P'  IntoWand true true (P'  Q) P Q.
273
Proof.
Robbert Krebbers's avatar
Robbert Krebbers committed
274
  rewrite /FromAssumption /IntoWand /= => <-. apply wand_intro_l.
275
276
  rewrite -{1}(affinely_persistently_idemp P) -and_sep_affinely_persistently.
  by rewrite -affinely_persistently_and impl_elim_r affinely_persistently_elim.
277
Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
278
279
280
281
282
283
284
285

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.

286
287
288
289
290
291
292
293
294
295
296
297
298
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.
299

Robbert Krebbers's avatar
Robbert Krebbers committed
300
301
302
303
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.

304
305
306
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
307
Global Instance into_wand_persistently_true q R P Q :
308
  IntoWand true q R P Q  IntoWand true q (bi_persistently R) P Q.
Robbert Krebbers's avatar
Robbert Krebbers committed
309
Proof. by rewrite /IntoWand /= persistently_idemp. Qed.
310
Global Instance into_wand_persistently_false `{!BiAffine PROP} q R P Q :
311
  IntoWand false q R P Q  IntoWand false q (bi_persistently R) P Q.
312
Proof. by rewrite /IntoWand persistently_elim. Qed.
313
Global Instance into_wand_embed `{BiEmbed PROP PROP'} p q R P Q :
314
315
  IntoWand p q R P Q  IntoWand p q R P Q.
Proof.
316
317
  rewrite /IntoWand -!embed_persistently_if -!embed_affinely_if
          -embed_wand => -> //.
318
Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
319

320
321
322
(* FromWand *)
Global Instance from_wand_wand P1 P2 : FromWand (P1 - P2) P1 P2.
Proof. by rewrite /FromWand. Qed.
323
Global Instance from_wand_embed `{BiEmbed PROP PROP'} P Q1 Q2 :
324
  FromWand P Q1 Q2  FromWand P Q1 Q2.
325
Proof. by rewrite /FromWand -embed_wand => <-. Qed.
326
327
328
329

(* FromImpl *)
Global Instance from_impl_impl P1 P2 : FromImpl (P1  P2) P1 P2.
Proof. by rewrite /FromImpl. Qed.
330
Global Instance from_impl_embed `{BiEmbed PROP PROP'} P Q1 Q2 :
331
  FromImpl P Q1 Q2  FromImpl P Q1 Q2.
332
Proof. by rewrite /FromImpl -embed_impl => <-. Qed.
333

Robbert Krebbers's avatar
Robbert Krebbers committed
334
335
336
337
(* 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 :
338
  FromAffinely P1 P1'  Persistent P1'  FromAnd (P1  P2) P1' P2 | 9.
339
Proof.
340
  rewrite /FromAffinely /FromAnd=> <- ?. by rewrite persistent_and_affinely_sep_l_1.
341
Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
342
Global Instance from_and_sep_persistent_r P1 P2 P2' :
343
  FromAffinely P2 P2'  Persistent P2'  FromAnd (P1  P2) P1 P2' | 10.
344
Proof.
345
  rewrite /FromAffinely /FromAnd=> <- ?. by rewrite persistent_and_affinely_sep_r_1.
346
Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
347
348
Global Instance from_and_sep_persistent P1 P2 :
  Persistent P1  Persistent P2  FromAnd (P1  P2) P1 P2 | 11.
349
Proof.
350
  rewrite /FromAffinely /FromAnd. intros ??. by rewrite -persistent_and_sep_1.
351
352
Qed.

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

Robbert Krebbers's avatar
Robbert Krebbers committed
356
Global Instance from_and_persistently P Q1 Q2 :
357
358
  FromAnd P Q1 Q2 
  FromAnd (bi_persistently P) (bi_persistently Q1) (bi_persistently Q2).
Robbert Krebbers's avatar
Robbert Krebbers committed
359
360
Proof. rewrite /FromAnd=> <-. by rewrite persistently_and. Qed.
Global Instance from_and_persistently_sep P Q1 Q2 :
361
362
  FromSep P Q1 Q2 
  FromAnd (bi_persistently P) (bi_persistently Q1) (bi_persistently Q2) | 11.
Robbert Krebbers's avatar
Robbert Krebbers committed
363
Proof. rewrite /FromAnd=> <-. by rewrite -persistently_and persistently_and_sep. Qed.
364

365
Global Instance from_and_embed `{BiEmbed PROP PROP'} P Q1 Q2 :
366
  FromAnd P Q1 Q2  FromAnd P Q1 Q2.
367
Proof. by rewrite /FromAnd -embed_and => <-. Qed.
368

Robbert Krebbers's avatar
Robbert Krebbers committed
369
370
371
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).
372
Proof. intros. by rewrite /FromAnd big_opL_cons persistent_and_sep_1. Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
373
374
375
376
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).
377
Proof. intros. by rewrite /FromAnd big_opL_app persistent_and_sep_1. Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
378
379
380
381
382

(* 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
383
  TCOr (Affine P1) (Absorbing P2)  TCOr (Absorbing P1) (Affine P2) 
Robbert Krebbers's avatar
Robbert Krebbers committed
384
385
386
387
388
389
  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.

390
391
392
393
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 :
394
  FromSep P Q1 Q2  FromSep (bi_absorbingly P) (bi_absorbingly Q1) (bi_absorbingly Q2).
395
Proof. rewrite /FromSep=> <-. by rewrite absorbingly_sep. Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
396
Global Instance from_sep_persistently P Q1 Q2 :
397
398
  FromSep P Q1 Q2 
  FromSep (bi_persistently P) (bi_persistently Q1) (bi_persistently Q2).
399
Proof. rewrite /FromSep=> <-. by rewrite persistently_sep_2. Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
400

401
Global Instance from_sep_embed `{BiEmbed PROP PROP'} P Q1 Q2 :
402
  FromSep P Q1 Q2  FromSep P Q1 Q2.
403
Proof. by rewrite /FromSep -embed_sep => <-. Qed.
404

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

Robbert Krebbers's avatar
Robbert Krebbers committed
413
(* IntoAnd *)
414
Global Instance into_and_and p P Q : IntoAnd p (P  Q) P Q | 10.
415
Proof. by rewrite /IntoAnd affinely_persistently_if_and. Qed.
416
Global Instance into_and_and_affine_l P Q Q' :
417
  Affine P  FromAffinely Q' Q  IntoAnd false (P  Q) P Q'.
418
419
Proof.
  intros. rewrite /IntoAnd /=.
420
  by rewrite -(affine_affinely P) affinely_and_l affinely_and (from_affinely Q').
421
422
Qed.
Global Instance into_and_and_affine_r P P' Q :
423
  Affine Q  FromAffinely P' P  IntoAnd false (P  Q) P' Q.
424
425
Proof.
  intros. rewrite /IntoAnd /=.
426
  by rewrite -(affine_affinely Q) affinely_and_r affinely_and (from_affinely P').
427
428
Qed.

429
Global Instance into_and_sep `{BiPositive PROP} P Q : IntoAnd true (P  Q) P Q.
430
431
432
Proof.
  by rewrite /IntoAnd /= persistently_sep -and_sep_persistently persistently_and.
Qed.
433
Global Instance into_and_sep_affine P Q :
Ralf Jung's avatar
Ralf Jung committed
434
  TCOr (Affine P) (Absorbing Q)  TCOr (Absorbing P) (Affine Q) 
435
436
  IntoAnd true (P  Q) P Q.
Proof. intros. by rewrite /IntoAnd /= sep_and. Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
437
438

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

441
442
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
443
Proof.
Robbert Krebbers's avatar
Robbert Krebbers committed
444
  rewrite /IntoAnd. destruct p; simpl.
445
446
  - by rewrite -affinely_and !persistently_affinely.
  - intros ->. by rewrite affinely_and.
Robbert Krebbers's avatar
Robbert Krebbers committed
447
Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
448
Global Instance into_and_persistently p P Q1 Q2 :
449
450
  IntoAnd p P Q1 Q2 
  IntoAnd p (bi_persistently P) (bi_persistently Q1) (bi_persistently Q2).
Robbert Krebbers's avatar
Robbert Krebbers committed
451
Proof.
Robbert Krebbers's avatar
Robbert Krebbers committed
452
453
454
  rewrite /IntoAnd /=. destruct p; simpl.
  - by rewrite -persistently_and !persistently_idemp.
  - intros ->. by rewrite persistently_and.
Robbert Krebbers's avatar
Robbert Krebbers committed
455
Qed.
456
Global Instance into_and_embed `{BiEmbed PROP PROP'} p P Q1 Q2 :
457
458
  IntoAnd p P Q1 Q2  IntoAnd p P Q1 Q2.
Proof.
459
460
  rewrite /IntoAnd -embed_and -!embed_persistently_if
          -!embed_affinely_if=> -> //.
461
Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
462

Robbert Krebbers's avatar
Robbert Krebbers committed
463
(* IntoSep *)
464
465
Global Instance into_sep_sep P Q : IntoSep (P  Q) P Q.
Proof. by rewrite /IntoSep. Qed.
466

467
Inductive AndIntoSep : PROP  PROP  PROP  PROP  Prop :=
468
469
  | 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.
470
471
472
473
474
475
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'.
476
Proof.
477
  destruct 2 as [P Q Q'|P Q]; rewrite /IntoSep.
478
479
480
  - 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.
481
Qed.
482
483
Global Instance into_sep_and_persistent_r P P' Q Q' :
  Persistent Q  AndIntoSep Q Q' P P'  IntoSep (P  Q) P' Q'.
484
Proof.
485
  destruct 2 as [Q P P'|Q P]; rewrite /IntoSep.
486
487
488
  - 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.
489
Qed.
490

491
492
493
Global Instance into_sep_pure φ ψ : @IntoSep PROP ⌜φ  ψ⌝ ⌜φ⌝ ⌜ψ⌝.
Proof. by rewrite /IntoSep pure_and persistent_and_sep_1. Qed.

494
Global Instance into_sep_embed `{BiEmbed PROP PROP'} P Q1 Q2 :
495
  IntoSep P Q1 Q2  IntoSep P Q1 Q2.
496
Proof. rewrite /IntoSep -embed_sep=> -> //. Qed.
497

498
499
500
501
502
503
504
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 :
505
506
  IntoSep P Q1 Q2  IntoSep (bi_affinely P) Q1 Q2 | 20.
Proof. rewrite /IntoSep /= => ->. by rewrite affinely_elim. Qed.
507

508
Global Instance into_sep_persistently `{BiPositive PROP} P Q1 Q2 :
509
510
  IntoSep P Q1 Q2 
  IntoSep (bi_persistently P) (bi_persistently Q1) (bi_persistently Q2).
511
Proof. rewrite /IntoSep /= => ->. by rewrite persistently_sep. Qed.
512
513
Global Instance into_sep_persistently_affine P Q1 Q2 :
  IntoSep P Q1 Q2 
Ralf Jung's avatar
Ralf Jung committed
514
  TCOr (Affine Q1) (Absorbing Q2)  TCOr (Absorbing Q1) (Affine Q2) 
515
516
  IntoSep (bi_persistently P) (bi_persistently Q1) (bi_persistently Q2).
Proof.
Ralf Jung's avatar
Ralf Jung committed
517
  rewrite /IntoSep /= => -> ??.
518
519
520
521
  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
522
  TCOr (Affine Q1) (Absorbing Q2)  TCOr (Absorbing Q1) (Affine Q2) 
523
524
  IntoSep ( P) ( Q1) ( Q2).
Proof.
Ralf Jung's avatar
Ralf Jung committed
525
  rewrite /IntoSep /= => -> ??.
526
527
  by rewrite sep_and affinely_persistently_and and_sep_affinely_persistently.
Qed.
528

529
530
531
(* 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. *)
532
Global Instance into_sep_big_sepL_cons {A} (Φ : nat  A  PROP) l x l' :
533
  IsCons l x l' 
534
  IntoSep ([ list] k  y  l, Φ k y)
535
    (Φ 0 x) ([ list] k  y  l', Φ (S k) y).
Robbert Krebbers's avatar
Robbert Krebbers committed
536
Proof. rewrite /IsCons=>->. by rewrite /IntoSep big_sepL_cons. Qed.
537
Global Instance into_sep_big_sepL_app {A} (Φ : nat  A  PROP) l l1 l2 :
538
  IsApp l l1 l2 
539
  IntoSep ([ list] k  y  l, Φ k y)
540
    ([ list] k  y  l1, Φ k y) ([ list] k  y  l2, Φ (length l1 + k) y).
Robbert Krebbers's avatar
Robbert Krebbers committed
541
542
543
544
545
546
547
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.
548
549
550
551
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 :
552
  FromOr P Q1 Q2  FromOr (bi_absorbingly P) (bi_absorbingly Q1) (bi_absorbingly Q2).
553
Proof. rewrite /FromOr=> <-. by rewrite absorbingly_or. Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
554
Global Instance from_or_persistently P Q1 Q2 :
555
556
  FromOr P Q1 Q2 
  FromOr (bi_persistently P) (bi_persistently Q1) (bi_persistently Q2).
Robbert Krebbers's avatar
Robbert Krebbers committed
557
Proof. rewrite /FromOr=> <-. by rewrite persistently_or. Qed.
558
Global Instance from_or_embed `{BiEmbed PROP PROP'} P Q1 Q2 :
559
  FromOr P Q1 Q2  FromOr P Q1 Q2.
560
Proof. by rewrite /FromOr -embed_or => <-. Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
561
562
563
564
565
566

(* 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.
567
568
569
570
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 :
571
  IntoOr P Q1 Q2  IntoOr (bi_absorbingly P) (bi_absorbingly Q1) (bi_absorbingly Q2).
572
Proof. rewrite /IntoOr=>->. by rewrite absorbingly_or. Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
573
Global Instance into_or_persistently P Q1 Q2 :
574
575
  IntoOr P Q1 Q2 
  IntoOr (bi_persistently P) (bi_persistently Q1) (bi_persistently Q2).
Robbert Krebbers's avatar
Robbert Krebbers committed
576
Proof. rewrite /IntoOr=>->. by rewrite persistently_or. Qed.
577
Global Instance into_or_embed `{BiEmbed PROP PROP'} P Q1 Q2 :
578
  IntoOr P Q1 Q2  IntoOr P Q1 Q2.
579
Proof. by rewrite /IntoOr -embed_or => <-. Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
580
581
582
583
584
585
586

(* 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.
587
588
589
590
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) :
591
  FromExist P Φ  FromExist (bi_absorbingly P) (λ a, bi_absorbingly (Φ a))%I.
592
Proof. rewrite /FromExist=> <-. by rewrite absorbingly_exist. Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
593
Global Instance from_exist_persistently {A} P (Φ : A  PROP) :
594
  FromExist P Φ  FromExist (bi_persistently P) (λ a, bi_persistently (Φ a))%I.
Robbert Krebbers's avatar
Robbert Krebbers committed
595
Proof. rewrite /FromExist=> <-. by rewrite persistently_exist. Qed.
596
Global Instance from_exist_embed `{BiEmbed PROP PROP'} {A} P (Φ : A  PROP) :
597
  FromExist P Φ  FromExist P (λ a, ⎡Φ a%I).
598
Proof. by rewrite /FromExist -embed_exist => <-. Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
599
600
601
602
603
604
605

(* 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.
606
607
608
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
609
610
611
612
613
614
615
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 φ :
616
  IntoPureT P φ  TCOr (Affine P) (Absorbing Q)  IntoExist (P  Q) (λ _ : φ, Q).
Robbert Krebbers's avatar
Robbert Krebbers committed
617
Proof.
618
  intros (φ'&->&?) ?. rewrite /IntoExist.
Robbert Krebbers's avatar
Robbert Krebbers committed
619
  eapply (pure_elim φ'); [by rewrite (into_pure P); apply sep_elim_l, _|]=>?.
Robbert Krebbers's avatar
Robbert Krebbers committed
620
621
  rewrite -exist_intro //. apply sep_elim_r, _.
Qed.
622
Global Instance into_exist_absorbingly {A} P (Φ : A  PROP) :
623
  IntoExist P Φ  IntoExist (bi_absorbingly P) (λ a, bi_absorbingly (Φ a))%I.
624
Proof. rewrite /IntoExist=> HP. by rewrite HP absorbingly_exist. Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
625
Global Instance into_exist_persistently {A} P (Φ : A  PROP) :
626
  IntoExist P Φ  IntoExist (bi_persistently P) (λ a, bi_persistently (Φ a))%I.
Robbert Krebbers's avatar
Robbert Krebbers committed
627
Proof. rewrite /IntoExist=> HP. by rewrite HP persistently_exist. Qed.
628
Global Instance into_exist_embed `{BiEmbed PROP PROP'} {A} P (Φ : A  PROP) :
629
  IntoExist P Φ  IntoExist P (λ a, ⎡Φ a%I).
630
Proof. by rewrite /IntoExist -embed_exist => <-. Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
631
632
633
634

(* IntoForall *)
Global Instance into_forall_forall {A} (Φ : A  PROP) : IntoForall ( a, Φ a) Φ.
Proof. by rewrite /IntoForall. Qed.
635
636
637
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.
Robbert Krebbers's avatar
Robbert Krebbers committed
638
Global Instance into_forall_persistently {A} P (Φ : A  PROP) :
639
  IntoForall P Φ  IntoForall (bi_persistently P) (λ a, bi_persistently (Φ a))%I.
Robbert Krebbers's avatar
Robbert Krebbers committed
640
Proof. rewrite /IntoForall=> HP. by rewrite HP persistently_forall. Qed.
641
Global Instance into_forall_embed `{BiEmbed PROP PROP'} {A} P (Φ : A  PROP) :
642
  IntoForall P Φ  IntoForall P (λ a, ⎡Φ a%I).
643
Proof. by rewrite /IntoForall -embed_forall => <-. Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
644
645
646
647
648
649
650
651

(* FromForall *)
Global Instance from_forall_forall {A} (Φ : A  PROP) :
  FromForall ( x, Φ x)%I Φ.
Proof. by rewrite /FromForall. Qed.
Global Instance from_forall_pure {A} (φ : A  Prop) :
  @FromForall PROP A ( a : A, φ a)%I (λ a,  φ a )%I.
Proof. by rewrite /FromForall pure_forall. Qed.
652
653
654
Global Instance from_forall_pure_not (φ : Prop) :
  @FromForall PROP φ (¬ φ⌝)%I (λ a : φ, False)%I.
Proof. by rewrite /FromForall pure_forall. Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
655
656
657
658
659
660
Global Instance from_forall_impl_pure P Q φ :
  IntoPureT P φ  FromForall (P  Q)%I (λ _ : φ, Q)%I.
Proof.
  intros (φ'&->&?). by rewrite /FromForall -pure_impl_forall (into_pure P).
Qed.
Global Instance from_forall_wand_pure P Q φ :
661
  IntoPureT P φ  TCOr (Affine P) (Absorbing Q) 
Robbert Krebbers's avatar
Robbert Krebbers committed
662
663
  FromForall (P - Q)%I (λ _ : φ, Q)%I.
Proof.
664
  intros (φ'&->&?) [|]; rewrite /FromForall; apply wand_intro_r.
665
  - rewrite -(affine_affinely P) (into_pure P) -persistent_and_affinely_sep_r.
Robbert Krebbers's avatar
Robbert Krebbers committed
666
667
668
669
    apply pure_elim_r=>?. by rewrite forall_elim.
  - by rewrite (into_pure P) -pure_wand_forall wand_elim_l.
Qed.

670
Global Instance from_forall_affinely `{BiAffine PROP} {A} P (Φ : A  PROP) :
671
672
673
674
  FromForall P Φ  FromForall (bi_affinely P)%I (λ a, bi_affinely (Φ a))%I.
Proof.
  rewrite /FromForall=> <-. rewrite affine_affinely. by setoid_rewrite affinely_elim.
Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
675
Global Instance from_forall_persistently {A} P (Φ : A  PROP) :
676
  FromForall P Φ  FromForall (bi_persistently P)%I (λ a, bi_persistently (Φ a))%I.
Robbert Krebbers's avatar
Robbert Krebbers committed
677
Proof. rewrite /FromForall=> <-. by rewrite persistently_forall. Qed.
678
Global Instance from_forall_embed `{BiEmbed PROP PROP'} {A} P (Φ : A  PROP) :
679
  FromForall P Φ  FromForall P%I (λ a, ⎡Φ a%I).
680
Proof. by rewrite /FromForall -embed_forall => <-. Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
681

682
683
684
685
(* IntoInv *)
Global Instance into_inv_embed {PROP' : bi} `{BiEmbed PROP PROP'} P N :
  IntoInv P N  IntoInv P N.

Robbert Krebbers's avatar
Robbert Krebbers committed
686
(* ElimModal *)
687
688
Global Instance elim_modal_wand φ P P' Q Q' R :
  ElimModal φ P P' Q Q'  ElimModal φ P P' (R - Q) (R - Q').
Robbert Krebbers's avatar
Robbert Krebbers committed
689
Proof.
690
691
  rewrite /ElimModal=> H Hφ. apply wand_intro_r.
  rewrite wand_curry -assoc (comm _ P') -wand_curry wand_elim_l; auto.
Robbert Krebbers's avatar
Robbert Krebbers committed
692
Qed.
693
694
Global Instance elim_modal_forall {A} φ P P' (Φ Ψ : A  PROP) :
  ( x, ElimModal φ P P' (Φ x) (Ψ x))  ElimModal φ P P' ( x, Φ x) ( x, Ψ x).