class_instances.v 79.1 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 Export modality_instances classes.
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 12 13 14 15
(* FromAffinely *)
Global Instance from_affinely_affine P : Affine P  FromAffinely P P.
Proof. intros. by rewrite /FromAffinely affinely_elim. Qed.
Global Instance from_affinely_default P : FromAffinely (bi_affinely P) P | 100.
Proof. by rewrite /FromAffinely. Qed.
16

17 18 19 20 21
(* IntoAbsorbingly *)
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.
22
Global Instance into_absorbingly_default P : IntoAbsorbingly (bi_absorbingly P) P | 100.
23
Proof. by rewrite /IntoAbsorbingly. Qed.
24

25
(* FromAssumption *)
26
Global Instance from_assumption_exact p P : FromAssumption p P P | 0.
27
Proof. by rewrite /FromAssumption /= affinely_persistently_if_elim. Qed.
28

29
Global Instance from_assumption_persistently_r P Q :
30
  FromAssumption true P Q  FromAssumption true P (bi_persistently Q).
Robbert Krebbers's avatar
Robbert Krebbers committed
31 32
Proof.
  rewrite /FromAssumption /= =><-.
33
  by rewrite -{1}affinely_persistently_idemp affinely_elim.
Robbert Krebbers's avatar
Robbert Krebbers committed
34
Qed.
35 36 37 38
Global Instance from_assumption_affinely_r P Q :
  FromAssumption true P Q  FromAssumption true P (bi_affinely Q).
Proof. rewrite /FromAssumption /= =><-. by rewrite affinely_idemp. Qed.
Global Instance from_assumption_absorbingly_r p P Q :
39
  FromAssumption p P Q  FromAssumption p P (bi_absorbingly Q).
40
Proof. rewrite /FromAssumption /= =><-. apply absorbingly_intro. Qed.
41

42 43 44 45 46 47 48 49 50 51 52 53
Global Instance from_assumption_affinely_plainly_l p P Q :
  FromAssumption true P Q  FromAssumption p ( P) Q.
Proof.
  rewrite /FromAssumption /= =><-.
  by rewrite affinely_persistently_if_elim plainly_elim_persistently.
Qed.
Global Instance from_assumption_plainly_l_true P Q :
  FromAssumption true P Q  FromAssumption true (bi_plainly P) Q.
Proof.
  rewrite /FromAssumption /= =><-.
  by rewrite persistently_elim plainly_elim_persistently.
Qed.
54
Global Instance from_assumption_plainly_l_false `{BiAffine PROP} P Q :
55 56 57 58 59
  FromAssumption true P Q  FromAssumption false (bi_plainly P) Q.
Proof.
  rewrite /FromAssumption /= =><-.
  by rewrite affine_affinely plainly_elim_persistently.
Qed.
60
Global Instance from_assumption_affinely_persistently_l p P Q :
61
  FromAssumption true P Q  FromAssumption p ( P) Q.
62
Proof. rewrite /FromAssumption /= =><-. by rewrite affinely_persistently_if_elim. Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
63
Global Instance from_assumption_persistently_l_true P Q :
64
  FromAssumption true P Q  FromAssumption true (bi_persistently P) Q.
Robbert Krebbers's avatar
Robbert Krebbers committed
65
Proof. rewrite /FromAssumption /= =><-. by rewrite persistently_idemp. Qed.
66
Global Instance from_assumption_persistently_l_false `{BiAffine PROP} P Q :
67
  FromAssumption true P Q  FromAssumption false (bi_persistently P) Q.
68 69 70 71
Proof. rewrite /FromAssumption /= =><-. by rewrite affine_affinely. Qed.
Global Instance from_assumption_affinely_l_true p P Q :
  FromAssumption p P Q  FromAssumption p (bi_affinely P) Q.
Proof. rewrite /FromAssumption /= =><-. by rewrite affinely_elim. Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
72 73

Global Instance from_assumption_forall {A} p (Φ : A  PROP) Q x :
74 75
  FromAssumption p (Φ x) Q  FromAssumption p ( x, Φ x) Q.
Proof. rewrite /FromAssumption=> <-. by rewrite forall_elim. Qed.
76 77

(* IntoPure *)
Robbert Krebbers's avatar
Robbert Krebbers committed
78 79 80
Global Instance into_pure_pure φ : @IntoPure PROP ⌜φ⌝ φ.
Proof. by rewrite /IntoPure. Qed.

Ralf Jung's avatar
Ralf Jung committed
81
Global Instance into_pure_pure_and (φ1 φ2 : Prop) P1 P2 :
Ralf Jung's avatar
Ralf Jung committed
82
  IntoPure P1 φ1  IntoPure P2 φ2  IntoPure (P1  P2) (φ1  φ2).
83
Proof. rewrite /IntoPure pure_and. by intros -> ->. Qed.
Ralf Jung's avatar
Ralf Jung committed
84
Global Instance into_pure_pure_or (φ1 φ2 : Prop) P1 P2 :
Ralf Jung's avatar
Ralf Jung committed
85
  IntoPure P1 φ1  IntoPure P2 φ2  IntoPure (P1  P2) (φ1  φ2).
