class_instances.v 44.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
10
11
12
13
14
15
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_persistently {A : ofeT} (x y : A) P :
  IntoInternalEq P x y  IntoInternalEq ( P) x y.
16
Proof. rewrite /IntoInternalEq=> ->. by rewrite persistently_elim. Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
17
18
19
20
21
22
23
24
25
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.

(* 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.
26
27

(* FromAssumption *)
28
Global Instance from_assumption_exact p P : FromAssumption p P P | 0.
Robbert Krebbers's avatar
Robbert Krebbers committed
29
Proof. by rewrite /FromAssumption /= bare_persistently_if_elim. Qed.
30

31
Global Instance from_assumption_persistently_r P Q :
32
  FromAssumption true P Q  FromAssumption true P ( Q).
Robbert Krebbers's avatar
Robbert Krebbers committed
33
34
35
36
37
38
39
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.
40

Robbert Krebbers's avatar
Robbert Krebbers committed
41
42
43
44
45
46
47
48
49
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.
50
51
52
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
53
54

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

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

62
Global Instance into_pure_eq {A : ofeT} (a b : A) :
63
64
  Discrete a  @IntoPure M (a  b) (a  b).
Proof. intros. by rewrite /IntoPure discrete_eq. Qed.
65

Ralf Jung's avatar
Ralf Jung committed
66
Global Instance into_pure_pure_and (φ1 φ2 : Prop) P1 P2 :
Ralf Jung's avatar
Ralf Jung committed
67
  IntoPure P1 φ1  IntoPure P2 φ2  IntoPure (P1  P2) (φ1  φ2).
68
Proof. rewrite /IntoPure pure_and. by intros -> ->. Qed.
Ralf Jung's avatar
Ralf Jung committed
69
Global Instance into_pure_pure_or (φ1 φ2 : Prop) P1 P2 :
Ralf Jung's avatar
Ralf Jung committed
70
  IntoPure P1 φ1  IntoPure P2 φ2  IntoPure (P1  P2) (φ1  φ2).
71
Proof. rewrite /IntoPure pure_or. by intros -> ->. Qed.
Ralf Jung's avatar
Ralf Jung committed
72
Global Instance into_pure_pure_impl (φ1 φ2 : Prop) P1 P2 :
Ralf Jung's avatar
Ralf Jung committed
73
  FromPure P1 φ1  IntoPure P2 φ2  IntoPure (P1  P2) (φ1  φ2).
74
Proof. rewrite /FromPure /IntoPure pure_impl. by intros -> ->. Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
75
76
77
78
79
80
81
82
83
84
85

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

Robbert Krebbers's avatar
Robbert Krebbers committed
90
91
92
Global Instance into_pure_bare P φ : IntoPure P φ  IntoPure ( P) φ.
Proof. rewrite /IntoPure=> ->. apply bare_elim. Qed.
Global Instance into_pure_persistently P φ : IntoPure P φ  IntoPure ( P) φ.
93
Proof. rewrite /IntoPure=> ->. apply: persistently_elim. Qed.
94

95
(* FromPure *)
Robbert Krebbers's avatar
Robbert Krebbers committed
96
97
Global Instance from_pure_pure φ : @FromPure PROP ⌜φ⌝ φ.
Proof. by rewrite /FromPure. Qed.
98
Global Instance from_pure_internal_eq {A : ofeT} (a b : A) :
Robbert Krebbers's avatar
Robbert Krebbers committed
99
100
  @FromPure PROP (a  b) (a  b).
Proof. by rewrite /FromPure pure_internal_eq. Qed.
101

Ralf Jung's avatar
Ralf Jung committed
102
Global Instance from_pure_pure_and (φ1 φ2 : Prop) P1 P2 :
103
  FromPure P1 φ1  FromPure P2 φ2  FromPure (P1  P2) (φ1  φ2).
104
Proof. rewrite /FromPure pure_and. by intros -> ->. Qed.
Ralf Jung's avatar
Ralf Jung committed
105
Global Instance from_pure_pure_or (φ1 φ2 : Prop) P1 P2 :
106
  FromPure P1 φ1  FromPure P2 φ2  FromPure (P1  P2) (φ1  φ2).
107
Proof. rewrite /FromPure pure_or. by intros -> ->. Qed.
Ralf Jung's avatar
Ralf Jung committed
108
Global Instance from_pure_pure_impl (φ1 φ2 : Prop) P1 P2 :
109
  IntoPure P1 φ1  FromPure P2 φ2  FromPure (P1  P2) (φ1  φ2).
110
Proof. rewrite /FromPure /IntoPure pure_impl. by intros -> ->. Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
111
112
113
114
115
116
117
118
119
120

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).
121
Proof. rewrite /FromPure=> <- <-. by rewrite pure_and persistent_and_sep_1. Qed.
Ralf Jung's avatar
Ralf Jung committed
122
Global Instance from_pure_pure_wand (φ1 φ2 : Prop) P1 P2 :
123
  IntoPure P1 φ1  FromPure P2 φ2  FromPure (P1 - P2) (φ1  φ2).
