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

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

11
(** AsEmpValid *)
12 13 14 15 16 17 18 19 20 21 22 23 24 25 26 27 28 29 30 31 32 33 34 35 36 37
Global Instance as_emp_valid_emp_valid {PROP : bi} (P : PROP) : AsEmpValid0 (bi_emp_valid P) P | 0.
Proof. by rewrite /AsEmpValid. Qed.
Global Instance as_emp_valid_entails {PROP : bi} (P Q : PROP) : AsEmpValid0 (P  Q) (P - Q).
Proof. split. apply bi.entails_wand. apply bi.wand_entails. Qed.
Global Instance as_emp_valid_equiv {PROP : bi} (P Q : PROP) : AsEmpValid0 (P  Q) (P - Q).
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.

38
(** FromAffinely *)
39 40
Global Instance from_affinely_affine P : Affine P  FromAffinely P P.
Proof. intros. by rewrite /FromAffinely affinely_elim. Qed.
41
Global Instance from_affinely_default P : FromAffinely (<affine> P) P | 100.
42
Proof. by rewrite /FromAffinely. Qed.
43 44 45
Global Instance from_affinely_intuitionistically P :
  FromAffinely ( P) (<pers> P) | 100.
Proof. by rewrite /FromAffinely. Qed.
46

47
(** IntoAbsorbingly *)
48 49 50 51
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.
52
Global Instance into_absorbingly_intuitionistically P :
53
  IntoAbsorbingly (<pers> P) ( P) | 2.
54 55 56
Proof.
  by rewrite /IntoAbsorbingly -absorbingly_intuitionistically_into_persistently.
Qed.
57
Global Instance into_absorbingly_default P : IntoAbsorbingly (<absorb> P) P | 100.
58
Proof. by rewrite /IntoAbsorbingly. Qed.
59

60
(** FromAssumption *)
61
Global Instance from_assumption_exact p P : FromAssumption p P P | 0.
62
Proof. by rewrite /FromAssumption /= intuitionistically_if_elim. Qed.
63

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

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

Global Instance from_assumption_forall {A} p (Φ : A  PROP) Q x :
121 122 123 124 125
  FromAssumption p (Φ x) Q  KnownLFromAssumption p ( x, Φ x) Q.
Proof.
  rewrite /KnownLFromAssumption /FromAssumption=> <-.
  by rewrite forall_elim.
Qed.
126

127
(** IntoPure *)
Robbert Krebbers's avatar
Robbert Krebbers committed
128 129 130
Global Instance into_pure_pure φ : @IntoPure PROP ⌜φ⌝ φ.
Proof. by rewrite /IntoPure. Qed.

Ralf Jung's avatar
Ralf Jung committed
131
Global Instance into_pure_pure_and (φ1 φ2 : Prop) P1 P2 :
Ralf Jung's avatar
Ralf Jung committed
132
  IntoPure P1 φ1  IntoPure P2 φ2  IntoPure (P1  P2) (φ1  φ2).
133
Proof. rewrite /IntoPure pure_and. by intros -> ->. Qed.
Ralf Jung's avatar
Ralf Jung committed
134
Global Instance into_pure_pure_or (φ1 φ2 : Prop) P1 P2 :
Ralf Jung's avatar
Ralf Jung committed
135
  IntoPure P1 φ1  IntoPure P2 φ2  IntoPure (P1  P2) (φ1  φ2).
136
Proof. rewrite /IntoPure pure_or. by intros -> ->. Qed.
Ralf Jung's avatar
Ralf Jung committed
137
Global Instance into_pure_pure_impl (φ1 φ2 : Prop) P1 P2 :
138 139
  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
140 141 142 143 144 145 146 147 148 149 150

Global Instance into_pure_exist {A} (Φ : A  PROP) (φ : A  Prop) :
  ( x, IntoPure (Φ x) (φ x))  IntoPure ( x, Φ x) ( x, φ x).
Proof. rewrite /IntoPure=>Hx. rewrite pure_exist. by setoid_rewrite Hx. Qed.
Global Instance into_pure_forall {A} (Φ : A  PROP) (φ : A  Prop) :
  ( x, IntoPure (Φ x) (φ x))  IntoPure ( x, Φ x) ( x, φ x).
