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

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

10
11
12
13
14
(* 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.
15

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

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

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

41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
Global Instance from_assumption_affinely_plainly_l p P Q :
  FromAssumption true P Q  FromAssumption p ( P) Q.
Proof.
  rewrite /FromAssumption /= =><-.
  by rewrite affinely_persistently_if_elim plainly_elim_persistently.
Qed.
Global Instance from_assumption_plainly_l_true P Q :
  FromAssumption true P Q  FromAssumption true (bi_plainly P) Q.
Proof.
  rewrite /FromAssumption /= =><-.
  by rewrite persistently_elim plainly_elim_persistently.
Qed.
Global Instance from_assumption_plainly_l_false `{AffineBI PROP} P Q :
  FromAssumption true P Q  FromAssumption false (bi_plainly P) Q.
Proof.
  rewrite /FromAssumption /= =><-.
  by rewrite affine_affinely plainly_elim_persistently.
Qed.
59
Global Instance from_assumption_affinely_persistently_l p P Q :
60
  FromAssumption true P Q  FromAssumption p ( P) Q.
61
Proof. rewrite /FromAssumption /= =><-. by rewrite affinely_persistently_if_elim. Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
62
Global Instance from_assumption_persistently_l_true P Q :
63
  FromAssumption true P Q  FromAssumption true (bi_persistently P) Q.
Robbert Krebbers's avatar
Robbert Krebbers committed
64
65
Proof. rewrite /FromAssumption /= =><-. by rewrite persistently_idemp. Qed.
Global Instance from_assumption_persistently_l_false `{AffineBI PROP} P Q :
66
  FromAssumption true P Q  FromAssumption false (bi_persistently P) Q.
67
68
69
70
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
71
72

Global Instance from_assumption_forall {A} p (Φ : A  PROP) Q x :
73
74
  FromAssumption p (Φ x) Q  FromAssumption p ( x, Φ x) Q.
Proof. rewrite /FromAssumption=> <-. by rewrite forall_elim. Qed.
75
76

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

80
Global Instance into_pure_eq {A : ofeT} (a b : A) :
81
82
  Discrete a  @IntoPure M (a  b) (a  b).
Proof. intros. by rewrite /IntoPure discrete_eq. Qed.
83

Ralf Jung's avatar
Ralf Jung committed
84
Global Instance into_pure_pure_and (φ1 φ2 : Prop) P1 P2 :
Ralf Jung's avatar
Ralf Jung committed
85
  IntoPure P1 φ1  IntoPure P2 φ2  IntoPure (P1  P2) (φ1  φ2).
86
Proof. rewrite /IntoPure pure_and. by intros -> ->. Qed.
Ralf Jung's avatar
Ralf Jung committed
87
Global Instance into_pure_pure_or (φ1 φ2 : Prop) P1 P2 :
Ralf Jung's avatar
Ralf Jung committed
88
  IntoPure P1 φ1  IntoPure P2 φ2  IntoPure (P1  P2) (φ1  φ2).
89
Proof. rewrite /IntoPure pure_or. by intros -> ->. Qed.
Ralf Jung's avatar
Ralf Jung committed
90
Global Instance into_pure_pure_impl (φ1 φ2 : Prop) P1 P2 :
Ralf Jung's avatar
Ralf Jung committed
91
  FromPure P1 φ1  IntoPure P2 φ2  IntoPure (P1  P2) (φ1  φ2).
92
Proof. rewrite /FromPure /IntoPure pure_impl. by intros -> ->. Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
93
94
95
96
97
98
99
100
101
102
103

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
104
Global Instance into_pure_pure_wand (φ1 φ2 : Prop) P1 P2 :
Ralf Jung's avatar
Ralf Jung committed
105
  FromPure P1 φ1  IntoPure P2 φ2  IntoPure (P1 - P2) (φ1  φ2).
Robbert Krebbers's avatar
Robbert Krebbers committed
106
Proof. rewrite /FromPure /IntoPure=> <- ->. by rewrite pure_impl impl_wand_2. Qed.
107

108
109
110
Global Instance into_pure_affinely P φ :
  IntoPure P φ  IntoPure (bi_affinely P) φ.
Proof. rewrite /IntoPure=> ->. apply affinely_elim. Qed.
111
Global Instance into_pure_absorbingly P φ : IntoPure P φ  IntoPure (bi_absorbingly P) φ.
112
Proof. rewrite /IntoPure=> ->. by rewrite absorbingly_pure. Qed.
113
114
Global Instance into_pure_plainly P φ : IntoPure P φ  IntoPure (bi_plainly P) φ.
Proof. rewrite /IntoPure=> ->. apply: plainly_elim. Qed.
115
116
Global Instance into_pure_persistently P φ :
  IntoPure P φ  IntoPure (bi_persistently P) φ.
117
Proof. rewrite /IntoPure=> ->. apply: persistently_elim. Qed.
118

119
(* FromPure *)
Robbert Krebbers's avatar
Robbert Krebbers committed
120
121
Global Instance from_pure_pure φ : @FromPure PROP ⌜φ⌝ φ.
Proof. by rewrite /FromPure. Qed.
122
Global Instance from_pure_internal_eq {A : ofeT} (a b : A) :
Robbert Krebbers's avatar
Robbert Krebbers committed
123
124
  @FromPure PROP (a  b) (a  b).
Proof. by rewrite /FromPure pure_internal_eq. Qed.
125

Ralf Jung's avatar
Ralf Jung committed
126
Global Instance from_pure_pure_and (φ1 φ2 : Prop) P1 P2 :
127
  FromPure P1 φ1  FromPure P2 φ2  FromPure (P1  P2) (φ1  φ2).
128
Proof. rewrite /FromPure pure_and. by intros -> ->. Qed.
Ralf Jung's avatar
Ralf Jung committed
129
Global Instance from_pure_pure_or (φ1 φ2 : Prop) P1 P2 :
130
  FromPure P1 φ1  FromPure P2 φ2  FromPure (P1  P2) (φ1  φ2).
131
Proof. rewrite /FromPure pure_or. by intros -> ->. Qed.
Ralf Jung's avatar
Ralf Jung committed
132
Global Instance from_pure_pure_impl (φ1 φ2 : Prop) P1 P2 :
133
  IntoPure P1 φ1  FromPure P2 φ2  FromPure (P1  P2) (φ1  φ2).
134
Proof. rewrite /FromPure /IntoPure pure_impl. by intros -> ->. Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
135
136
137
138
139
140
141
142
143
144

Global Instance from_pure_exist {A} (Φ : A  PROP) (φ : A  Prop) :
  ( x, FromPure (Φ x) (φ x))  FromPure ( x, Φ x) ( x, φ x).
Proof. rewrite /FromPure=>Hx. rewrite pure_exist. by setoid_rewrite Hx. Qed.
Global Instance from_pure_forall {A} (Φ : A  PROP) (φ : A  Prop) :
  ( x, FromPure (Φ x) (φ x))  FromPure ( x, Φ x) ( x, φ x).
Proof. rewrite /FromPure=>Hx. rewrite pure_forall. by setoid_rewrite Hx. Qed.

Global Instance from_pure_pure_sep (φ1 φ2 : Prop) P1 P2 :
  FromPure P1 φ1  FromPure P2 φ2  FromPure (P1  P2) (φ1  φ2).
145
Proof. rewrite /FromPure=> <- <-. by rewrite pure_and persistent_and_sep_1. Qed.
Ralf Jung's avatar
Ralf Jung committed
146
Global Instance from_pure_pure_wand (φ1 φ2 : Prop) P1 P2 :
147
  IntoPure P1 φ1  FromPure P2 φ2  FromPure (P1 - P2) (φ1  φ2).
148
Proof.
Robbert Krebbers's avatar
Robbert Krebbers committed
149
150
  rewrite /FromPure /IntoPure=> -> <-.
  by rewrite pure_wand_forall pure_impl pure_impl_forall.
151
152
Qed.

153
154
155
Global Instance from_pure_plainly P φ :
  FromPure P φ  FromPure (bi_plainly P) φ.
Proof. rewrite /FromPure=> <-. by rewrite plainly_pure. Qed.
156
157
Global Instance from_pure_persistently P φ :
  FromPure P φ  FromPure (bi_persistently P) φ.
Robbert Krebbers's avatar
Robbert Krebbers committed
158
Proof. rewrite /FromPure=> <-. by rewrite persistently_pure. Qed.
159
160
161
Global Instance from_pure_affinely P φ `{!Affine P} :
  FromPure P φ  FromPure (bi_affinely P) φ.
Proof. by rewrite /FromPure affine_affinely. Qed.
162
Global Instance from_pure_absorbingly P φ : FromPure P φ  FromPure (bi_absorbingly P) φ.
163
Proof. rewrite /FromPure=> <-. by rewrite absorbingly_pure. Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
164

165
166
167
168
(* IntoInternalEq *)
Global Instance into_internal_eq_internal_eq {A : ofeT} (x y : A) :
  @IntoInternalEq PROP A (x  y) x y.
Proof. by rewrite /IntoInternalEq. Qed.
169
170
171
172
Global Instance into_internal_eq_affinely {A : ofeT} (x y : A) P :
  IntoInternalEq P x y  IntoInternalEq (bi_affinely P) x y.
Proof. rewrite /IntoInternalEq=> ->. by rewrite affinely_elim. Qed.
Global Instance into_internal_eq_absorbingly {A : ofeT} (x y : A) P :
173
  IntoInternalEq P x y  IntoInternalEq (bi_absorbingly P) x y.
174
175
176
177
Proof. rewrite /IntoInternalEq=> ->. by rewrite absorbingly_internal_eq. Qed.
Global Instance into_internal_eq_plainly {A : ofeT} (x y : A) P :
  IntoInternalEq P x y  IntoInternalEq (bi_plainly P) x y.
Proof. rewrite /IntoInternalEq=> ->. by rewrite plainly_elim. Qed.
178
Global Instance into_internal_eq_persistently {A : ofeT} (x y : A) P :
179
  IntoInternalEq P x y  IntoInternalEq (bi_persistently P) x y.
180
181
Proof. rewrite /IntoInternalEq=> ->. by rewrite persistently_elim. Qed.

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

198
(* FromAlways *)
199
Global Instance from_always_here P : FromAlways false false false P P | 1.
200
Proof. by rewrite /FromAlways. Qed.
201
202
Global Instance from_always_plainly a pe pl P Q :
  FromAlways a pe pl P Q  FromAlways false true true (bi_plainly P) Q | 0.
203
Proof.
204
205
206
  rewrite /FromAlways /= => <-.
  destruct a, pe, pl; rewrite /= ?persistently_affinely ?plainly_affinely
       !persistently_plainly ?plainly_idemp ?plainly_persistently //.
Robbert Krebbers's avatar
Robbert Krebbers committed
207
Qed.
208
209
Global Instance from_always_persistently a pe pl P Q :
  FromAlways a pe pl P Q  FromAlways false true pl (bi_persistently P) Q | 0.
210
Proof.
211
212
  rewrite /FromAlways /= => <-.
  destruct a, pe; rewrite /= ?persistently_affinely ?persistently_idemp //.
213
Qed.
214
215
Global Instance from_always_affinely a pe pl P Q :
  FromAlways a pe pl P Q  FromAlways true pe pl (bi_affinely P) Q | 0.
216
Proof.
217
  rewrite /FromAlways /= => <-. destruct a; by rewrite /= ?affinely_idemp.
218
Qed.
219

Robbert Krebbers's avatar
Robbert Krebbers committed
220
221
222
(* IntoWand *)
Global Instance into_wand_wand p q P Q P' :
  FromAssumption q P P'  IntoWand p q (P' - Q) P Q.
223
Proof.
224
  rewrite /FromAssumption /IntoWand=> HP. by rewrite HP affinely_persistently_if_elim.
Robbert Krebbers's avatar
Robbert Krebbers committed
225
Qed.
226

Robbert Krebbers's avatar
Robbert Krebbers committed
227
228
229
230
231
232
Global Instance into_wand_impl_false_false `{!AffineBI PROP} P Q P' :
  FromAssumption false P P'  IntoWand false false (P'  Q) P Q.