124
Proof.
Robbert Krebbers's avatar
Robbert Krebbers committed
125
126
  rewrite /FromPure /IntoPure=> -> <-.
  by rewrite pure_wand_forall pure_impl pure_impl_forall.
127
128
Qed.

Robbert Krebbers's avatar
Robbert Krebbers committed
129
130
131
Global Instance from_pure_persistently P φ : FromPure P φ  FromPure ( P) φ.
Proof. rewrite /FromPure=> <-. by rewrite persistently_pure. Qed.

132
(* IntoPersistent *)
133
Global Instance into_persistent_persistently_trans p P Q :
134
  IntoPersistent true P Q  IntoPersistent p ( P) Q | 0.
Robbert Krebbers's avatar
Robbert Krebbers committed
135
136
137
138
139
140
141
Proof.
  rewrite /IntoPersistent /= => ->.
  destruct p; simpl; auto using persistently_idemp_1.
Qed.
Global Instance into_persistent_bare_trans p P Q :
  IntoPersistent p P Q  IntoPersistent p ( P) Q | 0.
Proof. rewrite /IntoPersistent /= => <-. by rewrite bare_elim. Qed.
142
Global Instance into_persistent_persistently P : IntoPersistent true P P | 1.
Robbert Krebbers's avatar
Robbert Krebbers committed
143
Proof. by rewrite /IntoPersistent. Qed.
144
145
Global Instance into_persistent_persistent P :
  Persistent P  IntoPersistent false P P | 100.
146
Proof. intros. by rewrite /IntoPersistent. Qed.
147

