class_instances_bi.v 50.6 KB
Newer Older
1
From stdpp Require Import nat_cancel.
2
From iris.bi Require Import bi tactics telescopes.
3
From iris.proofmode Require Import base modality_instances classes ltac_tactics.
4
Set Default Proof Using "Type".
Robbert Krebbers's avatar
Robbert Krebbers committed
5 6
Import bi.

7 8 9 10 11 12 13
(** The follow lemma is not an instance, but defined using a [Hint Extern] to
enable the better unification algorithm. *)
Lemma from_assumption_exact {PROP : bi} p (P : PROP) : FromAssumption p P P.
Proof. by rewrite /FromAssumption /= intuitionistically_if_elim. Qed.
Hint Extern 0 (FromAssumption _ _ _) =>
  notypeclasses refine (from_assumption_exact _ _) : typeclass_instances.

Robbert Krebbers's avatar
Robbert Krebbers committed
14 15 16
Section bi_instances.
Context {PROP : bi}.
Implicit Types P Q R : PROP.
17
Implicit Types mP : option PROP.
Robbert Krebbers's avatar
Robbert Krebbers committed
18

19
(** AsEmpValid *)
20
Global Instance as_emp_valid_emp_valid P : AsEmpValid0 (bi_emp_valid P) P | 0.
21
Proof. by rewrite /AsEmpValid. Qed.
22
Global Instance as_emp_valid_entails P Q : AsEmpValid0 (P  Q) (P - Q).
23
Proof. split. apply bi.entails_wand. apply bi.wand_entails. Qed.
24
Global Instance as_emp_valid_equiv P Q : AsEmpValid0 (P  Q) (P - Q).
25 26 27 28 29 30 31 32 33 34 35 36 37 38 39 40 41 42 43 44 45
Proof. split. apply bi.equiv_wand_iff. apply bi.wand_iff_equiv. Qed.

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.