86
Proof. rewrite /IntoPure pure_or. by intros -> ->. Qed.
Ralf Jung's avatar
Ralf Jung committed
87
Global Instance into_pure_pure_impl (φ1 φ2 : Prop) P1 P2 :
88 89
  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
90 91 92 93 94 95 96 97 98 99 100

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
101
Global Instance into_pure_pure_wand (φ1 φ2 : Prop) P1 P2 :
102 103 104 105 106 107 108
  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.
  rewrite {1}(persistent_absorbingly_affinely ⌜φ1%I) absorbingly_sep_l
          bi.wand_elim_r absorbing //.
Qed.
109

110 111 112
Global Instance into_pure_affinely P φ :
  IntoPure P φ  IntoPure (bi_affinely P) φ.
Proof. rewrite /IntoPure=> ->. apply affinely_elim. Qed.
113
Global Instance into_pure_absorbingly P φ : IntoPure P φ  IntoPure (bi_absorbingly P) φ.
114
Proof. rewrite /IntoPure=> ->. by rewrite absorbingly_pure. Qed.
115 116
Global Instance into_pure_plainly P φ : IntoPure P φ  IntoPure (bi_plainly P) φ.
Proof. rewrite /IntoPure=> ->. apply: plainly_elim. Qed.
117 118
Global Instance into_pure_persistently P φ :
  IntoPure P φ  IntoPure (bi_persistently P) φ.
119
Proof. rewrite /IntoPure=> ->. apply: persistently_elim. Qed.
120
Global Instance into_pure_embed `{BiEmbedding PROP PROP'} P φ :
121
  IntoPure P φ  IntoPure P φ.
122
Proof. rewrite /IntoPure=> ->. by rewrite bi_embed_pure. Qed.
123

124
(* FromPure *)
125 126 127 128 129 130 131 132 133 134 135 136 137 138 139 140 141 142 143 144 145 146 147 148 149 150 151 152 153 154 155 156 157 158 159 160 161 162 163 164 165 166 167 168 169 170 171 172 173
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.
174 175
Qed.

176
Global Instance from_pure_plainly P φ :
177
  FromPure false P φ  FromPure false (bi_plainly P) φ.
178
Proof. rewrite /FromPure=> <-. by rewrite plainly_pure. Qed.
179 180 181 182 183 184 185 186 187 188 189 190 191 192 193 194 195 196 197 198
Global Instance from_pure_persistently P a φ :
  FromPure true P φ  FromPure a (bi_persistently P) φ.
Proof.
  rewrite /FromPure=> <- /=.
  by rewrite persistently_affinely affinely_if_elim persistently_pure.
Qed.
Global Instance from_pure_affinely_true P φ :
  FromPure true P φ  FromPure true (bi_affinely P) φ.
Proof. rewrite /FromPure=><- /=. by rewrite affinely_idemp. Qed.
Global Instance from_pure_affinely_false P φ `{!Affine P} :
  FromPure false P φ  FromPure false (bi_affinely P) φ.
Proof. rewrite /FromPure /= affine_affinely //. Qed.

Global Instance from_pure_absorbingly P φ :
  FromPure true P φ  FromPure false (bi_absorbingly P) φ.