Robbert Krebbers's avatar
Robbert Krebbers committed
148
149
150
151
152
153
(* FromPersistent *)
Global Instance from_persistent_persistently P : FromPersistent ( P) P | 1.
Proof. by rewrite /FromPersistent. Qed.
Global Instance from_persistent_bare `{AffineBI PROP} P Q :
  FromPersistent P Q  FromPersistent ( P) Q.
Proof. rewrite /FromPersistent=> ->. by rewrite affine_bare. Qed.
154

Robbert Krebbers's avatar
Robbert Krebbers committed
155
156
157
(* IntoWand *)
Global Instance into_wand_wand p q P Q P' :
  FromAssumption q P P'  IntoWand p q (P' - Q) P Q.
158
Proof.
Robbert Krebbers's avatar
Robbert Krebbers committed
159
  rewrite /FromAssumption /IntoWand=> HP. by rewrite HP bare_persistently_if_elim.
Robbert Krebbers's avatar
Robbert Krebbers committed
160
Qed.
161

Robbert Krebbers's avatar
Robbert Krebbers committed
162
163
164
165
166
167
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
168

Robbert Krebbers's avatar
Robbert Krebbers committed
169
Global Instance into_wand_impl_false_true P Q P' :
170
  Absorbing P'  FromAssumption true P P' 
Robbert Krebbers's avatar
Robbert Krebbers committed
171
  IntoWand false true (P'  Q) P Q.
172
Proof.
173
  rewrite /IntoWand /FromAssumption /= => ? HP. apply wand_intro_l.
Robbert Krebbers's avatar
Robbert Krebbers committed
174
  rewrite -(bare_persistently_idemp P) HP.
175
  by rewrite -persistently_and_bare_sep_l persistently_elim impl_elim_r.
176
177
Qed.

Robbert Krebbers's avatar
Robbert Krebbers committed
178
Global Instance into_wand_impl_true_false P Q P' :
179
  Affine P'  FromAssumption false P P' 
Robbert Krebbers's avatar
Robbert Krebbers committed
180
  IntoWand true false (P'  Q) P Q.
181
Proof.
182
  rewrite /FromAssumption /IntoWand /= => ? HP. apply wand_intro_r.
Robbert Krebbers's avatar
Robbert Krebbers committed
183
184
  rewrite -persistently_and_bare_sep_l HP -{2}(affine_bare P') bare_and_l -bare_and_r.
  by rewrite bare_persistently_elim impl_elim_l.
185
Qed.
186

Robbert Krebbers's avatar
Robbert Krebbers committed
187
188
Global Instance into_wand_impl_true_true P Q P' :
  FromAssumption true P P'  IntoWand true true (P'  Q) P Q.
189
Proof.
Robbert Krebbers's avatar
Robbert Krebbers committed
190
  rewrite /FromAssumption /IntoWand /= => <-. apply wand_intro_l.
191
192
  rewrite -{1}(bare_persistently_idemp P) -and_sep_bare_persistently.
  by rewrite -bare_persistently_and impl_elim_r bare_persistently_elim.
193
Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
194
195
196
197
198
199
200
201
202
203
204
205
206
207
208
209
210

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.
211
Proof. by rewrite /IntoWand persistently_elim. Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
212
213
214
215
216
217

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 *)
218
219
Global Instance from_and_bare P : FromAnd ( P) emp P | 100.
Proof. by rewrite /FromAnd /bi_bare. Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
220
221
222
223
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.
224
Proof.
225
  rewrite /FromBare /FromAnd=> <- ?. by rewrite persistent_and_bare_sep_l_1.
226
Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
227
228
Global Instance from_and_sep_persistent_r P1 P2 P2' :
  FromBare P2 P2'  Persistent P2'  FromAnd (P1  P2) P1 P2' | 10.
229
Proof.
230
  rewrite /FromBare /FromAnd=> <- ?. by rewrite persistent_and_bare_sep_r_1.
231
Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
232
233
Global Instance from_and_sep_persistent P1 P2 :
  Persistent P1  Persistent P2  FromAnd (P1  P2) P1 P2 | 11.
234
Proof.
235
  rewrite /FromBare /FromAnd. intros ??. by rewrite -persistent_and_sep_1.
236
237
Qed.

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

Robbert Krebbers's avatar
Robbert Krebbers committed
241
242
243
244
245
246
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.
247

Robbert Krebbers's avatar
Robbert Krebbers committed
248
249
250
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).
251
Proof. intros. by rewrite /FromAnd big_opL_cons persistent_and_sep_1. Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
252
253
254
255
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).
256
Proof. intros. by rewrite /FromAnd big_opL_app persistent_and_sep_1. Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
257
258
259
260
261

(* 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 :
262
  TCOr (TCAnd (Affine P1) (Affine P2)) (TCAnd (Absorbing P1) (Absorbing P2)) 
Robbert Krebbers's avatar
Robbert Krebbers committed
263
264
265
266
267
268
269
270
  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).
271
Proof. rewrite /FromSep=> <-. by rewrite bare_sep_2. Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
272
273
Global Instance from_sep_persistently P Q1 Q2 :
  FromSep P Q1 Q2  FromSep ( P) ( Q1) ( Q2).
274
Proof. rewrite /FromSep=> <-. by rewrite persistently_sep_2. Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
275
276
277
278
279
280
281
282

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

Robbert Krebbers's avatar
Robbert Krebbers committed
284
(* IntoAnd *)
285
Global Instance into_and_and p P Q : IntoAnd p (P  Q) P Q | 10.
Robbert Krebbers's avatar
Robbert Krebbers committed
286
Proof. by rewrite /IntoAnd bare_persistently_if_and. Qed.
287
288
289
290
291
292
293
294
295
296
297
298
299
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 /=.
  by rewrite -(affine_bare P) bare_and_r bare_and (from_bare Q').
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 /=.
  by rewrite -(affine_bare Q) bare_and_l bare_and (from_bare P').
Qed.

300
301
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
302
303
304
305
306
307

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
308
Proof.
Robbert Krebbers's avatar
Robbert Krebbers committed
309
310
311
  rewrite /IntoAnd. destruct p; simpl.
  - by rewrite -bare_and !persistently_bare.
  - intros ->. by rewrite bare_and.
Robbert Krebbers's avatar
Robbert Krebbers committed
312
Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
313
314
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
315
Proof.
Robbert Krebbers's avatar
Robbert Krebbers committed
316
317
318
  rewrite /IntoAnd /=. destruct p; simpl.
  - by rewrite -persistently_and !persistently_idemp.
  - intros ->. by rewrite persistently_and.
Robbert Krebbers's avatar
Robbert Krebbers committed
319
320
Qed.

Robbert Krebbers's avatar
Robbert Krebbers committed
321
(* IntoSep *)
322
323
Global Instance into_sep_sep P Q : IntoSep (P  Q) P Q.
Proof. by rewrite /IntoSep. Qed.
324

325
326
327
328
329
330
331
332
333
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'.
334
Proof.
335
336
337
338
  destruct 2 as [P Q Q'|P Q]; rewrite /IntoSep.
  - rewrite -(from_bare Q') -(affine_bare P) bare_and_r -bare_and_l.
    by rewrite persistent_and_bare_sep_l_1.
  - by rewrite persistent_and_bare_sep_l_1.
339
Qed.
340
341
Global Instance into_sep_and_persistent_r P P' Q Q' :
  Persistent Q  AndIntoSep Q Q' P P'  IntoSep (P  Q) P' Q'.
342
Proof.
343
344
345
346
  destruct 2 as [Q P P'|Q P]; rewrite /IntoSep.
  - rewrite -(from_bare P') -(affine_bare Q) bare_and_l -bare_and_r.
    by rewrite persistent_and_bare_sep_r_1.
  - by rewrite persistent_and_bare_sep_r_1.
347
Qed.
348
349


350
351
352
353
354
355
356
357
358
Global Instance into_sep_pure φ ψ : @IntoSep PROP ⌜φ  ψ⌝ ⌜φ⌝ ⌜ψ⌝.
Proof. by rewrite /IntoSep pure_and persistent_and_sep_1. Qed.

Global Instance into_sep_bare `{PositiveBI PROP} P Q1 Q2 :
  IntoSep P Q1 Q2  IntoSep ( P) ( Q1) ( Q2).