Proof. rewrite /IntoPure=>Hx. rewrite -pure_forall_2. by setoid_rewrite Hx. Qed.

Global Instance into_pure_pure_sep (φ1 φ2 : Prop) P1 P2 :
  IntoPure P1 φ1  IntoPure P2 φ2  IntoPure (P1  P2) (φ1  φ2).
Proof. rewrite /IntoPure=> -> ->. by rewrite sep_and pure_and. Qed.
Ralf Jung's avatar
Ralf Jung committed
151
Global Instance into_pure_pure_wand (φ1 φ2 : Prop) P1 P2 :
152 153 154 155
  FromPure true P1 φ1  IntoPure P2 φ2  IntoPure (P1 - P2) (φ1  φ2).
Proof.
  rewrite /FromPure /IntoPure=> <- -> /=.
  rewrite pure_impl -impl_wand_2. apply bi.wand_intro_l.
156
  rewrite -{1}(persistent_absorbingly_affinely ⌜φ1%I) absorbingly_sep_l
157 158
          bi.wand_elim_r absorbing //.
Qed.
159

160
Global Instance into_pure_affinely P φ : IntoPure P φ  IntoPure (<affine> P) φ.
161
Proof. rewrite /IntoPure=> ->. apply affinely_elim. Qed.
162 163 164
Global Instance into_pure_intuitionistically P φ :
  IntoPure P φ  IntoPure ( P) φ.
Proof. rewrite /IntoPure=> ->. apply intuitionistically_elim. Qed.
165
Global Instance into_pure_absorbingly P φ : IntoPure P φ  IntoPure (<absorb> P) φ.
166 167
Proof. rewrite /IntoPure=> ->. by rewrite absorbingly_pure. Qed.
Global Instance into_pure_persistently P φ :
168
  IntoPure P φ  IntoPure (<pers> P) φ.
169
Proof. rewrite /IntoPure=> ->. apply: persistently_elim. Qed.
170
Global Instance into_pure_embed `{BiEmbed PROP PROP'} P φ :
171
  IntoPure P φ  IntoPure P φ.
172
Proof. rewrite /IntoPure=> ->. by rewrite embed_pure. Qed.
173

174
(** FromPure *)
175 176 177 178 179 180 181 182 183 184 185 186 187 188 189 190 191 192 193 194 195 196 197 198 199 200 201 202 203 204 205 206 207 208 209 210 211 212 213 214 215 216 217 218 219 220 221 222 223
Global Instance from_pure_pure a φ : @FromPure PROP a ⌜φ⌝ φ.
Proof. rewrite /FromPure. apply affinely_if_elim. Qed.
Global Instance from_pure_pure_and a (φ1 φ2 : Prop) P1 P2 :
  FromPure a P1 φ1  FromPure a P2 φ2  FromPure a (P1  P2) (φ1  φ2).
Proof. rewrite /FromPure pure_and=> <- <- /=. by rewrite affinely_if_and. Qed.
Global Instance from_pure_pure_or a (φ1 φ2 : Prop) P1 P2 :
  FromPure a P1 φ1  FromPure a P2 φ2  FromPure a (P1  P2) (φ1  φ2).
Proof. by rewrite /FromPure pure_or affinely_if_or=><- <-. Qed.
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.

Global Instance from_pure_pure_sep_true (φ1 φ2 : Prop) P1 P2 :
  FromPure true P1 φ1  FromPure true P2 φ2  FromPure true (P1  P2) (φ1  φ2).
Proof.
  rewrite /FromPure=> <- <- /=.
  by rewrite -persistent_and_affinely_sep_l affinely_and_r pure_and.
Qed.
Global Instance from_pure_pure_sep_false_l (φ1 φ2 : Prop) P1 P2 :
  FromPure false P1 φ1  FromPure true P2 φ2  FromPure false (P1  P2) (φ1  φ2).
Proof.
  rewrite /FromPure=> <- <- /=. by rewrite -persistent_and_affinely_sep_r pure_and.
Qed.
Global Instance from_pure_pure_sep_false_r (φ1 φ2 : Prop) P1 P2 :
  FromPure true P1 φ1  FromPure false P2 φ2  FromPure false (P1  P2) (φ1  φ2).
Proof.
  rewrite /FromPure=> <- <- /=. by rewrite -persistent_and_affinely_sep_l pure_and.
Qed.
Global Instance from_pure_pure_wand (φ1 φ2 : Prop) a P1 P2 :
  IntoPure P1 φ1  FromPure false P2 φ2  FromPure a (P1 - P2) (φ1  φ2).
Proof.
  rewrite /FromPure /IntoPure=> -> <- /=.
  by rewrite bi.affinely_if_elim pure_wand_forall pure_impl pure_impl_forall.
224 225
Qed.

226
Global Instance from_pure_persistently P a φ :
227
  FromPure true P φ  FromPure a (<pers> P) φ.
228 229
Proof.
  rewrite /FromPure=> <- /=.
Ralf Jung's avatar
Ralf Jung committed
230
  by rewrite persistently_affinely_elim affinely_if_elim persistently_pure.
231 232
Qed.
Global Instance from_pure_affinely_true P φ :
233
  FromPure true P φ  FromPure true (<affine> P) φ.
234 235
Proof. rewrite /FromPure=><- /=. by rewrite affinely_idemp. Qed.
Global Instance from_pure_affinely_false P φ `{!Affine P} :
236
  FromPure false P φ  FromPure false (<affine> P) φ.