Proof. rewrite /FromPure=> <- /=. apply persistent_absorbingly_affinely, _. Qed.
Global Instance from_pure_embed `{BiEmbedding PROP PROP'} a P φ :
  FromPure a P φ  FromPure a P φ.
Proof. rewrite /FromPure=> <-. by rewrite bi_embed_affinely_if bi_embed_pure. Qed.

199
(* IntoPersistent *)
200
Global Instance into_persistent_persistently p P Q :
201
  IntoPersistent true P Q  IntoPersistent p (bi_persistently P) Q | 0.
Robbert Krebbers's avatar
Robbert Krebbers committed
202 203 204 205
Proof.
  rewrite /IntoPersistent /= => ->.
  destruct p; simpl; auto using persistently_idemp_1.
Qed.
206 207 208
Global Instance into_persistent_affinely p P Q :
  IntoPersistent p P Q  IntoPersistent p (bi_affinely P) Q | 0.
Proof. rewrite /IntoPersistent /= => <-. by rewrite affinely_elim. Qed.
209
Global Instance into_persistent_embed `{BiEmbedding PROP PROP'} p P Q :
210 211
  IntoPersistent p P Q  IntoPersistent p P Q | 0.
Proof.
212
  rewrite /IntoPersistent -bi_embed_persistently -bi_embed_persistently_if=> -> //.
213
Qed.
214
Global Instance into_persistent_here P : IntoPersistent true P P | 1.
Robbert Krebbers's avatar
Robbert Krebbers committed
215
Proof. by rewrite /IntoPersistent. Qed.
216 217
Global Instance into_persistent_persistent P :
  Persistent P  IntoPersistent false P P | 100.
218
Proof. intros. by rewrite /IntoPersistent. Qed.
219

220 221
(* FromModal *)
Global Instance from_modal_affinely P :
222
  FromModal modality_affinely (bi_affinely P) (bi_affinely P) P | 2.
223 224 225
Proof. by rewrite /FromModal. Qed.

Global Instance from_modal_persistently P :
226
  FromModal modality_persistently (bi_persistently P) (bi_persistently P) P | 2.
227 228
Proof. by rewrite /FromModal. Qed.
Global Instance from_modal_affinely_persistently P :
229
  FromModal modality_affinely_persistently ( P) ( P) P | 1.
230 231
Proof. by rewrite /FromModal. Qed.
Global Instance from_modal_affinely_persistently_affine_bi P :
232
  BiAffine PROP  FromModal modality_persistently ( P) ( P) P | 0.
233 234 235
Proof. intros. by rewrite /FromModal /= affine_affinely. Qed.

Global Instance from_modal_plainly P :
236
  FromModal modality_plainly (bi_plainly P) (bi_plainly P) P | 2.
237 238
Proof. by rewrite /FromModal. Qed.
Global Instance from_modal_affinely_plainly P :
239
  FromModal modality_affinely_plainly ( P) ( P) P | 1.
240 241
Proof. by rewrite /FromModal. Qed.
Global Instance from_modal_affinely_plainly_affine_bi P :
242
  BiAffine PROP  FromModal modality_plainly ( P) ( P) P | 0.
243 244
Proof. intros. by rewrite /FromModal /= affine_affinely. Qed.

245 246 247 248 249
Global Instance from_modal_absorbingly P :
  FromModal modality_id (bi_absorbingly P) (bi_absorbingly P) P.
Proof. by rewrite /FromModal /= -absorbingly_intro. Qed.

(* When having a modality nested in an embedding, e.g. [ ⎡|==> P⎤ ], we prefer
250
the embedding over the modality. *)
251
Global Instance from_modal_embed `{BiEmbedding PROP PROP'} (P : PROP) :
252
  FromModal (@modality_embed PROP PROP' _ _) P P P.
253 254 255 256
Proof. by rewrite /FromModal. Qed.

Global Instance from_modal_id_embed `{BiEmbedding PROP PROP'} `(sel : A) P Q :
  FromModal modality_id sel P Q 
257
  FromModal modality_id sel P Q | 100.
258 259 260 261
Proof. by rewrite /FromModal /= =><-. Qed.

Global Instance from_modal_affinely_embed `{BiEmbedding PROP PROP'} `(sel : A) P Q :
  FromModal modality_affinely sel P Q 
262
  FromModal modality_affinely sel P Q | 100.
263
Proof. rewrite /FromModal /= =><-. by rewrite bi_embed_affinely. Qed.
264 265
Global Instance from_modal_persistently_embed `{BiEmbedding PROP PROP'} `(sel : A) P Q :
  FromModal modality_persistently sel P Q 
266
  FromModal modality_persistently sel P Q | 100.
267
Proof. rewrite /FromModal /= =><-. by rewrite bi_embed_persistently. Qed.
268 269
Global Instance from_modal_affinely_persistently_embed `{BiEmbedding PROP PROP'} `(sel : A) P Q :
  FromModal modality_affinely_persistently sel P Q 
270
  FromModal modality_affinely_persistently sel P Q | 100.
271 272 273
Proof.
  rewrite /FromModal /= =><-. by rewrite bi_embed_affinely bi_embed_persistently.
Qed.
274 275
Global Instance from_modal_plainly_embed `{BiEmbedding PROP PROP'} `(sel : A) P Q :
  FromModal modality_plainly sel P Q 
276
  FromModal modality_plainly sel P Q | 100.
277
Proof. rewrite /FromModal /= =><-. by rewrite bi_embed_plainly. Qed.
278 279
Global Instance from_modal_affinely_plainly_embed `{BiEmbedding PROP PROP'} `(sel : A) P Q :
  FromModal modality_affinely_plainly sel P Q 
280
  FromModal modality_affinely_plainly sel P Q | 100.
281 282
Proof.
  rewrite /FromModal /= =><-. by rewrite bi_embed_affinely bi_embed_plainly.
283
Qed.
284

Robbert Krebbers's avatar
Robbert Krebbers committed
285 286 287
(* IntoWand *)
Global Instance into_wand_wand p q P Q P' :
  FromAssumption q P P'  IntoWand p q (P' - Q) P Q.
288
Proof.
289
  rewrite /FromAssumption /IntoWand=> HP. by rewrite HP affinely_persistently_if_elim.
Robbert Krebbers's avatar
Robbert Krebbers committed
290
Qed.
291 292
Global Instance into_wand_impl_false_false P Q P' :
  Absorbing P'  Absorbing (P'  Q) 
Robbert Krebbers's avatar
Robbert Krebbers committed
293 294
  FromAssumption false P P'  IntoWand false false (P'  Q) P Q.
Proof.
295
  rewrite /FromAssumption /IntoWand /= => ?? ->. apply wand_intro_r.
Robbert Krebbers's avatar
Robbert Krebbers committed
296 297 298
  by rewrite sep_and impl_elim_l.
Qed.
Global Instance into_wand_impl_false_true P Q P' :
299
  Absorbing P'  FromAssumption true P P' 