Proof.
  rewrite /FromAssumption /IntoWand /= => ->. apply wand_intro_r.
  by rewrite sep_and impl_elim_l.
Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
233

Robbert Krebbers's avatar
Robbert Krebbers committed
234
Global Instance into_wand_impl_false_true P Q P' :
235
  Absorbing P'  FromAssumption true P P' 
Robbert Krebbers's avatar
Robbert Krebbers committed
236
  IntoWand false true (P'  Q) P Q.
237
Proof.
238
  rewrite /IntoWand /FromAssumption /= => ? HP. apply wand_intro_l.
239
240
  rewrite -(affinely_persistently_idemp P) HP.
  by rewrite -persistently_and_affinely_sep_l persistently_elim impl_elim_r.
241
242
Qed.

Robbert Krebbers's avatar
Robbert Krebbers committed
243
Global Instance into_wand_impl_true_false P Q P' :
244
  Affine P'  FromAssumption false P P' 
Robbert Krebbers's avatar
Robbert Krebbers committed
245
  IntoWand true false (P'  Q) P Q.
246
Proof.
247
  rewrite /FromAssumption /IntoWand /= => ? HP. apply wand_intro_r.
248
249
  rewrite -persistently_and_affinely_sep_l HP -{2}(affine_affinely P') -affinely_and_lr.
  by rewrite affinely_persistently_elim impl_elim_l.
250
Qed.
251

Robbert Krebbers's avatar
Robbert Krebbers committed
252
253
Global Instance into_wand_impl_true_true P Q P' :
  FromAssumption true P P'  IntoWand true true (P'  Q) P Q.
254
Proof.
Robbert Krebbers's avatar
Robbert Krebbers committed
255
  rewrite /FromAssumption /IntoWand /= => <-. apply wand_intro_l.
256
257
  rewrite -{1}(affinely_persistently_idemp P) -and_sep_affinely_persistently.
  by rewrite -affinely_persistently_and impl_elim_r affinely_persistently_elim.
258
Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
259
260
261
262
263
264
265
266
267
268
269
270

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.

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.

271
272
273
274
275
276
277
278
279
280
281
282
283
Global Instance into_wand_affinely_plainly p q R P Q :
  IntoWand p q R P Q  IntoWand p q ( R) P Q.
Proof. by rewrite /IntoWand affinely_plainly_elim. Qed.
Global Instance into_wand_plainly_true q R P Q :
  IntoWand true q R P Q  IntoWand true q (bi_plainly R) P Q.
Proof. by rewrite /IntoWand /= persistently_plainly plainly_elim_persistently. Qed.
Global Instance into_wand_plainly_false `{!AffineBI PROP} q R P Q :
  IntoWand false q R P Q  IntoWand false q (bi_plainly R) P Q.
Proof. by rewrite /IntoWand plainly_elim. Qed.

Global Instance into_wand_affinely_persistently p q R P Q :
  IntoWand p q R P Q  IntoWand p q ( R) P Q.
Proof. by rewrite /IntoWand affinely_persistently_elim. Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
284
Global Instance into_wand_persistently_true q R P Q :
285
  IntoWand true q R P Q  IntoWand true q (bi_persistently R) P Q.
Robbert Krebbers's avatar
Robbert Krebbers committed
286
287
Proof. by rewrite /IntoWand /= persistently_idemp. Qed.
Global Instance into_wand_persistently_false `{!AffineBI PROP} q R P Q :
288
  IntoWand false q R P Q  IntoWand false q (bi_persistently R) P Q.
289
Proof. by rewrite /IntoWand persistently_elim. Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
290
291
292
293
294

(* 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 :
295
  FromAffinely P1 P1'  Persistent P1'  FromAnd (P1  P2) P1' P2 | 9.
296
Proof.
297
  rewrite /FromAffinely /FromAnd=> <- ?. by rewrite persistent_and_affinely_sep_l_1.
298
Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
299
Global Instance from_and_sep_persistent_r P1 P2 P2' :
300
  FromAffinely P2 P2'  Persistent P2'  FromAnd (P1  P2) P1 P2' | 10.
301
Proof.
302
  rewrite /FromAffinely /FromAnd=> <- ?. by rewrite persistent_and_affinely_sep_r_1.
303
Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
304
305
Global Instance from_and_sep_persistent P1 P2 :
  Persistent P1  Persistent P2  FromAnd (P1  P2) P1 P2 | 11.
306
Proof.
307
  rewrite /FromAffinely /FromAnd. intros ??. by rewrite -persistent_and_sep_1.
308
309
Qed.

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

313
314
315
316
317
318
319
320
321
Global Instance from_and_plainly P Q1 Q2 :
  FromAnd P Q1 Q2 
  FromAnd (bi_plainly P) (bi_plainly Q1) (bi_plainly Q2).
Proof. rewrite /FromAnd=> <-. by rewrite plainly_and. Qed.
Global Instance from_and_plainly_sep P Q1 Q2 :
  FromSep P Q1 Q2 
  FromAnd (bi_plainly P) (bi_plainly Q1) (bi_plainly Q2) | 11.
Proof. rewrite /FromAnd=> <-. by rewrite -plainly_and plainly_and_sep. Qed.

Robbert Krebbers's avatar
Robbert Krebbers committed
322
Global Instance from_and_persistently P Q1 Q2 :
323
324
  FromAnd P Q1 Q2 
  FromAnd (bi_persistently P) (bi_persistently Q1) (bi_persistently Q2).
Robbert Krebbers's avatar
Robbert Krebbers committed
325
326
Proof. rewrite /FromAnd=> <-. by rewrite persistently_and. Qed.
Global Instance from_and_persistently_sep P Q1 Q2 :
327
328
  FromSep P Q1 Q2 
  FromAnd (bi_persistently P) (bi_persistently Q1) (bi_persistently Q2) | 11.
Robbert Krebbers's avatar
Robbert Krebbers committed
329
Proof. rewrite /FromAnd=> <-. by rewrite -persistently_and persistently_and_sep. Qed.
330

Robbert Krebbers's avatar
Robbert Krebbers committed
331
332
333
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).
334
Proof. intros. by rewrite /FromAnd big_opL_cons persistent_and_sep_1. Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
335
336
337
338
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).
339
Proof. intros. by rewrite /FromAnd big_opL_app persistent_and_sep_1. Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
340
341
342
343
344

(* 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 :
345
  TCOr (TCAnd (Affine P1) (Affine P2)) (TCAnd (Absorbing P1) (Absorbing P2)) 
Robbert Krebbers's avatar
Robbert Krebbers committed
346
347
348
349
350
351
  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.

352
353
354
355
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 :
356
  FromSep P Q1 Q2  FromSep (bi_absorbingly P) (bi_absorbingly Q1) (bi_absorbingly Q2).
357
Proof. rewrite /FromSep=> <-. by rewrite absorbingly_sep. Qed.
358
359
360
361
Global Instance from_sep_plainly P Q1 Q2 :
  FromSep P Q1 Q2 
  FromSep (bi_plainly P) (bi_plainly Q1) (bi_plainly Q2).
Proof. rewrite /FromSep=> <-. by rewrite plainly_sep_2. Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
362
Global Instance from_sep_persistently P Q1 Q2 :
363
364
  FromSep P Q1 Q2 
  FromSep (bi_persistently P) (bi_persistently Q1) (bi_persistently Q2).
365
Proof. rewrite /FromSep=> <-. by rewrite persistently_sep_2. Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
366
367
368
369
370
371
372
373

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.
374

Robbert Krebbers's avatar
Robbert Krebbers committed
375
(* IntoAnd *)
376
Global Instance into_and_and p P Q : IntoAnd p (P  Q) P Q | 10.
377
Proof. by rewrite /IntoAnd affinely_persistently_if_and. Qed.
378
Global Instance into_and_and_affine_l P Q Q' :
379
  Affine P  FromAffinely Q' Q  IntoAnd false (P  Q) P Q'.
380
381
Proof.
  intros. rewrite /IntoAnd /=.
382
  by rewrite -(affine_affinely P) affinely_and_l affinely_and (from_affinely Q').
383
384
Qed.
Global Instance into_and_and_affine_r P P' Q :
385
  Affine Q  FromAffinely P' P  IntoAnd false (P  Q) P' Q.
386
387
Proof.
  intros. rewrite /IntoAnd /=.
388
  by rewrite -(affine_affinely Q) affinely_and_r affinely_and (from_affinely P').
389
390
Qed.

391
Global Instance into_and_sep `{PositiveBI PROP} P Q : IntoAnd true (P  Q) P Q.
392
393
394
Proof.
  by rewrite /IntoAnd /= persistently_sep -and_sep_persistently persistently_and.
Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
395
396

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

399
400
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
401
Proof.
Robbert Krebbers's avatar
Robbert Krebbers committed
402
  rewrite /IntoAnd. destruct p; simpl.
403
404
  - by rewrite -affinely_and !persistently_affinely.
  - intros ->. by rewrite affinely_and.
Robbert Krebbers's avatar
Robbert Krebbers committed
405
Qed.
406
407
408
Global Instance into_and_plainly p P Q1 Q2 :
  IntoAnd p P Q1 Q2 
  IntoAnd p (bi_plainly P) (bi_plainly Q1) (bi_plainly Q2).
409
Proof.
410
411
412
413
414
  rewrite /IntoAnd /=. destruct p; simpl.
  - rewrite -plainly_and persistently_plainly -plainly_persistently
            -plainly_affinely => ->.
    by rewrite plainly_affinely plainly_persistently persistently_plainly.
  - intros ->. by rewrite plainly_and.
415
Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
416
Global Instance into_and_persistently p P Q1 Q2 :
417
418
  IntoAnd p P Q1 Q2 
  IntoAnd p (bi_persistently P) (bi_persistently Q1) (bi_persistently Q2).
Robbert Krebbers's avatar
Robbert Krebbers committed
419
Proof.
Robbert Krebbers's avatar
Robbert Krebbers committed
420
421
422
  rewrite /IntoAnd /=. destruct p; simpl.
  - by rewrite -persistently_and !persistently_idemp.
  - intros ->. by rewrite persistently_and.
Robbert Krebbers's avatar
Robbert Krebbers committed
423
424
Qed.

Robbert Krebbers's avatar
Robbert Krebbers committed
425
(* IntoSep *)
426
427
Global Instance into_sep_sep P Q : IntoSep (P  Q) P Q.
Proof. by rewrite /IntoSep. Qed.
428

429
Inductive AndIntoSep : PROP  PROP  PROP  PROP  Prop :=
430
431
  | 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.
432
433
434
435
436
437
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'.
438
Proof.
439
  destruct 2 as [P Q Q'|P Q]; rewrite /IntoSep.
440
441
442
  - 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.
443
Qed.
444
445
Global Instance into_sep_and_persistent_r P P' Q Q' :
  Persistent Q  AndIntoSep Q Q' P P'  IntoSep (P  Q) P' Q'.
446
Proof.
447
  destruct 2 as [Q P P'|Q P]; rewrite /IntoSep.
448
449
450
  - 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.
451
Qed.
452
453


454
455
456
Global Instance into_sep_pure φ ψ : @IntoSep PROP ⌜φ  ψ⌝ ⌜φ⌝ ⌜ψ⌝.
Proof. by rewrite /IntoSep pure_and persistent_and_sep_1. Qed.

457
458
459
460
461
(* FIXME: This instance is kind of strange, it just gets rid of the bi_affinely. Also, it
overlaps with `into_sep_affinely_later`, and hence has lower precedence. *)
Global Instance into_sep_affinely P Q1 Q2 :
  IntoSep P Q1 Q2  IntoSep (bi_affinely P) Q1 Q2 | 20.
Proof. rewrite /IntoSep /= => ->. by rewrite affinely_elim. Qed.
462

463
464
465
Global Instance into_sep_plainly `{PositiveBI PROP} P Q1 Q2 :
  IntoSep P Q1 Q2  IntoSep (bi_plainly P) (bi_plainly Q1) (bi_plainly Q2).
Proof. rewrite /IntoSep /= => ->. by rewrite plainly_sep. Qed.
466
Global Instance into_sep_persistently `{PositiveBI PROP} P Q1 Q2 :
467
468
  IntoSep P Q1 Q2 
  IntoSep (bi_persistently P) (bi_persistently Q1) (bi_persistently Q2).
469
Proof. rewrite /IntoSep /= => ->. by rewrite persistently_sep. Qed.
470

471
472
473
(* 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. *)
474
Global Instance into_sep_big_sepL_cons {A} (Φ : nat  A  PROP) l x l' :
475
  IsCons l x l' 
476
  IntoSep ([ list] k  y  l, Φ k y)
477
    (Φ 0 x) ([ list] k  y  l', Φ (S k) y).
Robbert Krebbers's avatar
Robbert Krebbers committed
478
Proof. rewrite /IsCons=>->. by rewrite /IntoSep big_sepL_cons. Qed.
479
Global Instance into_sep_big_sepL_app {A} (Φ : nat  A  PROP) l l1 l2 :
480
  IsApp l l1 l2 
481
  IntoSep ([ list] k  y  l, Φ k y)
482
    ([ list] k  y  l1, Φ k y) ([ list] k  y  l2, Φ (length l1 + k) y).
Robbert Krebbers's avatar
Robbert Krebbers committed
483
484
485
486
487
488
489
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.
490
491
492
493
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 :
494
  FromOr P Q1 Q2  FromOr (bi_absorbingly P) (bi_absorbingly Q1) (bi_absorbingly Q2).
495
Proof. rewrite /FromOr=> <-. by rewrite absorbingly_or. Qed.
496
497
498
Global Instance from_or_plainly P Q1 Q2 :
  FromOr P Q1 Q2  FromOr (bi_plainly P) (bi_plainly Q1) (bi_plainly Q2).
Proof. rewrite /FromOr=> <-. by rewrite plainly_or. Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
499
Global Instance from_or_persistently P Q1 Q2 :
500
501
  FromOr P Q1 Q2 
  FromOr (bi_persistently P) (bi_persistently Q1) (bi_persistently Q2).
Robbert Krebbers's avatar
Robbert Krebbers committed
502
503
504
505
506
507
508
Proof. rewrite /FromOr=> <-. by rewrite persistently_or. Qed.

(* 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.
509
510
511
512
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 :
513
  IntoOr P Q1 Q2  IntoOr (bi_absorbingly P) (bi_absorbingly Q1) (bi_absorbingly Q2).
514
Proof. rewrite /IntoOr=>->. by rewrite absorbingly_or. Qed.
515
516
517
Global Instance into_or_plainly P Q1 Q2 :
  IntoOr P Q1 Q2  IntoOr (bi_plainly P) (bi_plainly Q1) (bi_plainly Q2).
Proof. rewrite /IntoOr=>->. by rewrite plainly_or. Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
518
Global Instance into_or_persistently P Q1 Q2 :
519
520
  IntoOr P Q1 Q2 
  IntoOr (bi_persistently P) (bi_persistently Q1) (bi_persistently Q2).
Robbert Krebbers's avatar
Robbert Krebbers committed
521
522
523
524
525
526
527
528
Proof. rewrite /IntoOr=>->. by rewrite persistently_or. Qed.

(* 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.
529
530
531
532
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) :
533
  FromExist P Φ  FromExist (bi_absorbingly P) (λ a, bi_absorbingly (Φ a))%I.
534
Proof. rewrite /FromExist=> <-. by rewrite absorbingly_exist. Qed.
535
536
537
Global Instance from_exist_plainly {A} P (Φ : A  PROP) :
  FromExist P Φ  FromExist (bi_plainly P) (λ a, bi_plainly (Φ a))%I.
Proof. rewrite /FromExist=> <-. by rewrite plainly_exist. Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
538
Global Instance from_exist_persistently {A} P (Φ : A  PROP) :
539
  FromExist P Φ  FromExist (bi_persistently P) (λ a, bi_persistently (Φ a))%I.
Robbert Krebbers's avatar
Robbert Krebbers committed
540
541
542
543
544
545
546
547
Proof. rewrite /FromExist=> <-. by rewrite persistently_exist. Qed.

(* 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.
548
549
550
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
551
552
553
554
555
556
557
558
559
560
Global Instance into_exist_and_pure P Q φ :
  IntoPureT P φ  IntoExist (P  Q) (λ _ : φ, Q).
Proof.
  intros (φ'&->&?). rewrite /IntoExist (into_pure P).
  apply pure_elim_l=> Hφ. by rewrite -(exist_intro Hφ).
Qed.
Global Instance into_exist_sep_pure P Q φ :
  TCOr (Affine P) (Absorbing Q)  IntoPureT P φ  IntoExist (P  Q) (λ _ : φ, Q).
Proof.
  intros ? (φ'&->&?). rewrite /IntoExist.
Robbert Krebbers's avatar
Robbert Krebbers committed
561
  eapply (pure_elim φ'); [by rewrite (into_pure P); apply sep_elim_l, _|]=>?.
Robbert Krebbers's avatar
Robbert Krebbers committed
562
563
  rewrite -exist_intro //. apply sep_elim_r, _.
Qed.
564
Global Instance into_exist_absorbingly {A} P (Φ : A  PROP) :
565
  IntoExist P Φ  IntoExist (bi_absorbingly P) (λ a, bi_absorbingly (Φ a))%I.
566
Proof. rewrite /IntoExist=> HP. by rewrite HP absorbingly_exist. Qed.
567
568
569
Global Instance into_exist_plainly {A} P (Φ : A  PROP) :
  IntoExist P Φ  IntoExist (bi_plainly P) (λ a, bi_plainly (Φ a))%I.
Proof. rewrite /IntoExist=> HP. by rewrite HP plainly_exist. Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
570
Global Instance into_exist_persistently {A} P (Φ : A  PROP) :
571
  IntoExist P Φ  IntoExist (bi_persistently P) (λ a, bi_persistently (Φ a))%I.
Robbert Krebbers's avatar
Robbert Krebbers committed
572
573
574
575
576
Proof. rewrite /IntoExist=> HP. by rewrite HP persistently_exist. Qed.

(* IntoForall *)
Global Instance into_forall_forall {A} (Φ : A  PROP) : IntoForall ( a, Φ a) Φ.
Proof. by rewrite /IntoForall. Qed.
577
578
579
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.
580
581
582
Global Instance into_forall_plainly {A} P (Φ : A  PROP) :
  IntoForall P Φ  IntoForall (bi_plainly P) (λ a, bi_plainly (Φ a))%I.
Proof. rewrite /IntoForall=> HP. by rewrite HP plainly_forall. Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
583
Global Instance into_forall_persistently {A} P (Φ : A  PROP) :
584
  IntoForall P Φ  IntoForall (bi_persistently P) (λ a, bi_persistently (Φ a))%I.
Robbert Krebbers's avatar
Robbert Krebbers committed
585
586
587
588
589
590
591
592
593
Proof. rewrite /IntoForall=> HP. by rewrite HP persistently_forall. Qed.

(* 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.
594
595
596
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
597
598
599
600
601
602
603
604
605
606
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 φ :
  TCOr (Affine P) (Absorbing Q)  IntoPureT P φ 
  FromForall (P - Q)%I (λ _ : φ, Q)%I.
Proof.
  intros [|] (φ'&->&?); rewrite /FromForall; apply wand_intro_r.
607
  - rewrite -(affine_affinely P) (into_pure P) -persistent_and_affinely_sep_r.
Robbert Krebbers's avatar
Robbert Krebbers committed
608
609
610
611
    apply pure_elim_r=>?. by rewrite forall_elim.
  - by rewrite (into_pure P) -pure_wand_forall wand_elim_l.
Qed.

612
613
614
615
616
Global Instance from_forall_affinely `{AffineBI PROP} {A} P (Φ : A  PROP) :
  FromForall P Φ  FromForall (bi_affinely P)%I (λ a, bi_affinely (Φ a))%I.
Proof.
  rewrite /FromForall=> <-. rewrite affine_affinely. by setoid_rewrite affinely_elim.
Qed.
617
618
619
Global Instance from_forall_plainly {A} P (Φ : A  PROP) :
  FromForall P Φ  FromForall (bi_plainly P)%I (λ a, bi_plainly (Φ a))%I.
Proof. rewrite /FromForall=> <-. by rewrite plainly_forall. Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
620
Global Instance from_forall_persistently {A} P (Φ : A  PROP) :
621
  FromForall P Φ  FromForall (bi_persistently P)%I (λ a, bi_persistently (Φ a))%I.
Robbert Krebbers's avatar
Robbert Krebbers committed
622
623
624
625
626
627
628
629
630
631
632
633
634
635
Proof. rewrite /FromForall=> <-. by rewrite persistently_forall. Qed.

(* ElimModal *)
Global Instance elim_modal_wand P P' Q Q' R :
  ElimModal P P' Q Q'  ElimModal P P' (R - Q) (R - Q').
Proof.
  rewrite /ElimModal=> H. apply wand_intro_r.
  by rewrite wand_curry -assoc (comm _ P') -wand_curry wand_elim_l.
Qed.
Global Instance forall_modal_wand {A} P P' (Φ Ψ : A  PROP) :
  ( x, ElimModal P P' (Φ x) (Ψ x))  ElimModal P P' ( x, Φ x) ( x, Ψ x).
Proof.
  rewrite /ElimModal=> H. apply forall_intro=> a. by rewrite (forall_elim a).
Qed.
636
Global Instance elim_modal_absorbingly P Q : Absorbing Q  ElimModal (bi_absorbingly P) P Q Q.
637
Proof.
638
  rewrite /ElimModal=> H. by rewrite absorbingly_sep_l wand_elim_r absorbing_absorbingly.
639
Qed.
640
641

(* Frame *)
642
Global Instance frame_here_absorbing p R : Absorbing R  Frame p R R True | 0.
643
Proof. intros. by rewrite /Frame affinely_persistently_if_elim sep_elim_l. Qed.
644
Global Instance frame_here p R : Frame p R R emp | 1.
645
646
647
648
649
650
651
652
653
654
Proof. intros. by rewrite /Frame affinely_persistently_if_elim sep_elim_l. Qed.
Global Instance frame_affinely_here_absorbing p R :
  Absorbing R  Frame p (bi_affinely R) R True | 0.
Proof.
  intros. by rewrite /Frame affinely_persistently_if_elim affinely_elim sep_elim_l.
Qed.
Global Instance frame_affinely_here p R : Frame p (bi_affinely R) R emp | 1.
Proof.
  intros. by rewrite /Frame affinely_persistently_if_elim affinely_elim sep_elim_l.
Qed.
655

656
Global Instance frame_here_pure p φ Q : FromPure Q φ  Frame p ⌜φ⌝ Q True.
Robbert Krebbers's avatar
Robbert Krebbers committed
657
Proof.
658
  rewrite /FromPure /Frame=> <-. by rewrite affinely_persistently_if_elim sep_elim_l.
Robbert Krebbers's avatar
Robbert Krebbers committed
659
Qed.
660

Robbert Krebbers's avatar
Robbert Krebbers committed
661
662
663
Class MakeSep (P Q PQ : PROP) := make_sep : P  Q  PQ.
Arguments MakeSep _%I _%I _%I.
Global Instance make_sep_emp_l P : MakeSep emp P P.
664
Proof. by rewrite /MakeSep left_id. Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
665
Global Instance make_sep_emp_r P : MakeSep P emp P.
666
Proof. by rewrite /MakeSep right_id. Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
667
668
Global Instance make_sep_true_l P : Absorbing P  MakeSep True P P.
Proof. intros. by rewrite /MakeSep True_sep. Qed.
669
Global Instance make_and_emp_l_absorbingly P : MakeSep True P (bi_absorbingly P) | 10.
670
Proof. intros. by rewrite /MakeSep. Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
671
672
Global Instance make_sep_true_r P : Absorbing P  MakeSep P True P.
Proof. intros. by rewrite /MakeSep sep_True. Qed.
673
Global Instance make_and_emp_r_absorbingly P : MakeSep P True (bi_absorbingly P) | 10.
674
Proof. intros. by rewrite /MakeSep comm. Qed.
675
Global Instance make_sep_default P Q : MakeSep P Q (P  Q) | 100.
Robbert Krebbers's avatar
Robbert Krebbers committed
676
Proof. by rewrite /MakeSep. Qed.
677
678
679
680
681
682

Global Instance frame_sep_persistent_l R P1 P2 Q1 Q2 Q' :
  Frame true R P1 Q1  MaybeFrame true R P2 Q2  MakeSep Q1 Q2 Q' 
  Frame true R (P1  P2) Q' | 9.
Proof.
  rewrite /Frame /MaybeFrame /MakeSep /= => <- <- <-.
683
  rewrite {1}(affinely_persistently_sep_dup R). solve_sep_entails.
684
Qed.
685
Global Instance frame_sep_l R P1 P2 Q Q' :
686
  Frame false R P1 Q  MakeSep Q P2 Q'  Frame false R (P1  P2) Q' | 9.
687
Proof. rewrite /Frame /MakeSep => <- <-. by rewrite assoc. Qed.
688
689
690
Global Instance frame_sep_r p R P1 P2 Q Q' :
  Frame p R P2 Q  MakeSep P1 Q Q'  Frame p R (P1  P2) Q' | 10.
Proof. rewrite /Frame /MakeSep => <- <-. by rewrite assoc -(comm _ P1) assoc. Qed.
691

Robbert Krebbers's avatar
Robbert Krebbers committed
692
Global Instance frame_big_sepL_cons {A} p (Φ : nat  A  PROP) R Q l x l' :
693
694
695
696
  IsCons l x l' 
  Frame p R (Φ 0 x  [ list] k  y  l', Φ (S k) y) Q 
  Frame p R ([ list] k  y  l, Φ k y) Q.
Proof. rewrite /IsCons=>->. by rewrite /Frame big_sepL_cons. Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
697
Global Instance frame_big_sepL_app {A} p (Φ : nat  A  PROP) R Q l l1 l2 :
698
  IsApp l l1 l2 
699
  Frame p R (([ list] k  y  l1, Φ k y) 
700
           [ list] k  y  l2, Φ (length l1 + k) y) Q 
701
  Frame p R ([ list] k  y  l, Φ k y) Q.
702
Proof. rewrite /IsApp=>->. by rewrite /Frame big_opL_app. Qed.
703

Robbert Krebbers's avatar
Robbert Krebbers committed
704
705
Class MakeAnd (P Q PQ : PROP) := make_and : P  Q  PQ.
Arguments MakeAnd _%I _%I _%I.
706
707
708
709
Global Instance make_and_true_l P : MakeAnd True P P.
Proof. by rewrite /MakeAnd left_id. Qed.
Global Instance make_and_true_r P : MakeAnd P True P.
Proof. by rewrite /MakeAnd right_id. Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
710
711
Global Instance make_and_emp_l P : Affine P  MakeAnd emp P P.
Proof. intros. by rewrite /MakeAnd emp_and. Qed.