class_instances.v 48.9 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
10
11
12
13
14
15
16
Import bi.

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

(* 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.
Global Instance into_internal_eq_bare {A : ofeT} (x y : A) P :
  IntoInternalEq P x y  IntoInternalEq ( P) x y.
Proof. rewrite /IntoInternalEq=> ->. by rewrite bare_elim. Qed.
17
18
19
20
21
22
Global Instance into_internal_eq_sink {A : ofeT} (x y : A) P :
  IntoInternalEq P x y  IntoInternalEq ( P) x y.
Proof. rewrite /IntoInternalEq=> ->. by rewrite sink_internal_eq. Qed.
Global Instance into_internal_eq_persistently {A : ofeT} (x y : A) P :
  IntoInternalEq P x y  IntoInternalEq ( P) x y.
Proof. rewrite /IntoInternalEq=> ->. by rewrite persistently_elim. Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
23
24
25
26
27
28

(* FromBare *)
Global Instance from_bare_affine P : Affine P  FromBare P P.
Proof. intros. by rewrite /FromBare bare_elim. Qed.
Global Instance from_bare_default P : FromBare ( P) P | 100.
Proof. by rewrite /FromBare. Qed.
29

30
31
32
33
34
35
36
37
(* IntoSink *)
Global Instance into_sink_True : @IntoSink PROP True emp | 0.
Proof. by rewrite /IntoSink -sink_True_emp sink_pure. Qed.
Global Instance into_sink_absorbing P : Absorbing P  IntoSink P P | 1.
Proof. intros. by rewrite /IntoSink absorbing_sink. Qed.
Global Instance into_sink_default P : IntoSink ( P) P | 100.
Proof. by rewrite /IntoSink. Qed.

38
(* FromAssumption *)
39
Global Instance from_assumption_exact p P : FromAssumption p P P | 0.
Robbert Krebbers's avatar
Robbert Krebbers committed
40
Proof. by rewrite /FromAssumption /= bare_persistently_if_elim. Qed.
41

42
Global Instance from_assumption_persistently_r P Q :
43
  FromAssumption true P Q  FromAssumption true P ( Q).
Robbert Krebbers's avatar
Robbert Krebbers committed
44
45
46
47
48
49
50
Proof.
  rewrite /FromAssumption /= =><-.
  by rewrite -{1}bare_persistently_idemp bare_elim.
Qed.
Global Instance from_assumption_bare_r P Q :
  FromAssumption true P Q  FromAssumption true P ( Q).
Proof. rewrite /FromAssumption /= =><-. by rewrite bare_idemp. Qed.
51
52
53
Global Instance from_assumption_sink_r p P Q :
  FromAssumption p P Q  FromAssumption p P ( Q).
Proof. rewrite /FromAssumption /= =><-. apply sink_intro. Qed.
54

Robbert Krebbers's avatar
Robbert Krebbers committed
55
56
57
58
59
60
61
62
63
Global Instance from_assumption_bare_persistently_l p P Q :
  FromAssumption true P Q  FromAssumption p ( P) Q.
Proof. rewrite /FromAssumption /= =><-. by rewrite bare_persistently_if_elim. Qed.
Global Instance from_assumption_persistently_l_true P Q :
  FromAssumption true P Q  FromAssumption true ( P) Q.
Proof. rewrite /FromAssumption /= =><-. by rewrite persistently_idemp. Qed.
Global Instance from_assumption_persistently_l_false `{AffineBI PROP} P Q :
  FromAssumption true P Q  FromAssumption false ( P) Q.
Proof. rewrite /FromAssumption /= =><-. by rewrite affine_bare. Qed.
64
65
66
Global Instance from_assumption_bare_l_true p P Q :
  FromAssumption p P Q  FromAssumption p ( P) Q.
Proof. rewrite /FromAssumption /= =><-. by rewrite bare_elim. Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
67
68

Global Instance from_assumption_forall {A} p (Φ : A  PROP) Q x :
69
70
  FromAssumption p (Φ x) Q  FromAssumption p ( x, Φ x) Q.
Proof. rewrite /FromAssumption=> <-. by rewrite forall_elim. Qed.
71
72

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

76
Global Instance into_pure_eq {A : ofeT} (a b : A) :
77
78
  Discrete a  @IntoPure M (a  b) (a  b).
Proof. intros. by rewrite /IntoPure discrete_eq. Qed.
79

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

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

Robbert Krebbers's avatar
Robbert Krebbers committed
104
105
Global Instance into_pure_bare P φ : IntoPure P φ  IntoPure ( P) φ.
Proof. rewrite /IntoPure=> ->. apply bare_elim. Qed.
106
107
Global Instance into_pure_sink P φ : IntoPure P φ  IntoPure ( P) φ.
Proof. rewrite /IntoPure=> ->. by rewrite sink_pure. Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
108
Global Instance into_pure_persistently P φ : IntoPure P φ  IntoPure ( P) φ.
109
Proof. rewrite /IntoPure=> ->. apply: persistently_elim. Qed.
110

111
(* FromPure *)
Robbert Krebbers's avatar
Robbert Krebbers committed
112
113
Global Instance from_pure_pure φ : @FromPure PROP ⌜φ⌝ φ.
Proof. by rewrite /FromPure. Qed.
114
Global Instance from_pure_internal_eq {A : ofeT} (a b : A) :
Robbert Krebbers's avatar
Robbert Krebbers committed
115
116
  @FromPure PROP (a  b) (a  b).
Proof. by rewrite /FromPure pure_internal_eq. Qed.
117

Ralf Jung's avatar
Ralf Jung committed
118
Global Instance from_pure_pure_and (φ1 φ2 : Prop) P1 P2 :
119
  FromPure P1 φ1  FromPure P2 φ2  FromPure (P1  P2) (φ1  φ2).
120
Proof. rewrite /FromPure pure_and. by intros -> ->. Qed.
Ralf Jung's avatar
Ralf Jung committed
121
Global Instance from_pure_pure_or (φ1 φ2 : Prop) P1 P2 :
122
  FromPure P1 φ1  FromPure P2 φ2  FromPure (P1  P2) (φ1  φ2).
123
Proof. rewrite /FromPure pure_or. by intros -> ->. Qed.
Ralf Jung's avatar
Ralf Jung committed
124
Global Instance from_pure_pure_impl (φ1 φ2 : Prop) P1 P2 :
125
  IntoPure P1 φ1  FromPure P2 φ2  FromPure (P1  P2) (φ1  φ2).
126
Proof. rewrite /FromPure /IntoPure pure_impl. by intros -> ->. Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
127
128
129
130
131
132
133
134
135
136

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).
137
Proof. rewrite /FromPure=> <- <-. by rewrite pure_and persistent_and_sep_1. Qed.
Ralf Jung's avatar
Ralf Jung committed
138
Global Instance from_pure_pure_wand (φ1 φ2 : Prop) P1 P2 :
139
  IntoPure P1 φ1  FromPure P2 φ2  FromPure (P1 - P2) (φ1  φ2).
140
Proof.
Robbert Krebbers's avatar
Robbert Krebbers committed
141
142
  rewrite /FromPure /IntoPure=> -> <-.
  by rewrite pure_wand_forall pure_impl pure_impl_forall.
143
144
Qed.

Robbert Krebbers's avatar
Robbert Krebbers committed
145
146
Global Instance from_pure_persistently P φ : FromPure P φ  FromPure ( P) φ.
Proof. rewrite /FromPure=> <-. by rewrite persistently_pure. Qed.
147
148
Global Instance from_pure_sink P φ : FromPure P φ  FromPure ( P) φ.
Proof. rewrite /FromPure=> <-. by rewrite sink_pure. Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
149

150
(* IntoPersistent *)
151
Global Instance into_persistent_persistently p P Q :
152
  IntoPersistent true P Q  IntoPersistent p ( P) Q | 0.
Robbert Krebbers's avatar
Robbert Krebbers committed
153
154
155
156
Proof.
  rewrite /IntoPersistent /= => ->.
  destruct p; simpl; auto using persistently_idemp_1.
Qed.
157
Global Instance into_persistent_bare p P Q :
Robbert Krebbers's avatar
Robbert Krebbers committed
158
159
  IntoPersistent p P Q  IntoPersistent p ( P) Q | 0.
Proof. rewrite /IntoPersistent /= => <-. by rewrite bare_elim. Qed.
160
Global Instance into_persistent_here P : IntoPersistent true P P | 1.
Robbert Krebbers's avatar
Robbert Krebbers committed
161
Proof. by rewrite /IntoPersistent. Qed.
162
163
Global Instance into_persistent_persistent P :
  Persistent P  IntoPersistent false P P | 100.
164
Proof. intros. by rewrite /IntoPersistent. Qed.
165

Robbert Krebbers's avatar
Robbert Krebbers committed
166
(* FromPersistent *)
167
Global Instance from_persistent_here P : FromPersistent false false P P | 1.
Robbert Krebbers's avatar
Robbert Krebbers committed
168
Proof. by rewrite /FromPersistent. Qed.
169
170
171
172
173
174
175
176
Global Instance from_persistent_persistently a P Q :
  FromPersistent a false P Q  FromPersistent false true ( P) Q | 0.
Proof.
  rewrite /FromPersistent /= => <-. by destruct a; rewrite /= ?persistently_bare.
Qed.
Global Instance from_persistent_bare a p P Q :
  FromPersistent a p P Q  FromPersistent true p ( P) Q | 0.
Proof. rewrite /FromPersistent /= => <-. destruct a; by rewrite /= ?bare_idemp. Qed.
177

Robbert Krebbers's avatar
Robbert Krebbers committed
178
179
180
(* IntoWand *)
Global Instance into_wand_wand p q P Q P' :
  FromAssumption q P P'  IntoWand p q (P' - Q) P Q.
181
Proof.
Robbert Krebbers's avatar
Robbert Krebbers committed
182
  rewrite /FromAssumption /IntoWand=> HP. by rewrite HP bare_persistently_if_elim.
Robbert Krebbers's avatar
Robbert Krebbers committed
183
Qed.
184

Robbert Krebbers's avatar
Robbert Krebbers committed
185
186
187
188
189
190
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
191

Robbert Krebbers's avatar
Robbert Krebbers committed
192
Global Instance into_wand_impl_false_true P Q P' :
193
  Absorbing P'  FromAssumption true P P' 
Robbert Krebbers's avatar
Robbert Krebbers committed
194
  IntoWand false true (P'  Q) P Q.
195
Proof.
196
  rewrite /IntoWand /FromAssumption /= => ? HP. apply wand_intro_l.
Robbert Krebbers's avatar
Robbert Krebbers committed
197
  rewrite -(bare_persistently_idemp P) HP.
198
  by rewrite -persistently_and_bare_sep_l persistently_elim impl_elim_r.
199
200
Qed.

Robbert Krebbers's avatar
Robbert Krebbers committed
201
Global Instance into_wand_impl_true_false P Q P' :
202
  Affine P'  FromAssumption false P P' 
Robbert Krebbers's avatar
Robbert Krebbers committed
203
  IntoWand true false (P'  Q) P Q.
204
Proof.
205
  rewrite /FromAssumption /IntoWand /= => ? HP. apply wand_intro_r.
206
  rewrite -persistently_and_bare_sep_l HP -{2}(affine_bare P') -bare_and_lr.
Robbert Krebbers's avatar
Robbert Krebbers committed
207
  by rewrite bare_persistently_elim impl_elim_l.
208
Qed.
209

Robbert Krebbers's avatar
Robbert Krebbers committed
210
211
Global Instance into_wand_impl_true_true P Q P' :
  FromAssumption true P P'  IntoWand true true (P'  Q) P Q.
212
Proof.
Robbert Krebbers's avatar
Robbert Krebbers committed
213
  rewrite /FromAssumption /IntoWand /= => <-. apply wand_intro_l.
214
215
  rewrite -{1}(bare_persistently_idemp P) -and_sep_bare_persistently.
  by rewrite -bare_persistently_and impl_elim_r bare_persistently_elim.
216
Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
217
218
219
220
221
222
223
224
225
226
227
228
229
230
231
232
233

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.

Global Instance into_wand_persistently_true q R P Q :
  IntoWand true q R P Q  IntoWand true q ( R) P Q.
Proof. by rewrite /IntoWand /= persistently_idemp. Qed.
Global Instance into_wand_persistently_false `{!AffineBI PROP} q R P Q :
  IntoWand false q R P Q  IntoWand false q ( R) P Q.
234
Proof. by rewrite /IntoWand persistently_elim. Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
235
236
237
238
239
240
241
242
243
244

Global Instance into_wand_bare_persistently p q R P Q :
  IntoWand p q R P Q  IntoWand p q ( R) P Q.
Proof. by rewrite /IntoWand bare_persistently_elim. Qed.

(* 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 :
  FromBare P1 P1'  Persistent P1'  FromAnd (P1  P2) P1' P2 | 9.
245
Proof.
246
  rewrite /FromBare /FromAnd=> <- ?. by rewrite persistent_and_bare_sep_l_1.
247
Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
248
249
Global Instance from_and_sep_persistent_r P1 P2 P2' :
  FromBare P2 P2'  Persistent P2'  FromAnd (P1  P2) P1 P2' | 10.
250
Proof.
251
  rewrite /FromBare /FromAnd=> <- ?. by rewrite persistent_and_bare_sep_r_1.
252
Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
253
254
Global Instance from_and_sep_persistent P1 P2 :
  Persistent P1  Persistent P2  FromAnd (P1  P2) P1 P2 | 11.
255
Proof.
256
  rewrite /FromBare /FromAnd. intros ??. by rewrite -persistent_and_sep_1.
257
258
Qed.

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

Robbert Krebbers's avatar
Robbert Krebbers committed
262
263
264
265
266
267
Global Instance from_and_persistently P Q1 Q2 :
  FromAnd P Q1 Q2  FromAnd ( P) ( Q1) ( Q2).
Proof. rewrite /FromAnd=> <-. by rewrite persistently_and. Qed.
Global Instance from_and_persistently_sep P Q1 Q2 :
  FromSep P Q1 Q2  FromAnd ( P) ( Q1) ( Q2) | 11.
Proof. rewrite /FromAnd=> <-. by rewrite -persistently_and persistently_and_sep. Qed.
268

Robbert Krebbers's avatar
Robbert Krebbers committed
269
270
271
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).
272
Proof. intros. by rewrite /FromAnd big_opL_cons persistent_and_sep_1. Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
273
274
275
276
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).
277
Proof. intros. by rewrite /FromAnd big_opL_app persistent_and_sep_1. Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
278
279
280
281
282

