class_instances.v 45.8 KB
Newer Older
1
From stdpp Require Import nat_cancel.
2
3
4
From iris.bi Require Import bi telescopes.
From iris.proofmode Require Import base modality_instances classes.
From iris.proofmode Require Import ltac_tactics.
Ralf Jung's avatar
Ralf Jung committed
5
From iris.prelude Require Import options.
Robbert Krebbers's avatar
Robbert Krebbers committed
6
7
Import bi.

Robbert Krebbers's avatar
Robbert Krebbers committed
8
(* FIXME(Coq #6294): needs new unification *)
9
10
11
12
13
14
(** The lemma [from_assumption_exact is not an instance, but defined using
[notypeclasses refine] through [Hint Extern] to enable the better unification
algorithm. We use [shelve] to avoid the creation of unshelved goals for evars
by [refine], which otherwise causes TC search to fail. Such unshelved goals are
created for example when solving [FromAssumption p ?P ?Q] where both [?P] and
[?Q] are evars. See [test_iApply_evar] in [tests/proofmode] for an example. *)
15
16
Lemma from_assumption_exact {PROP : bi} p (P : PROP) : FromAssumption p P P.
Proof. by rewrite /FromAssumption /= intuitionistically_if_elim. Qed.
17
Global Hint Extern 0 (FromAssumption _ _ _) =>
18
  notypeclasses refine (from_assumption_exact _ _); shelve : typeclass_instances.
19

Robbert Krebbers's avatar
Robbert Krebbers committed
20
21
22
23
24
25
(* FIXME(Coq #6294): needs new unification *)
(** Similarly, the lemma [from_exist_exist] is defined using a [Hint Extern] to
enable the better unification algorithm.
See https://gitlab.mpi-sws.org/iris/iris/issues/288 *)
Lemma from_exist_exist {PROP : bi} {A} (Φ : A  PROP) : FromExist ( a, Φ a) Φ.
Proof. by rewrite /FromExist. Qed.
26
Global Hint Extern 0 (FromExist _ _) =>
Robbert Krebbers's avatar
Robbert Krebbers committed
27
28
  notypeclasses refine (from_exist_exist _) : typeclass_instances.

29
Section class_instances.
Robbert Krebbers's avatar
Robbert Krebbers committed
30
31
Context {PROP : bi}.
Implicit Types P Q R : PROP.
32
Implicit Types mP : option PROP.
Robbert Krebbers's avatar
Robbert Krebbers committed
33

34
(** AsEmpValid *)
35
Global Instance as_emp_valid_emp_valid P : AsEmpValid0 ( P) P | 0.
36
Proof. by rewrite /AsEmpValid. Qed.
37
Global Instance as_emp_valid_entails P Q : AsEmpValid0 (P  Q) (P - Q).
38
Proof. split; [ apply bi.entails_wand | apply bi.wand_entails ]. Qed.
39
Global Instance as_emp_valid_equiv P Q : AsEmpValid0 (P  Q) (P - Q).
40
Proof. split; [ apply bi.equiv_wand_iff | apply bi.wand_iff_equiv ]. Qed.
41
42
43
44
45
46
47
48

Global Instance as_emp_valid_forall {A : Type} (φ : A  Prop) (P : A  PROP) :
  ( x, AsEmpValid (φ x) (P x))  AsEmpValid ( x, φ x) ( x, P x).
Proof.
  rewrite /AsEmpValid=>H1. split=>H2.
  - apply bi.forall_intro=>?. apply H1, H2.
  - intros x. apply H1. revert H2. by rewrite (bi.forall_elim x).
Qed.
49
50
51
52
53
54
Global Instance as_emp_valid_tforall {TT : tele} (φ : TT  Prop) (P : TT  PROP) :
  ( x, AsEmpValid (φ x) (P x))  AsEmpValid (.. x, φ x) (.. x, P x).
Proof.
  rewrite /AsEmpValid !tforall_forall bi_tforall_forall.
  apply as_emp_valid_forall.
Qed.
55

56
(** FromAffinely *)
57
58
Global Instance from_affinely_affine P : Affine P  FromAffinely P P.
Proof. intros. by rewrite /FromAffinely affinely_elim. Qed.
59
Global Instance from_affinely_default P : FromAffinely (<affine> P) P | 100.
60
Proof. by rewrite /FromAffinely. Qed.
61
62
63
Global Instance from_affinely_intuitionistically P :
  FromAffinely ( P) (<pers> P) | 100.
Proof. by rewrite /FromAffinely. Qed.
64

65
(** IntoAbsorbingly *)
66
67
68
69
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.
70
Global Instance into_absorbingly_intuitionistically P :
71
  IntoAbsorbingly (<pers> P) ( P) | 2.
72
73
74
Proof.
  by rewrite /IntoAbsorbingly -absorbingly_intuitionistically_into_persistently.
Qed.
75
Global Instance into_absorbingly_default P : IntoAbsorbingly (<absorb> P) P | 100.
76
Proof. by rewrite /IntoAbsorbingly. Qed.
77

78
(** FromAssumption *)
79
Global Instance from_assumption_persistently_r P Q :
80
  FromAssumption true P Q  KnownRFromAssumption true P (<pers> Q).
Robbert Krebbers's avatar
Robbert Krebbers committed
81
Proof.
82
  rewrite /KnownRFromAssumption /FromAssumption /= =><-.
83
  apply intuitionistically_persistent.
Robbert Krebbers's avatar
Robbert Krebbers committed
84
Qed.
85
Global Instance from_assumption_affinely_r P Q :
86
  FromAssumption true P Q  KnownRFromAssumption true P (<affine> Q).
87
88
89
90
Proof.
  rewrite /KnownRFromAssumption /FromAssumption /= =><-.
  by rewrite affinely_idemp.
Qed.
91
92
93
94
95
96
Global Instance from_assumption_intuitionistically_r P Q :
  FromAssumption true P Q  KnownRFromAssumption true P ( Q).
Proof.
  rewrite /KnownRFromAssumption /FromAssumption /= =><-.
  by rewrite intuitionistically_idemp.
Qed.
97
Global Instance from_assumption_absorbingly_r p P Q :
98
  FromAssumption p P Q  KnownRFromAssumption p P (<absorb> Q).
99
100
101
102
Proof.
  rewrite /KnownRFromAssumption /FromAssumption /= =><-.
  apply absorbingly_intro.
Qed.
103

104
Global Instance from_assumption_intuitionistically_l p P Q :
105
106
107
  FromAssumption true P Q  KnownLFromAssumption p ( P) Q.
Proof.
  rewrite /KnownLFromAssumption /FromAssumption /= =><-.
108
  by rewrite intuitionistically_if_elim.
109
Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
110
Global Instance from_assumption_persistently_l_true P Q :
111
  FromAssumption true P Q  KnownLFromAssumption true (<pers> P) Q.
112
113
Proof.
  rewrite /KnownLFromAssumption /FromAssumption /= =><-.
Ralf Jung's avatar
Ralf Jung committed
114
  rewrite intuitionistically_persistently_elim //.
115
Qed.
116
Global Instance from_assumption_persistently_l_false `{BiAffine PROP} P Q :
117
  FromAssumption true P Q  KnownLFromAssumption false (<pers> P) Q.
118
119
Proof.
  rewrite /KnownLFromAssumption /FromAssumption /= =><-.
Ralf Jung's avatar
Ralf Jung committed
120
  by rewrite intuitionistically_into_persistently.
121
Qed.
122
Global Instance from_assumption_affinely_l_true p P Q :
123
  FromAssumption p P Q  KnownLFromAssumption p (<affine> P) Q.
124
125
126
127
Proof.
  rewrite /KnownLFromAssumption /FromAssumption /= =><-.
  by rewrite affinely_elim.
Qed.
128
129
130
131
132
133
Global Instance from_assumption_intuitionistically_l_true p P Q :
  FromAssumption p P Q  KnownLFromAssumption p ( P) Q.
Proof.
  rewrite /KnownLFromAssumption /FromAssumption /= =><-.
  by rewrite intuitionistically_elim.
Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
134
135

Global Instance from_assumption_forall {A} p (Φ : A  PROP) Q x :
136
137
138
139
140
  FromAssumption p (Φ x) Q  KnownLFromAssumption p ( x, Φ x) Q.
Proof.
  rewrite /KnownLFromAssumption /FromAssumption=> <-.
  by rewrite forall_elim.
Qed.
141
142
143
144
145
146
Global Instance from_assumption_tforall {TT : tele} p (Φ : TT  PROP) Q x :
  FromAssumption p (Φ x) Q  KnownLFromAssumption p (.. x, Φ x) Q.
Proof.
  rewrite /KnownLFromAssumption /FromAssumption=> <-.
  by rewrite bi_tforall_forall forall_elim.
Qed.
147

148
(** IntoPure *)
Robbert Krebbers's avatar
Robbert Krebbers committed
149
150
151
Global Instance into_pure_pure φ : @IntoPure PROP ⌜φ⌝ φ.
Proof. by rewrite /IntoPure. Qed.

Ralf Jung's avatar
Ralf Jung committed
152
Global Instance into_pure_pure_and (φ1 φ2 : Prop) P1 P2 :
Ralf Jung's avatar
Ralf Jung committed
153
  IntoPure P1 φ1  IntoPure P2 φ2  IntoPure (P1  P2) (φ1  φ2).
154
Proof. rewrite /IntoPure pure_and. by intros -> ->. Qed.
Ralf Jung's avatar
Ralf Jung committed
155
Global Instance into_pure_pure_or (φ1 φ2 : Prop) P1 P2 :
Ralf Jung's avatar
Ralf Jung committed
156
  IntoPure P1 φ1  IntoPure P2 φ2  IntoPure (P1  P2) (φ1  φ2).
157
Proof. rewrite /IntoPure pure_or. by intros -> ->. Qed.
158
Global Instance into_pure_pure_impl `{!BiPureForall PROP} (φ1 φ2 : Prop) P1 P2 :
159
  FromPure false P1 φ1  IntoPure P2 φ2  IntoPure (P1  P2) (φ1  φ2).
160
Proof. rewrite /FromPure /IntoPure /= => <- ->. apply pure_impl_2. Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
161
162
163
164

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.
165
166
167
Global Instance into_pure_texist {TT : tele} (Φ : TT  PROP) (φ : TT  Prop) :
  ( x, IntoPure (Φ x) (φ x))  IntoPure (.. x, Φ x) (.. x, φ x).
Proof. rewrite /IntoPure texist_exist bi_texist_exist. apply into_pure_exist. Qed.
168
169
Global Instance into_pure_forall `{!BiPureForall PROP}
    {A} (Φ : A  PROP) (φ : A  Prop) :
Robbert Krebbers's avatar
Robbert Krebbers committed
170
171
  ( x, IntoPure (Φ x) (φ x))  IntoPure ( x, Φ x) ( x, φ x).
Proof. rewrite /IntoPure=>Hx. rewrite -pure_forall_2. by setoid_rewrite Hx. Qed.
172
173
Global Instance into_pure_tforall `{!BiPureForall PROP}
    {TT : tele} (Φ : TT  PROP) (φ : TT  Prop) :
174
175
176
177
  ( x, IntoPure (Φ x) (φ x))  IntoPure (.. x, Φ x) (.. x, φ x).
Proof.
  rewrite /IntoPure !tforall_forall bi_tforall_forall. apply into_pure_forall.
Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
178
179
180
181

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.
182
Global Instance into_pure_pure_wand `{!BiPureForall PROP} a (φ1 φ2 : Prop) P1 P2 :
183
  FromPure a P1 φ1  IntoPure P2 φ2  IntoPure (P1 - P2) (φ1  φ2).
184
Proof.
185
186
187
  rewrite /FromPure /IntoPure=> <- -> /=. rewrite pure_impl.
  apply impl_intro_l, pure_elim_l=> ?. rewrite (pure_True φ1) //.
  by rewrite -affinely_affinely_if affinely_True_emp affinely_emp left_id.
188
Qed.
189

190
Global Instance into_pure_affinely P φ : IntoPure P φ  IntoPure (<affine> P) φ.
191
Proof. rewrite /IntoPure=> ->. apply affinely_elim. Qed.
192
193
194
Global Instance into_pure_intuitionistically P φ :
  IntoPure P φ  IntoPure ( P) φ.
Proof. rewrite /IntoPure=> ->. apply intuitionistically_elim. Qed.
195
Global Instance into_pure_absorbingly P φ : IntoPure P φ  IntoPure (<absorb> P) φ.
196
197
Proof. rewrite /IntoPure=> ->. by rewrite absorbingly_pure. Qed.
Global Instance into_pure_persistently P φ :
198
  IntoPure P φ  IntoPure (<pers> P) φ.
199
Proof. rewrite /IntoPure=> ->. apply: persistently_elim. Qed.
200

201
(** FromPure *)
202
203
204
205
206
207
208
209
210
211
212
213
214
215
216
217
218
219
Global Instance from_pure_emp : @FromPure PROP true emp True.
Proof. rewrite /FromPure /=. apply (affine _). Qed.
Global Instance from_pure_pure φ : @FromPure PROP false ⌜φ⌝ φ.
Proof. by rewrite /FromPure /=. Qed.
Global Instance from_pure_pure_and a1 a2 (φ1 φ2 : Prop) P1 P2 :
  FromPure a1 P1 φ1  FromPure a2 P2 φ2 
  FromPure (if a1 then true else a2) (P1  P2) (φ1  φ2).
Proof.
  rewrite /FromPure pure_and=> <- <- /=. rewrite affinely_if_and.
  f_equiv; apply affinely_if_flag_mono; destruct a1; naive_solver.
Qed.
Global Instance from_pure_pure_or a1 a2 (φ1 φ2 : Prop) P1 P2 :
  FromPure a1 P1 φ1  FromPure a2 P2 φ2 
  FromPure (if a1 then true else a2) (P1  P2) (φ1  φ2).
Proof.
  rewrite /FromPure pure_or=> <- <- /=. rewrite affinely_if_or.
  f_equiv; apply affinely_if_flag_mono; destruct a1; naive_solver.
Qed.
220
221
222
Global Instance from_pure_pure_impl a (φ1 φ2 : Prop) P1 P2 :
  IntoPure P1 φ1  FromPure a P2 φ2  FromPure a (P1  P2) (φ1  φ2).
Proof.
223
  rewrite /FromPure /IntoPure pure_impl_1=> -> <-. destruct a=>//=.
224
225
226
227
228
229
230
231
232
  apply bi.impl_intro_l. by rewrite affinely_and_r bi.impl_elim_r.
Qed.

Global Instance from_pure_exist {A} a (Φ : A  PROP) (φ : A  Prop) :
  ( x, FromPure a (Φ x) (φ x))  FromPure a ( x, Φ x) ( x, φ x).
Proof.
  rewrite /FromPure=>Hx. rewrite pure_exist affinely_if_exist.
  by setoid_rewrite Hx.
Qed.
233
234
235
Global Instance from_pure_texist {TT : tele} a (Φ : TT  PROP) (φ : TT  Prop) :
  ( x, FromPure a (Φ x) (φ x))  FromPure a (.. x, Φ x) (.. x, φ x).
Proof. rewrite /FromPure texist_exist bi_texist_exist. apply from_pure_exist. Qed.
236
237
238
Global Instance from_pure_forall {A} a (Φ : A  PROP) (φ : A  Prop) :
  ( x, FromPure a (Φ x) (φ x))  FromPure a ( x, Φ x) ( x, φ x).
Proof.
239
  rewrite /FromPure=>Hx. rewrite pure_forall_1. setoid_rewrite <-Hx.
240
241
  destruct a=>//=. apply affinely_forall.
Qed.
242
243
244
245
246
Global Instance from_pure_tforall {TT : tele} a (Φ : TT  PROP) (φ : TT  Prop) :
  ( x, FromPure a (Φ x) (φ x))  FromPure a (.. x, Φ x) (.. x, φ x).
Proof.
  rewrite /FromPure !tforall_forall bi_tforall_forall. apply from_pure_forall.
Qed.
247

248
249
250
Global Instance from_pure_pure_sep_true a1 a2 (φ1 φ2 : Prop) P1 P2 :
  FromPure a1 P1 φ1  FromPure a2 P2 φ2 
  FromPure (if a1 then a2 else false) (P1  P2) (φ1  φ2).
251
Proof.
252
253
254
  rewrite /FromPure=> <- <-. destruct a1; simpl.
  - by rewrite pure_and -persistent_and_affinely_sep_l affinely_if_and_r.
  - by rewrite pure_and -affinely_affinely_if -persistent_and_affinely_sep_r_1.
255
Qed.
256
257
258
259
Global Instance from_pure_pure_wand a (φ1 φ2 : Prop) P1 P2 :
  IntoPure P1 φ1  FromPure a P2 φ2 
  TCOr (TCEq a false) (Affine P1) 
  FromPure a (P1 - P2) (φ1  φ2).
260
Proof.
261
262
263
264
  rewrite /FromPure /IntoPure=> HP1 <- Ha /=. apply wand_intro_l.
  destruct a; simpl.
  - destruct Ha as [Ha|?]; first inversion Ha.
    rewrite -persistent_and_affinely_sep_r -(affine_affinely P1) HP1.
265
266
    by rewrite affinely_and_l pure_impl_1 impl_elim_r.
  - by rewrite HP1 sep_and pure_impl_1 impl_elim_r.
267
268
Qed.

269
Global Instance from_pure_persistently P a φ :
270
  FromPure true P φ  FromPure a (<pers> P) φ.
271
272
Proof.
  rewrite /FromPure=> <- /=.
Ralf Jung's avatar
Ralf Jung committed
273
  by rewrite persistently_affinely_elim affinely_if_elim persistently_pure.
274
Qed.
275
276
277
278
279
Global Instance from_pure_affinely_true a P φ :
  FromPure a P φ  FromPure true (<affine> P) φ.
Proof. rewrite /FromPure=><- /=. by rewrite -affinely_affinely_if affinely_idemp. Qed.
Global Instance from_pure_intuitionistically_true a P φ :
  FromPure a P φ  FromPure true ( P) φ.
280
Proof.
281
282
283
  rewrite /FromPure=><- /=.
  rewrite -intuitionistically_affinely_elim -affinely_affinely_if affinely_idemp.
  by rewrite intuitionistic_intuitionistically.
284
Qed.
285
286
Global Instance from_pure_absorbingly a P φ :
  FromPure a P φ  FromPure false (<absorb> P) φ.
287
Proof.
288
289
  rewrite /FromPure=> <- /=. rewrite -affinely_affinely_if.
  by rewrite -persistent_absorbingly_affinely_2.
290
Qed.
291

292
(** IntoPersistent *)
293
Global Instance into_persistent_persistently p P Q :
294
  IntoPersistent true P Q  IntoPersistent p (<pers> P) Q | 0.
Robbert Krebbers's avatar
Robbert Krebbers committed
295
296
297
298
Proof.
  rewrite /IntoPersistent /= => ->.
  destruct p; simpl; auto using persistently_idemp_1.
Qed.
299
Global Instance into_persistent_affinely p P Q :
300
  IntoPersistent p P Q  IntoPersistent p (<affine> P) Q | 0.
301
Proof. rewrite /IntoPersistent /= => <-. by rewrite affinely_elim. Qed.
302
Global Instance into_persistent_intuitionistically p P Q :
303
304
305
306
307
  IntoPersistent true P Q  IntoPersistent p ( P) Q | 0.
Proof.
  rewrite /IntoPersistent /= =><-.
  destruct p; simpl;
    eauto using persistently_mono, intuitionistically_elim,
Ralf Jung's avatar
Ralf Jung committed
308
    intuitionistically_into_persistently_1.
309
Qed.
310
Global Instance into_persistent_here P : IntoPersistent true P P | 1.
Robbert Krebbers's avatar
Robbert Krebbers committed
311
Proof. by rewrite /IntoPersistent. Qed.
312
313
Global Instance into_persistent_persistent P :
  Persistent P  IntoPersistent false P P | 100.
314
Proof. intros. by rewrite /IntoPersistent. Qed.
315

316
(** FromModal *)
317
Global Instance from_modal_affinely P :
318
  FromModal modality_affinely (<affine> P) (<affine> P) P | 2.
319
320
321
Proof. by rewrite /FromModal. Qed.

Global Instance from_modal_persistently P :
322
  FromModal modality_persistently (<pers> P) (<pers> P) P | 2.
323
Proof. by rewrite /FromModal. Qed.
324
325
Global Instance from_modal_intuitionistically P :
  FromModal modality_intuitionistically ( P) ( P) P | 1.
326
Proof. by rewrite /FromModal. Qed.
327
Global Instance from_modal_intuitionistically_affine_bi P :
328
  BiAffine PROP  FromModal modality_persistently ( P) ( P) P | 0.
Ralf Jung's avatar
Ralf Jung committed
329
330
331
Proof.
  intros. by rewrite /FromModal /= intuitionistically_into_persistently.
Qed.
332

333
Global Instance from_modal_absorbingly P :
334
  FromModal modality_id (<absorb> P) (<absorb> P) P.
335
336
Proof. by rewrite /FromModal /= -absorbingly_intro. Qed.

337
(** IntoWand *)
338
339
340
341
342
343
344
345
346
347
Global Instance into_wand_wand' p q (P Q P' Q' : PROP) :
  IntoWand' p q (P - Q) P' Q'  IntoWand p q (P - Q) P' Q' | 100.
Proof. done. Qed.
Global Instance into_wand_impl' p q (P Q P' Q' : PROP) :
  IntoWand' p q (P  Q) P' Q'  IntoWand p q (P  Q) P' Q' | 100.
Proof. done. Qed.
Global Instance into_wand_wandM' p q mP (Q P' Q' : PROP) :
  IntoWand' p q (mP -? Q) P' Q'  IntoWand p q (mP -? Q) P' Q' | 100.
Proof. done. Qed.

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

382
Global Instance into_wand_wandM p q mP' P Q :
383
  FromAssumption q P (default emp%I mP')  IntoWand p q (mP' -? Q) P Q.
384
385
Proof. rewrite /IntoWand wandM_sound. exact: into_wand_wand. Qed.

Robbert Krebbers's avatar
Robbert Krebbers committed
386
387
388
389
390
391
392
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.

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

Robbert Krebbers's avatar
Robbert Krebbers committed
407
408
409
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.
410
Global Instance into_wand_tforall {TT : tele} p q (Φ : TT  PROP) P Q x :
411
412
413
  IntoWand p q (Φ x) P Q  IntoWand p q (.. x, Φ x) P Q.
Proof. rewrite /IntoWand=> <-. by rewrite bi_tforall_forall (forall_elim x). Qed.

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
Global Instance into_wand_affine p q R P Q :
  IntoWand p q R P Q  IntoWand p q (<affine> R) (<affine> P) (<affine> Q).
Proof.
  rewrite /IntoWand /= => HR. apply wand_intro_r. destruct p; simpl in *.
  - rewrite (affinely_elim R) -(affine_affinely ( R)%I) HR. destruct q; simpl in *.
    + rewrite (affinely_elim P) -{2}(affine_affinely ( P)%I).
      by rewrite affinely_sep_2 wand_elim_l.
    + by rewrite affinely_sep_2 wand_elim_l.
  - rewrite HR. destruct q; simpl in *.
    + rewrite (affinely_elim P) -{2}(affine_affinely ( P)%I).
      by rewrite affinely_sep_2 wand_elim_l.
    + by rewrite affinely_sep_2 wand_elim_l.
Qed.
(* In case the argument is affine, but the wand resides in the spatial context,
we can only eliminate the affine modality in the argument. This would lead to
the following instance:

  IntoWand false q R P Q → IntoWand' false q R (<affine> P) Q.

This instance is redundant, however, since the elimination of the affine
modality is already covered by the [IntoAssumption] instances that are used at
the leaves of the instance search for [IntoWand]. *)
Global Instance into_wand_affine_args q R P Q :
  IntoWand true q R P Q  IntoWand' true q R (<affine> P) (<affine> Q).
Proof.
  rewrite /IntoWand' /IntoWand /= => HR. apply wand_intro_r.
  rewrite -(affine_affinely ( R)%I) HR. destruct q; simpl.
  - rewrite (affinely_elim P) -{2}(affine_affinely ( P)%I).
    by rewrite affinely_sep_2 wand_elim_l.
  - by rewrite affinely_sep_2 wand_elim_l.
Qed.

446
Global Instance into_wand_intuitionistically p q R P Q :
447
448
  IntoWand true q R P Q  IntoWand p q ( R) P Q.
Proof. rewrite /IntoWand /= => ->. by rewrite {1}intuitionistically_if_elim. Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
449
Global Instance into_wand_persistently_true q R P Q :
450
  IntoWand true q R P Q  IntoWand true q (<pers> R) P Q.
Ralf Jung's avatar
Ralf Jung committed
451
Proof. by rewrite /IntoWand /= intuitionistically_persistently_elim. Qed.
452
453
454
Global Instance into_wand_persistently_false q R P Q :
  Absorbing R  IntoWand false q R P Q  IntoWand false q (<pers> R) P Q.
Proof. intros ?. by rewrite /IntoWand persistently_elim. Qed.
455

456
(** FromWand *)
457
458
Global Instance from_wand_wand P1 P2 : FromWand (P1 - P2) P1 P2.
Proof. by rewrite /FromWand. Qed.
459
Global Instance from_wand_wandM mP1 P2 :
460
  FromWand (mP1 -? P2) (default emp mP1)%I P2.
461
Proof. by rewrite /FromWand wandM_sound. Qed.
462

463
(** FromImpl *)
464
465
466
Global Instance from_impl_impl P1 P2 : FromImpl (P1  P2) P1 P2.
Proof. by rewrite /FromImpl. Qed.

467
(** FromAnd *)
Robbert Krebbers's avatar
Robbert Krebbers committed
468
469
470
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 :
471
  Persistent P1  IntoAbsorbingly P1' P1  FromAnd (P1  P2) P1' P2 | 9.
472
Proof.
473
474
475
  rewrite /IntoAbsorbingly /FromAnd=> ? ->.
  rewrite persistent_and_affinely_sep_l_1 {1}(persistent_persistently_2 P1).
  by rewrite absorbingly_elim_persistently -{2}(intuitionistically_elim P1).
476
Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
477
Global Instance from_and_sep_persistent_r P1 P2 P2' :
478
  Persistent P2  IntoAbsorbingly P2' P2  FromAnd (P1  P2) P1 P2' | 10.
479
Proof.
480
481
482
  rewrite /IntoAbsorbingly /FromAnd=> ? ->.
  rewrite persistent_and_affinely_sep_r_1 {1}(persistent_persistently_2 P2).
  by rewrite absorbingly_elim_persistently -{2}(intuitionistically_elim P2).
483
484
Qed.

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

Robbert Krebbers's avatar
Robbert Krebbers committed
488
Global Instance from_and_persistently P Q1 Q2 :
489
  FromAnd P Q1 Q2 
490
  FromAnd (<pers> P) (<pers> Q1) (<pers> Q2).
Robbert Krebbers's avatar
Robbert Krebbers committed
491
492
Proof. rewrite /FromAnd=> <-. by rewrite persistently_and. Qed.
Global Instance from_and_persistently_sep P Q1 Q2 :
493
  FromSep P Q1 Q2 
494
  FromAnd (<pers> P) (<pers> Q1) (<pers> Q2) | 11.
Robbert Krebbers's avatar
Robbert Krebbers committed
495
Proof. rewrite /FromAnd=> <-. by rewrite -persistently_and persistently_and_sep. Qed.
496

497
498
Global Instance from_and_big_sepL_cons_persistent {A} (Φ : nat  A  PROP) l x l' :
  IsCons l x l' 
Robbert Krebbers's avatar
Robbert Krebbers committed
499
  Persistent (Φ 0 x) 
500
501
502
503
  FromAnd ([ list] k  y  l, Φ k y) (Φ 0 x) ([ list] k  y  l', Φ (S k) y).
Proof. rewrite /IsCons=> -> ?. by rewrite /FromAnd big_sepL_cons persistent_and_sep_1. Qed.
Global Instance from_and_big_sepL_app_persistent {A} (Φ : nat  A  PROP) l l1 l2 :
  IsApp l l1 l2 
Robbert Krebbers's avatar
Robbert Krebbers committed
504
  ( k y, Persistent (Φ k y)) 
505
  FromAnd ([ list] k  y  l, Φ k y)
Robbert Krebbers's avatar
Robbert Krebbers committed
506
    ([ list] k  y  l1, Φ k y) ([ list] k  y  l2, Φ (length l1 + k) y).
507
Proof. rewrite /IsApp=> -> ?. by rewrite /FromAnd big_sepL_app persistent_and_sep_1. Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
508

509
510
511
512
513
514
515
516
517
518
519
520
521
522
523
524
525
526
527
528
529
530
Global Instance from_and_big_sepL2_cons_persistent {A B}
    (Φ : nat  A  B  PROP) l1 x1 l1' l2 x2 l2' :
  IsCons l1 x1 l1'  IsCons l2 x2 l2' 
  Persistent (Φ 0 x1 x2) 
  FromAnd ([ list] k  y1;y2  l1;l2, Φ k y1 y2)
    (Φ 0 x1 x2) ([ list] k  y1;y2  l1';l2', Φ (S k) y1 y2).
Proof.
  rewrite /IsCons=> -> -> ?.
  by rewrite /FromAnd big_sepL2_cons persistent_and_sep_1.
Qed.
Global Instance from_and_big_sepL2_app_persistent {A B}
    (Φ : nat  A  B  PROP) l1 l1' l1'' l2 l2' l2'' :
  IsApp l1 l1' l1''  IsApp l2 l2' l2'' 
  ( k y1 y2, Persistent (Φ k y1 y2)) 
  FromAnd ([ list] k  y1;y2  l1;l2, Φ k y1 y2)
    ([ list] k  y1;y2  l1';l2', Φ k y1 y2)
    ([ list] k  y1;y2  l1'';l2'', Φ (length l1' + k) y1 y2).
Proof.
  rewrite /IsApp=> -> -> ?. rewrite /FromAnd persistent_and_sep_1.
  apply wand_elim_l', big_sepL2_app.
Qed.

531
532
Global Instance from_and_big_sepMS_disj_union_persistent
    `{Countable A} (Φ : A  PROP) X1 X2 :
533
  ( y, Persistent (Φ y)) 
534
535
  FromAnd ([ mset] y  X1  X2, Φ y) ([ mset] y  X1, Φ y) ([ mset] y  X2, Φ y).
Proof. intros. by rewrite /FromAnd big_sepMS_disj_union persistent_and_sep_1. Qed.
536

537
(** FromSep *)
Robbert Krebbers's avatar
Robbert Krebbers committed
538
539
540
Global Instance from_sep_sep P1 P2 : FromSep (P1  P2) P1 P2 | 100.
Proof. by rewrite /FromSep. Qed.
Global Instance from_sep_and P1 P2 :
Ralf Jung's avatar
Ralf Jung committed
541
  TCOr (Affine P1) (Absorbing P2)  TCOr (Absorbing P1) (Affine P2) 
Robbert Krebbers's avatar
Robbert Krebbers committed
542
543
544
545
546
547
  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.

548
Global Instance from_sep_affinely P Q1 Q2 :
549
  FromSep P Q1 Q2  FromSep (<affine> P) (<affine> Q1) (<affine> Q2).
550
Proof. rewrite /FromSep=> <-. by rewrite affinely_sep_2. Qed.
551
552
553
Global Instance from_sep_intuitionistically P Q1 Q2 :
  FromSep P Q1 Q2  FromSep ( P) ( Q1) ( Q2).
Proof. rewrite /FromSep=> <-. by rewrite intuitionistically_sep_2. Qed.
554
Global Instance from_sep_absorbingly P Q1 Q2 :
555
  FromSep P Q1 Q2  FromSep (<absorb> P) (<absorb> Q1) (<absorb> Q2).
556
Proof. rewrite /FromSep=> <-. by rewrite absorbingly_sep. Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
557
Global Instance from_sep_persistently P Q1 Q2 :
558
  FromSep P Q1 Q2 
559
  FromSep (<pers> P) (<pers> Q1) (<pers> Q2).
560
Proof. rewrite /FromSep=> <-. by rewrite persistently_sep_2. Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
561

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

572
573
574
575
576
577
578
579
580
581
582
583
584
585
Global Instance from_sep_big_sepL2_cons {A B} (Φ : nat  A  B  PROP)
    l1 x1 l1' l2 x2 l2' :
  IsCons l1 x1 l1'  IsCons l2 x2 l2' 
  FromSep ([ list] k  y1;y2  l1;l2, Φ k y1 y2)
    (Φ 0 x1 x2) ([ list] k  y1;y2  l1';l2', Φ (S k) y1 y2).
Proof. rewrite /IsCons=> -> ->. by rewrite /FromSep big_sepL2_cons. Qed.
Global Instance from_sep_big_sepL2_app {A B} (Φ : nat  A  B  PROP)
    l1 l1' l1'' l2 l2' l2'' :
  IsApp l1 l1' l1''  IsApp l2 l2' l2'' 
  FromSep ([ list] k  y1;y2  l1;l2, Φ k y1 y2)
    ([ list] k  y1;y2  l1';l2', Φ k y1 y2)
    ([ list] k  y1;y2  l1'';l2'', Φ (length l1' + k) y1 y2).
Proof. rewrite /IsApp=>-> ->. apply wand_elim_l', big_sepL2_app. Qed.

586
587
588
Global Instance from_sep_big_sepMS_disj_union `{Countable A} (Φ : A  PROP) X1 X2 :
  FromSep ([ mset] y  X1  X2, Φ y) ([ mset] y  X1, Φ y) ([ mset] y  X2, Φ y).
Proof. by rewrite /FromSep big_sepMS_disj_union. Qed.
589

590
(** IntoAnd *)
591
Global Instance into_and_and p P Q : IntoAnd p (P  Q) P Q | 10.
592
Proof. by rewrite /IntoAnd intuitionistically_if_and. Qed.
593
Global Instance into_and_and_affine_l P Q Q' :
594
  Affine P  FromAffinely Q' Q  IntoAnd false (P  Q) P Q'.
595
596
Proof.
  intros. rewrite /IntoAnd /=.
597
  by rewrite -(affine_affinely P) affinely_and_l affinely_and (from_affinely Q').
598
599
Qed.
Global Instance into_and_and_affine_r P P' Q :
600
  Affine Q  FromAffinely P' P  IntoAnd false (P  Q) P' Q.
601
602
Proof.
  intros. rewrite /IntoAnd /=.
603
  by rewrite -(affine_affinely Q) affinely_and_r affinely_and (from_affinely P').
604
605
Qed.

606
Global Instance into_and_sep `{BiPositive PROP} P Q : IntoAnd true (P  Q) P Q.
607
Proof.
608
609
  rewrite /IntoAnd /= intuitionistically_sep
    -and_sep_intuitionistically intuitionistically_and //.
610
Qed.
611
Global Instance into_and_sep_affine p P Q :
Ralf Jung's avatar
Ralf Jung committed
612
  TCOr (Affine P) (Absorbing Q)  TCOr (Absorbing P) (Affine Q) 
613
  IntoAnd p (P  Q) P Q.
614
Proof. intros. by rewrite /IntoAnd /= sep_and. Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
615
616

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

619
Global Instance into_and_affinely p P Q1 Q2 :
620
  IntoAnd p P Q1 Q2  IntoAnd p (<affine> P) (<affine> Q1) (<affine> Q2).
Robbert Krebbers's avatar
Robbert Krebbers committed
621
Proof.
Robbert Krebbers's avatar
Robbert Krebbers committed
622
  rewrite /IntoAnd. destruct p; simpl.
Ralf Jung's avatar
Ralf Jung committed
623
  - rewrite -affinely_and !intuitionistically_affinely_elim //.
624
  - intros ->. by rewrite affinely_and.
Robbert Krebbers's avatar
Robbert Krebbers committed
625
Qed.
626
627
628
629
630
631
632
Global Instance into_and_intuitionistically p P Q1 Q2 :
  IntoAnd p P Q1 Q2  IntoAnd p ( P) ( Q1) ( Q2).
Proof.
  rewrite /IntoAnd. destruct p; simpl.
  - rewrite -intuitionistically_and !intuitionistically_idemp //.
  - intros ->. by rewrite intuitionistically_and.
Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
633
Global Instance into_and_persistently p P Q1 Q2 :
634
  IntoAnd p P Q1 Q2 
635
  IntoAnd p (<pers> P) (<pers> Q1) (<pers> Q2).
Robbert Krebbers's avatar
Robbert Krebbers committed
636
Proof.
Robbert Krebbers's avatar
Robbert Krebbers committed
637
  rewrite /IntoAnd /=. destruct p; simpl.
Ralf Jung's avatar
Ralf Jung committed
638
  - rewrite -persistently_and !intuitionistically_persistently_elim //.
Robbert Krebbers's avatar
Robbert Krebbers committed
639
  - intros ->. by rewrite persistently_and.
Robbert Krebbers's avatar
Robbert Krebbers committed
640
641
Qed.

642
(** IntoSep *)
643
644
Global Instance into_sep_sep P Q : IntoSep (P  Q) P Q.
Proof. by rewrite /IntoSep. Qed.
645

646
Inductive AndIntoSep : PROP  PROP  PROP  PROP  Prop :=
647
  | and_into_sep_affine P Q Q' : Affine P  FromAffinely Q' Q  AndIntoSep P P Q Q'
648
  | and_into_sep P Q : AndIntoSep P (<affine> P)%I Q Q.
649
650
651
652
653
654
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'.
655
Proof.
656
  destruct 2 as [P Q Q'|P Q]; rewrite /IntoSep.
657
  - rewrite -(from_affinely Q' Q) -(affine_affinely P) affinely_and_lr.
658
659
    by rewrite persistent_and_affinely_sep_l_1.
  - by rewrite persistent_and_affinely_sep_l_1.
660
Qed.
661
662
Global Instance into_sep_and_persistent_r P P' Q Q' :
  Persistent Q  AndIntoSep Q Q' P P'  IntoSep (P  Q) P' Q'.
663
Proof.
664
  destruct 2 as [Q P P'|Q P]; rewrite /IntoSep.
665
  - rewrite -(from_affinely P' P) -(affine_affinely Q) -affinely_and_lr.
666
667
    by rewrite persistent_and_affinely_sep_r_1.
  - by rewrite persistent_and_affinely_sep_r_1.
668
Qed.
669

670
671
672
Global Instance into_sep_pure φ ψ : @IntoSep PROP ⌜φ  ψ⌝ ⌜φ⌝ ⌜ψ⌝.
Proof. by rewrite /IntoSep pure_and persistent_and_sep_1. Qed.

673
Global Instance into_sep_affinely `{BiPositive PROP} P Q1 Q2 :
674
  IntoSep P Q1 Q2  IntoSep (<affine> P) (<affine> Q1) (<affine> Q2) | 0.
675
Proof. rewrite /IntoSep /= => ->. by rewrite affinely_sep. Qed.
676
677
678
Global Instance into_sep_intuitionistically `{BiPositive PROP} P Q1 Q2 :
  IntoSep P Q1 Q2  IntoSep ( P) ( Q1) ( Q2) | 0.
Proof. rewrite /IntoSep /= => ->. by rewrite intuitionistically_sep. Qed.
679
680
681
682
(* FIXME: This instance is kind of strange, it just gets rid of the bi_affinely.
Also, it overlaps with `into_sep_affinely_later`, and hence has lower
precedence. *)
Global Instance into_sep_affinely_trim P Q1 Q2 :
683
  IntoSep P Q1 Q2  IntoSep (<affine> P) Q1 Q2 | 20.
684
Proof. rewrite /IntoSep /= => ->. by rewrite affinely_elim. Qed.
685

686
Global Instance into_sep_persistently `{BiPositive PROP} P Q1 Q2 :
687
  IntoSep P Q1 Q2 
688
  IntoSep (<pers> P) (<pers> Q1) (<pers> Q2).
689
Proof. rewrite /IntoSep /= => ->. by rewrite persistently_sep. Qed.
690
691