237
Proof. rewrite /FromPure /= affine_affinely //. Qed.
238 239 240
Global Instance from_pure_intuitionistically_true P φ :
  FromPure true P φ  FromPure true ( P) φ.
Proof.
Ralf Jung's avatar
Ralf Jung committed
241
  rewrite /FromPure=><- /=. rewrite intuitionistically_affinely_elim.
242 243
  rewrite {1}(persistent ⌜φ⌝%I) //.
Qed.
244

245 246 247 248 249 250
Global Instance from_pure_absorbingly P φ p :
  FromPure true P φ  FromPure p (<absorb> P) φ.
Proof.
  rewrite /FromPure=> <- /=.
  rewrite persistent_absorbingly_affinely affinely_if_elim //.
Qed.
251
Global Instance from_pure_embed `{BiEmbed PROP PROP'} a P φ :
252
  FromPure a P φ  FromPure a P φ.
Robbert Krebbers's avatar
Robbert Krebbers committed
253
Proof. rewrite /FromPure=> <-. by rewrite -embed_pure embed_affinely_if_2. Qed.
254

255
(** IntoPersistent *)
256
Global Instance into_persistent_persistently p P Q :
257
  IntoPersistent true P Q  IntoPersistent p (<pers> P) Q | 0.
Robbert Krebbers's avatar
Robbert Krebbers committed
258 259 260 261
Proof.
  rewrite /IntoPersistent /= => ->.
  destruct p; simpl; auto using persistently_idemp_1.
Qed.
262
Global Instance into_persistent_affinely p P Q :
263
  IntoPersistent p P Q  IntoPersistent p (<affine> P) Q | 0.
264
Proof. rewrite /IntoPersistent /= => <-. by rewrite affinely_elim. Qed.
265
Global Instance into_persistent_intuitionistically p P Q :
266 267 268 269 270
  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
271
    intuitionistically_into_persistently_1.
272
Qed.
273
Global Instance into_persistent_embed `{BiEmbed PROP PROP'} p P Q :
274 275
  IntoPersistent p P Q  IntoPersistent p P Q | 0.
Proof.
276
  rewrite /IntoPersistent -embed_persistently -embed_persistently_if=> -> //.
277
Qed.
278
Global Instance into_persistent_here P : IntoPersistent true P P | 1.
Robbert Krebbers's avatar
Robbert Krebbers committed
279
Proof. by rewrite /IntoPersistent. Qed.
280 281
Global Instance into_persistent_persistent P :
  Persistent P  IntoPersistent false P P | 100.
282
Proof. intros. by rewrite /IntoPersistent. Qed.
283

284
(** FromModal *)
285
Global Instance from_modal_affinely P :
286
  FromModal modality_affinely (<affine> P) (<affine> P) P | 2.
287 288 289
Proof. by rewrite /FromModal. Qed.

Global Instance from_modal_persistently P :
290
  FromModal modality_persistently (<pers> P) (<pers> P) P | 2.
291
Proof. by rewrite /FromModal. Qed.
292 293
Global Instance from_modal_intuitionistically P :
  FromModal modality_intuitionistically ( P) ( P) P | 1.
294
Proof. by rewrite /FromModal. Qed.
295
Global Instance from_modal_intuitionistically_affine_bi P :
296
  BiAffine PROP  FromModal modality_persistently ( P) ( P) P | 0.
Ralf Jung's avatar
Ralf Jung committed
297 298 299
Proof.
  intros. by rewrite /FromModal /= intuitionistically_into_persistently.
Qed.
300

301
Global Instance from_modal_absorbingly P :
302
  FromModal modality_id (<absorb> P) (<absorb> P) P.
303 304 305
Proof. by rewrite /FromModal /= -absorbingly_intro. Qed.

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

311
Global Instance from_modal_id_embed `{BiEmbed PROP PROP'} `(sel : A) P Q :
312
  FromModal modality_id sel P Q 
313
  FromModal modality_id sel P Q | 100.
314 315
Proof. by rewrite /FromModal /= =><-. Qed.

316
Global Instance from_modal_affinely_embed `{BiEmbed PROP PROP'} `(sel : A) P Q :
317
  FromModal modality_affinely sel P Q 
318
  FromModal modality_affinely sel P Q | 100.
Robbert Krebbers's avatar
Robbert Krebbers committed
319
Proof. rewrite /FromModal /= =><-. by rewrite embed_affinely_2. Qed.
320
Global Instance from_modal_persistently_embed `{BiEmbed PROP PROP'} `(sel : A) P Q :
321
  FromModal modality_persistently sel P Q 
322
  FromModal modality_persistently sel P Q | 100.
323
Proof. rewrite /FromModal /= =><-. by rewrite embed_persistently. Qed.
324 325 326
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
327
Proof. rewrite /FromModal /= =><-. by rewrite embed_intuitionistically_2. Qed.
328

329
(** IntoWand *)
Robbert Krebbers's avatar
Robbert Krebbers committed
330 331
Global Instance into_wand_wand p q P Q P' :
  FromAssumption q P P'  IntoWand p q (P' - Q) P Q.