(* 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 :
283
  TCOr (TCAnd (Affine P1) (Affine P2)) (TCAnd (Absorbing P1) (Absorbing P2)) 
Robbert Krebbers's avatar
Robbert Krebbers committed
284
285
286
287
288
289
290
291
  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.

Global Instance from_sep_bare P Q1 Q2 :
  FromSep P Q1 Q2  FromSep ( P) ( Q1) ( Q2).
292
Proof. rewrite /FromSep=> <-. by rewrite bare_sep_2. Qed.
293
294
295
Global Instance from_sep_sink P Q1 Q2 :
  FromSep P Q1 Q2  FromSep ( P) ( Q1) ( Q2).
Proof. rewrite /FromSep=> <-. by rewrite sink_sep. Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
296
297
Global Instance from_sep_persistently P Q1 Q2 :
  FromSep P Q1 Q2  FromSep ( P) ( Q1) ( Q2).
298
Proof. rewrite /FromSep=> <-. by rewrite persistently_sep_2. Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
299
300
301
302
303
304
305
306

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

Robbert Krebbers's avatar
Robbert Krebbers committed
308
(* IntoAnd *)
309
Global Instance into_and_and p P Q : IntoAnd p (P  Q) P Q | 10.
Robbert Krebbers's avatar
Robbert Krebbers committed
310
Proof. by rewrite /IntoAnd bare_persistently_if_and. Qed.
311
312
313
314
Global Instance into_and_and_affine_l P Q Q' :
  Affine P  FromBare Q' Q  IntoAnd false (P  Q) P Q'.
Proof.
  intros. rewrite /IntoAnd /=.
315
  by rewrite -(affine_bare P) bare_and_l bare_and (from_bare Q').
316
317
318
319
320
Qed.
Global Instance into_and_and_affine_r P P' Q :
  Affine Q  FromBare P' P  IntoAnd false (P  Q) P' Q.
Proof.
  intros. rewrite /IntoAnd /=.
321
  by rewrite -(affine_bare Q) bare_and_r bare_and (from_bare P').
322
323
Qed.

324
325
Global Instance into_and_sep `{PositiveBI PROP} P Q : IntoAnd true (P  Q) P Q.
Proof. by rewrite /IntoAnd /= persistently_sep -and_sep_persistently persistently_and. Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
326
327
328
329
330
331

Global Instance into_and_pure p φ ψ : @IntoAnd PROP p ⌜φ  ψ⌝ ⌜φ⌝ ⌜ψ⌝.
Proof. by rewrite /IntoAnd pure_and bare_persistently_if_and. Qed.

Global Instance into_and_bare p P Q1 Q2 :
  IntoAnd p P Q1 Q2  IntoAnd p ( P) ( Q1) ( Q2).
Robbert Krebbers's avatar
Robbert Krebbers committed
332
Proof.
Robbert Krebbers's avatar
Robbert Krebbers committed
333
334
335
  rewrite /IntoAnd. destruct p; simpl.
  - by rewrite -bare_and !persistently_bare.
  - intros ->. by rewrite bare_and.
Robbert Krebbers's avatar
Robbert Krebbers committed
336
Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
337
338
Global Instance into_and_persistently p P Q1 Q2 :
  IntoAnd p P Q1 Q2  IntoAnd p ( P) ( Q1) ( Q2).
Robbert Krebbers's avatar
Robbert Krebbers committed
339
Proof.
Robbert Krebbers's avatar
Robbert Krebbers committed
340
341
342
  rewrite /IntoAnd /=. destruct p; simpl.
  - by rewrite -persistently_and !persistently_idemp.
  - intros ->. by rewrite persistently_and.
Robbert Krebbers's avatar
Robbert Krebbers committed
343
344
Qed.

Robbert Krebbers's avatar
Robbert Krebbers committed
345
(* IntoSep *)
346
347
Global Instance into_sep_sep P Q : IntoSep (P  Q) P Q.
Proof. by rewrite /IntoSep. Qed.
348

349
350
351
352
353
354
355
356
357
Inductive AndIntoSep : PROP  PROP  PROP  PROP  Prop :=
  | and_into_sep_affine P Q Q' : Affine P  FromBare Q' Q  AndIntoSep P P Q Q'
  | and_into_sep P Q : AndIntoSep P ( P)%I Q Q.
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'.
358
Proof.
359
  destruct 2 as [P Q Q'|P Q]; rewrite /IntoSep.
360
  - rewrite -(from_bare Q') -(affine_bare P) bare_and_lr.
361
362
    by rewrite persistent_and_bare_sep_l_1.
  - by rewrite persistent_and_bare_sep_l_1.
363
Qed.
364
365
Global Instance into_sep_and_persistent_r P P' Q Q' :
  Persistent Q  AndIntoSep Q Q' P P'  IntoSep (P  Q) P' Q'.
366
Proof.
367
  destruct 2 as [Q P P'|Q P]; rewrite /IntoSep.
368
  - rewrite -(from_bare P') -(affine_bare Q) -bare_and_lr.
369
370
    by rewrite persistent_and_bare_sep_r_1.
  - by rewrite persistent_and_bare_sep_r_1.
371
Qed.
372
373


374
375
376
Global Instance into_sep_pure φ ψ : @IntoSep PROP ⌜φ  ψ⌝ ⌜φ⌝ ⌜ψ⌝.
Proof. by rewrite /IntoSep pure_and persistent_and_sep_1. Qed.

377
378
379
380
381
382
(* FIXME: This instance is kind of strange, it just gets rid of the ■. Also, it
overlaps with `into_sep_bare_later`, and hence has lower precedence. *)
Global Instance into_sep_bare P Q1 Q2 :
  IntoSep P Q1 Q2  IntoSep ( P) Q1 Q2 | 20.
Proof. rewrite /IntoSep /= => ->. by rewrite bare_elim. Qed.

383
384
385
Global Instance into_sep_persistently `{PositiveBI PROP} P Q1 Q2 :
  IntoSep P Q1 Q2  IntoSep ( P) ( Q1) ( Q2).
Proof. rewrite /IntoSep /= => ->. by rewrite persistently_sep. Qed.
386

387
388
389
(* 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. *)
390
Global Instance into_sep_big_sepL_cons {A} (Φ : nat  A  PROP) l x l' :
391
  IsCons l x l' 
392
  IntoSep ([ list] k  y  l, Φ k y)
393
    (Φ 0 x) ([ list] k  y  l', Φ (S k) y).
Robbert Krebbers's avatar
Robbert Krebbers committed
394
Proof. rewrite /IsCons=>->. by rewrite /IntoSep big_sepL_cons. Qed.
395
Global Instance into_sep_big_sepL_app {A} (Φ : nat  A  PROP) l l1 l2 :
396
  IsApp l l1 l2 
397
  IntoSep ([ list] k  y  l, Φ k y)
398
    ([ list] k  y  l1, Φ k y) ([ list] k  y  l2, Φ (length l1 + k) y).
Robbert Krebbers's avatar
Robbert Krebbers committed
399
400
401
402
403
404
405
406
407
408
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.
Global Instance from_or_bare P Q1 Q2 :
  FromOr P Q1 Q2  FromOr ( P) ( Q1) ( Q2).
Proof. rewrite /FromOr=> <-. by rewrite bare_or. Qed.
409
410
411
Global Instance from_or_sink P Q1 Q2 :
  FromOr P Q1 Q2  FromOr ( P) ( Q1) ( Q2).
Proof. rewrite /FromOr=> <-. by rewrite sink_or. Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
412
413
414
415
416
417
418
419
420
421
422
423
Global Instance from_or_persistently P Q1 Q2 :
  FromOr P Q1 Q2  FromOr ( P) ( Q1) ( Q2).
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.
Global Instance into_or_bare P Q1 Q2 :
  IntoOr P Q1 Q2  IntoOr ( P) ( Q1) ( Q2).
Proof. rewrite /IntoOr=>->. by rewrite bare_or. Qed.
424
425
426
Global Instance into_or_sink P Q1 Q2 :
  IntoOr P Q1 Q2  IntoOr ( P) ( Q1) ( Q2).
Proof. rewrite /IntoOr=>->. by rewrite sink_or. Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
427
428
429
430
431
432
433
434
435
436
437
438
439
Global Instance into_or_persistently P Q1 Q2 :
  IntoOr P Q1 Q2  IntoOr ( P) ( Q1) ( Q2).
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.
Global Instance from_exist_bare {A} P (Φ : A  PROP) :
  FromExist P Φ  FromExist ( P) (λ a,  (Φ a))%I.
Proof. rewrite /FromExist=> <-. by rewrite bare_exist. Qed.
440
441
442
Global Instance from_exist_sink {A} P (Φ : A  PROP) :
  FromExist P Φ  FromExist ( P) (λ a,  (Φ a))%I.
Proof. rewrite /FromExist=> <-. by rewrite sink_exist. Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
443
444
445
446
447
448
449
450
451
452
453
454
455
456
457
458
459
460
461
462
463
464
465
Global Instance from_exist_persistently {A} P (Φ : A  PROP) :
  FromExist P Φ  FromExist ( P) (λ a,  (Φ a))%I.
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.
Global Instance into_exist_bare {A} P (Φ : A  PROP) :
  IntoExist P Φ  IntoExist ( P) (λ a,  (Φ a))%I.
Proof. rewrite /IntoExist=> HP. by rewrite HP bare_exist. Qed.
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
466
  eapply (pure_elim φ'); [by rewrite (into_pure P); apply sep_elim_l, _|]=>?.
Robbert Krebbers's avatar
Robbert Krebbers committed
467
468
  rewrite -exist_intro //. apply sep_elim_r, _.
Qed.
469
470
471
Global Instance into_exist_sink {A} P (Φ : A  PROP) :
  IntoExist P Φ  IntoExist ( P) (λ a,  (Φ a))%I.
Proof. rewrite /IntoExist=> HP. by rewrite HP sink_exist. Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
472
473
474
475
476
477
478
479
480
481
482
483
484
485
486
487
488
489
490
491
492
493
494
495
496
497
498
499
500
501
502
503
504
505
506
507
508
509
510
511
512
513
514
515
516
517
518
519
520
521
522
523
Global Instance into_exist_persistently {A} P (Φ : A  PROP) :
  IntoExist P Φ  IntoExist ( P) (λ a,  (Φ a))%I.
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.
Global Instance into_forall_bare {A} P (Φ : A  PROP) :
  IntoForall P Φ  IntoForall ( P) (λ a,  (Φ a))%I.
Proof. rewrite /IntoForall=> HP. by rewrite HP bare_forall. Qed.
Global Instance into_forall_persistently {A} P (Φ : A  PROP) :
  IntoForall P Φ  IntoForall ( P) (λ a,  (Φ a))%I.
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.
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.
  - rewrite -(affine_bare P) (into_pure P) -persistent_and_bare_sep_r.
    apply pure_elim_r=>?. by rewrite forall_elim.
  - by rewrite (into_pure P) -pure_wand_forall wand_elim_l.
Qed.

Global Instance from_forall_persistently {A} P (Φ : A  PROP) :
  FromForall P Φ  FromForall ( P)%I (λ a,  (Φ a))%I.
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.
524
525
526
527
Global Instance elim_modal_sink P Q : Absorbing Q  ElimModal ( P) P Q Q.
Proof.
  rewrite /ElimModal=> H. by rewrite sink_sep_l wand_elim_r absorbing_sink.
Qed.
528
529

(* Frame *)
530
Global Instance frame_here_absorbing p R : Absorbing R  Frame p R R True | 0.
Robbert Krebbers's avatar
Robbert Krebbers committed
531
Proof. intros. by rewrite /Frame bare_persistently_if_elim sep_elim_l. Qed.
532
Global Instance frame_here p R : Frame p R R emp | 1.
Robbert Krebbers's avatar
Robbert Krebbers committed
533
Proof. intros. by rewrite /Frame bare_persistently_if_elim sep_elim_l. Qed.
534
535
536
537
538
Global Instance frame_bare_here_absorbing p R : Absorbing R  Frame p ( R) R True | 0.
Proof. intros. by rewrite /Frame bare_persistently_if_elim bare_elim sep_elim_l. Qed.
Global Instance frame_bare_here p R : Frame p ( R) R emp | 1.
Proof. intros. by rewrite /Frame bare_persistently_if_elim bare_elim sep_elim_l. Qed.

539
Global Instance frame_here_pure p φ Q : FromPure Q φ  Frame p ⌜φ⌝ Q True.
Robbert Krebbers's avatar
Robbert Krebbers committed
540
541
542
Proof.
  rewrite /FromPure /Frame=> <-. by rewrite bare_persistently_if_elim sep_elim_l.
Qed.
543

Robbert Krebbers's avatar
Robbert Krebbers committed
544
545
546
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.
547
Proof. by rewrite /MakeSep left_id. Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
548
Global Instance make_sep_emp_r P : MakeSep P emp P.
549
Proof. by rewrite /MakeSep right_id. Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
550
551
Global Instance make_sep_true_l P : Absorbing P  MakeSep True P P.
Proof. intros. by rewrite /MakeSep True_sep. Qed.
552
553
Global Instance make_and_emp_l_sink P : MakeSep True P ( P) | 10.
Proof. intros. by rewrite /MakeSep. Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
554
555
Global Instance make_sep_true_r P : Absorbing P  MakeSep P True P.
Proof. intros. by rewrite /MakeSep sep_True. Qed.
556
557
Global Instance make_and_emp_r_sink P : MakeSep P True ( P) | 10.
Proof. intros. by rewrite /MakeSep comm. Qed.
558
Global Instance make_sep_default P Q : MakeSep P Q (P  Q) | 100.
Robbert Krebbers's avatar
Robbert Krebbers committed
559
Proof. by rewrite /MakeSep. Qed.
560
561
562
563
564
565

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 /= => <- <- <-.
566
  rewrite {1}(bare_persistently_sep_dup R). solve_sep_entails.
567
Qed.
568
Global Instance frame_sep_l R P1 P2 Q Q' :
569
  Frame false R P1 Q  MakeSep Q P2 Q'  Frame false R (P1  P2) Q' | 9.
570
Proof. rewrite /Frame /MakeSep => <- <-. by rewrite assoc. Qed.
571
572
573
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.
574

Robbert Krebbers's avatar
Robbert Krebbers committed
575
Global Instance frame_big_sepL_cons {A} p (Φ : nat  A  PROP) R Q l x l' :
576
577
578
579
  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
580
Global Instance frame_big_sepL_app {A} p (Φ : nat  A  PROP) R Q l l1 l2 :
581
  IsApp l l1 l2 
582
  Frame p R (([ list] k  y  l1, Φ k y) 
583
           [ list] k  y  l2, Φ (length l1 + k) y) Q 
584
  Frame p R ([ list] k  y  l, Φ k y) Q.
585
Proof. rewrite /IsApp=>->. by rewrite /Frame big_opL_app. Qed.
586

Robbert Krebbers's avatar
Robbert Krebbers committed
587
588
Class MakeAnd (P Q PQ : PROP) := make_and : P  Q  PQ.
Arguments MakeAnd _%I _%I _%I.
589
590
591
592
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
593
594
Global Instance make_and_emp_l P : Affine P  MakeAnd emp P P.
Proof. intros. by rewrite /MakeAnd emp_and. Qed.
595
596
Global Instance make_and_emp_l_bare P : MakeAnd emp P ( P) | 10.
Proof. intros. by rewrite /MakeAnd. Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
597
598
Global Instance make_and_emp_r P : Affine P  MakeAnd P emp P.
Proof. intros. by rewrite /MakeAnd and_emp. Qed.
599
600
Global Instance make_and_emp_r_bare P : MakeAnd P emp ( P) | 10.
Proof. intros. by rewrite /MakeAnd comm. Qed.
601
Global Instance make_and_default P Q : MakeAnd P Q (P  Q) | 100.
Robbert Krebbers's avatar
Robbert Krebbers committed
602
603
604
605
606
607
608
609
610
611
612
613
614
615
616
617
618
619
620
621
622
623
624
625
626
627
628
629
Proof. by rewrite /MakeAnd. Qed.

Global Instance frame_and_l p R P1 P2 Q1 Q2 Q :
  Frame p R P1 Q1  MaybeFrame p R P2 Q2 
  MakeAnd Q1 Q2 Q  Frame p R (P1  P2) Q | 9.
Proof.
  rewrite /Frame /MakeAnd => <- <- <- /=.
  auto using and_intro, and_elim_l, and_elim_r, sep_mono.
Qed.
Global Instance frame_and_persistent_r R P1 P2 Q2 Q :
  Frame true R P2 Q2 
  MakeAnd P1 Q2 Q  Frame true R (P1  P2) Q | 10.
Proof.
  rewrite /Frame /MakeAnd => <- <- /=. rewrite -!persistently_and_bare_sep_l.
  auto using and_intro, and_elim_l', and_elim_r'.
Qed.
Global Instance frame_and_r R P1 P2 Q2 Q :
  TCOr (Affine R) (Absorbing P1) 
  Frame false R P2 Q2 
  MakeAnd P1 Q2 Q  Frame false R (P1  P2) Q | 10.
Proof.
  rewrite /Frame /MakeAnd=> ? <- <- /=. apply and_intro.
  - by rewrite and_elim_l sep_elim_r.
  - by rewrite and_elim_r.
Qed.

Class MakeOr (P Q PQ : PROP) := make_or : P  Q  PQ.
Arguments MakeOr _%I _%I _%I.
630
631
632
633
Global Instance make_or_true_l P : MakeOr True P True.
Proof. by rewrite /MakeOr left_absorb. Qed.
Global Instance make_or_true_r P : MakeOr P True True.
Proof. by rewrite /MakeOr right_absorb. Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
634
635
636
637
Global Instance make_or_emp_l P : Affine P  MakeOr emp P emp.
Proof. intros. by rewrite /MakeOr emp_or. Qed.
Global Instance make_or_emp_r P : Affine P  MakeOr P emp emp.
Proof. intros. by rewrite /MakeOr or_emp. Qed.
638
Global Instance make_or_default P Q : MakeOr P Q (P  Q) | 100.
Robbert Krebbers's avatar
Robbert Krebbers committed
639
Proof. by rewrite /MakeOr. Qed.
640
641
642
643
644
645
646
647
648

Global Instance frame_or_persistent_l R P1 P2 Q1 Q2 Q :
  Frame true R P1 Q1  MaybeFrame true R P2 Q2  MakeOr Q1 Q2 Q 
  Frame true R (P1  P2) Q | 9.
Proof. rewrite /Frame /MakeOr => <- <- <-. by rewrite -sep_or_l. Qed.
Global Instance frame_or_persistent_r R P1 P2 Q1 Q2 Q :
  MaybeFrame true R P2 Q2  MakeOr P1 Q2 Q 
  Frame true R (P1  P2) Q | 10.
Proof.
Robbert Krebbers's avatar
Robbert Krebbers committed
649
650
  rewrite /Frame /MaybeFrame /MakeOr => <- <- /=.
  by rewrite sep_or_l sep_elim_r.
651
Qed.
652
Global Instance frame_or R P1 P2 Q1 Q2 Q :
653
654
  Frame false R P1 Q1  Frame false R P2 Q2  MakeOr Q1 Q2 Q 
  Frame false R (P1  P2) Q.
655
656
Proof. rewrite /Frame /MakeOr => <- <- <-. by rewrite -sep_or_l. Qed.

657
658
Global Instance frame_wand p R P1 P2 Q2 :
  Frame p R P2 Q2  Frame p R (P1 - P2) (P1 - Q2).
659
660
661
662
663
Proof.
  rewrite /Frame=> ?. apply wand_intro_l.
  by rewrite assoc (comm _ P1) -assoc wand_elim_r.
Qed.

Robbert Krebbers's avatar
Robbert Krebbers committed
664
665
Class MakeBare (P Q : PROP) := make_bare :  P  Q.
Arguments MakeBare _%I _%I.
666
667
668
Global Instance make_bare_True : MakeBare True emp | 0.
Proof. by rewrite /MakeBare bare_True_emp bare_emp. Qed.
Global Instance make_bare_affine P : Affine P  MakeBare P P | 1.
Robbert Krebbers's avatar
Robbert Krebbers committed
669
670
671
Proof. intros. by rewrite /MakeBare affine_bare. Qed.
Global Instance make_bare_default P : MakeBare P ( P) | 100.
Proof. by rewrite /MakeBare. Qed.
672

Robbert Krebbers's avatar
Robbert Krebbers committed
673
674
Global Instance frame_bare R P Q Q' :
  Frame true R P Q  MakeBare Q Q'  Frame true R ( P) Q'.
675
676
677
678
Proof.
  rewrite /Frame /MakeBare=> <- <- /=.
  by rewrite -{1}bare_idemp bare_sep_2.
Qed.
679

680
681
682
683
684
685
686
687
688
689
690
691
692
693
Class MakeSink (P Q : PROP) := make_sink :  P  Q.
Arguments MakeSink _%I _%I.
Global Instance make_sink_emp : MakeSink emp True | 0.
Proof. by rewrite /MakeSink -sink_True_emp sink_pure. Qed.
(* Note: there is no point in having an instance `Absorbing P → MakeSink P P`
because framing will never turn a proposition that is not absorbing into
something that is absorbing. *)
Global Instance make_sink_default P : MakeSink P ( P) | 100.
Proof. by rewrite /MakeSink. Qed.

Global Instance frame_sink p R P Q Q' :
  Frame p R P Q  MakeSink Q Q'  Frame p R ( P) Q'.
Proof. rewrite /Frame /MakeSink=> <- <- /=. by rewrite sink_sep_r. Qed.

Robbert Krebbers's avatar
Robbert Krebbers committed
694
695
Class MakePersistently (P Q : PROP) := make_persistently :  P  Q.
Arguments MakePersistently _%I _%I.
696
697
Global Instance make_persistently_true : MakePersistently True True.
Proof. by rewrite /MakePersistently persistently_pure. Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
698
699
Global Instance make_persistently_emp : MakePersistently emp True.
Proof. by rewrite /MakePersistently -persistently_True_emp persistently_pure. Qed.
700
Global Instance make_persistently_default P : MakePersistently P ( P) | 100.
Robbert Krebbers's avatar
Robbert Krebbers committed
701
Proof. by rewrite /MakePersistently. Qed.
702

703
704
Global Instance frame_persistently R P Q Q' :
  Frame true R P Q  MakePersistently Q Q'  Frame true R ( P) Q'.
705
Proof.
706
707
708
  rewrite /Frame /MakePersistently=> <- <- /=. rewrite -persistently_and_bare_sep_l.
  by rewrite -persistently_sep_2 -persistently_and_sep_l_1 persistently_bare
              persistently_idemp.
709
710
Qed.

Robbert Krebbers's avatar
Robbert Krebbers committed
711
Global Instance frame_exist {A} p R (Φ Ψ : A  PROP) :
712
  ( a, Frame p R (Φ a) (Ψ a))  Frame p R ( x, Φ x) ( x, Ψ x).
713
Proof. rewrite /Frame=> ?. by rewrite sep_exist_l; apply exist_mono. Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
714
Global Instance frame_forall {A} p R (Φ Ψ : A  PROP) :
715
  ( a, Frame p R (Φ a) (Ψ a))  Frame p R ( x, Φ x) ( x, Ψ x).
716
Proof. rewrite /Frame=> ?. by rewrite sep_forall_l; apply forall_mono. Qed.
717
718
719
720

(* FromModal *)
Global Instance from_modal_sink P : FromModal ( P) P.
Proof. apply sink_intro. Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
721
722
End bi_instances.

723

Robbert Krebbers's avatar
Robbert Krebbers committed
724
725
726
727
728
729
730
731
732
733
734
735
736
737
738
739
740
741
742
743
744
745
746
747
748
749
750
Section sbi_instances.
Context {PROP : sbi}.
Implicit Types P Q R : PROP.

(* FromAssumption *)
Global Instance from_assumption_later p P Q :
  FromAssumption p P Q  FromAssumption p P ( Q)%I.
Proof. rewrite /FromAssumption=>->. apply later_intro. Qed.
Global Instance from_assumption_laterN n p P Q :
  FromAssumption p P Q  FromAssumption p P (^n Q)%I.
Proof. rewrite /FromAssumption=>->. apply laterN_intro. Qed.
Global Instance from_assumption_except_0 p P Q :
  FromAssumption p P Q  FromAssumption p P ( Q)%I.
Proof. rewrite /FromAssumption=>->. apply except_0_intro. Qed.

(* FromPure *)
Global Instance from_pure_later P φ : FromPure P φ  FromPure ( P) φ.
Proof. rewrite /FromPure=> ->. apply later_intro. Qed.
Global Instance from_pure_laterN n P φ : FromPure P φ  FromPure (^n P) φ.
Proof. rewrite /FromPure=> ->. apply laterN_intro. Qed.
Global Instance from_pure_except_0 P φ : FromPure P φ  FromPure ( P) φ.
Proof. rewrite /FromPure=> ->. apply except_0_intro. Qed.

(* IntoWand *)
Global Instance into_wand_later p q R P Q :
  IntoWand p q R P Q  IntoWand p q ( R) ( P) ( Q).
Proof.
751
  rewrite /IntoWand /= => HR. by rewrite !later_bare_persistently_if_2 -later_wand HR.
Robbert Krebbers's avatar
Robbert Krebbers committed
752
753
754
755
756
757
Qed.

Global Instance into_wand_later_args p q R P Q :
  IntoWand p q R P Q  IntoWand' p q R ( P) ( Q).
Proof.
  rewrite /IntoWand' /IntoWand /= => HR.
758
  by rewrite !later_bare_persistently_if_2 (later_intro (?p R)%I) -later_wand HR.
Robbert Krebbers's avatar
Robbert Krebbers committed
759
760
761
762
763
Qed.

Global Instance into_wand_laterN n p q R P Q :
  IntoWand p q R P Q  IntoWand p q (^n R) (^n P) (^n Q).
Proof.
764
  rewrite /IntoWand /= => HR. by rewrite !laterN_bare_persistently_if_2 -laterN_wand HR.
Robbert Krebbers's avatar
Robbert Krebbers committed
765
766
767
768
769
770
Qed.

Global Instance into_wand_laterN_args n p q R P Q :
  IntoWand p q R P Q  IntoWand' p q R (^n P) (^n Q).
Proof.
  rewrite /IntoWand' /IntoWand /= => HR.
771
  by rewrite !laterN_bare_persistently_if_2 (laterN_intro _ (?p R)%I) -laterN_wand HR.
Robbert Krebbers's avatar
Robbert Krebbers committed
772
Qed.
773

Robbert Krebbers's avatar
Robbert Krebbers committed
774
775
776
777
778
779
780
781
782
783
784
785
786
787
788
789
790
791
792
793
794
795
796
797
798
799
800
(* FromAnd *)
Global Instance from_and_later P Q1 Q2 :
  FromAnd P Q1 Q2  FromAnd ( P) ( Q1) ( Q2).
Proof. rewrite /FromAnd=> <-. by rewrite later_and. Qed.
Global Instance from_and_laterN n P Q1 Q2 :
  FromAnd P Q1 Q2  FromAnd (^n P) (^n Q1) (^n Q2).
Proof. rewrite /FromAnd=> <-. by rewrite laterN_and. Qed.
Global Instance from_and_except_0 P Q1 Q2 :
  FromAnd P Q1 Q2  FromAnd ( P) ( Q1) ( Q2).
Proof. rewrite /FromAnd=><-. by rewrite except_0_and. Qed.

(* FromSep *)
Global Instance from_sep_later P Q1 Q2 :
  FromSep P Q1 Q2  FromSep ( P) ( Q1) ( Q2).
Proof. rewrite /FromSep=> <-. by rewrite later_sep. Qed.
Global Instance from_sep_laterN n P Q1 Q2 :
  FromSep P Q1 Q2  FromSep (^n P) (^n Q1) (^n Q2).
Proof. rewrite /FromSep=> <-. by rewrite laterN_sep. Qed.
Global Instance from_sep_except_0 P Q1 Q2 :
  FromSep P Q1 Q2  FromSep ( P) ( Q1) ( Q2).
Proof. rewrite /FromSep=><-. by rewrite except_0_sep. Qed.

(* IntoAnd *)
Global Instance into_and_later p P Q1 Q2 :
  IntoAnd p P Q1 Q2  IntoAnd p ( P) ( Q1) ( Q2).
Proof.
  rewrite /IntoAnd=> HP. apply bare_persistently_if_intro'.
801
  by rewrite later_bare_persistently_if_2 HP bare_persistently_if_elim later_and.
Robbert Krebbers's avatar
Robbert Krebbers committed
802
803
804
805
806
Qed.
Global Instance into_and_laterN n p P Q1 Q2 :
  IntoAnd p P Q1 Q2  IntoAnd p (^n P) (^n Q1) (^n Q2).
Proof.
  rewrite /IntoAnd=> HP. apply bare_persistently_if_intro'.
807
  by rewrite laterN_bare_persistently_if_2 HP bare_persistently_if_elim laterN_and.
Robbert Krebbers's avatar
Robbert Krebbers committed
808
809
810
811
812
Qed.
Global Instance into_and_except_0 p P Q1 Q2 :
  IntoAnd p P Q1 Q2  IntoAnd p ( P) ( Q1) ( Q2).
Proof.
  rewrite /IntoAnd=> HP. apply bare_persistently_if_intro'.
813
  by rewrite except_0_bare_persistently_if_2 HP bare_persistently_if_elim except_0_and.
Robbert Krebbers's avatar
Robbert Krebbers committed
814
815
816
Qed.

(* IntoSep *)
817
818
819
820
821
822
823
824
825
Global Instance into_sep_later P Q1 Q2 :
  IntoSep P Q1 Q2  IntoSep ( P) ( Q1) ( Q2).
Proof. rewrite /IntoSep=> ->. by rewrite later_sep. Qed.
Global Instance into_sep_laterN n P Q1 Q2 :
  IntoSep P Q1 Q2  IntoSep (^n P) (^n Q1) (^n Q2).
Proof. rewrite /IntoSep=> ->. by rewrite laterN_sep. Qed.
Global Instance into_sep_except_0 P Q1 Q2 :
  IntoSep P Q1 Q2  IntoSep ( P) ( Q1) ( Q2).
Proof. rewrite /IntoSep=> ->. by rewrite except_0_sep. Qed.
Robbert Krebbers's avatar