(* We add a useless hypothesis [BiEmbed PROP PROP'] in order to make
   sure this instance is not used when there is no embedding between
   PROP and PROP'.
   The first [`{BiEmbed PROP PROP'}] is not considered as a premise by
   Coq TC search mechanism because the rest of the hypothesis is dependent
   on it. *)
Global Instance as_emp_valid_embed `{BiEmbed PROP PROP'} (φ : Prop) (P : PROP) :
  BiEmbed PROP PROP' 
  AsEmpValid0 φ P  AsEmpValid φ P.
Proof. rewrite /AsEmpValid0 /AsEmpValid=> _ ->. rewrite embed_emp_valid //. Qed.

46
(** FromAffinely *)
47 48
Global Instance from_affinely_affine P : Affine P  FromAffinely P P.
Proof. intros. by rewrite /FromAffinely affinely_elim. Qed.
49
Global Instance from_affinely_default P : FromAffinely (<affine> P) P | 100.
50
Proof. by rewrite /FromAffinely. Qed.
51 52 53
Global Instance from_affinely_intuitionistically P :
  FromAffinely ( P) (<pers> P) | 100.
Proof. by rewrite /FromAffinely. Qed.
54

55
(** IntoAbsorbingly *)
56 57 58 59
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.
60
Global Instance into_absorbingly_intuitionistically P :
61
  IntoAbsorbingly (<pers> P) ( P) | 2.
62 63 64
Proof.
  by rewrite /IntoAbsorbingly -absorbingly_intuitionistically_into_persistently.
Qed.
65
Global Instance into_absorbingly_default P : IntoAbsorbingly (<absorb> P) P | 100.
66
Proof. by rewrite /IntoAbsorbingly. Qed.
67

68
(** FromAssumption *)
69
Global Instance from_assumption_persistently_r P Q :
70
  FromAssumption true P Q  KnownRFromAssumption true P (<pers> Q).
Robbert Krebbers's avatar
Robbert Krebbers committed
71
Proof.
72
  rewrite /KnownRFromAssumption /FromAssumption /= =><-.
73
  apply intuitionistically_persistent.
Robbert Krebbers's avatar
Robbert Krebbers committed
74
Qed.
75
Global Instance from_assumption_affinely_r P Q :
76
  FromAssumption true P Q  KnownRFromAssumption true P (<affine> Q).
77 78 79 80
Proof.
  rewrite /KnownRFromAssumption /FromAssumption /= =><-.
  by rewrite affinely_idemp.
Qed.
81 82 83 84 85 86
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.
87
Global Instance from_assumption_absorbingly_r p P Q :
88
  FromAssumption p P Q  KnownRFromAssumption p P (<absorb> Q).
89 90 91 92
Proof.
  rewrite /KnownRFromAssumption /FromAssumption /= =><-.
  apply absorbingly_intro.
Qed.
93

94
Global Instance from_assumption_intuitionistically_l p P Q :
95 96 97
  FromAssumption true P Q  KnownLFromAssumption p ( P) Q.
Proof.
  rewrite /KnownLFromAssumption /FromAssumption /= =><-.
98
  by rewrite intuitionistically_if_elim.
99
Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
100
Global Instance from_assumption_persistently_l_true P Q :
101
  FromAssumption true P Q  KnownLFromAssumption true (<pers> P) Q.
102 103
Proof.
  rewrite /KnownLFromAssumption /FromAssumption /= =><-.
Ralf Jung's avatar
Ralf Jung committed
104
  rewrite intuitionistically_persistently_elim //.
105
Qed.
106
Global Instance from_assumption_persistently_l_false `{BiAffine PROP} P Q :
107
  FromAssumption true P Q  KnownLFromAssumption false (<pers> P) Q.
108 109
Proof.
  rewrite /KnownLFromAssumption /FromAssumption /= =><-.
Ralf Jung's avatar
Ralf Jung committed
110
  by rewrite intuitionistically_into_persistently.
111
Qed.
112
Global Instance from_assumption_affinely_l_true p P Q :
113
  FromAssumption p P Q  KnownLFromAssumption p (<affine> P) Q.
114 115 116 117
Proof.
  rewrite /KnownLFromAssumption /FromAssumption /= =><-.
  by rewrite affinely_elim.
Qed.
118 119 120 121 122 123
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
124 125

Global Instance from_assumption_forall {A} p (Φ : A  PROP) Q x :
126 127 128 129 130
  FromAssumption p (Φ x) Q  KnownLFromAssumption p ( x, Φ x) Q.
Proof.
  rewrite /KnownLFromAssumption /FromAssumption=> <-.
  by rewrite forall_elim.
Qed.
131

132 133 134 135
Global Instance from_assumption_bupd `{BiBUpd PROP} p P Q :
  FromAssumption p P Q  KnownRFromAssumption p P (|==> Q).
Proof. rewrite /KnownRFromAssumption /FromAssumption=>->. apply bupd_intro. Qed.

136
(** IntoPure *)
Robbert Krebbers's avatar
Robbert Krebbers committed
137 138 139
Global Instance into_pure_pure φ : @IntoPure PROP ⌜φ⌝ φ.
Proof. by rewrite /IntoPure. Qed.

Ralf Jung's avatar
Ralf Jung committed
140
Global Instance into_pure_pure_and (φ1 φ2 : Prop) P1 P2 :
Ralf Jung's avatar
Ralf Jung committed
141
  IntoPure P1 φ1  IntoPure P2 φ2  IntoPure (P1  P2) (φ1  φ2).
142
Proof. rewrite /IntoPure pure_and. by intros -> ->. Qed.
Ralf Jung's avatar
Ralf Jung committed
143
Global Instance into_pure_pure_or (φ1 φ2 : Prop) P1 P2 :
Ralf Jung's avatar
Ralf Jung committed
144
  IntoPure P1 φ1  IntoPure P2 φ2  IntoPure (P1  P2) (φ1  φ2).
145
Proof. rewrite /IntoPure pure_or. by intros -> ->. Qed.
Ralf Jung's avatar
Ralf Jung committed
146
Global Instance into_pure_pure_impl (φ1 φ2 : Prop) P1 P2 :
147 148
  FromPure false P1 φ1  IntoPure P2 φ2  IntoPure (P1  P2) (φ1  φ2).
Proof. rewrite /FromPure /IntoPure pure_impl=> <- -> //. Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
149 150 151 152 153 154 155 156 157 158 159

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.
160 161
Global Instance into_pure_pure_wand a (φ1 φ2 : Prop) P1 P2 :
  FromPure a P1 φ1  IntoPure P2 φ2  IntoPure (P1 - P2) (φ1  φ2).
162
Proof.
163 164 165
  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.
166
Qed.
167

168
Global Instance into_pure_affinely P φ : IntoPure P φ  IntoPure (<affine> P) φ.
169
Proof. rewrite /IntoPure=> ->. apply affinely_elim. Qed.
170 171 172
Global Instance into_pure_intuitionistically P φ :
  IntoPure P φ  IntoPure ( P) φ.
Proof. rewrite /IntoPure=> ->. apply intuitionistically_elim. Qed.
173
Global Instance into_pure_absorbingly P φ : IntoPure P φ  IntoPure (<absorb> P) φ.
174 175
Proof. rewrite /IntoPure=> ->. by rewrite absorbingly_pure. Qed.
Global Instance into_pure_persistently P φ :
176
  IntoPure P φ  IntoPure (<pers> P) φ.
177
Proof. rewrite /IntoPure=> ->. apply: persistently_elim. Qed.
178
Global Instance into_pure_embed `{BiEmbed PROP PROP'} P φ :
179
  IntoPure P φ  IntoPure P φ.
180
Proof. rewrite /IntoPure=> ->. by rewrite embed_pure. Qed.
181

182
(** FromPure *)
183 184 185 186 187 188 189 190 191 192 193 194 195 196 197 198 199 200
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.
201 202 203 204 205 206 207 208 209 210 211 212 213 214 215 216 217 218 219 220
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.
  rewrite /FromPure /IntoPure pure_impl=> -> <-. destruct a=>//=.
  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.
Global Instance from_pure_forall {A} a (Φ : A  PROP) (φ : A  Prop) :
  ( x, FromPure a (Φ x) (φ x))  FromPure a ( x, Φ x) ( x, φ x).
Proof.
  rewrite /FromPure=>Hx. rewrite pure_forall. setoid_rewrite <-Hx.
  destruct a=>//=. apply affinely_forall.
Qed.

221 222 223
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).
224
Proof.
225 226 227
  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.
228
Qed.
229 230 231 232
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).
233
Proof.
234 235 236 237 238 239
  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.
    by rewrite affinely_and_l pure_impl impl_elim_r.
  - by rewrite HP1 sep_and pure_impl impl_elim_r.
240 241
Qed.

242
Global Instance from_pure_persistently P a φ :
243
  FromPure true P φ  FromPure a (<pers> P) φ.
244 245
Proof.
  rewrite /FromPure=> <- /=.
Ralf Jung's avatar
Ralf Jung committed
246
  by rewrite persistently_affinely_elim affinely_if_elim persistently_pure.
247
Qed.
248 249 250 251 252
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) φ.
253
Proof.
254 255 256
  rewrite /FromPure=><- /=.
  rewrite -intuitionistically_affinely_elim -affinely_affinely_if affinely_idemp.
  by rewrite intuitionistic_intuitionistically.
257
Qed.
258 259
Global Instance from_pure_absorbingly a P φ :
  FromPure a P φ  FromPure false (<absorb> P) φ.
260
Proof.
261 262
  rewrite /FromPure=> <- /=. rewrite -affinely_affinely_if.
  by rewrite -persistent_absorbingly_affinely_2.
263
Qed.
264
Global Instance from_pure_embed `{BiEmbed PROP PROP'} a P φ :
265
  FromPure a P φ  FromPure a P φ.
Robbert Krebbers's avatar
Robbert Krebbers committed
266
Proof. rewrite /FromPure=> <-. by rewrite -embed_pure embed_affinely_if_2. Qed.
267

268 269 270 271
Global Instance from_pure_bupd `{BiBUpd PROP} a P φ :
  FromPure a P φ  FromPure a (|==> P) φ.
Proof. rewrite /FromPure=> <-. apply bupd_intro. Qed.

272
(** IntoPersistent *)
273
Global Instance into_persistent_persistently p P Q :
274
  IntoPersistent true P Q  IntoPersistent p (<pers> P) Q | 0.
Robbert Krebbers's avatar
Robbert Krebbers committed
275 276 277 278
Proof.
  rewrite /IntoPersistent /= => ->.
  destruct p; simpl; auto using persistently_idemp_1.
Qed.
279
Global Instance into_persistent_affinely p P Q :
280
  IntoPersistent p P Q  IntoPersistent p (<affine> P) Q | 0.
281
Proof. rewrite /IntoPersistent /= => <-. by rewrite affinely_elim. Qed.
282
Global Instance into_persistent_intuitionistically p P Q :
283 284 285 286 287
  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
288
    intuitionistically_into_persistently_1.
289
Qed.
290
Global Instance into_persistent_embed `{BiEmbed PROP PROP'} p P Q :
291 292
  IntoPersistent p P Q  IntoPersistent p P Q | 0.
Proof.
293
  rewrite /IntoPersistent -embed_persistently -embed_persistently_if=> -> //.
294
Qed.
295
Global Instance into_persistent_here P : IntoPersistent true P P | 1.
Robbert Krebbers's avatar
Robbert Krebbers committed
296
Proof. by rewrite /IntoPersistent. Qed.
297 298
Global Instance into_persistent_persistent P :
  Persistent P  IntoPersistent false P P | 100.
299
Proof. intros. by rewrite /IntoPersistent. Qed.
300

301
(** FromModal *)
302
Global Instance from_modal_affinely P :
303
  FromModal modality_affinely (<affine> P) (<affine> P) P | 2.
304 305 306
Proof. by rewrite /FromModal. Qed.

Global Instance from_modal_persistently P :
307
  FromModal modality_persistently (<pers> P) (<pers> P) P | 2.
308
Proof. by rewrite /FromModal. Qed.
309 310
Global Instance from_modal_intuitionistically P :
  FromModal modality_intuitionistically ( P) ( P) P | 1.
311
Proof. by rewrite /FromModal. Qed.
312
Global Instance from_modal_intuitionistically_affine_bi P :
313
  BiAffine PROP  FromModal modality_persistently ( P) ( P) P | 0.
Ralf Jung's avatar
Ralf Jung committed
314 315 316
Proof.
  intros. by rewrite /FromModal /= intuitionistically_into_persistently.
Qed.
317

318
Global Instance from_modal_absorbingly P :
319
  FromModal modality_id (<absorb> P) (<absorb> P) P.
320 321 322
Proof. by rewrite /FromModal /= -absorbingly_intro. Qed.

(* When having a modality nested in an embedding, e.g. [ ⎡|==> P⎤ ], we prefer
323
the embedding over the modality. *)
324 325
Global Instance from_modal_embed `{BiEmbed PROP PROP'} (P : PROP) :
  FromModal (@modality_embed PROP PROP' _) P P P.
326 327
Proof. by rewrite /FromModal. Qed.

328
Global Instance from_modal_id_embed `{BiEmbed PROP PROP'} `(sel : A) P Q :
329
  FromModal modality_id sel P Q 
330
  FromModal modality_id sel P Q | 100.
331 332
Proof. by rewrite /FromModal /= =><-. Qed.

333
Global Instance from_modal_affinely_embed `{BiEmbed PROP PROP'} `(sel : A) P Q :
334
  FromModal modality_affinely sel P Q 
335
  FromModal modality_affinely sel P Q | 100.
Robbert Krebbers's avatar
Robbert Krebbers committed
336
Proof. rewrite /FromModal /= =><-. by rewrite embed_affinely_2. Qed.
337
Global Instance from_modal_persistently_embed `{BiEmbed PROP PROP'} `(sel : A) P Q :
338
  FromModal modality_persistently sel P Q 
339
  FromModal modality_persistently sel P Q | 100.
340
Proof. rewrite /FromModal /= =><-. by rewrite embed_persistently. Qed.
341 342 343
Global Instance from_modal_intuitionistically_embed `{BiEmbed PROP PROP'} `(sel : A) P Q :
  FromModal modality_intuitionistically sel P Q 
  FromModal modality_intuitionistically sel P Q | 100.
Robbert Krebbers's avatar
Robbert Krebbers committed
344
Proof. rewrite /FromModal /= =><-. by rewrite embed_intuitionistically_2. Qed.
345

346 347 348 349
Global Instance from_modal_bupd `{BiBUpd PROP} P :
  FromModal modality_id (|==> P) (|==> P) P.
Proof. by rewrite /FromModal /= -bupd_intro. Qed.

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

395
Global Instance into_wand_wandM p q mP' P Q :
396
  FromAssumption q P (default emp%I mP')  IntoWand p q (mP' -? Q) P Q.
397 398
Proof. rewrite /IntoWand wandM_sound. exact: into_wand_wand. Qed.

Robbert Krebbers's avatar
Robbert Krebbers committed
399 400 401 402 403 404 405
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.

406 407 408
Global Instance into_wand_forall_prop_true p (φ : Prop) P :
  IntoWand p true ( _ : φ, P)  φ  P.
Proof.
409 410
  rewrite /IntoWand (intuitionistically_if_elim p) /=
          -impl_wand_intuitionistically -pure_impl_forall
411 412 413 414 415 416
          bi.persistently_elim //.
Qed.
Global Instance into_wand_forall_prop_false p (φ : Prop) P :
  Absorbing P  IntoWand p false ( _ : φ, P)  φ  P.
Proof.
  intros ?.
417
  rewrite /IntoWand (intuitionistically_if_elim p) /= pure_wand_forall //.
418
Qed.
419

Robbert Krebbers's avatar
Robbert Krebbers committed
420 421 422 423
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.

424 425 426 427
Global Instance into_wand_tforall {A} p q (Φ : tele_arg A  PROP) P Q x :
  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.

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

460
Global Instance into_wand_intuitionistically p q R P Q :
461 462
  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
463
Global Instance into_wand_persistently_true q R P Q :
464
  IntoWand true q R P Q  IntoWand true q (<pers> R) P Q.
Ralf Jung's avatar
Ralf Jung committed
465
Proof. by rewrite /IntoWand /= intuitionistically_persistently_elim. Qed.
466 467 468
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.
469

470 471 472
Global Instance into_wand_embed `{BiEmbed PROP PROP'} p q R P Q :
  IntoWand p q R P Q  IntoWand p q R P Q.
Proof. by rewrite /IntoWand !embed_intuitionistically_if_2 -embed_wand=> ->. Qed.
473 474 475 476 477 478 479 480 481 482 483 484 485 486 487 488 489 490 491 492 493 494 495

(* There are two versions for [IntoWand ⎡RR⎤ ...] with the argument being
[<affine> ⎡PP⎤]. When the wand [⎡RR⎤] resides in the intuitionistic context
the result of wand elimination will have the affine modality. Otherwise, it
won't. Note that when the wand [⎡RR⎤] is under an affine modality, the instance
[into_wand_affine] would already have been used. *)
Global Instance into_wand_affine_embed_true `{BiEmbed PROP PROP'} q (PP QQ RR : PROP) :
  IntoWand true q RR PP QQ  IntoWand true q RR (<affine> PP) (<affine> QQ) | 100.
Proof.
  rewrite /IntoWand /=.
  rewrite -(intuitionistically_idemp  _ %I) embed_intuitionistically_2=> ->.
  apply bi.wand_intro_l. destruct q; simpl.
  - rewrite affinely_elim  -(intuitionistically_idemp  _ %I).
    rewrite embed_intuitionistically_2 intuitionistically_sep_2 -embed_sep.
    by rewrite wand_elim_r intuitionistically_affinely.
  - by rewrite intuitionistically_affinely affinely_sep_2 -embed_sep wand_elim_r.
Qed.
Global Instance into_wand_affine_embed_false `{BiEmbed PROP PROP'} q (PP QQ RR : PROP) :
  IntoWand false q RR (<affine> PP) QQ  IntoWand false q RR (<affine> PP) QQ | 100.
Proof.
  rewrite /IntoWand /= => ->.
  by rewrite embed_affinely_2 embed_intuitionistically_if_2 embed_wand.
Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
496

497 498 499 500 501 502 503 504 505 506 507 508 509 510 511 512 513 514 515 516

Global Instance into_wand_bupd `{BiBUpd PROP} p q R P Q :
  IntoWand false false R P Q  IntoWand p q (|==> R) (|==> P) (|==> Q).
Proof.
  rewrite /IntoWand /= => HR. rewrite !intuitionistically_if_elim HR.
  apply wand_intro_l. by rewrite bupd_sep wand_elim_r.
Qed.
Global Instance into_wand_bupd_persistent `{BiBUpd PROP} p q R P Q :
  IntoWand false q R P Q  IntoWand p q (|==> R) P (|==> Q).
Proof.
  rewrite /IntoWand /= => HR. rewrite intuitionistically_if_elim HR.
  apply wand_intro_l. by rewrite bupd_frame_l wand_elim_r.
Qed.
Global Instance into_wand_bupd_args `{BiBUpd PROP} p q R P Q :
  IntoWand p false R P Q  IntoWand' p q R (|==> P) (|==> Q).
Proof.
  rewrite /IntoWand' /IntoWand /= => ->.
  apply wand_intro_l. by rewrite intuitionistically_if_elim bupd_wand_r.
Qed.

517
(** FromWand *)
518 519
Global Instance from_wand_wand P1 P2 : FromWand (P1 - P2) P1 P2.
Proof. by rewrite /FromWand. Qed.
520
Global Instance from_wand_wandM mP1 P2 :
521
  FromWand (mP1 -? P2) (default emp mP1)%I P2.
522
Proof. by rewrite /FromWand wandM_sound. Qed.
523
Global Instance from_wand_embed `{BiEmbed PROP PROP'} P Q1 Q2 :
524
  FromWand P Q1 Q2  FromWand P Q1 Q2.
525
Proof. by rewrite /FromWand -embed_wand => <-. Qed.
526

527
(** FromImpl *)
528 529
Global Instance from_impl_impl P1 P2 : FromImpl (P1  P2) P1 P2.
Proof. by rewrite /FromImpl. Qed.
530
Global Instance from_impl_embed `{BiEmbed PROP PROP'} P Q1 Q2 :
531
  FromImpl P Q1 Q2  FromImpl P Q1 Q2.
532
Proof. by rewrite /FromImpl -embed_impl => <-. Qed.
533

534
(** FromAnd *)
Robbert Krebbers's avatar
Robbert Krebbers committed
535 536 537
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 :
538
  Persistent P1  IntoAbsorbingly P1' P1  FromAnd (P1  P2) P1' P2 | 9.
539
Proof.
540 541 542
  rewrite /IntoAbsorbingly /FromAnd=> ? ->.
  rewrite persistent_and_affinely_sep_l_1 {1}(persistent_persistently_2 P1).
  by rewrite absorbingly_elim_persistently -{2}(intuitionistically_elim P1).
543
Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
544
Global Instance from_and_sep_persistent_r P1 P2 P2' :
545
  Persistent P2  IntoAbsorbingly P2' P2  FromAnd (P1  P2) P1 P2' | 10.
546
Proof.
547 548 549
  rewrite /IntoAbsorbingly /FromAnd=> ? ->.
  rewrite persistent_and_affinely_sep_r_1 {1}(persistent_persistently_2 P2).
  by rewrite absorbingly_elim_persistently -{2}(intuitionistically_elim P2).
550 551
Qed.

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

Robbert Krebbers's avatar
Robbert Krebbers committed
555
Global Instance from_and_persistently P Q1 Q2 :
556
  FromAnd P Q1 Q2 
557
  FromAnd (<pers> P) (<pers> Q1) (<pers> Q2).
Robbert Krebbers's avatar
Robbert Krebbers committed
558 559
Proof. rewrite /FromAnd=> <-. by rewrite persistently_and. Qed.
Global Instance from_and_persistently_sep P Q1 Q2 :
560
  FromSep P Q1 Q2 
561
  FromAnd (<pers> P) (<pers> Q1) (<pers> Q2) | 11.
Robbert Krebbers's avatar
Robbert Krebbers committed
562
Proof. rewrite /FromAnd=> <-. by rewrite -persistently_and persistently_and_sep. Qed.
563

564
Global Instance from_and_embed `{BiEmbed PROP PROP'} P Q1 Q2 :
565
  FromAnd P Q1 Q2  FromAnd P Q1 Q2.
566
Proof. by rewrite /FromAnd -embed_and => <-. Qed.
567

568 569
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
570
  Persistent (Φ 0 x) 
571 572 573 574
  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
575
  ( k y, Persistent (Φ k y)) 
576
  FromAnd ([ list] k  y  l, Φ k y)
Robbert Krebbers's avatar
Robbert Krebbers committed
577
    ([ list] k  y  l1, Φ k y) ([ list] k  y  l2, Φ (length l1 + k) y).
578
Proof. rewrite /IsApp=> -> ?. by rewrite /FromAnd big_sepL_app persistent_and_sep_1. Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
579

580 581 582 583 584 585 586 587 588 589 590 591 592 593 594 595 596 597 598 599 600 601
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.

602 603
Global Instance from_and_big_sepMS_disj_union_persistent
    `{Countable A} (Φ : A  PROP) X1 X2 :
604
  ( y, Persistent (Φ y)) 
605 606
  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.
607

608
(** FromSep *)
Robbert Krebbers's avatar
Robbert Krebbers committed
609 610 611
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
612
  TCOr (Affine P1) (Absorbing P2)  TCOr (Absorbing P1) (Affine P2) 
Robbert Krebbers's avatar
Robbert Krebbers committed
613 614 615 616 617 618
  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.

619
Global Instance from_sep_affinely P Q1 Q2 :
620
  FromSep P Q1 Q2  FromSep (<affine> P) (<affine> Q1) (<affine> Q2).
621
Proof. rewrite /FromSep=> <-. by rewrite affinely_sep_2. Qed.
622 623 624
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.
625
Global Instance from_sep_absorbingly P Q1 Q2 :
626
  FromSep P Q1 Q2  FromSep (<absorb> P) (<absorb> Q1) (<absorb> Q2).
627
Proof. rewrite /FromSep=> <-. by rewrite absorbingly_sep. Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
628
Global Instance from_sep_persistently P Q1 Q2 :
629
  FromSep P Q1 Q2 
630
  FromSep (<pers> P) (<pers> Q1) (<pers> Q2).
631
Proof. rewrite /FromSep=> <-. by rewrite persistently_sep_2. Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
632

633
Global Instance from_sep_embed `{BiEmbed PROP PROP'} P Q1 Q2 :
634
  FromSep P Q1 Q2  FromSep P Q1 Q2.
635
Proof. by rewrite /FromSep -embed_sep => <-. Qed.
636

637 638 639 640 641 642 643
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
644
    ([ list] k  y  l1, Φ k y) ([ list] k  y  l2, Φ (length l1 + k) y).
645
Proof. rewrite /IsApp=> ->. by rewrite /FromSep big_opL_app. Qed.
646

647 648 649 650 651 652 653 654 655 656 657 658 659 660
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.

661 662 663
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.
664

665 666 667 668
Global Instance from_sep_bupd `{BiBUpd PROP} P Q1 Q2 :
  FromSep P Q1 Q2  FromSep (|==> P) (|==> Q1) (|==> Q2).
Proof. rewrite /FromSep=><-. apply bupd_sep. Qed.

669
(** IntoAnd *)
670
Global Instance into_and_and p P Q : IntoAnd p (P  Q) P Q | 10.
671
Proof. by rewrite /IntoAnd intuitionistically_if_and. Qed.
672
Global Instance into_and_and_affine_l P Q Q' :
673
  Affine P  FromAffinely Q' Q  IntoAnd false (P  Q) P Q'.
674 675
Proof.
  intros. rewrite /IntoAnd /=.
676
  by rewrite -(affine_affinely P) affinely_and_l affinely_and (from_affinely Q').
677 678
Qed.
Global Instance into_and_and_affine_r P P' Q :
679
  Affine Q  FromAffinely P' P  IntoAnd false (P  Q) P' Q.
680 681
Proof.
  intros. rewrite /IntoAnd /=.
682
  by rewrite -(affine_affinely Q) affinely_and_r affinely_and (from_affinely P').
683 684
Qed.

685
Global Instance into_and_sep `{BiPositive PROP} P Q : IntoAnd true (P  Q) P Q.
686
Proof.
687
  rewrite /IntoAnd /= intuitionistically_sep -and_sep_intuitionistically intuitionistically_and //.
688
Qed.
689
Global Instance into_and_sep_affine P Q :
Ralf Jung's avatar
Ralf Jung committed
690
  TCOr (Affine P) (Absorbing Q)  TCOr (Absorbing P) (Affine Q) 
691 692
  IntoAnd true (P  Q) P Q.
Proof. intros. by rewrite /IntoAnd /= sep_and. Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
693 694

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

697
Global Instance into_and_affinely p P Q1 Q2 :
698
  IntoAnd p P Q1 Q2  IntoAnd p (<affine> P) (<affine> Q1) (<affine> Q2).
Robbert Krebbers's avatar
Robbert Krebbers committed
699
Proof.
Robbert Krebbers's avatar
Robbert Krebbers committed
700
  rewrite /IntoAnd. destruct p; simpl.
Ralf Jung's avatar
Ralf Jung committed
701
  - rewrite -affinely_and !intuitionistically_affinely_elim //.
702
  - intros ->. by rewrite affinely_and.
Robbert Krebbers's avatar
Robbert Krebbers committed
703
Qed.
704 705 706 707 708 709 710
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
711
Global Instance into_and_persistently p P Q1 Q2 :
712
  IntoAnd p P Q1 Q2 
713
  IntoAnd p (<pers> P) (<pers> Q1) (<pers> Q2).
Robbert Krebbers's avatar
Robbert Krebbers committed
714
Proof.
Robbert Krebbers's avatar
Robbert Krebbers committed
715
  rewrite /IntoAnd /=. destruct p; simpl.
Ralf Jung's avatar
Ralf Jung committed
716
  - rewrite -persistently_and !intuitionistically_persistently_elim //.
Robbert Krebbers's avatar
Robbert Krebbers committed
717
  - intros ->. by rewrite persistently_and.
Robbert Krebbers's avatar
Robbert Krebbers committed
718
Qed.
719
Global Instance into_and_embed `{BiEmbed PROP PROP'} p P Q1 Q2 :
720 721
  IntoAnd p P Q1 Q2  IntoAnd p P Q1 Q2.
Proof.
Robbert Krebbers's avatar
Robbert Krebbers committed
722 723
  rewrite /IntoAnd -embed_and=> HP. apply intuitionistically_if_intro'.
  by rewrite embed_intuitionistically_if_2 HP intuitionistically_if_elim.
724
Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
725

726
(** IntoSep *)
727 728
Global Instance into_sep_sep P Q : IntoSep (P  Q) P Q.
Proof. by rewrite /IntoSep. Qed.
729

730
Inductive AndIntoSep : PROP  PROP  PROP  PROP  Prop :=
731
  | and_into_sep_affine P Q Q' : Affine P  FromAffinely Q' Q  AndIntoSep P P Q Q'
732
  | and_into_sep P Q : AndIntoSep P (<affine> P)%I Q Q.
733 734 735 736 737 738
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'.
739
Proof.
740
  destruct 2 as [P Q Q'|P Q]; rewrite /IntoSep.
741
  - rewrite -(from_affinely Q' Q) -(affine_affinely P) affinely_and_lr.
742 743
    by rewrite persistent_and_affinely_sep_l_1.
  - by rewrite persistent_and_affinely_sep_l_1.
744
Qed.
745 746
Global Instance into_sep_and_persistent_r P P' Q Q' :
  Persistent Q  AndIntoSep Q Q' P P'  IntoSep (P  Q) P' Q'.
747
Proof.
748
  destruct 2 as [Q P P'|Q P]; rewrite /IntoSep.
749
  - rewrite -(from_affinely P' P) -(affine_affinely Q) -affinely_and_lr.
750 751
    by rewrite persistent_and_affinely_sep_r_1.
  - by rewrite persistent_and_affinely_sep_r_1.
752
Qed.
753

754 755 756
Global Instance into_sep_pure φ ψ : @IntoSep PROP ⌜φ  ψ⌝ ⌜φ⌝ ⌜ψ⌝.
Proof. by rewrite /IntoSep pure_and persistent_and_sep_1. Qed.

757
Global Instance into_sep_embed `{BiEmbed PROP PROP'} P Q1 Q2 :
758
  IntoSep P Q1 Q2  IntoSep P Q1 Q2.
759
Proof. rewrite /IntoSep -embed_sep=> -> //. Qed.
760