332
Proof.
333
  rewrite /FromAssumption /IntoWand=> HP. by rewrite HP intuitionistically_if_elim.
Robbert Krebbers's avatar
Robbert Krebbers committed
334
Qed.
335 336
Global Instance into_wand_impl_false_false P Q P' :
  Absorbing P'  Absorbing (P'  Q) 
Robbert Krebbers's avatar
Robbert Krebbers committed
337 338
  FromAssumption false P P'  IntoWand false false (P'  Q) P Q.
Proof.
339
  rewrite /FromAssumption /IntoWand /= => ?? ->. apply wand_intro_r.
Robbert Krebbers's avatar
Robbert Krebbers committed
340 341 342
  by rewrite sep_and impl_elim_l.
Qed.
Global Instance into_wand_impl_false_true P Q P' :
343
  Absorbing P'  FromAssumption true P P' 
Robbert Krebbers's avatar
Robbert Krebbers committed
344
  IntoWand false true (P'  Q) P Q.
345
Proof.
346
  rewrite /IntoWand /FromAssumption /= => ? HP. apply wand_intro_l.
347 348
  rewrite -(intuitionistically_idemp P) HP.
  by rewrite -persistently_and_intuitionistically_sep_l persistently_elim impl_elim_r.
349
Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
350
Global Instance into_wand_impl_true_false P Q P' :
351
  Affine P'  FromAssumption false P P' 
Robbert Krebbers's avatar
Robbert Krebbers committed
352
  IntoWand true false (P'  Q) P Q.
353
Proof.
354
  rewrite /FromAssumption /IntoWand /= => ? HP. apply wand_intro_r.
355
  rewrite HP sep_and intuitionistically_elim impl_elim_l //.
356
Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
357 358
Global Instance into_wand_impl_true_true P Q P' :
  FromAssumption true P P'  IntoWand true true (P'  Q) P Q.
359
Proof.
Robbert Krebbers's avatar
Robbert Krebbers committed
360
  rewrite /FromAssumption /IntoWand /= => <-. apply wand_intro_l.
361
  rewrite sep_and [( (_  _))%I]intuitionistically_elim impl_elim_r //.
362
Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
363 364 365 366 367 368 369 370

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.

371 372 373
Global Instance into_wand_forall_prop_true p (φ : Prop) P :
  IntoWand p true ( _ : φ, P)  φ  P.
Proof.
374 375
  rewrite /IntoWand (intuitionistically_if_elim p) /=
          -impl_wand_intuitionistically -pure_impl_forall
376 377 378 379 380 381
          bi.persistently_elim //.
Qed.
Global Instance into_wand_forall_prop_false p (φ : Prop) P :
  Absorbing P  IntoWand p false ( _ : φ, P)  φ  P.
Proof.
  intros ?.
382
  rewrite /IntoWand (intuitionistically_if_elim p) /= pure_wand_forall //.
383
Qed.
384

Robbert Krebbers's avatar
Robbert Krebbers committed
385 386 387 388
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.

389 390 391 392 393 394 395 396 397 398 399 400 401 402 403 404 405 406 407 408 409 410 411 412 413 414 415 416 417 418 419 420
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.

421
Global Instance into_wand_intuitionistically p q R P Q :
422 423
  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
424
Global Instance into_wand_persistently_true q R P Q :
425
  IntoWand true q R P Q  IntoWand true q (<pers> R) P Q.
Ralf Jung's avatar
Ralf Jung committed
426
Proof. by rewrite /IntoWand /= intuitionistically_persistently_elim. Qed.
427 428 429
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.
430

431 432 433
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.
434 435 436 437 438 439 440 441 442 443 444 445 446 447 448 449 450 451 452 453 454 455 456

(* 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
457

458
(** FromWand *)
459 460
Global Instance from_wand_wand P1 P2 : FromWand (P1 - P2) P1 P2.
Proof. by rewrite /FromWand. Qed.
461
Global Instance from_wand_embed `{BiEmbed PROP PROP'} P Q1 Q2 :
462
  FromWand P Q1 Q2  FromWand P Q1 Q2.
463
Proof. by rewrite /FromWand -embed_wand => <-. Qed.
464

465
(** FromImpl *)
466 467
Global Instance from_impl_impl P1 P2 : FromImpl (P1  P2) P1 P2.
Proof. by rewrite /FromImpl. Qed.
468
Global Instance from_impl_embed `{BiEmbed PROP PROP'} P Q1 Q2 :
469
  FromImpl P Q1 Q2  FromImpl P Q1 Q2.
470
Proof. by rewrite /FromImpl -embed_impl => <-. Qed.
471

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

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

Robbert Krebbers's avatar
Robbert Krebbers committed
493
Global Instance from_and_persistently P Q1 Q2 :
494
  FromAnd P Q1 Q2 
495
  FromAnd (<pers> P) (<pers> Q1) (<pers> Q2).
Robbert Krebbers's avatar
Robbert Krebbers committed
496 497
Proof. rewrite /FromAnd=> <-. by rewrite persistently_and. Qed.
Global Instance from_and_persistently_sep P Q1 Q2 :
498
  FromSep P Q1 Q2 
499
  FromAnd (<pers> P) (<pers> Q1) (<pers> Q2) | 11.
Robbert Krebbers's avatar
Robbert Krebbers committed
500
Proof. rewrite /FromAnd=> <-. by rewrite -persistently_and persistently_and_sep. Qed.
501

502
Global Instance from_and_embed `{BiEmbed PROP PROP'} P Q1 Q2 :
503
  FromAnd P Q1 Q2  FromAnd P Q1 Q2.
504
Proof. by rewrite /FromAnd -embed_and => <-. Qed.
505

Robbert Krebbers's avatar
Robbert Krebbers committed
506 507 508
Global Instance from_and_big_sepL_cons_persistent {A} (Φ : nat  A  PROP) x l :
  Persistent (Φ 0 x) 
  FromAnd ([ list] k  y  x :: l, Φ k y) (Φ 0 x) ([ list] k  y  l, Φ (S k) y).
509
Proof. intros. by rewrite /FromAnd big_opL_cons persistent_and_sep_1. Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
510 511 512 513
Global Instance from_and_big_sepL_app_persistent {A} (Φ : nat  A  PROP) l1 l2 :
  ( k y, Persistent (Φ k y)) 
  FromAnd ([ list] k  y  l1 ++ l2, Φ k y)
    ([ list] k  y  l1, Φ k y) ([ list] k  y  l2, Φ (length l1 + k) y).
514
Proof. intros. by rewrite /FromAnd big_opL_app persistent_and_sep_1. Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
515

516
(** FromSep *)
Robbert Krebbers's avatar
Robbert Krebbers committed
517 518 519
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
520
  TCOr (Affine P1) (Absorbing P2)  TCOr (Absorbing P1) (Affine P2) 
Robbert Krebbers's avatar
Robbert Krebbers committed
521 522 523 524 525 526
  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.

527
Global Instance from_sep_affinely P Q1 Q2 :
528
  FromSep P Q1 Q2  FromSep (<affine> P) (<affine> Q1) (<affine> Q2).
529
Proof. rewrite /FromSep=> <-. by rewrite affinely_sep_2. Qed.
530 531 532
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.
533
Global Instance from_sep_absorbingly P Q1 Q2 :
534
  FromSep P Q1 Q2  FromSep (<absorb> P) (<absorb> Q1) (<absorb> Q2).
535
Proof. rewrite /FromSep=> <-. by rewrite absorbingly_sep. Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
536
Global Instance from_sep_persistently P Q1 Q2 :
537
  FromSep P Q1 Q2 
538
  FromSep (<pers> P) (<pers> Q1) (<pers> Q2).
539
Proof. rewrite /FromSep=> <-. by rewrite persistently_sep_2. Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
540

541
Global Instance from_sep_embed `{BiEmbed PROP PROP'} P Q1 Q2 :
542
  FromSep P Q1 Q2  FromSep P Q1 Q2.
543
Proof. by rewrite /FromSep -embed_sep => <-. Qed.
544

Robbert Krebbers's avatar
Robbert Krebbers committed
545 546 547 548 549 550 551
Global Instance from_sep_big_sepL_cons {A} (Φ : nat  A  PROP) x l :
  FromSep ([ list] k  y  x :: l, Φ k y) (Φ 0 x) ([ list] k  y  l, Φ (S k) y).
Proof. by rewrite /FromSep big_sepL_cons. Qed.
Global Instance from_sep_big_sepL_app {A} (Φ : nat  A  PROP) l1 l2 :
  FromSep ([ list] k  y  l1 ++ l2, Φ k y)
    ([ list] k  y  l1, Φ k y) ([ list] k  y  l2, Φ (length l1 + k) y).
Proof. by rewrite /FromSep big_opL_app. Qed.
552

553
(** IntoAnd *)
554
Global Instance into_and_and p P Q : IntoAnd p (P  Q) P Q | 10.
555
Proof. by rewrite /IntoAnd intuitionistically_if_and. Qed.
556
Global Instance into_and_and_affine_l P Q Q' :
557
  Affine P  FromAffinely Q' Q  IntoAnd false (P  Q) P Q'.
558 559
Proof.
  intros. rewrite /IntoAnd /=.
560
  by rewrite -(affine_affinely P) affinely_and_l affinely_and (from_affinely Q').
561 562
Qed.
Global Instance into_and_and_affine_r P P' Q :
563
  Affine Q  FromAffinely P' P  IntoAnd false (P  Q) P' Q.
564 565
Proof.
  intros. rewrite /IntoAnd /=.
566
  by rewrite -(affine_affinely Q) affinely_and_r affinely_and (from_affinely P').
567 568
Qed.

569
Global Instance into_and_sep `{BiPositive PROP} P Q : IntoAnd true (P  Q) P Q.
570
Proof.
571
  rewrite /IntoAnd /= intuitionistically_sep -and_sep_intuitionistically intuitionistically_and //.
572
Qed.
573
Global Instance into_and_sep_affine P Q :
Ralf Jung's avatar
Ralf Jung committed
574
  TCOr (Affine P) (Absorbing Q)  TCOr (Absorbing P) (Affine Q) 
575 576
  IntoAnd true (P  Q) P Q.
Proof. intros. by rewrite /IntoAnd /= sep_and. Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
577 578

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

581
Global Instance into_and_affinely p P Q1 Q2 :
582
  IntoAnd p P Q1 Q2  IntoAnd p (<affine> P) (<affine> Q1) (<affine> Q2).
Robbert Krebbers's avatar
Robbert Krebbers committed
583
Proof.
Robbert Krebbers's avatar
Robbert Krebbers committed
584
  rewrite /IntoAnd. destruct p; simpl.
Ralf Jung's avatar
Ralf Jung committed
585
  - rewrite -affinely_and !intuitionistically_affinely_elim //.
586
  - intros ->. by rewrite affinely_and.
Robbert Krebbers's avatar
Robbert Krebbers committed
587
Qed.
588 589 590 591 592 593 594
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
595
Global Instance into_and_persistently p P Q1 Q2 :
596
  IntoAnd p P Q1 Q2 
597
  IntoAnd p (<pers> P) (<pers> Q1) (<pers> Q2).
Robbert Krebbers's avatar
Robbert Krebbers committed
598
Proof.
Robbert Krebbers's avatar
Robbert Krebbers committed
599
  rewrite /IntoAnd /=. destruct p; simpl.
Ralf Jung's avatar
Ralf Jung committed
600
  - rewrite -persistently_and !intuitionistically_persistently_elim //.
Robbert Krebbers's avatar
Robbert Krebbers committed
601
  - intros ->. by rewrite persistently_and.
Robbert Krebbers's avatar
Robbert Krebbers committed
602
Qed.
603
Global Instance into_and_embed `{BiEmbed PROP PROP'} p P Q1 Q2 :
604 605
  IntoAnd p P Q1 Q2  IntoAnd p P Q1 Q2.
Proof.
Robbert Krebbers's avatar
Robbert Krebbers committed
606 607
  rewrite /IntoAnd -embed_and=> HP. apply intuitionistically_if_intro'.
  by rewrite embed_intuitionistically_if_2 HP intuitionistically_if_elim.
608
Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
609

610
(** IntoSep *)
611 612
Global Instance into_sep_sep P Q : IntoSep (P  Q) P Q.
Proof. by rewrite /IntoSep. Qed.
613

614
Inductive AndIntoSep : PROP  PROP  PROP  PROP  Prop :=
615
  | and_into_sep_affine P Q Q' : Affine P  FromAffinely Q' Q  AndIntoSep P P Q Q'
616
  | and_into_sep P Q : AndIntoSep P (<affine> P)%I Q Q.
617 618 619 620 621 622
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'.
623
Proof.
624
  destruct 2 as [P Q Q'|P Q]; rewrite /IntoSep.
625 626 627
  - rewrite -(from_affinely Q') -(affine_affinely P) affinely_and_lr.
    by rewrite persistent_and_affinely_sep_l_1.
  - by rewrite persistent_and_affinely_sep_l_1.
628
Qed.
629 630
Global Instance into_sep_and_persistent_r P P' Q Q' :
  Persistent Q  AndIntoSep Q Q' P P'  IntoSep (P  Q) P' Q'.
631
Proof.
632
  destruct 2 as [Q P P'|Q P]; rewrite /IntoSep.
633 634 635
  - rewrite -(from_affinely P') -(affine_affinely Q) -affinely_and_lr.
    by rewrite persistent_and_affinely_sep_r_1.
  - by rewrite persistent_and_affinely_sep_r_1.
636
Qed.
637

638 639 640
Global Instance into_sep_pure φ ψ : @IntoSep PROP ⌜φ  ψ⌝ ⌜φ⌝ ⌜ψ⌝.
Proof. by rewrite /IntoSep pure_and persistent_and_sep_1. Qed.

641
Global Instance into_sep_embed `{BiEmbed PROP PROP'} P Q1 Q2 :
642
  IntoSep P Q1 Q2  IntoSep P Q1 Q2.
643
Proof. rewrite /IntoSep -embed_sep=> -> //. Qed.
644

645
Global Instance into_sep_affinely `{BiPositive PROP} P Q1 Q2 :
646
  IntoSep P Q1 Q2  IntoSep (<affine> P) (<affine> Q1) (<affine> Q2) | 0.
647
Proof. rewrite /IntoSep /= => ->. by rewrite affinely_sep. Qed.
648 649 650
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.
651 652 653 654
(* 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 :
655
  IntoSep P Q1 Q2  IntoSep (<affine> P) Q1 Q2 | 20.
656
Proof. rewrite /IntoSep /= => ->. by rewrite affinely_elim. Qed.
657

658
Global Instance into_sep_persistently `{BiPositive PROP} P Q1 Q2 :
659
  IntoSep P Q1 Q2 
660
  IntoSep (<pers> P) (<pers> Q1) (<pers> Q2).