class_instances_bi.v 49.2 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 7 8 9
Import bi.

Section bi_instances.
Context {PROP : bi}.
Implicit Types P Q R : PROP.
10
Implicit Types mP : option PROP.
Robbert Krebbers's avatar
Robbert Krebbers committed
11

12
(** AsEmpValid *)
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 38
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.

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

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

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

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

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

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

128 129 130 131
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.

132
(** IntoPure *)
Robbert Krebbers's avatar
Robbert Krebbers committed
133 134 135
Global Instance into_pure_pure φ : @IntoPure PROP ⌜φ⌝ φ.
Proof. by rewrite /IntoPure. Qed.

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

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
156
Global Instance into_pure_pure_wand (φ1 φ2 : Prop) P1 P2 :
157 158 159 160
  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.
161
  rewrite -{1}(persistent_absorbingly_affinely ⌜φ1%I) absorbingly_sep_l
162 163
          bi.wand_elim_r absorbing //.
Qed.
164

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

179
(** FromPure *)
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 224 225 226 227 228
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.
229 230
Qed.

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

250 251 252 253 254 255
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.
256
Global Instance from_pure_embed `{BiEmbed PROP PROP'} a P φ :
257
  FromPure a P φ  FromPure a P φ.
Robbert Krebbers's avatar
Robbert Krebbers committed
258
Proof. rewrite /FromPure=> <-. by rewrite -embed_pure embed_affinely_if_2. Qed.
259

260 261 262 263
Global Instance from_pure_bupd `{BiBUpd PROP} a P φ :
  FromPure a P φ  FromPure a (|==> P) φ.
Proof. rewrite /FromPure=> <-. apply bupd_intro. Qed.

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

293
(** FromModal *)
294
Global Instance from_modal_affinely P :
295
  FromModal modality_affinely (<affine> P) (<affine> P) P | 2.
296 297 298
Proof. by rewrite /FromModal. Qed.

Global Instance from_modal_persistently P :
299
  FromModal modality_persistently (<pers> P) (<pers> P) P | 2.
300
Proof. by rewrite /FromModal. Qed.
301 302
Global Instance from_modal_intuitionistically P :
  FromModal modality_intuitionistically ( P) ( P) P | 1.
303
Proof. by rewrite /FromModal. Qed.
304
Global Instance from_modal_intuitionistically_affine_bi P :
305
  BiAffine PROP  FromModal modality_persistently ( P) ( P) P | 0.
Ralf Jung's avatar
Ralf Jung committed
306 307 308
Proof.
  intros. by rewrite /FromModal /= intuitionistically_into_persistently.
Qed.
309

310
Global Instance from_modal_absorbingly P :
311
  FromModal modality_id (<absorb> P) (<absorb> P) P.
312 313 314
Proof. by rewrite /FromModal /= -absorbingly_intro. Qed.

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

320
Global Instance from_modal_id_embed `{BiEmbed PROP PROP'} `(sel : A) P Q :
321
  FromModal modality_id sel P Q 
322
  FromModal modality_id sel P Q | 100.
323 324
Proof. by rewrite /FromModal /= =><-. Qed.

325
Global Instance from_modal_affinely_embed `{BiEmbed PROP PROP'} `(sel : A) P Q :
326
  FromModal modality_affinely sel P Q 
327
  FromModal modality_affinely sel P Q | 100.
Robbert Krebbers's avatar
Robbert Krebbers committed
328
Proof. rewrite /FromModal /= =><-. by rewrite embed_affinely_2. Qed.
329
Global Instance from_modal_persistently_embed `{BiEmbed PROP PROP'} `(sel : A) P Q :
330
  FromModal modality_persistently sel P Q 
331
  FromModal modality_persistently sel P Q | 100.
332
Proof. rewrite /FromModal /= =><-. by rewrite embed_persistently. Qed.
333 334 335
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
336
Proof. rewrite /FromModal /= =><-. by rewrite embed_intuitionistically_2. Qed.
337

