class_instances.v 50 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 *)
Ralf Jung's avatar
Ralf Jung committed
9
(** The lemma [from_assumption_exact] is not an instance, but defined using
10
11
12
13
14
[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
Global Instance into_absorbingly_True : @IntoAbsorbingly PROP True emp | 0.
67
Proof. by rewrite /IntoAbsorbingly -absorbingly_emp_True. Qed.
68
69
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
  rewrite /FromPure /IntoPure=> <- -> /=. rewrite pure_impl.
  apply impl_intro_l, pure_elim_l=> ?. rewrite (pure_True φ1) //.
187
  by rewrite -affinely_affinely_if affinely_True_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

Ralf Jung's avatar
Ralf Jung committed
201
202
203
204
205
206
207
208
Global Instance into_pure_big_sepL {A}
    (Φ : nat  A  PROP) (φ : nat  A  Prop) (l : list A) :
  ( k x, IntoPure (Φ k x) (φ k x)) 
  IntoPure ([ list] kx  l, Φ k x) ( k x, l !! k = Some x  φ k x).
Proof.
  rewrite /IntoPure. intros HΦ.
  setoid_rewrite HΦ. rewrite big_sepL_pure_1. done.
Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
209
210
211
212
Global Instance into_pure_big_sepM `{Countable K} {A}
    (Φ : K  A  PROP) (φ : K  A  Prop) (m : gmap K A) :
  ( k x, IntoPure (Φ k x) (φ k x)) 
  IntoPure ([ map] kx  m, Φ k x) (map_Forall φ m).
Ralf Jung's avatar
Ralf Jung committed
213
214
215
216
Proof.
  rewrite /IntoPure. intros HΦ.
  setoid_rewrite HΦ. rewrite big_sepM_pure_1. done.
Qed.
Ralf Jung's avatar
Ralf Jung committed
217
218
219
220
221
222
223
224
225
226
227
228
229
230
231
232
Global Instance into_pure_big_sepS `{Countable A}
    (Φ : A  PROP) (φ : A  Prop) (X : gset A) :
  ( x, IntoPure (Φ x) (φ x)) 
  IntoPure ([ set] x  X, Φ x) (set_Forall φ X).
Proof.
  rewrite /IntoPure. intros HΦ.
  setoid_rewrite HΦ. rewrite big_sepS_pure_1. done.
Qed.
Global Instance into_pure_big_sepMS `{Countable A}
    (Φ : A  PROP) (φ : A  Prop) (X : gmultiset A) :
  ( x, IntoPure (Φ x) (φ x)) 
  IntoPure ([ mset] x  X, Φ x) ( y : A, y  X  φ y).
Proof.
  rewrite /IntoPure. intros HΦ.
  setoid_rewrite HΦ. rewrite big_sepMS_pure_1. done.
Qed.
Ralf Jung's avatar
Ralf Jung committed
233

234
(** FromPure *)
235
236
237
238
239
240
241
242
243
244
245
246
247
248
249
250
251
252
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.
253
254
255
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.
256
  rewrite /FromPure /IntoPure pure_impl_1=> -> <-. destruct a=>//=.
257
258
259
260
261
262
263
264
265
  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.
266
267
268
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.
269
270
271
Global Instance from_pure_forall {A} a (Φ : A  PROP) (φ : A  Prop) :
  ( x, FromPure a (Φ x) (φ x))  FromPure a ( x, Φ x) ( x, φ x).
Proof.
272
  rewrite /FromPure=>Hx. rewrite pure_forall_1. setoid_rewrite <-Hx.
273
274
  destruct a=>//=. apply affinely_forall.
Qed.
275
276
277
278
279
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.
280

281
282
283
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).
284
Proof.
285
286
287
  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.
288
Qed.
289
290
291
292
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).
293
Proof.
294
295
296
297
  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.
298
299
    by rewrite affinely_and_l pure_impl_1 impl_elim_r.
  - by rewrite HP1 sep_and pure_impl_1 impl_elim_r.
300
301
Qed.

302
Global Instance from_pure_persistently P a φ :
303
  FromPure true P φ  FromPure a (<pers> P) φ.
304
305
Proof.
  rewrite /FromPure=> <- /=.
Ralf Jung's avatar
Ralf Jung committed
306
  by rewrite persistently_affinely_elim affinely_if_elim persistently_pure.
307
Qed.
308
309
310
311
312
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) φ.
313
Proof.
314
315
316
  rewrite /FromPure=><- /=.
  rewrite -intuitionistically_affinely_elim -affinely_affinely_if affinely_idemp.
  by rewrite intuitionistic_intuitionistically.
317
Qed.
318
319
Global Instance from_pure_absorbingly a P φ :
  FromPure a P φ  FromPure false (<absorb> P) φ.
320
Proof.
321
322
  rewrite /FromPure=> <- /=. rewrite -affinely_affinely_if.
  by rewrite -persistent_absorbingly_affinely_2.
323
Qed.
324

Ralf Jung's avatar
Ralf Jung committed
325
326
327
328
329
330
331
332
333
334
335
336
Global Instance from_pure_big_sepL {A}
    a (Φ : nat  A  PROP) (φ : nat  A  Prop) (l : list A) :
  ( k x, FromPure a (Φ k x) (φ k x)) 
  TCOr (TCEq a true) (BiAffine PROP) 
  FromPure a ([ list] kx  l, Φ k x) ( k x, l !! k = Some x  φ k x).
Proof.
  rewrite /FromPure. destruct a; simpl; intros HΦ Haffine.
  - rewrite big_sepL_affinely_pure_2.
    setoid_rewrite HΦ. done.
  - destruct Haffine as [[=]%TCEq_eq|?].
    rewrite -big_sepL_pure. setoid_rewrite HΦ. done.
Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
337
338
339
Global Instance from_pure_big_sepM `{Countable K} {A}
    a (Φ : K  A  PROP) (φ : K  A  Prop) (m : gmap K A) :
  ( k x, FromPure a (Φ k x) (φ k x)) 
Ralf Jung's avatar
Ralf Jung committed
340
341
342
343
344
345
  TCOr (TCEq a true) (BiAffine PROP) 
  FromPure a ([ map] kx  m, Φ k x) (map_Forall φ m).
Proof.
  rewrite /FromPure. destruct a; simpl; intros HΦ Haffine.
  - rewrite big_sepM_affinely_pure_2.
    setoid_rewrite HΦ. done.
Robbert Krebbers's avatar
Robbert Krebbers committed
346
347
  - destruct Haffine as [[=]%TCEq_eq|?].
    rewrite -big_sepM_pure. setoid_rewrite HΦ. done.
Ralf Jung's avatar
Ralf Jung committed
348
Qed.
Ralf Jung's avatar
Ralf Jung committed
349
350
351
352
353
354
355
356
357
358
359
360
361
362
363
364
365
366
367
368
369
370
371
372
Global Instance from_pure_big_sepS `{Countable A}
    a (Φ : A  PROP) (φ : A  Prop) (X : gset A) :
  ( x, FromPure a (Φ x) (φ x)) 
  TCOr (TCEq a true) (BiAffine PROP) 
  FromPure a ([ set] x  X, Φ x) (set_Forall φ X).
Proof.
  rewrite /FromPure. destruct a; simpl; intros HΦ Haffine.
  - rewrite big_sepS_affinely_pure_2.
    setoid_rewrite HΦ. done.
  - destruct Haffine as [[=]%TCEq_eq|?].
    rewrite -big_sepS_pure. setoid_rewrite HΦ. done.
Qed.
Global Instance from_pure_big_sepMS `{Countable A}
    a (Φ : A  PROP) (φ : A  Prop) (X : gmultiset A) :
  ( x, FromPure a (Φ x) (φ x)) 
  TCOr (TCEq a true) (BiAffine PROP) 
  FromPure a ([ mset] x  X, Φ x) ( y : A, y  X  φ y).
Proof.
  rewrite /FromPure. destruct a; simpl; intros HΦ Haffine.
  - rewrite big_sepMS_affinely_pure_2.
    setoid_rewrite HΦ. done.
  - destruct Haffine as [[=]%TCEq_eq|?].
    rewrite -big_sepMS_pure. setoid_rewrite HΦ. done.
Qed.
Ralf Jung's avatar
Ralf Jung committed
373

374
(** IntoPersistent *)
375
Global Instance into_persistent_persistently p P Q :
376
  IntoPersistent true P Q  IntoPersistent p (<pers> P) Q | 0.
Robbert Krebbers's avatar
Robbert Krebbers committed
377
378
379
380
Proof.
  rewrite /IntoPersistent /= => ->.
  destruct p; simpl; auto using persistently_idemp_1.
Qed.
381
Global Instance into_persistent_affinely p P Q :
382
  IntoPersistent p P Q  IntoPersistent p (<affine> P) Q | 0.
383
Proof. rewrite /IntoPersistent /= => <-. by rewrite affinely_elim. Qed.
384
Global Instance into_persistent_intuitionistically p P Q :
385
386
387
388
389
  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
390
    intuitionistically_into_persistently_1.
391
Qed.
392
Global Instance into_persistent_here P : IntoPersistent true P P | 1.
Robbert Krebbers's avatar
Robbert Krebbers committed
393
Proof. by rewrite /IntoPersistent. Qed.
394
395
Global Instance into_persistent_persistent P :
  Persistent P  IntoPersistent false P P | 100.
396
Proof. intros. by rewrite /IntoPersistent. Qed.
397

398
(** FromModal *)
399
Global Instance from_modal_affinely P :
Ralf Jung's avatar
Ralf Jung committed
400
  FromModal True modality_affinely (<affine> P) (<affine> P) P | 2.
401
402
403
Proof. by rewrite /FromModal. Qed.

Global Instance from_modal_persistently P :
Ralf Jung's avatar
Ralf Jung committed
404
  FromModal True modality_persistently (<pers> P) (<pers> P) P | 2.
405
Proof. by rewrite /FromModal. Qed.
406
Global Instance from_modal_intuitionistically P :
Ralf Jung's avatar
Ralf Jung committed
407
  FromModal True modality_intuitionistically ( P) ( P) P | 1.
408
Proof. by rewrite /FromModal. Qed.
409
Global Instance from_modal_intuitionistically_affine_bi P :
Ralf Jung's avatar
Ralf Jung committed
410
  BiAffine PROP  FromModal True modality_persistently ( P) ( P) P | 0.
Ralf Jung's avatar
Ralf Jung committed
411
412
413
Proof.
  intros. by rewrite /FromModal /= intuitionistically_into_persistently.
Qed.
414

415
Global Instance from_modal_absorbingly P :
Ralf Jung's avatar
Ralf Jung committed
416
  FromModal True modality_id (<absorb> P) (<absorb> P) P.
417
418
Proof. by rewrite /FromModal /= -absorbingly_intro. Qed.

419
(** IntoWand *)
420
421
422
423
424
425
426
427
428
429
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
430
431
Global Instance into_wand_wand p q P Q P' :
  FromAssumption q P P'  IntoWand p q (P' - Q) P Q.
432
Proof.
433
  rewrite /FromAssumption /IntoWand=> HP. by rewrite HP intuitionistically_if_elim.
Robbert Krebbers's avatar
Robbert Krebbers committed
434
Qed.
435
436
437
438
439
440
441
442
(** Implication instances
  Generally we assume [P → ...] is written in cases where that would be
  equivalent to [<affine> P -∗ ...], i.e., [P] is absorbing and persistent. The
  workhorse of the [IntoWand false] instances (i.e., the implication being taken
  from the spatial context) is [persistent_impl_wand_affinely].
  If the premise does not come from the intuitionistic context (second parameter [false]),
  we add an affinely modality, as if the user had written the magic wand form. *)
(** To make sure this always applies for affine BIs, we also allow [BiAffine] here. *)
443
Global Instance into_wand_impl_false_false P Q P' :
444
445
446
447
448
449
450
451
452
453
454
  Absorbing P' 
  TCOr (Persistent P') (BiAffine PROP) 
  (* FIXME: use FromAssumption instead of MakeAffinely?
  But then needless <affine> modalities get added. *)
  MakeAffinely P' P 
  IntoWand false false (P'  Q) P Q.
Proof.
  rewrite /MakeAffinely /IntoWand /= => ? Hpers <-. apply wand_intro_l.
  destruct Hpers.
  - rewrite persistent_impl_wand_affinely wand_elim_r //.
  - rewrite impl_wand_1 affinely_elim wand_elim_r //.
Robbert Krebbers's avatar
Robbert Krebbers committed
455
456
Qed.
Global Instance into_wand_impl_false_true P Q P' :
457
458
  Absorbing P' 
  FromAssumption true P P' 
Robbert Krebbers's avatar
Robbert Krebbers committed
459
  IntoWand false true (P'  Q) P Q.
460
Proof.
461
  rewrite /IntoWand /FromAssumption /= => ? HP. apply wand_intro_l.
462
463
  rewrite -(persistently_elim P').
  rewrite persistent_impl_wand_affinely.
464
  rewrite -(intuitionistically_idemp P) HP.
465
  apply wand_elim_r.
466
Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
467
Global Instance into_wand_impl_true_false P Q P' :
468
469
470
  (* FIXME: use FromAssumption instead of MakeAffinely?
  But then needless <affine> modalities get added. *)
  MakeAffinely P' P 
Robbert Krebbers's avatar
Robbert Krebbers committed
471
  IntoWand true false (P'  Q) P Q.
472
Proof.
473
474
  rewrite /MakeAffinely /IntoWand /= => <-. apply wand_intro_r.
  rewrite sep_and intuitionistically_elim affinely_elim impl_elim_l //.
475
Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
476
Global Instance into_wand_impl_true_true P Q P' :
477
478
  FromAssumption true P P' 
  IntoWand true true (P'  Q) P Q.
479
Proof.
Robbert Krebbers's avatar
Robbert Krebbers committed
480
  rewrite /FromAssumption /IntoWand /= => <-. apply wand_intro_l.
481
  rewrite sep_and [( (_  _))%I]intuitionistically_elim impl_elim_r //.
482
Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
483

484
Global Instance into_wand_wandM p q mP' P Q :
485
  FromAssumption q P (default emp%I mP')  IntoWand p q (mP' -? Q) P Q.
486
487
Proof. rewrite /IntoWand wandM_sound. exact: into_wand_wand. Qed.

Robbert Krebbers's avatar
Robbert Krebbers committed
488
489
490
491
492
493
494
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.

495
496
497
Global Instance into_wand_forall_prop_true p (φ : Prop) P :
  IntoWand p true ( _ : φ, P)  φ  P.
Proof.
498
499
  rewrite /IntoWand (intuitionistically_if_elim p) /=
          -impl_wand_intuitionistically -pure_impl_forall
500
501
502
503
504
505
          bi.persistently_elim //.
Qed.
Global Instance into_wand_forall_prop_false p (φ : Prop) P :
  Absorbing P  IntoWand p false ( _ : φ, P)  φ  P.
Proof.
  intros ?.
506
  rewrite /IntoWand (intuitionistically_if_elim p) /= pure_wand_forall //.
507
Qed.
508

Robbert Krebbers's avatar
Robbert Krebbers committed
509
510
511
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.
512
Global Instance into_wand_tforall {TT : tele} p q (Φ : TT  PROP) P Q x :
513
514
515
  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.

516
517
518
519
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 *.
520
521
  - rewrite (affinely_elim R) -(affine_affinely ( R)) HR. destruct q; simpl in *.
    + rewrite (affinely_elim P) -{2}(affine_affinely ( P)).
522
523
524
      by rewrite affinely_sep_2 wand_elim_l.
    + by rewrite affinely_sep_2 wand_elim_l.
  - rewrite HR. destruct q; simpl in *.
525
    + rewrite (affinely_elim P) -{2}(affine_affinely ( P)).
526
527
528
529
530
531
532
533
534
535
536
537
538
539
540
541
      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.
542
543
  rewrite -(affine_affinely ( R)) HR. destruct q; simpl.
  - rewrite (affinely_elim P) -{2}(affine_affinely ( P)).
544
545
546
547
    by rewrite affinely_sep_2 wand_elim_l.
  - by rewrite affinely_sep_2 wand_elim_l.
Qed.

548
Global Instance into_wand_intuitionistically p q R P Q :
549
550
  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
551
Global Instance into_wand_persistently_true q R P Q :
552
  IntoWand true q R P Q  IntoWand true q (<pers> R) P Q.
Ralf Jung's avatar
Ralf Jung committed
553
Proof. by rewrite /IntoWand /= intuitionistically_persistently_elim. Qed.
554
555
556
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.
557

558
(** FromWand *)
559
560
Global Instance from_wand_wand P1 P2 : FromWand (P1 - P2) P1 P2.
Proof. by rewrite /FromWand. Qed.
561
Global Instance from_wand_wandM mP1 P2 :
562
  FromWand (mP1 -? P2) (default emp mP1)%I P2.
563
Proof. by rewrite /FromWand wandM_sound. Qed.
564

565
(** FromImpl *)
566
567
568
Global Instance from_impl_impl P1 P2 : FromImpl (P1  P2) P1 P2.
Proof. by rewrite /FromImpl. Qed.

569
(** FromAnd *)
Robbert Krebbers's avatar
Robbert Krebbers committed
570
571
572
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 :
573
  Persistent P1  IntoAbsorbingly P1' P1  FromAnd (P1  P2) P1' P2 | 9.
574
Proof.
575
576
577
  rewrite /IntoAbsorbingly /FromAnd=> ? ->.
  rewrite persistent_and_affinely_sep_l_1 {1}(persistent_persistently_2 P1).
  by rewrite absorbingly_elim_persistently -{2}(intuitionistically_elim P1).
578
Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
579
Global Instance from_and_sep_persistent_r P1 P2 P2' :
580
  Persistent P2  IntoAbsorbingly P2' P2  FromAnd (P1  P2) P1 P2' | 10.
581
Proof.
582
583
584
  rewrite /IntoAbsorbingly /FromAnd=> ? ->.
  rewrite persistent_and_affinely_sep_r_1 {1}(persistent_persistently_2 P2).
  by rewrite absorbingly_elim_persistently -{2}(intuitionistically_elim P2).
585
586
Qed.

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

Robbert Krebbers's avatar
Robbert Krebbers committed
590
Global Instance from_and_persistently P Q1 Q2 :
591
  FromAnd P Q1 Q2 
592
  FromAnd (<pers> P) (<pers> Q1) (<pers> Q2).
Robbert Krebbers's avatar
Robbert Krebbers committed
593
594
Proof. rewrite /FromAnd=> <-. by rewrite persistently_and. Qed.
Global Instance from_and_persistently_sep P Q1 Q2 :
595
  FromSep P Q1 Q2 
596
  FromAnd (<pers> P) (<pers> Q1) (<pers> Q2) | 11.
Robbert Krebbers's avatar
Robbert Krebbers committed
597
Proof. rewrite /FromAnd=> <-. by rewrite -persistently_and persistently_and_sep. Qed.
598

599
600
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
601
  Persistent (Φ 0 x) 
602
603
604
605
  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
606
  ( k y, Persistent (Φ k y)) 
607
  FromAnd ([ list] k  y  l, Φ k y)
Robbert Krebbers's avatar
Robbert Krebbers committed
608
    ([ list] k  y  l1, Φ k y) ([ list] k  y  l2, Φ (length l1 + k) y).
609
Proof. rewrite /IsApp=> -> ?. by rewrite /FromAnd big_sepL_app persistent_and_sep_1. Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
610

611
612
613
614
615
616
617
618
619
620
621
622
623
624
625
626
627
628
629
630
631
632
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.

633
634
Global Instance from_and_big_sepMS_disj_union_persistent
    `{Countable A} (Φ : A  PROP) X1 X2 :
635
  ( y, Persistent (Φ y)) 
636
637
  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.
638

639
(** FromSep *)
Robbert Krebbers's avatar
Robbert Krebbers committed
640
641
642
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
643
  TCOr (Affine P1) (Absorbing P2)  TCOr (Absorbing P1) (Affine P2) 
Robbert Krebbers's avatar
Robbert Krebbers committed
644
645
646
647
648
649
  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.

650
Global Instance from_sep_affinely P Q1 Q2 :
651
  FromSep P Q1 Q2  FromSep (<affine> P) (<affine> Q1) (<affine> Q2).
652
Proof. rewrite /FromSep=> <-. by rewrite affinely_sep_2. Qed.
653
654
655
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.
656
Global Instance from_sep_absorbingly P Q1 Q2 :
657
  FromSep P Q1 Q2  FromSep (<absorb> P) (<absorb> Q1) (<absorb> Q2).
658
Proof. rewrite /FromSep=> <-. by rewrite absorbingly_sep. Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
659
Global Instance from_sep_persistently P Q1 Q2 :
660
  FromSep P Q1 Q2 
661
  FromSep (<pers> P) (<pers> Q1) (<pers> Q2).
662
Proof. rewrite /FromSep=> <-. by rewrite persistently_sep_2. Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
663

664
665
666
667
668
669
670
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
671
    ([ list] k  y  l1, Φ k y) ([ list] k  y  l2, Φ (length l1 + k) y).
672
Proof. rewrite /IsApp=> ->. by rewrite /FromSep big_opL_app. Qed.
673

674
675
676
677
678
679
680
681
682
683
684
685
686
687
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.

688
689
690
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.
691

692
(** IntoAnd *)
693
Global Instance into_and_and p P Q : IntoAnd p (P  Q) P Q | 10.
694
Proof. by rewrite /IntoAnd intuitionistically_if_and. Qed.
695
Global Instance into_and_and_affine_l P Q Q' :
696
  Affine P  FromAffinely Q' Q  IntoAnd false (P  Q) P Q'.
697
698
Proof.
  intros. rewrite /IntoAnd /=.
699
  by rewrite -(affine_affinely P) affinely_and_l affinely_and (from_affinely Q').
700
701
Qed.
Global Instance into_and_and_affine_r P P' Q :
702
  Affine Q  FromAffinely P' P  IntoAnd false (P  Q) P' Q.
703
704
Proof.
  intros. rewrite /IntoAnd /=.
705
  by rewrite -(affine_affinely Q) affinely_and_r affinely_and (from_affinely P').
706
707
Qed.

708
Global Instance into_and_sep `{BiPositive PROP} P Q : IntoAnd true (P  Q) P Q.
709
Proof.
710
711
  rewrite /IntoAnd /= intuitionistically_sep
    -and_sep_intuitionistically intuitionistically_and //.
712
Qed.
713
Global Instance into_and_sep_affine p P Q :
Ralf Jung's avatar
Ralf Jung committed
714
  TCOr (Affine P) (Absorbing Q)  TCOr (Absorbing P) (Affine Q) 
715
  IntoAnd p (P  Q) P Q.
716
Proof. intros. by rewrite /IntoAnd /= sep_and. Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
717
718

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

721
Global Instance into_and_affinely p P Q1 Q2 :
722
  IntoAnd p P Q1 Q2  IntoAnd p (<affine> P) (<affine> Q1) (<affine> Q2).
Robbert Krebbers's avatar
Robbert Krebbers committed
723
Proof.
Robbert Krebbers's avatar
Robbert Krebbers committed
724
  rewrite /IntoAnd. destruct p; simpl.
Ralf Jung's avatar
Ralf Jung committed
725
  - rewrite -affinely_and !intuitionistically_affinely_elim //.
726
  - intros ->. by rewrite affinely_and.
Robbert Krebbers's avatar
Robbert Krebbers committed
727
Qed.
728
729
730
731
732
733
734
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
735
Global Instance into_and_persistently p P Q1 Q2 :
736
  IntoAnd p P Q1 Q2 
737