Robbert Krebbers's avatar
Robbert Krebbers committed
300
  IntoWand false true (P'  Q) P Q.
301
Proof.
302
  rewrite /IntoWand /FromAssumption /= => ? HP. apply wand_intro_l.
303 304
  rewrite -(affinely_persistently_idemp P) HP.
  by rewrite -persistently_and_affinely_sep_l persistently_elim impl_elim_r.
305
Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
306
Global Instance into_wand_impl_true_false P Q P' :
307
  Affine P'  FromAssumption false P P' 
Robbert Krebbers's avatar
Robbert Krebbers committed
308
  IntoWand true false (P'  Q) P Q.
309
Proof.
310
  rewrite /FromAssumption /IntoWand /= => ? HP. apply wand_intro_r.
311 312
  rewrite -persistently_and_affinely_sep_l HP -{2}(affine_affinely P') -affinely_and_lr.
  by rewrite affinely_persistently_elim impl_elim_l.
313
Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
314 315
Global Instance into_wand_impl_true_true P Q P' :
  FromAssumption true P P'  IntoWand true true (P'  Q) P Q.
316
Proof.
Robbert Krebbers's avatar
Robbert Krebbers committed
317
  rewrite /FromAssumption /IntoWand /= => <-. apply wand_intro_l.
318 319
  rewrite -{1}(affinely_persistently_idemp P) -and_sep_affinely_persistently.
  by rewrite -affinely_persistently_and impl_elim_r affinely_persistently_elim.
320
Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
321 322 323 324 325 326 327 328

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.

329 330 331 332 333 334 335 336 337 338 339 340 341
Global Instance into_wand_forall_prop_true p (φ : Prop) P :
  IntoWand p true ( _ : φ, P)  φ  P.
Proof.
  rewrite /IntoWand (affinely_persistently_if_elim p) /=
          -impl_wand_affinely_persistently -pure_impl_forall
          bi.persistently_elim //.
Qed.
Global Instance into_wand_forall_prop_false p (φ : Prop) P :
  Absorbing P  IntoWand p false ( _ : φ, P)  φ  P.
Proof.
  intros ?.
  rewrite /IntoWand (affinely_persistently_if_elim p) /= pure_wand_forall //.
Qed.
342

Robbert Krebbers's avatar
Robbert Krebbers committed
343 344 345 346
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.

347 348 349 350 351 352
Global Instance into_wand_affinely_plainly p q R P Q :
  IntoWand p q R P Q  IntoWand p q ( R) P Q.
Proof. by rewrite /IntoWand affinely_plainly_elim. Qed.
Global Instance into_wand_plainly_true q R P Q :
  IntoWand true q R P Q  IntoWand true q (bi_plainly R) P Q.
Proof. by rewrite /IntoWand /= persistently_plainly plainly_elim_persistently. Qed.
353
Global Instance into_wand_plainly_false `{!BiAffine PROP} q R P Q :
354 355 356 357 358 359
  IntoWand false q R P Q  IntoWand false q (bi_plainly R) P Q.
Proof. by rewrite /IntoWand plainly_elim. Qed.

Global Instance into_wand_affinely_persistently p q R P Q :
  IntoWand p q R P Q  IntoWand p q ( R) P Q.
Proof. by rewrite /IntoWand affinely_persistently_elim. Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
360
Global Instance into_wand_persistently_true q R P Q :
361
  IntoWand true q R P Q  IntoWand true q (bi_persistently R) P Q.
Robbert Krebbers's avatar
Robbert Krebbers committed
362
Proof. by rewrite /IntoWand /= persistently_idemp. Qed.
363
Global Instance into_wand_persistently_false `{!BiAffine PROP} q R P Q :
364
  IntoWand false q R P Q  IntoWand false q (bi_persistently R) P Q.
365
Proof. by rewrite /IntoWand persistently_elim. Qed.
366
Global Instance into_wand_embed `{BiEmbedding PROP PROP'} p q R P Q :
367 368
  IntoWand p q R P Q  IntoWand p q R P Q.
Proof.
369 370
  rewrite /IntoWand -!bi_embed_persistently_if -!bi_embed_affinely_if
          -bi_embed_wand => -> //.
371
Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
372

373 374 375 376 377 378 379 380 381 382 383 384 385 386
(* FromWand *)
Global Instance from_wand_wand P1 P2 : FromWand (P1 - P2) P1 P2.
Proof. by rewrite /FromWand. Qed.
Global Instance from_wand_embed `{BiEmbedding PROP PROP'} P Q1 Q2 :
  FromWand P Q1 Q2  FromWand P Q1 Q2.
Proof. by rewrite /FromWand -bi_embed_wand => <-. Qed.

(* FromImpl *)
Global Instance from_impl_impl P1 P2 : FromImpl (P1  P2) P1 P2.
Proof. by rewrite /FromImpl. Qed.
Global Instance from_impl_embed `{BiEmbedding PROP PROP'} P Q1 Q2 :
  FromImpl P Q1 Q2  FromImpl P Q1 Q2.
Proof. by rewrite /FromImpl -bi_embed_impl => <-. Qed.

Robbert Krebbers's avatar
Robbert Krebbers committed
387 388 389 390
(* FromAnd *)
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 :
391
  FromAffinely P1 P1'  Persistent P1'  FromAnd (P1  P2) P1' P2 | 9.
392
Proof.
393
  rewrite /FromAffinely /FromAnd=> <- ?. by rewrite persistent_and_affinely_sep_l_1.
394
Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
395
Global Instance from_and_sep_persistent_r P1 P2 P2' :
396
  FromAffinely P2 P2'  Persistent P2'  FromAnd (P1  P2) P1 P2' | 10.
397
Proof.
398
  rewrite /FromAffinely /FromAnd=> <- ?. by rewrite persistent_and_affinely_sep_r_1.
399
Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
400 401
Global Instance from_and_sep_persistent P1 P2 :
  Persistent P1  Persistent P2  FromAnd (P1  P2) P1 P2 | 11.
402
Proof.
403
  rewrite /FromAffinely /FromAnd. intros ??. by rewrite -persistent_and_sep_1.
404 405
Qed.

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

409 410 411 412 413 414 415 416 417
Global Instance from_and_plainly P Q1 Q2 :
  FromAnd P Q1 Q2 
  FromAnd (bi_plainly P) (bi_plainly Q1) (bi_plainly Q2).
Proof. rewrite /FromAnd=> <-. by rewrite plainly_and. Qed.
Global Instance from_and_plainly_sep P Q1 Q2 :
  FromSep P Q1 Q2 
  FromAnd (bi_plainly P) (bi_plainly Q1) (bi_plainly Q2) | 11.
Proof. rewrite /FromAnd=> <-. by rewrite -plainly_and plainly_and_sep. Qed.

Robbert Krebbers's avatar
Robbert Krebbers committed
418
Global Instance from_and_persistently P Q1 Q2 :
419 420
  FromAnd P Q1 Q2 
  FromAnd (bi_persistently P) (bi_persistently Q1) (bi_persistently Q2).
Robbert Krebbers's avatar
Robbert Krebbers committed
421 422
Proof. rewrite /FromAnd=> <-. by rewrite persistently_and. Qed.
Global Instance from_and_persistently_sep P Q1 Q2 :
423 424
  FromSep P Q1 Q2 
  FromAnd (bi_persistently P) (bi_persistently Q1) (bi_persistently Q2) | 11.
Robbert Krebbers's avatar
Robbert Krebbers committed
425
Proof. rewrite /FromAnd=> <-. by rewrite -persistently_and persistently_and_sep. Qed.
426

427
Global Instance from_and_embed `{BiEmbedding PROP PROP'} P Q1 Q2 :
428
  FromAnd P Q1 Q2  FromAnd P Q1 Q2.
429
Proof. by rewrite /FromAnd -bi_embed_and => <-. Qed.
430

Robbert Krebbers's avatar
Robbert Krebbers committed
431 432 433
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).
434
Proof. intros. by rewrite /FromAnd big_opL_cons persistent_and_sep_1. Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
435 436 437 438
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).
439
Proof. intros. by rewrite /FromAnd big_opL_app persistent_and_sep_1. Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
440 441 442 443 444

(* FromSep *)
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
445
  TCOr (Affine P1) (Absorbing P2)  TCOr (Absorbing P1) (Affine P2) 
Robbert Krebbers's avatar
Robbert Krebbers committed
446 447 448 449 450 451
  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.

452 453 454 455
Global Instance from_sep_affinely P Q1 Q2 :
  FromSep P Q1 Q2  FromSep (bi_affinely P) (bi_affinely Q1) (bi_affinely Q2).
Proof. rewrite /FromSep=> <-. by rewrite affinely_sep_2. Qed.
Global Instance from_sep_absorbingly P Q1 Q2 :
456
  FromSep P Q1 Q2  FromSep (bi_absorbingly P) (bi_absorbingly Q1) (bi_absorbingly Q2).
457
Proof. rewrite /FromSep=> <-. by rewrite absorbingly_sep. Qed.
458 459 460 461
Global Instance from_sep_plainly P Q1 Q2 :
  FromSep P Q1 Q2 
  FromSep (bi_plainly P) (bi_plainly Q1) (bi_plainly Q2).
Proof. rewrite /FromSep=> <-. by rewrite plainly_sep_2. Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
462
Global Instance from_sep_persistently P Q1 Q2 :
463 464
  FromSep P Q1 Q2 
  FromSep (bi_persistently P) (bi_persistently Q1) (bi_persistently Q2).
465
Proof. rewrite /FromSep=> <-. by rewrite persistently_sep_2. Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
466

467
Global Instance from_sep_embed `{BiEmbedding PROP PROP'} P Q1 Q2 :
468
  FromSep P Q1 Q2  FromSep P Q1 Q2.
469
Proof. by rewrite /FromSep -bi_embed_sep => <-. Qed.
470

Robbert Krebbers's avatar
Robbert Krebbers committed
471 472 473 474 475 476 477
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.
478

Robbert Krebbers's avatar
Robbert Krebbers committed
479
(* IntoAnd *)
480
Global Instance into_and_and p P Q : IntoAnd p (P  Q) P Q | 10.
481
Proof. by rewrite /IntoAnd affinely_persistently_if_and. Qed.
482
Global Instance into_and_and_affine_l P Q Q' :
483
  Affine P  FromAffinely Q' Q  IntoAnd false (P  Q) P Q'.
484 485
Proof.
  intros. rewrite /IntoAnd /=.
486
  by rewrite -(affine_affinely P) affinely_and_l affinely_and (from_affinely Q').
487 488
Qed.
Global Instance into_and_and_affine_r P P' Q :
489
  Affine Q  FromAffinely P' P  IntoAnd false (P  Q) P' Q.
490 491
Proof.
  intros. rewrite /IntoAnd /=.
492
  by rewrite -(affine_affinely Q) affinely_and_r affinely_and (from_affinely P').
493 494
Qed.

495
Global Instance into_and_sep `{BiPositive PROP} P Q : IntoAnd true (P  Q) P Q.
496 497 498
Proof.
  by rewrite /IntoAnd /= persistently_sep -and_sep_persistently persistently_and.
Qed.
499
Global Instance into_and_sep_affine P Q :
Ralf Jung's avatar
Ralf Jung committed
500
  TCOr (Affine P) (Absorbing Q)  TCOr (Absorbing P) (Affine Q) 
501 502
  IntoAnd true (P  Q) P Q.
Proof. intros. by rewrite /IntoAnd /= sep_and. Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
503 504

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

507 508
Global Instance into_and_affinely p P Q1 Q2 :
  IntoAnd p P Q1 Q2  IntoAnd p (bi_affinely P) (bi_affinely Q1) (bi_affinely Q2).
Robbert Krebbers's avatar
Robbert Krebbers committed
509
Proof.
Robbert Krebbers's avatar
Robbert Krebbers committed
510
  rewrite /IntoAnd. destruct p; simpl.
511 512
  - by rewrite -affinely_and !persistently_affinely.
  - intros ->. by rewrite affinely_and.
Robbert Krebbers's avatar
Robbert Krebbers committed
513
Qed.
514 515 516
Global Instance into_and_plainly p P Q1 Q2 :
  IntoAnd p P Q1 Q2 
  IntoAnd p (bi_plainly P) (bi_plainly Q1) (bi_plainly Q2).
517
Proof.
518 519 520 521 522
  rewrite /IntoAnd /=. destruct p; simpl.
  - rewrite -plainly_and persistently_plainly -plainly_persistently
            -plainly_affinely => ->.
    by rewrite plainly_affinely plainly_persistently persistently_plainly.
  - intros ->. by rewrite plainly_and.
523
Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
524
Global Instance into_and_persistently p P Q1 Q2 :
525 526
  IntoAnd p P Q1 Q2 
  IntoAnd p (bi_persistently P) (bi_persistently Q1) (bi_persistently Q2).
Robbert Krebbers's avatar
Robbert Krebbers committed
527
Proof.
Robbert Krebbers's avatar
Robbert Krebbers committed
528 529 530
  rewrite /IntoAnd /=. destruct p; simpl.
  - by rewrite -persistently_and !persistently_idemp.
  - intros ->. by rewrite persistently_and.
Robbert Krebbers's avatar
Robbert Krebbers committed
531
Qed.
532
Global Instance into_and_embed `{BiEmbedding PROP PROP'} p P Q1 Q2 :
533 534
  IntoAnd p P Q1 Q2  IntoAnd p P Q1 Q2.
Proof.
535 536
  rewrite /IntoAnd -bi_embed_and -!bi_embed_persistently_if
          -!bi_embed_affinely_if=> -> //.
537
Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
538

Robbert Krebbers's avatar
Robbert Krebbers committed
539
(* IntoSep *)
540 541
Global Instance into_sep_sep P Q : IntoSep (P  Q) P Q.
Proof. by rewrite /IntoSep. Qed.
542

543
Inductive AndIntoSep : PROP  PROP  PROP  PROP  Prop :=
544 545
  | and_into_sep_affine P Q Q' : Affine P  FromAffinely Q' Q  AndIntoSep P P Q Q'
  | and_into_sep P Q : AndIntoSep P (bi_affinely P)%I Q Q.
546 547 548 549 550 551
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'.
552
Proof.
553
  destruct 2 as [P Q Q'|P Q]; rewrite /IntoSep.
554 555 556
  - 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.
557
Qed.
558 559
Global Instance into_sep_and_persistent_r P P' Q Q' :
  Persistent Q  AndIntoSep Q Q' P P'  IntoSep (P  Q) P' Q'.
560
Proof.
561
  destruct 2 as [Q P P'|Q P]; rewrite /IntoSep.
562 563 564
  - 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.
565
Qed.
566

567 568 569
Global Instance into_sep_pure φ ψ : @IntoSep PROP ⌜φ  ψ⌝ ⌜φ⌝ ⌜ψ⌝.
Proof. by rewrite /IntoSep pure_and persistent_and_sep_1. Qed.

570
Global Instance into_sep_embed `{BiEmbedding PROP PROP'} P Q1 Q2 :
571
  IntoSep P Q1 Q2  IntoSep P Q1 Q2.
572
Proof. rewrite /IntoSep -bi_embed_sep=> -> //. Qed.
573

574 575 576 577 578 579 580
Global Instance into_sep_affinely `{BiPositive PROP} P Q1 Q2 :
  IntoSep P Q1 Q2  IntoSep (bi_affinely P) (bi_affinely Q1) (bi_affinely Q2) | 0.
Proof. rewrite /IntoSep /= => ->. by rewrite affinely_sep. Qed.
(* 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 :
581 582
  IntoSep P Q1 Q2  IntoSep (bi_affinely P) Q1 Q2 | 20.
Proof. rewrite /IntoSep /= => ->. by rewrite affinely_elim. Qed.
583

584
Global Instance into_sep_plainly `{BiPositive PROP} P Q1 Q2 :
585 586
  IntoSep P Q1 Q2  IntoSep (bi_plainly P) (bi_plainly Q1) (bi_plainly Q2).
Proof. rewrite /IntoSep /= => ->. by rewrite plainly_sep. Qed.
587 588
Global Instance into_sep_plainly_affine P Q1 Q2 :
  IntoSep P Q1 Q2 
Ralf Jung's avatar
Ralf Jung committed
589
  TCOr (Affine Q1) (Absorbing Q2)  TCOr (Absorbing Q1) (Affine Q2) 
590 591
  IntoSep (bi_plainly P) (bi_plainly Q1) (bi_plainly Q2).
Proof.
Ralf Jung's avatar
Ralf Jung committed
592
  rewrite /IntoSep /= => -> ??. by rewrite sep_and plainly_and plainly_and_sep_l_1.
593 594
Qed.

595
Global Instance into_sep_persistently `{BiPositive PROP} P Q1 Q2 :
596 597
  IntoSep P Q1 Q2 
  IntoSep (bi_persistently P) (bi_persistently Q1) (bi_persistently Q2).
598
Proof. rewrite /IntoSep /= => ->. by rewrite persistently_sep. Qed.
599 600
Global Instance into_sep_persistently_affine P Q1 Q2 :
  IntoSep P Q1 Q2 
Ralf Jung's avatar
Ralf Jung committed
601
  TCOr (Affine Q1) (Absorbing Q2)  TCOr (Absorbing Q1) (Affine Q2) 
602 603
  IntoSep (bi_persistently P) (bi_persistently Q1) (bi_persistently Q2).
Proof.
Ralf Jung's avatar
Ralf Jung committed
604
  rewrite /IntoSep /= => -> ??.
605 606 607 608
  by rewrite sep_and persistently_and persistently_and_sep_l_1.
Qed.
Global Instance into_sep_affinely_persistently_affine P Q1 Q2 :
  IntoSep P Q1 Q2 
Ralf Jung's avatar
Ralf Jung committed
609
  TCOr (Affine Q1) (Absorbing Q2)  TCOr (Absorbing Q1) (Affine Q2) 
610 611
  IntoSep ( P) ( Q1) ( Q2).
Proof.
Ralf Jung's avatar
Ralf Jung committed
612
  rewrite /IntoSep /= => -> ??.
613 614
  by rewrite sep_and affinely_persistently_and and_sep_affinely_persistently.
Qed.
615

616 617 618
(* We use [IsCons] and [IsApp] to make sure that [frame_big_sepL_cons] and
[frame_big_sepL_app] cannot be applied repeatedly often when having
[ [∗ list] k ↦ x ∈ ?e, Φ k x] with [?e] an evar. *)
619
Global Instance into_sep_big_sepL_cons {A} (Φ : nat  A  PROP) l x l' :
620
  IsCons l x l' 
621
  IntoSep ([ list] k  y  l, Φ k y)
622
    (Φ 0 x) ([ list] k  y  l', Φ (S k) y).
Robbert Krebbers's avatar
Robbert Krebbers committed
623
Proof. rewrite /IsCons=>->. by rewrite /IntoSep big_sepL_cons. Qed.
624
Global Instance into_sep_big_sepL_app {A} (Φ : nat  A  PROP) l l1 l2 :
625
  IsApp l l1 l2 
626
  IntoSep ([ list] k  y  l, Φ k y)
627
    ([ list] k  y  l1, Φ k y) ([ list] k  y  l2, Φ (length l1 + k) y).
Robbert Krebbers's avatar
Robbert Krebbers committed
628 629 630 631 632 633 634
Proof. rewrite /IsApp=>->. by rewrite /IntoSep big_sepL_app. Qed.

(* FromOr *)
Global Instance from_or_or P1 P2 : FromOr (P1  P2) P1 P2.
Proof. by rewrite /FromOr. Qed.
Global Instance from_or_pure φ ψ : @FromOr PROP ⌜φ  ψ⌝ ⌜φ⌝ ⌜ψ⌝.
Proof. by rewrite /FromOr pure_or. Qed.
635 636 637 638
Global Instance from_or_affinely P Q1 Q2 :
  FromOr P Q1 Q2  FromOr (bi_affinely P) (bi_affinely Q1) (bi_affinely Q2).
Proof. rewrite /FromOr=> <-. by rewrite affinely_or. Qed.
Global Instance from_or_absorbingly P Q1 Q2 :
639
  FromOr P Q1 Q2  FromOr (bi_absorbingly P) (bi_absorbingly Q1) (bi_absorbingly Q2).
640
Proof. rewrite /FromOr=> <-. by rewrite absorbingly_or. Qed.
641 642
Global Instance from_or_plainly P Q1 Q2 :
  FromOr P Q1 Q2  FromOr (bi_plainly P) (bi_plainly Q1) (bi_plainly Q2).
643
Proof. rewrite /FromOr=> <-. by rewrite -plainly_or_2. Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
644
Global Instance from_or_persistently P Q1 Q2 :
645 646
  FromOr P Q1 Q2 
  FromOr (bi_persistently P) (bi_persistently Q1) (bi_persistently Q2).
Robbert Krebbers's avatar
Robbert Krebbers committed
647
Proof. rewrite /FromOr=> <-. by rewrite persistently_or. Qed.
648
Global Instance from_or_embed `{BiEmbedding PROP PROP'} P Q1 Q2 :
649
  FromOr P Q1 Q2  FromOr P Q1 Q2.
650
Proof. by rewrite /FromOr -bi_embed_or => <-. Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
651 652 653 654 655 656

(* IntoOr *)
Global Instance into_or_or P Q : IntoOr (P  Q) P Q.
Proof. by rewrite /IntoOr. Qed.
Global Instance into_or_pure φ ψ : @IntoOr PROP ⌜φ  ψ⌝ ⌜φ⌝ ⌜ψ⌝.
Proof. by rewrite /IntoOr pure_or. Qed.
657 658 659 660
Global Instance into_or_affinely P Q1 Q2 :
  IntoOr P Q1 Q2  IntoOr (bi_affinely P) (bi_affinely Q1) (bi_affinely Q2).
Proof. rewrite /IntoOr=>->. by rewrite affinely_or. Qed.
Global Instance into_or_absorbingly P Q1 Q2 :
661
  IntoOr P Q1 Q2  IntoOr (bi_absorbingly P) (bi_absorbingly Q1) (bi_absorbingly Q2).
662
Proof. rewrite /IntoOr=>->. by rewrite absorbingly_or. Qed.
663
Global Instance into_or_plainly `{BiPlainlyExist PROP} P Q1 Q2 :
664 665
  IntoOr P Q1 Q2  IntoOr (bi_plainly P) (bi_plainly Q1) (bi_plainly Q2).
Proof. rewrite /IntoOr=>->. by rewrite plainly_or. Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
666
Global Instance into_or_persistently P Q1 Q2 :
667 668
  IntoOr P Q1 Q2 
  IntoOr (bi_persistently P) (bi_persistently Q1) (bi_persistently Q2).
Robbert Krebbers's avatar
Robbert Krebbers committed
669
Proof. rewrite /IntoOr=>->. by rewrite persistently_or. Qed.
670
Global Instance into_or_embed `{BiEmbedding PROP PROP'} P Q1 Q2 :
671
  IntoOr P Q1 Q2  IntoOr P Q1 Q2.
672
Proof. by rewrite /IntoOr -bi_embed_or => <-. Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
673 674 675 676 677 678 679

(* FromExist *)
Global Instance from_exist_exist {A} (Φ : A  PROP): FromExist ( a, Φ a) Φ.
Proof. by rewrite /FromExist. Qed.
Global Instance from_exist_pure {A} (φ : A  Prop) :
  @FromExist PROP A  x, φ x (λ a, ⌜φ a)%I.
Proof. by rewrite /FromExist pure_exist. Qed.
680 681 682 683
Global Instance from_exist_affinely {A} P (Φ : A  PROP) :
  FromExist P Φ  FromExist (bi_affinely P) (λ a, bi_affinely (Φ a))%I.
Proof. rewrite /FromExist=> <-. by rewrite affinely_exist. Qed.
Global Instance from_exist_absorbingly {A} P (Φ : A  PROP) :
684
  FromExist P Φ  FromExist (bi_absorbingly P) (λ a, bi_absorbingly (Φ a))%I.
685
Proof. rewrite /FromExist=> <-. by rewrite absorbingly_exist. Qed.
686 687
Global Instance from_exist_plainly {A} P (Φ : A  PROP) :
  FromExist P Φ  FromExist (bi_plainly P) (λ a, bi_plainly (Φ a))%I.
688
Proof. rewrite /FromExist=> <-. by rewrite -plainly_exist_2. Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
689
Global Instance from_exist_persistently {A} P (Φ : A  PROP) :
690
  FromExist P Φ  FromExist (bi_persistently P) (λ a, bi_persistently (Φ a))%I.
Robbert Krebbers's avatar
Robbert Krebbers committed
691
Proof. rewrite /FromExist=> <-. by rewrite persistently_exist. Qed.
692
Global Instance from_exist_embed `{BiEmbedding PROP PROP'} {A} P (Φ : A  PROP) :
693
  FromExist P Φ  FromExist P (λ a, ⎡Φ a%I).