338 339 340 341
Global Instance from_modal_bupd `{BiBUpd PROP} P :
  FromModal modality_id (|==> P) (|==> P) P.
Proof. by rewrite /FromModal /= -bupd_intro. Qed.

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

387 388 389 390
Global Instance into_wand_wandM p q mP' P Q :
  FromAssumption q P (pm_default emp%I mP')  IntoWand p q (mP' -? Q) P Q.
Proof. rewrite /IntoWand wandM_sound. exact: into_wand_wand. Qed.

Robbert Krebbers's avatar
Robbert Krebbers committed
391 392 393 394 395 396 397
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.

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

Robbert Krebbers's avatar
Robbert Krebbers committed
412 413 414 415
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.

416 417 418 419
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.

420 421 422 423 424 425 426 427 428 429 430 431 432 433 434 435 436 437 438 439 440 441 442 443 444 445 446 447 448 449 450 451
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.

452
Global Instance into_wand_intuitionistically p q R P Q :
453 454
  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
455
Global Instance into_wand_persistently_true q R P Q :
456
  IntoWand true q R P Q  IntoWand true q (<pers> R) P Q.
Ralf Jung's avatar
Ralf Jung committed
457
Proof. by rewrite /IntoWand /= intuitionistically_persistently_elim. Qed.
458 459 460
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.
461

462 463 464
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.
465 466 467 468 469 470 471 472 473 474 475 476 477 478 479 480 481 482 483 484 485 486 487

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

489 490 491 492 493 494 495 496 497 498 499 500 501 502 503 504 505 506 507 508

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.

509
(** FromWand *)
510 511
Global Instance from_wand_wand P1 P2 : FromWand (P1 - P2) P1 P2.
Proof. by rewrite /FromWand. Qed.
512 513 514
Global Instance from_wand_wandM mP1 P2 :
  FromWand (mP1 -? P2) (pm_default emp mP1)%I P2.
Proof. by rewrite /FromWand wandM_sound. Qed.
515
Global Instance from_wand_embed `{BiEmbed PROP PROP'} P Q1 Q2 :
516
  FromWand P Q1 Q2  FromWand P Q1 Q2.
517
Proof. by rewrite /FromWand -embed_wand => <-. Qed.
518

519
(** FromImpl *)
520 521
Global Instance from_impl_impl P1 P2 : FromImpl (P1  P2) P1 P2.
Proof. by rewrite /FromImpl. Qed.
522
Global Instance from_impl_embed `{BiEmbed PROP PROP'} P Q1 Q2 :
523
  FromImpl P Q1 Q2  FromImpl P Q1 Q2.
524
Proof. by rewrite /FromImpl -embed_impl => <-. Qed.
525

526
(** FromAnd *)
Robbert Krebbers's avatar
Robbert Krebbers committed
527 528 529
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 :
530
  Persistent P1  IntoAbsorbingly P1' P1  FromAnd (P1  P2) P1' P2 | 9.
531
Proof.
532 533 534
  rewrite /IntoAbsorbingly /FromAnd=> ? ->.
  rewrite persistent_and_affinely_sep_l_1 {1}(persistent_persistently_2 P1).
  by rewrite absorbingly_elim_persistently -{2}(intuitionistically_elim P1).
535
Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
536
Global Instance from_and_sep_persistent_r P1 P2 P2' :
537
  Persistent P2  IntoAbsorbingly P2' P2  FromAnd (P1  P2) P1 P2' | 10.
538
Proof.
539 540 541
  rewrite /IntoAbsorbingly /FromAnd=> ? ->.
  rewrite persistent_and_affinely_sep_r_1 {1}(persistent_persistently_2 P2).
  by rewrite absorbingly_elim_persistently -{2}(intuitionistically_elim P2).
542 543
Qed.

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

Robbert Krebbers's avatar
Robbert Krebbers committed
547
Global Instance from_and_persistently P Q1 Q2 :
548
  FromAnd P Q1 Q2 
549
  FromAnd (<pers> P) (<pers> Q1) (<pers> Q2).
Robbert Krebbers's avatar
Robbert Krebbers committed
550 551
Proof. rewrite /FromAnd=> <-. by rewrite persistently_and. Qed.
Global Instance from_and_persistently_sep P Q1 Q2 :
552
  FromSep P Q1 Q2 
553
  FromAnd (<pers> P) (<pers> Q1) (<pers> Q2) | 11.
Robbert Krebbers's avatar
Robbert Krebbers committed
554
Proof. rewrite /FromAnd=> <-. by rewrite -persistently_and persistently_and_sep. Qed.
555

556
Global Instance from_and_embed `{BiEmbed PROP PROP'} P Q1 Q2 :
557
  FromAnd P Q1 Q2  FromAnd P Q1 Q2.
558
Proof. by rewrite /FromAnd -embed_and => <-. Qed.
559

560 561
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
562
  Persistent (Φ 0 x) 
563 564 565 566
  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
567
  ( k y, Persistent (Φ k y)) 
568
  FromAnd ([ list] k  y  l, Φ k y)
Robbert Krebbers's avatar
Robbert Krebbers committed
569
    ([ list] k  y  l1, Φ k y) ([ list] k  y  l2, Φ (length l1 + k) y).
570
Proof. rewrite /IsApp=> -> ?. by rewrite /FromAnd big_sepL_app persistent_and_sep_1. Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
571

572 573 574 575 576 577 578 579 580 581 582 583 584 585 586 587 588 589 590 591 592 593
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.

594
(** FromSep *)
Robbert Krebbers's avatar
Robbert Krebbers committed
595 596 597
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
598
  TCOr (Affine P1) (Absorbing P2)  TCOr (Absorbing P1) (Affine P2) 
Robbert Krebbers's avatar
Robbert Krebbers committed
599 600 601 602 603 604
  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.

605
Global Instance from_sep_affinely P Q1 Q2 :
606
  FromSep P Q1 Q2  FromSep (<affine> P) (<affine> Q1) (<affine> Q2).
607
Proof. rewrite /FromSep=> <-. by rewrite affinely_sep_2. Qed.
608 609 610
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.
611
Global Instance from_sep_absorbingly P Q1 Q2 :
612
  FromSep P Q1 Q2  FromSep (<absorb> P) (<absorb> Q1) (<absorb> Q2).
613
Proof. rewrite /FromSep=> <-. by rewrite absorbingly_sep. Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
614
Global Instance from_sep_persistently P Q1 Q2 :
615
  FromSep P Q1 Q2 
616
  FromSep (<pers> P) (<pers> Q1) (<pers> Q2).
617
Proof. rewrite /FromSep=> <-. by rewrite persistently_sep_2. Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
618

619
Global Instance from_sep_embed `{BiEmbed PROP PROP'} P Q1 Q2 :
620
  FromSep P Q1 Q2  FromSep P Q1 Q2.
621
Proof. by rewrite /FromSep -embed_sep => <-. Qed.
622

623 624 625 626 627 628 629
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
630
    ([ list] k  y  l1, Φ k y) ([ list] k  y  l2, Φ (length l1 + k) y).
631
Proof. rewrite /IsApp=> ->. by rewrite /FromSep big_opL_app. Qed.
632

633 634 635 636 637 638 639 640 641 642 643 644 645 646
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.

647 648 649 650
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.

651
(** IntoAnd *)
652
Global Instance into_and_and p P Q : IntoAnd p (P  Q) P Q | 10.
653
Proof. by rewrite /IntoAnd intuitionistically_if_and. Qed.
654
Global Instance into_and_and_affine_l P Q Q' :
655
  Affine P  FromAffinely Q' Q  IntoAnd false (P  Q) P Q'.
656 657
Proof.
  intros. rewrite /IntoAnd /=.
658
  by rewrite -(affine_affinely P) affinely_and_l affinely_and (from_affinely Q').
659 660
Qed.
Global Instance into_and_and_affine_r P P' Q :
661
  Affine Q  FromAffinely P' P  IntoAnd false (P  Q) P' Q.
662 663
Proof.
  intros. rewrite /IntoAnd /=.
664
  by rewrite -(affine_affinely Q) affinely_and_r affinely_and (from_affinely P').
665 666
Qed.

667
Global Instance into_and_sep `{BiPositive PROP} P Q : IntoAnd true (P  Q) P Q.
668
Proof.
669
  rewrite /IntoAnd /= intuitionistically_sep -and_sep_intuitionistically intuitionistically_and //.
670
Qed.
671
Global Instance into_and_sep_affine P Q :
Ralf Jung's avatar
Ralf Jung committed
672
  TCOr (Affine P) (Absorbing Q)  TCOr (Absorbing P) (Affine Q) 
673 674
  IntoAnd true (P  Q) P Q.
Proof. intros. by rewrite /IntoAnd /= sep_and. Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
675 676

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