class_instances.v 76.5 KB
Newer Older
1
From iris.proofmode Require Export classes.
Robbert Krebbers's avatar
Robbert Krebbers committed
2
From iris.bi Require Import bi tactics.
3
Set Default Proof Using "Type".
Robbert Krebbers's avatar
Robbert Krebbers committed
4 5
Import bi.

Robbert Krebbers's avatar
Robbert Krebbers committed
6 7 8 9 10 11 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 38 39 40 41 42 43 44 45 46 47 48 49 50 51 52 53 54 55
Section always_modalities.
  Context {PROP : bi}.
  Lemma always_modality_persistently_mixin :
    always_modality_mixin (@bi_persistently PROP) AIEnvId AIEnvClear.
  Proof.
    split; eauto using equiv_entails_sym, persistently_intro, persistently_mono,
      persistently_and, persistently_sep_2 with typeclass_instances.
  Qed.
  Definition always_modality_persistently :=
    AlwaysModality _ always_modality_persistently_mixin.

  Lemma always_modality_affinely_mixin :
    always_modality_mixin (@bi_affinely PROP) AIEnvId (AIEnvForall Affine).
  Proof.
    split; eauto using equiv_entails_sym, affinely_intro, affinely_mono,
      affinely_and, affinely_sep_2 with typeclass_instances.
  Qed.
  Definition always_modality_affinely :=
    AlwaysModality _ always_modality_affinely_mixin.

  Lemma always_modality_affinely_persistently_mixin :
    always_modality_mixin (λ P : PROP,  P)%I AIEnvId AIEnvIsEmpty.
  Proof.
    split; eauto using equiv_entails_sym, affinely_persistently_emp,
      affinely_mono, persistently_mono, affinely_persistently_idemp,
      affinely_persistently_and, affinely_persistently_sep_2 with typeclass_instances.
  Qed.
  Definition always_modality_affinely_persistently :=
    AlwaysModality _ always_modality_affinely_persistently_mixin.

  Lemma always_modality_plainly_mixin :
    always_modality_mixin (@bi_plainly PROP) (AIEnvForall Plain) AIEnvClear.
  Proof.
    split; eauto using equiv_entails_sym, plainly_intro, plainly_mono,
      plainly_and, plainly_sep_2 with typeclass_instances.
  Qed.
  Definition always_modality_plainly :=
    AlwaysModality _ always_modality_plainly_mixin.

  Lemma always_modality_affinely_plainly_mixin :
    always_modality_mixin (λ P : PROP,  P)%I (AIEnvForall Plain) AIEnvIsEmpty.
  Proof.
    split; eauto using equiv_entails_sym, affinely_plainly_emp, affinely_intro,
      plainly_intro, affinely_mono, plainly_mono, affinely_plainly_idemp,
      affinely_plainly_and, affinely_plainly_sep_2 with typeclass_instances.
  Qed.
  Definition always_modality_affinely_plainly :=
    AlwaysModality _ always_modality_affinely_plainly_mixin.
End always_modalities.

Robbert Krebbers's avatar
Robbert Krebbers committed
56 57 58 59
Section bi_instances.
Context {PROP : bi}.
Implicit Types P Q R : PROP.

60 61 62 63 64
(* 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.
65

66 67 68 69 70
(* 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.
71
Global Instance into_absorbingly_default P : IntoAbsorbingly (bi_absorbingly P) P | 100.
72
Proof. by rewrite /IntoAbsorbingly. Qed.
73

74
(* FromAssumption *)
75
Global Instance from_assumption_exact p P : FromAssumption p P P | 0.
76
Proof. by rewrite /FromAssumption /= affinely_persistently_if_elim. Qed.
77

78
Global Instance from_assumption_persistently_r P Q :
79
  FromAssumption true P Q  FromAssumption true P (bi_persistently Q).
Robbert Krebbers's avatar
Robbert Krebbers committed
80 81
Proof.
  rewrite /FromAssumption /= =><-.
82
  by rewrite -{1}affinely_persistently_idemp affinely_elim.
Robbert Krebbers's avatar
Robbert Krebbers committed
83
Qed.
84 85 86 87
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 :
88
  FromAssumption p P Q  FromAssumption p P (bi_absorbingly Q).
89
Proof. rewrite /FromAssumption /= =><-. apply absorbingly_intro. Qed.
90

91 92 93 94 95 96 97 98 99 100 101 102
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.
103
Global Instance from_assumption_plainly_l_false `{BiAffine PROP} P Q :
104 105 106 107 108
  FromAssumption true P Q  FromAssumption false (bi_plainly P) Q.
Proof.
  rewrite /FromAssumption /= =><-.
  by rewrite affine_affinely plainly_elim_persistently.
Qed.
109
Global Instance from_assumption_affinely_persistently_l p P Q :
110
  FromAssumption true P Q  FromAssumption p ( P) Q.
111
Proof. rewrite /FromAssumption /= =><-. by rewrite affinely_persistently_if_elim. Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
112
Global Instance from_assumption_persistently_l_true P Q :
113
  FromAssumption true P Q  FromAssumption true (bi_persistently P) Q.
Robbert Krebbers's avatar
Robbert Krebbers committed
114
Proof. rewrite /FromAssumption /= =><-. by rewrite persistently_idemp. Qed.
115
Global Instance from_assumption_persistently_l_false `{BiAffine PROP} P Q :
116
  FromAssumption true P Q  FromAssumption false (bi_persistently P) Q.
117 118 119 120
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
121 122

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

126 127 128 129
Global Instance from_assumption_bupd `{BUpdFacts PROP} p P Q :
  FromAssumption p P Q  FromAssumption p P (|==> Q).
Proof. rewrite /FromAssumption=>->. apply bupd_intro. Qed.

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

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

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
154
Global Instance into_pure_pure_wand (φ1 φ2 : Prop) P1 P2 :
155 156
  FromPure P1 φ1  IntoPure P2 φ2  IntoPure (P1 - P2) (φ1  φ2).
Proof. rewrite /FromPure /IntoPure=> <- ->. by rewrite pure_impl impl_wand_2. Qed.
157

158 159 160
Global Instance into_pure_affinely P φ :
  IntoPure P φ  IntoPure (bi_affinely P) φ.
Proof. rewrite /IntoPure=> ->. apply affinely_elim. Qed.
161
Global Instance into_pure_absorbingly P φ : IntoPure P φ  IntoPure (bi_absorbingly P) φ.
162
Proof. rewrite /IntoPure=> ->. by rewrite absorbingly_pure. Qed.
163 164
Global Instance into_pure_plainly P φ : IntoPure P φ  IntoPure (bi_plainly P) φ.
Proof. rewrite /IntoPure=> ->. apply: plainly_elim. Qed.
165 166
Global Instance into_pure_persistently P φ :
  IntoPure P φ  IntoPure (bi_persistently P) φ.
167
Proof. rewrite /IntoPure=> ->. apply: persistently_elim. Qed.
168
Global Instance into_pure_embed `{BiEmbedding PROP PROP'} P φ :
169
  IntoPure P φ  IntoPure P φ.
170
Proof. rewrite /IntoPure=> ->. by rewrite bi_embed_pure. Qed.
171

172
(* FromPure *)
173 174 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
Global Instance from_pure_pure φ : @FromPure PROP ⌜φ⌝ φ.
Proof. by rewrite /FromPure. Qed.
Global Instance from_pure_pure_and (φ1 φ2 : Prop) P1 P2 :
  FromPure P1 φ1  FromPure P2 φ2  FromPure (P1  P2) (φ1  φ2).
Proof. rewrite /FromPure pure_and. by intros -> ->. Qed.
Global Instance from_pure_pure_or (φ1 φ2 : Prop) P1 P2 :
  FromPure P1 φ1  FromPure P2 φ2  FromPure (P1  P2) (φ1  φ2).
Proof. rewrite /FromPure pure_or. by intros -> ->. Qed.
Global Instance from_pure_pure_impl (φ1 φ2 : Prop) P1 P2 :
  IntoPure P1 φ1  FromPure P2 φ2  FromPure (P1  P2) (φ1  φ2).
Proof. rewrite /FromPure /IntoPure pure_impl. by intros -> ->. Qed.

Global Instance from_pure_exist {A} (Φ : A  PROP) (φ : A  Prop) :
  ( x, FromPure (Φ x) (φ x))  FromPure ( x, Φ x) ( x, φ x).
Proof. rewrite /FromPure=>Hx. rewrite pure_exist. by setoid_rewrite Hx. Qed.
Global Instance from_pure_forall {A} (Φ : A  PROP) (φ : A  Prop) :
  ( x, FromPure (Φ x) (φ x))  FromPure ( x, Φ x) ( x, φ x).
Proof. rewrite /FromPure=>Hx. rewrite pure_forall. by setoid_rewrite Hx. Qed.

Global Instance from_pure_pure_sep (φ1 φ2 : Prop) P1 P2 :
  FromPure P1 φ1  FromPure P2 φ2  FromPure (P1  P2) (φ1  φ2).
Proof. rewrite /FromPure=> <- <-. by rewrite pure_and persistent_and_sep_1. Qed.
Global Instance from_pure_pure_wand (φ1 φ2 : Prop) P1 P2 :
  IntoPure P1 φ1  FromPure P2 φ2  FromPure (P1 - P2) (φ1  φ2).
Proof.
  rewrite /FromPure /IntoPure=> -> <-.
  by rewrite pure_wand_forall pure_impl pure_impl_forall.
200 201
Qed.

202
Global Instance from_pure_plainly P φ :
203
  FromPure P φ  FromPure (bi_plainly P) φ.
204
Proof. rewrite /FromPure=> <-. by rewrite plainly_pure. Qed.
205 206 207 208 209 210 211 212 213 214 215 216 217 218 219
Global Instance from_pure_persistently P φ :
  FromPure P φ  FromPure (bi_persistently P) φ.
Proof. rewrite /FromPure=> <-. by rewrite persistently_pure. Qed.
Global Instance from_pure_affinely P φ `{!Affine P} :
  FromPure P φ  FromPure (bi_affinely P) φ.
Proof. by rewrite /FromPure affine_affinely. Qed.
Global Instance from_pure_absorbingly P φ : FromPure P φ  FromPure (bi_absorbingly P) φ.
Proof. rewrite /FromPure=> <-. by rewrite absorbingly_pure. Qed.
Global Instance from_pure_embed `{BiEmbedding PROP PROP'} P φ :
  FromPure P φ  FromPure P φ.
Proof. rewrite /FromPure=> <-. by rewrite bi_embed_pure. Qed.

Global Instance from_pure_bupd `{BUpdFacts PROP} P φ :
  FromPure P φ  FromPure (|==> P) φ.
Proof. rewrite /FromPure=> ->. apply bupd_intro. Qed.
220

221
(* IntoPersistent *)
222
Global Instance into_persistent_persistently p P Q :
223
  IntoPersistent true P Q  IntoPersistent p (bi_persistently P) Q | 0.
Robbert Krebbers's avatar
Robbert Krebbers committed
224 225 226 227
Proof.
  rewrite /IntoPersistent /= => ->.
  destruct p; simpl; auto using persistently_idemp_1.
Qed.
228 229 230
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.
231
Global Instance into_persistent_embed `{BiEmbedding PROP PROP'} p P Q :
232 233
  IntoPersistent p P Q  IntoPersistent p P Q | 0.
Proof.
234
  rewrite /IntoPersistent -bi_embed_persistently -bi_embed_persistently_if=> -> //.
235
Qed.
236
Global Instance into_persistent_here P : IntoPersistent true P P | 1.
Robbert Krebbers's avatar
Robbert Krebbers committed
237
Proof. by rewrite /IntoPersistent. Qed.
238 239
Global Instance into_persistent_persistent P :
  Persistent P  IntoPersistent false P P | 100.
240
Proof. intros. by rewrite /IntoPersistent. Qed.
241

242
(* FromAlways *)
Robbert Krebbers's avatar
Robbert Krebbers committed
243 244
Global Instance from_always_affinely P :
  FromAlways always_modality_affinely (bi_affinely P) P | 2.
245
Proof. by rewrite /FromAlways. Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
246 247 248 249 250 251 252 253 254 255 256 257 258 259 260 261 262 263 264 265 266 267 268 269 270 271 272 273 274 275 276 277

Global Instance from_always_persistently P :
  FromAlways always_modality_persistently (bi_persistently P) P | 2.
Proof. by rewrite /FromAlways. Qed.
Global Instance from_always_affinely_persistently P :
  FromAlways always_modality_affinely_persistently ( P) P | 1.
Proof. by rewrite /FromAlways. Qed.
Global Instance from_always_affinely_persistently_affine_bi P :
  BiAffine PROP  FromAlways always_modality_persistently ( P) P | 0.
Proof. intros. by rewrite /FromAlways /= affine_affinely. Qed.

Global Instance from_always_plainly P :
  FromAlways always_modality_plainly (bi_plainly P) P | 2.
Proof. by rewrite /FromAlways. Qed.
Global Instance from_always_affinely_plainly P :
  FromAlways always_modality_affinely_plainly ( P) P | 1.
Proof. by rewrite /FromAlways. Qed.
Global Instance from_always_affinely_plainly_affine_bi P :
  BiAffine PROP  FromAlways always_modality_plainly ( P) P | 0.
Proof. intros. by rewrite /FromAlways /= affine_affinely. Qed.

Global Instance from_always_affinely_embed `{BiEmbedding PROP PROP'} P Q :
  FromAlways always_modality_affinely P Q 
  FromAlways always_modality_affinely P Q.
Proof. rewrite /FromAlways /= =><-. by rewrite bi_embed_affinely. Qed.
Global Instance from_always_persistently_embed `{BiEmbedding PROP PROP'} P Q :
  FromAlways always_modality_persistently P Q 
  FromAlways always_modality_persistently P Q.
Proof. rewrite /FromAlways /= =><-. by rewrite bi_embed_persistently. Qed.
Global Instance from_always_affinely_persistently_embed `{BiEmbedding PROP PROP'} P Q :
  FromAlways always_modality_affinely_persistently P Q 
  FromAlways always_modality_affinely_persistently P Q.
278
Proof.
Robbert Krebbers's avatar
Robbert Krebbers committed
279
  rewrite /FromAlways /= =><-. by rewrite bi_embed_affinely bi_embed_persistently.
280
Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
281 282 283 284 285 286 287
Global Instance from_always_plainly_embed `{BiEmbedding PROP PROP'} P Q :
  FromAlways always_modality_plainly P Q 
  FromAlways always_modality_plainly P Q.
Proof. rewrite /FromAlways /= =><-. by rewrite bi_embed_plainly. Qed.
Global Instance from_always_affinely_plainly_embed `{BiEmbedding PROP PROP'} P Q :
  FromAlways always_modality_affinely_plainly P Q 
  FromAlways always_modality_affinely_plainly P Q.
288
Proof.
Robbert Krebbers's avatar
Robbert Krebbers committed
289
  rewrite /FromAlways /= =><-. by rewrite bi_embed_affinely bi_embed_plainly.
290
Qed.
291

Robbert Krebbers's avatar
Robbert Krebbers committed
292 293 294
(* IntoWand *)
Global Instance into_wand_wand p q P Q P' :
  FromAssumption q P P'  IntoWand p q (P' - Q) P Q.
295
Proof.
296
  rewrite /FromAssumption /IntoWand=> HP. by rewrite HP affinely_persistently_if_elim.
Robbert Krebbers's avatar
Robbert Krebbers committed
297
Qed.
298

299 300
Global Instance into_wand_impl_false_false P Q P' :
  Absorbing P'  Absorbing (P'  Q) 
Robbert Krebbers's avatar
Robbert Krebbers committed
301 302
  FromAssumption false P P'  IntoWand false false (P'  Q) P Q.
Proof.
303
  rewrite /FromAssumption /IntoWand /= => ?? ->. apply wand_intro_r.
Robbert Krebbers's avatar
Robbert Krebbers committed
304 305
  by rewrite sep_and impl_elim_l.
Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
306

Robbert Krebbers's avatar
Robbert Krebbers committed
307
Global Instance into_wand_impl_false_true P Q P' :
308
  Absorbing P'  FromAssumption true P P' 
Robbert Krebbers's avatar
Robbert Krebbers committed
309
  IntoWand false true (P'  Q) P Q.
310
Proof.
311
  rewrite /IntoWand /FromAssumption /= => ? HP. apply wand_intro_l.
312 313
  rewrite -(affinely_persistently_idemp P) HP.
  by rewrite -persistently_and_affinely_sep_l persistently_elim impl_elim_r.
314 315
Qed.

Robbert Krebbers's avatar
Robbert Krebbers committed
316
Global Instance into_wand_impl_true_false P Q P' :
317
  Affine P'  FromAssumption false P P' 
Robbert Krebbers's avatar
Robbert Krebbers committed
318
  IntoWand true false (P'  Q) P Q.
319
Proof.
320
  rewrite /FromAssumption /IntoWand /= => ? HP. apply wand_intro_r.
321 322
  rewrite -persistently_and_affinely_sep_l HP -{2}(affine_affinely P') -affinely_and_lr.
  by rewrite affinely_persistently_elim impl_elim_l.
323
Qed.
324

Robbert Krebbers's avatar
Robbert Krebbers committed
325 326
Global Instance into_wand_impl_true_true P Q P' :
  FromAssumption true P P'  IntoWand true true (P'  Q) P Q.
327
Proof.
Robbert Krebbers's avatar
Robbert Krebbers committed
328
  rewrite /FromAssumption /IntoWand /= => <-. apply wand_intro_l.
329 330
  rewrite -{1}(affinely_persistently_idemp P) -and_sep_affinely_persistently.
  by rewrite -affinely_persistently_and impl_elim_r affinely_persistently_elim.
331
Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
332 333 334 335 336 337 338 339

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.

340 341 342 343 344 345 346 347 348 349 350 351 352
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.
353

Robbert Krebbers's avatar
Robbert Krebbers committed
354 355 356 357
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.

358 359 360 361 362 363
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.
364
Global Instance into_wand_plainly_false `{!BiAffine PROP} q R P Q :
365 366 367 368 369 370
  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
371
Global Instance into_wand_persistently_true q R P Q :
372
  IntoWand true q R P Q  IntoWand true q (bi_persistently R) P Q.
Robbert Krebbers's avatar
Robbert Krebbers committed
373
Proof. by rewrite /IntoWand /= persistently_idemp. Qed.
374
Global Instance into_wand_persistently_false `{!BiAffine PROP} q R P Q :
375
  IntoWand false q R P Q  IntoWand false q (bi_persistently R) P Q.
376
Proof. by rewrite /IntoWand persistently_elim. Qed.
377
Global Instance into_wand_embed `{BiEmbedding PROP PROP'} p q R P Q :
378 379
  IntoWand p q R P Q  IntoWand p q R P Q.
Proof.
380 381
  rewrite /IntoWand -!bi_embed_persistently_if -!bi_embed_affinely_if
          -bi_embed_wand => -> //.
382
Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
383

384 385 386 387 388 389 390 391 392 393 394 395 396 397 398 399 400 401 402 403 404
Global Instance into_wand_bupd `{BUpdFacts PROP} p q R P Q :
  IntoWand false false R P Q  IntoWand p q (|==> R) (|==> P) (|==> Q).
Proof.
  rewrite /IntoWand /= => HR. rewrite !affinely_persistently_if_elim HR.
  apply wand_intro_l. by rewrite bupd_sep wand_elim_r.
Qed.

Global Instance into_wand_bupd_persistent `{BUpdFacts PROP} p q R P Q :
  IntoWand false q R P Q  IntoWand p q (|==> R) P (|==> Q).
Proof.
  rewrite /IntoWand /= => HR. rewrite affinely_persistently_if_elim HR.
  apply wand_intro_l. by rewrite bupd_frame_l wand_elim_r.
Qed.

Global Instance into_wand_bupd_args `{BUpdFacts 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 affinely_persistently_if_elim bupd_wand_r.
Qed.

405 406 407 408 409 410 411 412 413 414 415 416 417 418
(* 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
419 420 421 422
(* 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 :
423
  FromAffinely P1 P1'  Persistent P1'  FromAnd (P1  P2) P1' P2 | 9.
424
Proof.
425
  rewrite /FromAffinely /FromAnd=> <- ?. by rewrite persistent_and_affinely_sep_l_1.
426
Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
427
Global Instance from_and_sep_persistent_r P1 P2 P2' :
428
  FromAffinely P2 P2'  Persistent P2'  FromAnd (P1  P2) P1 P2' | 10.
429
Proof.
430
  rewrite /FromAffinely /FromAnd=> <- ?. by rewrite persistent_and_affinely_sep_r_1.
431
Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
432 433
Global Instance from_and_sep_persistent P1 P2 :
  Persistent P1  Persistent P2  FromAnd (P1  P2) P1 P2 | 11.
434
Proof.
435
  rewrite /FromAffinely /FromAnd. intros ??. by rewrite -persistent_and_sep_1.
436 437
Qed.

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

441 442 443 444 445 446 447 448 449
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
450
Global Instance from_and_persistently P Q1 Q2 :
451 452
  FromAnd P Q1 Q2 
  FromAnd (bi_persistently P) (bi_persistently Q1) (bi_persistently Q2).
Robbert Krebbers's avatar
Robbert Krebbers committed
453 454
Proof. rewrite /FromAnd=> <-. by rewrite persistently_and. Qed.
Global Instance from_and_persistently_sep P Q1 Q2 :
455 456
  FromSep P Q1 Q2 
  FromAnd (bi_persistently P) (bi_persistently Q1) (bi_persistently Q2) | 11.
Robbert Krebbers's avatar
Robbert Krebbers committed
457
Proof. rewrite /FromAnd=> <-. by rewrite -persistently_and persistently_and_sep. Qed.
458

459
Global Instance from_and_embed `{BiEmbedding PROP PROP'} P Q1 Q2 :
460
  FromAnd P Q1 Q2  FromAnd P Q1 Q2.
461
Proof. by rewrite /FromAnd -bi_embed_and => <-. Qed.
462

Robbert Krebbers's avatar
Robbert Krebbers committed
463 464 465
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).
466
Proof. intros. by rewrite /FromAnd big_opL_cons persistent_and_sep_1. Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
467 468 469 470
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).
471
Proof. intros. by rewrite /FromAnd big_opL_app persistent_and_sep_1. Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
472 473 474 475 476

(* 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 :
477
  TCOr (TCAnd (Affine P1) (Affine P2)) (TCAnd (Absorbing P1) (Absorbing P2)) 
Robbert Krebbers's avatar
Robbert Krebbers committed
478 479 480 481 482 483
  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.

484 485 486 487
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 :
488
  FromSep P Q1 Q2  FromSep (bi_absorbingly P) (bi_absorbingly Q1) (bi_absorbingly Q2).
489
Proof. rewrite /FromSep=> <-. by rewrite absorbingly_sep. Qed.
490 491 492 493
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
494
Global Instance from_sep_persistently P Q1 Q2 :
495 496
  FromSep P Q1 Q2 
  FromSep (bi_persistently P) (bi_persistently Q1) (bi_persistently Q2).
497
Proof. rewrite /FromSep=> <-. by rewrite persistently_sep_2. Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
498

499
Global Instance from_sep_embed `{BiEmbedding PROP PROP'} P Q1 Q2 :
500
  FromSep P Q1 Q2  FromSep P Q1 Q2.
501
Proof. by rewrite /FromSep -bi_embed_sep => <-. Qed.
502

Robbert Krebbers's avatar
Robbert Krebbers committed
503 504 505 506 507 508 509
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.
510

511 512 513 514
Global Instance from_sep_bupd `{BUpdFacts PROP} P Q1 Q2 :
  FromSep P Q1 Q2  FromSep (|==> P) (|==> Q1) (|==> Q2).
Proof. rewrite /FromSep=><-. apply bupd_sep. Qed.

Robbert Krebbers's avatar
Robbert Krebbers committed
515
(* IntoAnd *)
516
Global Instance into_and_and p P Q : IntoAnd p (P  Q) P Q | 10.
517
Proof. by rewrite /IntoAnd affinely_persistently_if_and. Qed.
518
Global Instance into_and_and_affine_l P Q Q' :
519
  Affine P  FromAffinely Q' Q  IntoAnd false (P  Q) P Q'.
520 521
Proof.
  intros. rewrite /IntoAnd /=.
522
  by rewrite -(affine_affinely P) affinely_and_l affinely_and (from_affinely Q').
523 524
Qed.
Global Instance into_and_and_affine_r P P' Q :
525
  Affine Q  FromAffinely P' P  IntoAnd false (P  Q) P' Q.
526 527
Proof.
  intros. rewrite /IntoAnd /=.
528
  by rewrite -(affine_affinely Q) affinely_and_r affinely_and (from_affinely P').
529 530
Qed.

531
Global Instance into_and_sep `{BiPositive PROP} P Q : IntoAnd true (P  Q) P Q.
532 533 534
Proof.
  by rewrite /IntoAnd /= persistently_sep -and_sep_persistently persistently_and.
Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
535 536

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

539 540
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
541
Proof.
Robbert Krebbers's avatar
Robbert Krebbers committed
542
  rewrite /IntoAnd. destruct p; simpl.
543 544
  - by rewrite -affinely_and !persistently_affinely.
  - intros ->. by rewrite affinely_and.
Robbert Krebbers's avatar
Robbert Krebbers committed
545
Qed.
546 547 548
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).
549
Proof.
550 551 552 553 554
  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.
555
Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
556
Global Instance into_and_persistently p P Q1 Q2 :
557 558
  IntoAnd p P Q1 Q2 
  IntoAnd p (bi_persistently P) (bi_persistently Q1) (bi_persistently Q2).
Robbert Krebbers's avatar
Robbert Krebbers committed
559
Proof.
Robbert Krebbers's avatar
Robbert Krebbers committed
560 561 562
  rewrite /IntoAnd /=. destruct p; simpl.
  - by rewrite -persistently_and !persistently_idemp.
  - intros ->. by rewrite persistently_and.
Robbert Krebbers's avatar
Robbert Krebbers committed
563
Qed.
564
Global Instance into_and_embed `{BiEmbedding PROP PROP'} p P Q1 Q2 :
565 566
  IntoAnd p P Q1 Q2  IntoAnd p P Q1 Q2.
Proof.
567 568
  rewrite /IntoAnd -bi_embed_and -!bi_embed_persistently_if
          -!bi_embed_affinely_if=> -> //.
569
Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
570

Robbert Krebbers's avatar
Robbert Krebbers committed
571
(* IntoSep *)
572 573
Global Instance into_sep_sep P Q : IntoSep (P  Q) P Q.
Proof. by rewrite /IntoSep. Qed.
574

575
Inductive AndIntoSep : PROP  PROP  PROP  PROP  Prop :=
576 577
  | 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.
578 579 580 581 582 583
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'.
584
Proof.
585
  destruct 2 as [P Q Q'|P Q]; rewrite /IntoSep.
586 587 588
  - 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.
589
Qed.
590 591
Global Instance into_sep_and_persistent_r P P' Q Q' :
  Persistent Q  AndIntoSep Q Q' P P'  IntoSep (P  Q) P' Q'.
592
Proof.
593
  destruct 2 as [Q P P'|Q P]; rewrite /IntoSep.
594 595 596
  - 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.
597
Qed.
598 599


600 601 602
Global Instance into_sep_pure φ ψ : @IntoSep PROP ⌜φ  ψ⌝ ⌜φ⌝ ⌜ψ⌝.
Proof. by rewrite /IntoSep pure_and persistent_and_sep_1. Qed.

603
Global Instance into_sep_embed `{BiEmbedding PROP PROP'} P Q1 Q2 :
604
  IntoSep P Q1 Q2  IntoSep P Q1 Q2.
605
Proof. rewrite /IntoSep -bi_embed_sep=> -> //. Qed.
606

607 608 609 610 611
(* 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 P Q1 Q2 :
  IntoSep P Q1 Q2  IntoSep (bi_affinely P) Q1 Q2 | 20.
Proof. rewrite /IntoSep /= => ->. by rewrite affinely_elim. Qed.
612

613
Global Instance into_sep_plainly `{BiPositive PROP} P Q1 Q2 :
614 615
  IntoSep P Q1 Q2  IntoSep (bi_plainly P) (bi_plainly Q1) (bi_plainly Q2).
Proof. rewrite /IntoSep /= => ->. by rewrite plainly_sep. Qed.
616
Global Instance into_sep_persistently `{BiPositive PROP} P Q1 Q2 :
617 618
  IntoSep P Q1 Q2 
  IntoSep (bi_persistently P) (bi_persistently Q1) (bi_persistently Q2).
619
Proof. rewrite /IntoSep /= => ->. by rewrite persistently_sep. Qed.
620

621 622 623
(* 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. *)
624
Global Instance into_sep_big_sepL_cons {A} (Φ : nat  A  PROP) l x l' :
625
  IsCons l x l' 
626
  IntoSep ([ list] k  y  l, Φ k y)
627
    (Φ 0 x) ([ list] k  y  l', Φ (S k) y).
Robbert Krebbers's avatar
Robbert Krebbers committed
628
Proof. rewrite /IsCons=>->. by rewrite /IntoSep big_sepL_cons. Qed.
629
Global Instance into_sep_big_sepL_app {A} (Φ : nat  A  PROP) l l1 l2 :
630
  IsApp l l1 l2 
631
  IntoSep ([ list] k  y  l, Φ k y)
632
    ([ list] k  y  l1, Φ k y) ([ list] k  y  l2, Φ (length l1 + k) y).
Robbert Krebbers's avatar
Robbert Krebbers committed
633 634 635 636 637 638 639
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.
640 641 642 643
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 :
644
  FromOr P Q1 Q2  FromOr (bi_absorbingly P) (bi_absorbingly Q1) (bi_absorbingly Q2).
645
Proof. rewrite /FromOr=> <-. by rewrite absorbingly_or. Qed.
646 647
Global Instance from_or_plainly P Q1 Q2 :
  FromOr P Q1 Q2  FromOr (bi_plainly P) (bi_plainly Q1) (bi_plainly Q2).
648
Proof. rewrite /FromOr=> <-. by rewrite -plainly_or_2. Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
649
Global Instance from_or_persistently P Q1 Q2 :
650 651
  FromOr P Q1 Q2 
  FromOr (bi_persistently P) (bi_persistently Q1) (bi_persistently Q2).
Robbert Krebbers's avatar
Robbert Krebbers committed
652
Proof. rewrite /FromOr=> <-. by rewrite persistently_or. Qed.
653
Global Instance from_or_embed `{BiEmbedding PROP PROP'} P Q1 Q2 :
654
  FromOr P Q1 Q2  FromOr P Q1 Q2.
655
Proof. by rewrite /FromOr -bi_embed_or => <-. Qed.
656 657 658 659 660 661
Global Instance from_or_bupd `{BUpdFacts PROP} P Q1 Q2 :
  FromOr P Q1 Q2  FromOr (|==> P) (|==> Q1) (|==> Q2).
Proof.
  rewrite /FromOr=><-.
  apply or_elim; apply bupd_mono; auto using or_intro_l, or_intro_r.
Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
662 663 664 665 666 667

(* 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.
668 669 670 671
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 :
672
  IntoOr P Q1 Q2  IntoOr (bi_absorbingly P) (bi_absorbingly Q1) (bi_absorbingly Q2).
673
Proof. rewrite /IntoOr=>->. by rewrite absorbingly_or. Qed.
674
Global Instance into_or_plainly `{BiPlainlyExist PROP} P Q1 Q2 :
675 676
  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
677
Global Instance into_or_persistently P Q1 Q2 :
678 679
  IntoOr P Q1 Q2 
  IntoOr (bi_persistently P) (bi_persistently Q1) (bi_persistently Q2).
Robbert Krebbers's avatar
Robbert Krebbers committed
680
Proof. rewrite /IntoOr=>->. by rewrite persistently_or. Qed.
681
Global Instance into_or_embed `{BiEmbedding PROP PROP'} P Q1 Q2 :
682
  IntoOr P Q1 Q2  IntoOr P Q1 Q2.
683
Proof. by rewrite /IntoOr -bi_embed_or => <-. Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
684 685 686 687 688 689 690

(* 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.
691 692 693 694
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) :
695
  FromExist P Φ  FromExist (bi_absorbingly P) (λ a, bi_absorbingly (Φ a))%I.
696
Proof. rewrite /FromExist=> <-. by rewrite absorbingly_exist. Qed.
697 698
Global Instance from_exist_plainly {A} P (Φ : A  PROP) :
  FromExist P Φ  FromExist (bi_plainly P) (λ a, bi_plainly (Φ a))%I.
699
Proof. rewrite /FromExist=> <-. by rewrite -plainly_exist_2. Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
700
Global Instance from_exist_persistently {A} P (Φ : A  PROP) :
701
  FromExist P Φ  FromExist (bi_persistently P) (λ a, bi_persistently (Φ a))%I.
Robbert Krebbers's avatar
Robbert Krebbers committed
702
Proof. rewrite /FromExist=> <-. by rewrite persistently_exist. Qed.
703
Global Instance from_exist_embed `{BiEmbedding PROP PROP'} {A} P (Φ : A  PROP) :
704
  FromExist P Φ  FromExist P (λ a, ⎡Φ a%I).
705
Proof. by rewrite /FromExist -bi_embed_exist => <-. Qed.
706 707 708 709 710
Global Instance from_exist_bupd `{BUpdFacts PROP} {A} P (Φ : A  PROP) :
  FromExist P Φ  FromExist (|==> P) (λ a, |==> Φ a)%I.
Proof.
  rewrite /FromExist=><-. apply exist_elim=> a. by rewrite -(exist_intro a).
Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
711 712 713 714 715 716 717

(* IntoExist *)
Global Instance into_exist_exist {A} (Φ : A  PROP) : IntoExist ( a, Φ a) Φ.
Proof. by rewrite /IntoExist. Qed.
Global Instance into_exist_pure {A} (φ : A  Prop) :
  @IntoExist PROP A  x, φ x (λ a, ⌜φ a)%I.
Proof. by rewrite /IntoExist pure_exist. Qed.
718 719 720
Global Instance into_exist_affinely {A} P (Φ : A  PROP) :
  IntoExist P Φ  IntoExist (bi_affinely P) (λ a, bi_affinely (Φ a))%I.
Proof. rewrite /IntoExist=> HP. by rewrite HP affinely_exist. Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
721 722 723 724 725 726 727 728 729 730
Global Instance into_exist_and_pure P Q φ :
  IntoPureT P φ  IntoExist (P  Q) (λ _ : φ, Q).
Proof.
  intros (φ'&->&?). rewrite /IntoExist (into_pure P).
  apply pure_elim_l=> Hφ. by rewrite -(exist_intro Hφ).
Qed.
Global Instance into_exist_sep_pure P Q φ :
  TCOr (Affine P) (Absorbing Q)  IntoPureT P φ  IntoExist (P  Q) (λ _ : φ, Q).
Proof.
  intros ? (φ'&->&?). rewrite /IntoExist.
Robbert Krebbers's avatar
Robbert Krebbers committed
731
  eapply (pure_elim φ'); [by rewrite (into_pure P); apply sep_elim_l, _|]=>?.
Robbert Krebbers's avatar
Robbert Krebbers committed
732 733
  rewrite -exist_intro //. apply sep_elim_r, _.
Qed.
734
Global Instance into_exist_absorbingly {A} P (Φ : A  PROP) :
735
  IntoExist P Φ  IntoExist (bi_absorbingly P) (λ a, bi_absorbingly (Φ a))%I.
736
Proof. rewrite /IntoExist=> HP. by rewrite HP absorbingly_exist. Qed.
737
Global Instance into_exist_plainly `{BiPlainlyExist PROP} {A} P (Φ : A  PROP) :
738 739
  IntoExist P Φ  IntoExist (bi_plainly P) (λ a, bi_plainly (Φ a))%I.
Proof. rewrite /IntoExist=> HP. by rewrite HP plainly_exist. Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
740
Global Instance into_exist_persistently {A} P (Φ : A  PROP) :
741
  IntoExist P Φ  IntoExist (bi_persistently P) (λ a, bi_persistently (Φ a))%I.
Robbert Krebbers's avatar
Robbert Krebbers committed
742
Proof. rewrite /IntoExist=> HP. by rewrite HP persistently_exist. Qed.
743
Global Instance into_exist_embed `{BiEmbedding PROP PROP'} {A} P (Φ : A  PROP) :
744
  IntoExist P Φ  IntoExist P (λ a, ⎡Φ a%I).
745
Proof. by rewrite /IntoExist -bi_embed_exist => <-. Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
746 747 748 749

(* IntoForall *)
Global Instance into_forall_forall {A} (Φ : A  PROP) : IntoForall ( a, Φ a) Φ.
Proof. by rewrite /IntoForall. Qed.
750 751 752
Global Instance into_forall_affinely {A} P (Φ : A  PROP) :
  IntoForall P Φ  IntoForall (bi_affinely P) (λ a, bi_affinely (Φ a))%I.
Proof. rewrite /IntoForall=> HP. by rewrite HP affinely_forall. Qed.
753 754 755
Global Instance into_forall_plainly {A} P (Φ : A  PROP) :
  IntoForall P Φ  IntoForall (bi_plainly P) (λ a, bi_plainly (Φ a))%I.
Proof. rewrite /IntoForall=> HP. by rewrite HP plainly_forall. Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
756
Global Instance into_forall_persistently {A} P (Φ : A  PROP) :
757
  IntoForall P Φ  IntoForall (bi_persistently P) (λ a, bi_persistently (Φ a))%I.
Robbert Krebbers's avatar
Robbert Krebbers committed
758
Proof. rewrite /IntoForall=> HP. by rewrite HP persistently_forall. Qed.
759
Global Instance into_forall_embed `{BiEmbedding PROP PROP'} {A} P (Φ : A  PROP) :
760
  IntoForall P Φ  IntoForall P (λ a, ⎡Φ a%I).
761
Proof. by rewrite /IntoForall -bi_embed_forall => <-. Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
762 763 764 765 766 767 768 769

(* FromForall *)
Global Instance from_forall_forall {A} (Φ : A  PROP) :
  FromForall ( x, Φ x)%I Φ.
Proof. by rewrite /FromForall. Qed.
Global Instance from_forall_pure {A} (φ : A  Prop) :
  @FromForall PROP A ( a : A, φ a)%I (λ a,  φ a )%I.
Proof. by rewrite /FromForall pure_forall. Qed.
770 771 772
Global Instance from_forall_pure_not (φ : Prop) :
  @FromForall PROP φ (¬ φ⌝)%I (λ a : φ, False)%I.
Proof. by rewrite /FromForall pure_forall. Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
773 774 775 776 777 778 779 780 781 782
Global Instance from_forall_impl_pure P Q φ :
  IntoPureT P φ  FromForall (P  Q)%I (λ _ : φ, Q)%I.
Proof.
  intros (φ'&->&?). by rewrite /FromForall -pure_impl_forall (into_pure P).
Qed.
Global Instance from_forall_wand_pure P Q φ :
  TCOr (Affine P) (Absorbing Q)  IntoPureT P φ 
  FromForall (P - Q)%I (λ _ : φ, Q)%I.
Proof.
  intros [|] (φ'&->&?); rewrite /FromForall; apply wand_intro_r.
783
  - rewrite -(affine_affinely P) (into_pure P) -persistent_and_affinely_sep_r.
Robbert Krebbers's avatar
Robbert Krebbers committed
784 785 786 787
    apply pure_elim_r=>?. by rewrite forall_elim.
  - by rewrite (into_pure P) -pure_wand_forall wand_elim_l.
Qed.

788
Global Instance from_forall_affinely `{BiAffine PROP} {A} P (Φ : A  PROP) :
789 790 791 792
  FromForall P Φ  FromForall (bi_affinely P)%I (λ a, bi_affinely (Φ a))%I.
Proof.
  rewrite /FromForall=> <-. rewrite affine_affinely. by setoid_rewrite affinely_elim.
Qed.
793 794 795
Global Instance from_forall_plainly {A} P (Φ : A  PROP) :
  FromForall P Φ  FromForall (bi_plainly P)%I (λ a, bi_plainly (Φ a))%I.
Proof. rewrite /FromForall=> <-. by rewrite plainly_forall. Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
796
Global Instance from_forall_persistently {A} P (Φ : A  PROP) :
797
  FromForall P Φ  FromForall (bi_persistently P)%I (λ a, bi_persistently (Φ a))%I.
Robbert Krebbers's avatar
Robbert Krebbers committed
798
Proof. rewrite /FromForall=> <-. by rewrite persistently_forall. Qed.
799
Global Instance from_forall_embed `{BiEmbedding PROP PROP'} {A} P (Φ : A  PROP) :
800
  FromForall P Φ  FromForall P%I (λ a, ⎡Φ a%I).
Jacques-Henri Jourdan's avatar