class_instances_bi.v 49.2 KB
Newer Older
1
From stdpp Require Import nat_cancel.
2
From iris.bi Require Import bi tactics telescopes.
3
From iris.proofmode Require Import base modality_instances classes ltac_tactics.
4
Set Default Proof Using "Type".
Robbert Krebbers's avatar
Robbert Krebbers committed
5
6
7
8
9
Import bi.

Section bi_instances.
Context {PROP : bi}.
Implicit Types P Q R : PROP.
10
Implicit Types mP : option PROP.
Robbert Krebbers's avatar
Robbert Krebbers committed
11

12
(** AsEmpValid *)
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
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.

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

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

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

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

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

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

128
129
130
131
Global Instance from_assumption_bupd `{BiBUpd PROP} p P Q :
  FromAssumption p P Q  KnownRFromAssumption p P (|==> Q).
Proof. rewrite /KnownRFromAssumption /FromAssumption=>->. apply bupd_intro. Qed.

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

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

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
156
Global Instance into_pure_pure_wand (φ1 φ2 : Prop) P1 P2 :
157
158
159
160
  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.
161
  rewrite -{1}(persistent_absorbingly_affinely ⌜φ1%I) absorbingly_sep_l
162
163
          bi.wand_elim_r absorbing //.
Qed.
164

165
Global Instance into_pure_affinely P φ : IntoPure P φ  IntoPure (<affine> P) φ.
166
Proof. rewrite /IntoPure=> ->. apply affinely_elim. Qed.
167
168
169
Global Instance into_pure_intuitionistically P φ :
  IntoPure P φ  IntoPure ( P) φ.
Proof. rewrite /IntoPure=> ->. apply intuitionistically_elim. Qed.
170
Global Instance into_pure_absorbingly P φ : IntoPure P φ  IntoPure (<absorb> P) φ.
171
172
Proof. rewrite /IntoPure=> ->. by rewrite absorbingly_pure. Qed.
Global Instance into_pure_persistently P φ :
173
  IntoPure P φ  IntoPure (<pers> P) φ.
174
Proof. rewrite /IntoPure=> ->. apply: persistently_elim. Qed.
175
Global Instance into_pure_embed `{BiEmbed PROP PROP'} P φ :
176
  IntoPure P φ  IntoPure P φ.
177
Proof. rewrite /IntoPure=> ->. by rewrite embed_pure. Qed.
178

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

231
Global Instance from_pure_persistently P a φ :
232
  FromPure true P φ  FromPure a (<pers> P) φ.
233
234
Proof.
  rewrite /FromPure=> <- /=.
Ralf Jung's avatar
Ralf Jung committed
235
  by rewrite persistently_affinely_elim affinely_if_elim persistently_pure.
236
237
Qed.
Global Instance from_pure_affinely_true P φ :
238
  FromPure true P φ  FromPure true (<affine> P) φ.
239
240
Proof. rewrite /FromPure=><- /=. by rewrite affinely_idemp. Qed.
Global Instance from_pure_affinely_false P φ `{!Affine P} :
241
  FromPure false P φ  FromPure false (<affine> P) φ.
242
Proof. rewrite /FromPure /= affine_affinely //. Qed.
243
244
245
Global Instance from_pure_intuitionistically_true P φ :
  FromPure true P φ  FromPure true ( P) φ.
Proof.
Ralf Jung's avatar
Ralf Jung committed
246
  rewrite /FromPure=><- /=. rewrite intuitionistically_affinely_elim.
247
248
  rewrite {1}(persistent ⌜φ⌝%I) //.
Qed.
249

250
251
252
253
254
255
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.
256
Global Instance from_pure_embed `{BiEmbed PROP PROP'} a P φ :
257
  FromPure a P φ  FromPure a P φ.
Robbert Krebbers's avatar
Robbert Krebbers committed
258
Proof. rewrite /FromPure=> <-. by rewrite -embed_pure embed_affinely_if_2. Qed.
259

260
261
262
263
Global Instance from_pure_bupd `{BiBUpd PROP} a P φ :
  FromPure a P φ  FromPure a (|==> P) φ.
Proof. rewrite /FromPure=> <-. apply bupd_intro. Qed.

264
(** IntoPersistent *)
265
Global Instance into_persistent_persistently p P Q :
266
  IntoPersistent true P Q  IntoPersistent p (<pers> P) Q | 0.
Robbert Krebbers's avatar
Robbert Krebbers committed
267
268
269
270
Proof.
  rewrite /IntoPersistent /= => ->.
  destruct p; simpl; auto using persistently_idemp_1.
Qed.
271
Global Instance into_persistent_affinely p P Q :
272
  IntoPersistent p P Q  IntoPersistent p (<affine> P) Q | 0.
273
Proof. rewrite /IntoPersistent /= => <-. by rewrite affinely_elim. Qed.
274
Global Instance into_persistent_intuitionistically p P Q :
275
276
277
278
279
  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
280
    intuitionistically_into_persistently_1.
281
Qed.
282
Global Instance into_persistent_embed `{BiEmbed PROP PROP'} p P Q :
283
284
  IntoPersistent p P Q  IntoPersistent p P Q | 0.
Proof.
285
  rewrite /IntoPersistent -embed_persistently -embed_persistently_if=> -> //.
286
Qed.
287
Global Instance into_persistent_here P : IntoPersistent true P P | 1.
Robbert Krebbers's avatar
Robbert Krebbers committed
288
Proof. by rewrite /IntoPersistent. Qed.
289
290
Global Instance into_persistent_persistent P :
  Persistent P  IntoPersistent false P P | 100.
291
Proof. intros. by rewrite /IntoPersistent. Qed.
292

293
(** FromModal *)
294
Global Instance from_modal_affinely P :
295
  FromModal modality_affinely (<affine> P) (<affine> P) P | 2.
296
297
298
Proof. by rewrite /FromModal. Qed.

Global Instance from_modal_persistently P :
299
  FromModal modality_persistently (<pers> P) (<pers> P) P | 2.
300
Proof. by rewrite /FromModal. Qed.
301
302
Global Instance from_modal_intuitionistically P :
  FromModal modality_intuitionistically ( P) ( P) P | 1.
303
Proof. by rewrite /FromModal. Qed.
304
Global Instance from_modal_intuitionistically_affine_bi P :
305
  BiAffine PROP  FromModal modality_persistently ( P) ( P) P | 0.
Ralf Jung's avatar
Ralf Jung committed
306
307
308
Proof.
  intros. by rewrite /FromModal /= intuitionistically_into_persistently.
Qed.
309

310
Global Instance from_modal_absorbingly P :
311
  FromModal modality_id (<absorb> P) (<absorb> P) P.
312
313
314
Proof. by rewrite /FromModal /= -absorbingly_intro. Qed.

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

320
Global Instance from_modal_id_embed `{BiEmbed PROP PROP'} `(sel : A) P Q :
321
  FromModal modality_id sel P Q 
322
  FromModal modality_id sel P Q | 100.
323
324
Proof. by rewrite /FromModal /= =><-. Qed.

325
Global Instance from_modal_affinely_embed `{BiEmbed PROP PROP'} `(sel : A) P Q :
326
  FromModal modality_affinely sel P Q 
327
  FromModal modality_affinely sel P Q | 100.
Robbert Krebbers's avatar
Robbert Krebbers committed
328
Proof. rewrite /FromModal /= =><-. by rewrite embed_affinely_2. Qed.
329
Global Instance from_modal_persistently_embed `{BiEmbed PROP PROP'} `(sel : A) P Q :
330
  FromModal modality_persistently sel P Q 
331
  FromModal modality_persistently sel P Q | 100.
332
Proof. rewrite /FromModal /= =><-. by rewrite embed_persistently. Qed.
333
334
335
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
336
Proof. rewrite /FromModal /= =><-. by rewrite embed_intuitionistically_2. Qed.
337

338
339
340
341
Global Instance from_modal_bupd `{BiBUpd PROP} P :
  FromModal modality_id (|==> P) (|==> P) P.
Proof. by rewrite /FromModal /= -bupd_intro. Qed.

342
(** IntoWand *)
343
344
345
346
347
348
349
350
351
352
Global Instance into_wand_wand' p q (P Q P' Q' : PROP) :
  IntoWand' p q (P - Q) P' Q'  IntoWand p q (P - Q) P' Q' | 100.
Proof. done. Qed.
Global Instance into_wand_impl' p q (P Q P' Q' : PROP) :
  IntoWand' p q (P  Q) P' Q'  IntoWand p q (P  Q) P' Q' | 100.
Proof. done. Qed.
Global Instance into_wand_wandM' p q mP (Q P' Q' : PROP) :
  IntoWand' p q (mP -? Q) P' Q'  IntoWand p q (mP -? Q) P' Q' | 100.
Proof. done. Qed.

Robbert Krebbers's avatar
Robbert Krebbers committed
353
354
Global Instance into_wand_wand p q P Q P' :
  FromAssumption q P P'  IntoWand p q (P' - Q) P Q.
355
Proof.
356
  rewrite /FromAssumption /IntoWand=> HP. by rewrite HP intuitionistically_if_elim.
Robbert Krebbers's avatar
Robbert Krebbers committed
357
Qed.
358
359
Global Instance into_wand_impl_false_false P Q P' :
  Absorbing P'  Absorbing (P'  Q) 
Robbert Krebbers's avatar
Robbert Krebbers committed
360
361
  FromAssumption false P P'  IntoWand false false (P'  Q) P Q.
Proof.
362
  rewrite /FromAssumption /IntoWand /= => ?? ->. apply wand_intro_r.
Robbert Krebbers's avatar
Robbert Krebbers committed
363
364
365
  by rewrite sep_and impl_elim_l.
Qed.
Global Instance into_wand_impl_false_true P Q P' :
366
  Absorbing P'  FromAssumption true P P' 
Robbert Krebbers's avatar
Robbert Krebbers committed
367
  IntoWand false true (P'  Q) P Q.
368
Proof.
369
  rewrite /IntoWand /FromAssumption /= => ? HP. apply wand_intro_l.
370
371
  rewrite -(intuitionistically_idemp P) HP.
  by rewrite -persistently_and_intuitionistically_sep_l persistently_elim impl_elim_r.
372
Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
373
Global Instance into_wand_impl_true_false P Q P' :
374
  Affine P'  FromAssumption false P P' 
Robbert Krebbers's avatar
Robbert Krebbers committed
375
  IntoWand true false (P'  Q) P Q.
376
Proof.
377
  rewrite /FromAssumption /IntoWand /= => ? HP. apply wand_intro_r.
378
  rewrite HP sep_and intuitionistically_elim impl_elim_l //.
379
Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
380
381
Global Instance into_wand_impl_true_true P Q P' :
  FromAssumption true P P'  IntoWand true true (P'  Q) P Q.
382
Proof.
Robbert Krebbers's avatar
Robbert Krebbers committed
383
  rewrite /FromAssumption /IntoWand /= => <-. apply wand_intro_l.
384
  rewrite sep_and [( (_  _))%I]intuitionistically_elim impl_elim_r //.
385
Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
386

387
388
389
390
Global Instance into_wand_wandM p q mP' P Q :
  FromAssumption q P (pm_default emp%I mP')  IntoWand p q (mP' -? Q) P Q.
Proof. rewrite /IntoWand wandM_sound. exact: into_wand_wand. Qed.

Robbert Krebbers's avatar
Robbert Krebbers committed
391
392
393
394
395
396
397
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.

398
399
400
Global Instance into_wand_forall_prop_true p (φ : Prop) P :
  IntoWand p true ( _ : φ, P)  φ  P.
Proof.
401
402
  rewrite /IntoWand (intuitionistically_if_elim p) /=
          -impl_wand_intuitionistically -pure_impl_forall
403
404
405
406
407
408
          bi.persistently_elim //.
Qed.
Global Instance into_wand_forall_prop_false p (φ : Prop) P :
  Absorbing P  IntoWand p false ( _ : φ, P)  φ  P.
Proof.
  intros ?.
409
  rewrite /IntoWand (intuitionistically_if_elim p) /= pure_wand_forall //.
410
Qed.
411

Robbert Krebbers's avatar
Robbert Krebbers committed
412
413
414
415
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.

416
417
418
419
Global Instance into_wand_tforall {A} p q (Φ : tele_arg A  PROP) P Q x :
  IntoWand p q (Φ x) P Q  IntoWand p q (.. x, Φ x) P Q.
Proof. rewrite /IntoWand=> <-. by rewrite bi_tforall_forall (forall_elim x). Qed.

420
421
422
423
424
425
426
427
428
429
430
431
432
433
434
435
436
437
438
439
440
441
442
443
444
445
446
447
448
449
450
451
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.

452
Global Instance into_wand_intuitionistically p q R P Q :
453
454
  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
455
Global Instance into_wand_persistently_true q R P Q :
456
  IntoWand true q R P Q  IntoWand true q (<pers> R) P Q.
Ralf Jung's avatar
Ralf Jung committed
457
Proof. by rewrite /IntoWand /= intuitionistically_persistently_elim. Qed.
458
459
460
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.
461

462
463
464
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.
465
466
467
468
469
470
471
472
473
474
475
476
477
478
479
480
481
482
483
484
485
486
487

(* 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
488

489
490
491
492
493
494
495
496
497
498
499
500
501
502
503
504
505
506
507
508

Global Instance into_wand_bupd `{BiBUpd PROP} p q R P Q :
  IntoWand false false R P Q  IntoWand p q (|==> R) (|==> P) (|==> Q).
Proof.
  rewrite /IntoWand /= => HR. rewrite !intuitionistically_if_elim HR.
  apply wand_intro_l. by rewrite bupd_sep wand_elim_r.
Qed.
Global Instance into_wand_bupd_persistent `{BiBUpd PROP} p q R P Q :
  IntoWand false q R P Q  IntoWand p q (|==> R) P (|==> Q).
Proof.
  rewrite /IntoWand /= => HR. rewrite intuitionistically_if_elim HR.
  apply wand_intro_l. by rewrite bupd_frame_l wand_elim_r.
Qed.
Global Instance into_wand_bupd_args `{BiBUpd PROP} p q R P Q :
  IntoWand p false R P Q  IntoWand' p q R (|==> P) (|==> Q).
Proof.
  rewrite /IntoWand' /IntoWand /= => ->.
  apply wand_intro_l. by rewrite intuitionistically_if_elim bupd_wand_r.
Qed.

509
(** FromWand *)
510
511
Global Instance from_wand_wand P1 P2 : FromWand (P1 - P2) P1 P2.
Proof. by rewrite /FromWand. Qed.
512
513
514
Global Instance from_wand_wandM mP1 P2 :
  FromWand (mP1 -? P2) (pm_default emp mP1)%I P2.
Proof. by rewrite /FromWand wandM_sound. Qed.
515
Global Instance from_wand_embed `{BiEmbed PROP PROP'} P Q1 Q2 :
516
  FromWand P Q1 Q2  FromWand P Q1 Q2.
517
Proof. by rewrite /FromWand -embed_wand => <-. Qed.
518

519
(** FromImpl *)
520
521
Global Instance from_impl_impl P1 P2 : FromImpl (P1  P2) P1 P2.
Proof. by rewrite /FromImpl. Qed.
522
Global Instance from_impl_embed `{BiEmbed PROP PROP'} P Q1 Q2 :
523
  FromImpl P Q1 Q2  FromImpl P Q1 Q2.
524
Proof. by rewrite /FromImpl -embed_impl => <-. Qed.
525

526
(** FromAnd *)
Robbert Krebbers's avatar
Robbert Krebbers committed
527
528
529
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 :
530
  Persistent P1  IntoAbsorbingly P1' P1  FromAnd (P1  P2) P1' P2 | 9.
531
Proof.
532
533
534
  rewrite /IntoAbsorbingly /FromAnd=> ? ->.
  rewrite persistent_and_affinely_sep_l_1 {1}(persistent_persistently_2 P1).
  by rewrite absorbingly_elim_persistently -{2}(intuitionistically_elim P1).
535
Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
536
Global Instance from_and_sep_persistent_r P1 P2 P2' :
537
  Persistent P2  IntoAbsorbingly P2' P2  FromAnd (P1  P2) P1 P2' | 10.
538
Proof.
539
540
541
  rewrite /IntoAbsorbingly /FromAnd=> ? ->.
  rewrite persistent_and_affinely_sep_r_1 {1}(persistent_persistently_2 P2).
  by rewrite absorbingly_elim_persistently -{2}(intuitionistically_elim P2).
542
543
Qed.

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

Robbert Krebbers's avatar
Robbert Krebbers committed
547
Global Instance from_and_persistently P Q1 Q2 :
548
  FromAnd P Q1 Q2 
549
  FromAnd (<pers> P) (<pers> Q1) (<pers> Q2).
Robbert Krebbers's avatar
Robbert Krebbers committed
550
551
Proof. rewrite /FromAnd=> <-. by rewrite persistently_and. Qed.
Global Instance from_and_persistently_sep P Q1 Q2 :
552
  FromSep P Q1 Q2 
553
  FromAnd (<pers> P) (<pers> Q1) (<pers> Q2) | 11.
Robbert Krebbers's avatar
Robbert Krebbers committed
554
Proof. rewrite /FromAnd=> <-. by rewrite -persistently_and persistently_and_sep. Qed.
555

556
Global Instance from_and_embed `{BiEmbed PROP PROP'} P Q1 Q2 :
557
  FromAnd P Q1 Q2  FromAnd P Q1 Q2.
558
Proof. by rewrite /FromAnd -embed_and => <-. Qed.
559

560
561
Global Instance from_and_big_sepL_cons_persistent {A} (Φ : nat  A  PROP) l x l' :
  IsCons l x l' 
Robbert Krebbers's avatar
Robbert Krebbers committed
562
  Persistent (Φ 0 x) 
563
564
565
566
  FromAnd ([ list] k  y  l, Φ k y) (Φ 0 x) ([ list] k  y  l', Φ (S k) y).
Proof. rewrite /IsCons=> -> ?. by rewrite /FromAnd big_sepL_cons persistent_and_sep_1. Qed.
Global Instance from_and_big_sepL_app_persistent {A} (Φ : nat  A  PROP) l l1 l2 :
  IsApp l l1 l2 
Robbert Krebbers's avatar
Robbert Krebbers committed
567
  ( k y, Persistent (Φ k y)) 
568
  FromAnd ([ list] k  y  l, Φ k y)
Robbert Krebbers's avatar
Robbert Krebbers committed
569
    ([ list] k  y  l1, Φ k y) ([ list] k  y  l2, Φ (length l1 + k) y).
570
Proof. rewrite /IsApp=> -> ?. by rewrite /FromAnd big_sepL_app persistent_and_sep_1. Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
571

572
573
574
575
576
577
578
579
580
581
582
583
584
585
586
587
588
589
590
591
592
593
Global Instance from_and_big_sepL2_cons_persistent {A B}
    (Φ : nat  A  B  PROP) l1 x1 l1' l2 x2 l2' :
  IsCons l1 x1 l1'  IsCons l2 x2 l2' 
  Persistent (Φ 0 x1 x2) 
  FromAnd ([ list] k  y1;y2  l1;l2, Φ k y1 y2)
    (Φ 0 x1 x2) ([ list] k  y1;y2  l1';l2', Φ (S k) y1 y2).
Proof.
  rewrite /IsCons=> -> -> ?.
  by rewrite /FromAnd big_sepL2_cons persistent_and_sep_1.
Qed.
Global Instance from_and_big_sepL2_app_persistent {A B}
    (Φ : nat  A  B  PROP) l1 l1' l1'' l2 l2' l2'' :
  IsApp l1 l1' l1''  IsApp l2 l2' l2'' 
  ( k y1 y2, Persistent (Φ k y1 y2)) 
  FromAnd ([ list] k  y1;y2  l1;l2, Φ k y1 y2)
    ([ list] k  y1;y2  l1';l2', Φ k y1 y2)
    ([ list] k  y1;y2  l1'';l2'', Φ (length l1' + k) y1 y2).
Proof.
  rewrite /IsApp=> -> -> ?. rewrite /FromAnd persistent_and_sep_1.
  apply wand_elim_l', big_sepL2_app.
Qed.

594
(** FromSep *)
Robbert Krebbers's avatar
Robbert Krebbers committed
595
596
597
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
598
  TCOr (Affine P1) (Absorbing P2)  TCOr (Absorbing P1) (Affine P2) 
Robbert Krebbers's avatar
Robbert Krebbers committed
599
600
601
602
603
604
  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.

605
Global Instance from_sep_affinely P Q1 Q2 :
606
  FromSep P Q1 Q2  FromSep (<affine> P) (<affine> Q1) (<affine> Q2).
607
Proof. rewrite /FromSep=> <-. by rewrite affinely_sep_2. Qed.
608
609
610
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.
611
Global Instance from_sep_absorbingly P Q1 Q2 :
612
  FromSep P Q1 Q2  FromSep (<absorb> P) (<absorb> Q1) (<absorb> Q2).
613
Proof. rewrite /FromSep=> <-. by rewrite absorbingly_sep. Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
614
Global Instance from_sep_persistently P Q1 Q2 :
615
  FromSep P Q1 Q2 
616
  FromSep (<pers> P) (<pers> Q1) (<pers> Q2).
617
Proof. rewrite /FromSep=> <-. by rewrite persistently_sep_2. Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
618

619
Global Instance from_sep_embed `{BiEmbed PROP PROP'} P Q1 Q2 :
620
  FromSep P Q1 Q2  FromSep P Q1 Q2.
621
Proof. by rewrite /FromSep -embed_sep => <-. Qed.
622

623
624
625
626
627
628
629
Global Instance from_sep_big_sepL_cons {A} (Φ : nat  A  PROP) l x l' :
  IsCons l x l' 
  FromSep ([ list] k  y  l, Φ k y) (Φ 0 x) ([ list] k  y  l', Φ (S k) y).
Proof. rewrite /IsCons=> ->. by rewrite /FromSep big_sepL_cons. Qed.
Global Instance from_sep_big_sepL_app {A} (Φ : nat  A  PROP) l l1 l2 :
  IsApp l l1 l2 
  FromSep ([ list] k  y  l, Φ k y)
Robbert Krebbers's avatar
Robbert Krebbers committed
630
    ([ list] k  y  l1, Φ k y) ([ list] k  y  l2, Φ (length l1 + k) y).
631
Proof. rewrite /IsApp=> ->. by rewrite /FromSep big_opL_app. Qed.
632

633
634
635
636
637
638
639
640
641
642
643
644
645
646
Global Instance from_sep_big_sepL2_cons {A B} (Φ : nat  A  B  PROP)
    l1 x1 l1' l2 x2 l2' :
  IsCons l1 x1 l1'  IsCons l2 x2 l2' 
  FromSep ([ list] k  y1;y2  l1;l2, Φ k y1 y2)
    (Φ 0 x1 x2) ([ list] k  y1;y2  l1';l2', Φ (S k) y1 y2).
Proof. rewrite /IsCons=> -> ->. by rewrite /FromSep big_sepL2_cons. Qed.
Global Instance from_sep_big_sepL2_app {A B} (Φ : nat  A  B  PROP)
    l1 l1' l1'' l2 l2' l2'' :
  IsApp l1 l1' l1''  IsApp l2 l2' l2'' 
  FromSep ([ list] k  y1;y2  l1;l2, Φ k y1 y2)
    ([ list] k  y1;y2  l1';l2', Φ k y1 y2)
    ([ list] k  y1;y2  l1'';l2'', Φ (length l1' + k) y1 y2).
Proof. rewrite /IsApp=>-> ->. apply wand_elim_l', big_sepL2_app. Qed.

647
648
649
650
Global Instance from_sep_bupd `{BiBUpd PROP} P Q1 Q2 :
  FromSep P Q1 Q2  FromSep (|==> P) (|==> Q1) (|==> Q2).
Proof. rewrite /FromSep=><-. apply bupd_sep. Qed.

651
(** IntoAnd *)
652
Global Instance into_and_and p P Q : IntoAnd p (P  Q) P Q | 10.
653
Proof. by rewrite /IntoAnd intuitionistically_if_and. Qed.
654
Global Instance into_and_and_affine_l P Q Q' :
655
  Affine P  FromAffinely Q' Q  IntoAnd false (P  Q) P Q'.
656
657
Proof.
  intros. rewrite /IntoAnd /=.
658
  by rewrite -(affine_affinely P) affinely_and_l affinely_and (from_affinely Q').
659
660
Qed.
Global Instance into_and_and_affine_r P P' Q :
661
  Affine Q  FromAffinely P' P  IntoAnd false (P  Q) P' Q.
662
663
Proof.
  intros. rewrite /IntoAnd /=.
664
  by rewrite -(affine_affinely Q) affinely_and_r affinely_and (from_affinely P').
665
666
Qed.

667
Global Instance into_and_sep `{BiPositive PROP} P Q : IntoAnd true (P  Q) P Q.
668
Proof.
669
  rewrite /IntoAnd /= intuitionistically_sep -and_sep_intuitionistically intuitionistically_and //.
670
Qed.
671
Global Instance into_and_sep_affine P Q :
Ralf Jung's avatar
Ralf Jung committed
672
  TCOr (Affine P) (Absorbing Q)  TCOr (Absorbing P) (Affine Q) 
673
674
  IntoAnd true (P  Q) P Q.
Proof. intros. by rewrite /IntoAnd /= sep_and. Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
675
676

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

679
Global Instance into_and_affinely p P Q1 Q2 :
680
  IntoAnd p P Q1 Q2  IntoAnd p (<affine> P) (<affine> Q1) (<affine> Q2).
Robbert Krebbers's avatar
Robbert Krebbers committed
681
Proof.
Robbert Krebbers's avatar
Robbert Krebbers committed
682
  rewrite /IntoAnd. destruct p; simpl.
Ralf Jung's avatar
Ralf Jung committed
683
  - rewrite -affinely_and !intuitionistically_affinely_elim //.
684
  - intros ->. by rewrite affinely_and.
Robbert Krebbers's avatar
Robbert Krebbers committed
685
Qed.
686
687
688
689
690
691
692
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
693
Global Instance into_and_persistently p P Q1 Q2 :
694
  IntoAnd p P Q1 Q2 
695
  IntoAnd p (<pers> P) (<pers> Q1) (<pers> Q2).
Robbert Krebbers's avatar
Robbert Krebbers committed
696
Proof.
Robbert Krebbers's avatar
Robbert Krebbers committed
697
  rewrite /IntoAnd /=. destruct p; simpl.
Ralf Jung's avatar
Ralf Jung committed
698
  - rewrite -persistently_and !intuitionistically_persistently_elim //.
Robbert Krebbers's avatar
Robbert Krebbers committed
699
  - intros ->. by rewrite persistently_and.
Robbert Krebbers's avatar
Robbert Krebbers committed
700
Qed.
701
Global Instance into_and_embed `{BiEmbed PROP PROP'} p P Q1 Q2 :
702
703
  IntoAnd p P Q1 Q2  IntoAnd p P Q1 Q2.
Proof.
Robbert Krebbers's avatar
Robbert Krebbers committed
704
705
  rewrite /IntoAnd -embed_and=> HP. apply intuitionistically_if_intro'.
  by rewrite embed_intuitionistically_if_2 HP intuitionistically_if_elim.
706
Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
707

708
(** IntoSep *)
709
710
Global Instance into_sep_sep P Q : IntoSep (P  Q) P Q.
Proof. by rewrite /IntoSep. Qed.
711

712
Inductive AndIntoSep : PROP  PROP  PROP  PROP  Prop :=
713
  | and_into_sep_affine P Q Q' : Affine P  FromAffinely Q' Q  AndIntoSep P P Q Q'
714
  | and_into_sep P Q : AndIntoSep P (<affine> P)%I Q Q.
715
716
717
718
719
720
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'.
721
Proof.
722
  destruct 2 as [P Q Q'|P Q]; rewrite /IntoSep.
723
724
725
  - 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.
726
Qed.
727
728
Global Instance into_sep_and_persistent_r P P' Q Q' :
  Persistent Q  AndIntoSep Q Q' P P'  IntoSep (P  Q) P' Q'.
729
Proof.
730
  destruct 2 as [Q P P'|Q P]; rewrite /IntoSep.
731
732
733
  - 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.
734
Qed.
735

736
737
738
Global Instance into_sep_pure φ ψ : @IntoSep PROP ⌜φ  ψ⌝ ⌜φ⌝ ⌜ψ⌝.
Proof. by rewrite /IntoSep pure_and persistent_and_sep_1. Qed.

739
Global Instance into_sep_embed `{BiEmbed PROP PROP'} P Q1 Q2 :
740
  IntoSep P Q1 Q2  IntoSep P Q1 Q2.
741
Proof. rewrite /IntoSep -embed_sep=> -> //. Qed.
742

743
Global Instance into_sep_affinely `{BiPositive PROP} P Q1 Q2 :
744
  IntoSep P Q1 Q2  IntoSep (<affine> P) (<affine> Q1) (<affine> Q2) | 0.
Robbert Krebbers's avatar