Proof. rewrite /IntoSep /= => ->. by rewrite bare_sep. Qed.
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.
359

360
361
362
(* 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. *)
363
Global Instance into_sep_big_sepL_cons {A} (Φ : nat  A  PROP) l x l' :
364
  IsCons l x l' 
365
  IntoSep ([ list] k  y  l, Φ k y)
366
    (Φ 0 x) ([ list] k  y  l', Φ (S k) y).
Robbert Krebbers's avatar
Robbert Krebbers committed
367
Proof. rewrite /IsCons=>->. by rewrite /IntoSep big_sepL_cons. Qed.
368
Global Instance into_sep_big_sepL_app {A} (Φ : nat  A  PROP) l l1 l2 :
369
  IsApp l l1 l2 
370
  IntoSep ([ list] k  y  l, Φ k y)
371
    ([ list] k  y  l1, Φ k y) ([ list] k  y  l2, Φ (length l1 + k) y).
Robbert Krebbers's avatar
Robbert Krebbers committed
372
373
374
375
376
377
378
379
380
381
382
383
384
385
386
387
388
389
390
391
392
393
394
395
396
397
398
399
400
401
402
403
404
405
406
407
408
409
410
411
412
413
414
415
416
417
418
419
420
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
452
453
454
455
456
457
458
459
460
461
462
463
464
465
466
467
468
469
470
471
472
473
474
475
476
477
478
479
480
481
482
483
484
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.
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.
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.
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.
  eapply (pure_elim φ'); [by rewrite (into_pure P); apply absorbing, _|]=>?.
  rewrite -exist_intro //. apply sep_elim_r, _.
Qed.
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.
485
486

(* Frame *)
487
Global Instance frame_here_absorbing p R : Absorbing R  Frame p R R True | 0.
Robbert Krebbers's avatar
Robbert Krebbers committed
488
Proof. intros. by rewrite /Frame bare_persistently_if_elim sep_elim_l. Qed.
489
Global Instance frame_here p R : Frame p R R emp | 1.
Robbert Krebbers's avatar
Robbert Krebbers committed
490
Proof. intros. by rewrite /Frame bare_persistently_if_elim sep_elim_l. Qed.
491
492
493
494
495
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.

496
Global Instance frame_here_pure p φ Q : FromPure Q φ  Frame p ⌜φ⌝ Q True.
Robbert Krebbers's avatar
Robbert Krebbers committed
497
498
499
Proof.
  rewrite /FromPure /Frame=> <-. by rewrite bare_persistently_if_elim sep_elim_l.
Qed.
500

Robbert Krebbers's avatar
Robbert Krebbers committed
501
502
503
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.
504
Proof. by rewrite /MakeSep left_id. Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
505
Global Instance make_sep_emp_r P : MakeSep P emp P.
506
Proof. by rewrite /MakeSep right_id. Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
507
508
509
510
Global Instance make_sep_true_l P : Absorbing P  MakeSep True P P.
Proof. intros. by rewrite /MakeSep True_sep. Qed.
Global Instance make_sep_true_r P : Absorbing P  MakeSep P True P.
Proof. intros. by rewrite /MakeSep sep_True. Qed.
511
Global Instance make_sep_default P Q : MakeSep P Q (P  Q) | 100.
Robbert Krebbers's avatar
Robbert Krebbers committed
512
Proof. by rewrite /MakeSep. Qed.
513
514
515
516
517
518

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 /= => <- <- <-.
519
  rewrite {1}(bare_persistently_sep_dup R). solve_sep_entails.
520
Qed.
521
Global Instance frame_sep_l R P1 P2 Q Q' :
522
  Frame false R P1 Q  MakeSep Q P2 Q'  Frame false R (P1  P2) Q' | 9.
523
Proof. rewrite /Frame /MakeSep => <- <-. by rewrite assoc. Qed.
524
525
526
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.
527

Robbert Krebbers's avatar
Robbert Krebbers committed
528
Global Instance frame_big_sepL_cons {A} p (Φ : nat  A  PROP) R Q l x l' :
529
530
531
532
  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
533
Global Instance frame_big_sepL_app {A} p (Φ : nat  A  PROP) R Q l l1 l2 :
534
  IsApp l l1 l2 
535
  Frame p R (([ list] k  y  l1, Φ k y) 
536
           [ list] k  y  l2, Φ (length l1 + k) y) Q 
537
  Frame p R ([ list] k  y  l, Φ k y) Q.
538
Proof. rewrite /IsApp=>->. by rewrite /Frame big_opL_app. Qed.
539

Robbert Krebbers's avatar
Robbert Krebbers committed
540
541
Class MakeAnd (P Q PQ : PROP) := make_and : P  Q  PQ.
Arguments MakeAnd _%I _%I _%I.
542
543
544
545
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
546
547
Global Instance make_and_emp_l P : Affine P  MakeAnd emp P P.
Proof. intros. by rewrite /MakeAnd emp_and. Qed.
548
549
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
550
551
Global Instance make_and_emp_r P : Affine P  MakeAnd P emp P.
Proof. intros. by rewrite /MakeAnd and_emp. Qed.
552
553
Global Instance make_and_emp_r_bare P : MakeAnd P emp ( P) | 10.
Proof. intros. by rewrite /MakeAnd comm. Qed.
554
Global Instance make_and_default P Q : MakeAnd P Q (P  Q) | 100.
Robbert Krebbers's avatar
Robbert Krebbers committed
555
556
557
558
559
560
561
562
563
564
565
566
567
568
569
570
571
572
573
574
575
576
577
578
579
580
581
582
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.
583
584
585
586
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
587
588
589
590
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.
591
Global Instance make_or_default P Q : MakeOr P Q (P  Q) | 100.
Robbert Krebbers's avatar
Robbert Krebbers committed
592
Proof. by rewrite /MakeOr. Qed.
593
594
595
596
597
598
599
600
601

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
602
603
  rewrite /Frame /MaybeFrame /MakeOr => <- <- /=.
  by rewrite sep_or_l sep_elim_r.
604
Qed.
605
Global Instance frame_or R P1 P2 Q1 Q2 Q :
606
607
  Frame false R P1 Q1  Frame false R P2 Q2  MakeOr Q1 Q2 Q 
  Frame false R (P1  P2) Q.
608
609
Proof. rewrite /Frame /MakeOr => <- <- <-. by rewrite -sep_or_l. Qed.

610
611
Global Instance frame_wand p R P1 P2 Q2 :
  Frame p R P2 Q2  Frame p R (P1 - P2) (P1 - Q2).
612
613
614
615
616
Proof.
  rewrite /Frame=> ?. apply wand_intro_l.
  by rewrite assoc (comm _ P1) -assoc wand_elim_r.
Qed.

Robbert Krebbers's avatar
Robbert Krebbers committed
617
618
Class MakeBare (P Q : PROP) := make_bare :  P  Q.
Arguments MakeBare _%I _%I.
619
620
621
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
622
623
624
Proof. intros. by rewrite /MakeBare affine_bare. Qed.
Global Instance make_bare_default P : MakeBare P ( P) | 100.
Proof. by rewrite /MakeBare. Qed.
625

Robbert Krebbers's avatar
Robbert Krebbers committed
626
627
Global Instance frame_bare R P Q Q' :
  Frame true R P Q  MakeBare Q Q'  Frame true R ( P) Q'.
628
629
630
631
Proof.
  rewrite /Frame /MakeBare=> <- <- /=.
  by rewrite -{1}bare_idemp bare_sep_2.
Qed.
632

Robbert Krebbers's avatar
Robbert Krebbers committed
633
634
Class MakePersistently (P Q : PROP) := make_persistently :  P  Q.
Arguments MakePersistently _%I _%I.
635
636
Global Instance make_persistently_true : MakePersistently True True.
Proof. by rewrite /MakePersistently persistently_pure. Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
637
638
Global Instance make_persistently_emp : MakePersistently emp True.
Proof. by rewrite /MakePersistently -persistently_True_emp persistently_pure. Qed.
639
Global Instance make_persistently_default P : MakePersistently P ( P) | 100.
Robbert Krebbers's avatar
Robbert Krebbers committed
640
Proof. by rewrite /MakePersistently. Qed.
641

642
643
Global Instance frame_persistently R P Q Q' :
  Frame true R P Q  MakePersistently Q Q'  Frame true R ( P) Q'.
644
Proof.
645
646
647
  rewrite /Frame /MakePersistently=> <- <- /=. rewrite -persistently_and_bare_sep_l.
  by rewrite -persistently_sep_2 -persistently_and_sep_l_1 persistently_bare
              persistently_idemp.
648
649
Qed.

Robbert Krebbers's avatar
Robbert Krebbers committed
650
Global Instance frame_exist {A} p R (Φ Ψ : A  PROP) :
651
  ( a, Frame p R (Φ a) (Ψ a))  Frame p R ( x, Φ x) ( x, Ψ x).
652
Proof. rewrite /Frame=> ?. by rewrite sep_exist_l; apply exist_mono. Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
653
Global Instance frame_forall {A} p R (Φ Ψ : A  PROP) :
654
  ( a, Frame p R (Φ a) (Ψ a))  Frame p R ( x, Φ x) ( x, Ψ x).
655
Proof. rewrite /Frame=> ?. by rewrite sep_forall_l; apply forall_mono. Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
656
657
658
659
660
661
662
663
664
665
666
667
668
669
670
671
672
673
674
675
676
677
678
679
680
681
682
683
684
685
686
687
688
689
690
691
692
693
694
695
696
697
698
699
700
701
702
703
704
705
706
End bi_instances.

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.
  rewrite /IntoWand /= => HR. by rewrite !bare_persistently_if_later -later_wand HR.
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.
  by rewrite !bare_persistently_if_later (later_intro (?p R)%I) -later_wand HR.
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.
  rewrite /IntoWand /= => HR. by rewrite !bare_persistently_if_laterN -laterN_wand HR.
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.
  by rewrite !bare_persistently_if_laterN (laterN_intro _ (?p R)%I) -laterN_wand HR.
Qed.
707

Robbert Krebbers's avatar
Robbert Krebbers committed
708
709
710
711
712
713
714
715
716
717
718
719
720
721
722
723
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
(* 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'.
  by rewrite bare_persistently_if_later HP bare_persistently_if_elim later_and.
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'.
  by rewrite bare_persistently_if_laterN HP bare_persistently_if_elim laterN_and.
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'.
  by rewrite bare_persistently_if_except_0 HP bare_persistently_if_elim except_0_and.
Qed.

(* IntoSep *)
751
752
753
754
755
756
757
758
759
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.
760

761
(* FromOr *)
762
763
Global Instance from_or_later P Q1 Q2 :
  FromOr P Q1 Q2  FromOr ( P) ( Q1) ( Q2).
764
Proof. rewrite /FromOr=><-. by rewrite later_or. Qed.
765
766
767
Global Instance from_or_laterN n P Q1 Q2 :
  FromOr P Q1 Q2  FromOr (^n P) (^n Q1) (^n Q2).
Proof. rewrite /FromOr=><-. by rewrite laterN_or. Qed.
768
769
770
Global Instance from_or_except_0 P Q1 Q2 :
  FromOr P Q1 Q2  FromOr ( P) ( Q1) ( Q2).
Proof. rewrite /FromOr=><-. by rewrite except_0_or. Qed.
771
772
773
774
775

(* IntoOr *)
Global Instance into_or_later P Q1 Q2 :
  IntoOr P Q1 Q2  IntoOr ( P) ( Q1) ( Q2).
Proof. rewrite /IntoOr=>->. by rewrite later_or. Qed.
776
777
778
Global Instance into_or_laterN n P Q1 Q2 :
  IntoOr P Q1 Q2  IntoOr (^n P) (^n Q1) (^n Q2).
Proof. rewrite /IntoOr=>->. by rewrite laterN_or. Qed.
779
780
781
Global Instance into_or_except_0 P Q1 Q2 :
  IntoOr P Q1 Q2  IntoOr ( P) ( Q1) ( Q2).
Proof. rewrite /IntoOr=>->. by rewrite except_0_or. Qed.
782
783

(* FromExist *)
Robbert Krebbers's avatar
Robbert Krebbers committed
784
Global Instance from_exist_later {A} P (Φ : A  PROP) :
785
  FromExist P Φ  FromExist ( P) (λ a,  (Φ a))%I.
786
787
788
Proof.
  rewrite /FromExist=> <-. apply exist_elim=>x. apply later_mono, exist_intro.
Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
789
Global Instance from_exist_laterN {A} n P (Φ : A  PROP) :
790
791
792
793
  FromExist P Φ  FromExist (^n P) (λ a, ^n (Φ a))%I.
Proof.
  rewrite /FromExist=> <-. apply exist_elim=>x. apply laterN_mono, exist_intro.
Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
794
Global Instance from_exist_except_0 {A} P (Φ : A  PROP) :
795
796
  FromExist P Φ  FromExist ( P) (λ a,  (Φ a))%I.
Proof. rewrite /FromExist=> <-. by rewrite except_0_exist_2. Qed.
797
798

(* IntoExist *)
Robbert Krebbers's avatar
Robbert Krebbers committed
799
Global Instance into_exist_later {A} P (Φ : A  PROP) :
800
801
  IntoExist P Φ  Inhabited A  IntoExist ( P) (λ a,  (Φ a))%I.
Proof. rewrite /IntoExist=> HP ?. by rewrite HP later_exist. Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
802
Global Instance into_exist_laterN {A} n P (Φ : A  PROP) :
803
804
  IntoExist P Φ  Inhabited A  IntoExist (^n P) (λ a, ^n (Φ a))%I.
Proof. rewrite /IntoExist=> HP ?. by rewrite HP laterN_exist. Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
805
Global Instance into_exist_except_0 {A} P (Φ : A  PROP) :
806
807
  IntoExist P Φ  Inhabited A  IntoExist ( P) (λ a,  (Φ a))%I.
Proof. rewrite /IntoExist=> HP ?. by rewrite HP except_0_exist. Qed.
808

809
(* IntoForall *)
Robbert Krebbers's avatar
Robbert Krebbers committed
810
Global Instance into_forall_later {A} P (Φ : A  PROP) :
811
812
  IntoForall P Φ  IntoForall ( P) (λ a,  (Φ a))%I.
Proof. rewrite /IntoForall=> HP. by rewrite HP later_forall. Qed.
813

814
(* FromForall *)
Robbert Krebbers's avatar
Robbert Krebbers committed
815
816
Global Instance from_forall_later {A} P (Φ : A  PROP) :
  FromForall P Φ  FromForall ( P)%I (λ a,  (Φ a))%I.
817
818
Proof. rewrite /FromForall=> <-. by rewrite later_forall. Qed.

Robbert Krebbers's avatar
Robbert Krebbers committed
819
820
821
822
823
824
(* IsExcept0 *)
Global Instance is_except_0_except_0 P : IsExcept0 ( P).
Proof. by rewrite /IsExcept0 except_0_idemp. Qed.
Global Instance is_except_0_later P : IsExcept0 ( P).
Proof. by rewrite /IsExcept0 except_0_later. Qed.

825
826
(* FromModal *)
Global Instance from_modal_later P : FromModal ( P) P.
827
Proof. apply later_intro. Qed.
828
Global Instance from_modal_except_0 P : FromModal ( P) P.
829
830
831
Proof. apply except_0_intro. Qed.

(* ElimModal *)
Robbert Krebbers's avatar
Robbert Krebbers committed
832
Global Instance elim_modal_except_0 P Q : IsExcept0 Q  ElimModal ( P) P Q Q.
833
Proof.
Robbert Krebbers's avatar
Robbert Krebbers committed
834
835
  intros. rewrite /ElimModal (except_0_intro (_ - _)%I).
  by rewrite -except_0_sep wand_elim_r.
836
Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed