Library iris.proofmode.class_instances_bi

From stdpp Require Import nat_cancel.
From iris.bi Require Import bi tactics telescopes.
From iris.proofmode Require Import base modality_instances classes ltac_tactics.
Set Default Proof Using "Type".
Import bi.

The lemma from_assumption_exact is not an instance, but defined using [notypeclasses refine] through [Hint Extern] to enable the better unification algorithm. We use [shelve] to avoid the creation of unshelved goals for evars by [refine], which otherwise causes TC search to fail. Such unshelved goals are created for example when solving [FromAssumption p ?P ?Q] where both [?P] and [?Q] are evars. See [test_iApply_evar] in [tests/proofmode] for an example.
Lemma from_assumption_exact {PROP : bi} p (P : PROP) : FromAssumption p P P.
Proof. by rewrite /FromAssumption /= intuitionistically_if_elim. Qed.
Hint Extern 0 (FromAssumption _ _ _) ⇒
  notypeclasses refine (from_assumption_exact _ _); shelve : typeclass_instances.

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

AsEmpValid
Global Instance as_emp_valid_emp_valid P : AsEmpValid0 (bi_emp_valid P) P | 0.
Proof. by rewrite /AsEmpValid. Qed.
Global Instance as_emp_valid_entails P Q : AsEmpValid0 (P Q) (P -∗ Q).
Proof. split. apply bi.entails_wand. apply bi.wand_entails. Qed.
Global Instance as_emp_valid_equiv P Q : 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 /AsEmpValidH1. splitH2.
  - apply bi.forall_intro=>?. apply H1, H2.
  - intros x. apply H1. revert H2. by rewrite (bi.forall_elim x).
Qed.

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.

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 (<affine> P) P | 100.
Proof. by rewrite /FromAffinely. Qed.
Global Instance from_affinely_intuitionistically P :
  FromAffinely ( P) (<pers> P) | 100.
Proof. by rewrite /FromAffinely. Qed.

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.
Global Instance into_absorbingly_intuitionistically P :
  IntoAbsorbingly (<pers> P) ( P) | 2.
Proof.
  by rewrite /IntoAbsorbingly -absorbingly_intuitionistically_into_persistently.
Qed.
Global Instance into_absorbingly_default P : IntoAbsorbingly (<absorb> P) P | 100.
Proof. by rewrite /IntoAbsorbingly. Qed.

FromAssumption
Global Instance from_assumption_persistently_r P Q :
  FromAssumption true P Q KnownRFromAssumption true P (<pers> Q).
Proof.
  rewrite /KnownRFromAssumption /FromAssumption /= =><-.
  apply intuitionistically_persistent.
Qed.
Global Instance from_assumption_affinely_r P Q :
  FromAssumption true P Q KnownRFromAssumption true P (<affine> Q).
Proof.
  rewrite /KnownRFromAssumption /FromAssumption /= =><-.
  by rewrite affinely_idemp.
Qed.
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.
Global Instance from_assumption_absorbingly_r p P Q :
  FromAssumption p P Q KnownRFromAssumption p P (<absorb> Q).
Proof.
  rewrite /KnownRFromAssumption /FromAssumption /= =><-.
  apply absorbingly_intro.
Qed.

Global Instance from_assumption_intuitionistically_l p P Q :
  FromAssumption true P Q KnownLFromAssumption p ( P) Q.
Proof.
  rewrite /KnownLFromAssumption /FromAssumption /= =><-.
  by rewrite intuitionistically_if_elim.
Qed.
Global Instance from_assumption_persistently_l_true P Q :
  FromAssumption true P Q KnownLFromAssumption true (<pers> P) Q.
Proof.
  rewrite /KnownLFromAssumption /FromAssumption /= =><-.
  rewrite intuitionistically_persistently_elim //.
Qed.
Global Instance from_assumption_persistently_l_false `{BiAffine PROP} P Q :
  FromAssumption true P Q KnownLFromAssumption false (<pers> P) Q.
Proof.
  rewrite /KnownLFromAssumption /FromAssumption /= =><-.
  by rewrite intuitionistically_into_persistently.
Qed.
Global Instance from_assumption_affinely_l_true p P Q :
  FromAssumption p P Q KnownLFromAssumption p (<affine> P) Q.
Proof.
  rewrite /KnownLFromAssumption /FromAssumption /= =><-.
  by rewrite affinely_elim.
Qed.
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.

Global Instance from_assumption_forall {A} p (Φ : A PROP) Q x :
  FromAssumption p (Φ x) Q KnownLFromAssumption p ( x, Φ x) Q.
Proof.
  rewrite /KnownLFromAssumption /FromAssumption⇒ <-.
  by rewrite forall_elim.
Qed.

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.

IntoPure
Global Instance into_pure_pure φ : @IntoPure PROP φ φ.
Proof. by rewrite /IntoPure. Qed.

Global Instance into_pure_pure_and (φ1 φ2 : Prop) P1 P2 :
  IntoPure P1 φ1 IntoPure P2 φ2 IntoPure (P1 P2) (φ1 φ2).
Proof. rewrite /IntoPure pure_and. by intros → →. Qed.
Global Instance into_pure_pure_or (φ1 φ2 : Prop) P1 P2 :
  IntoPure P1 φ1 IntoPure P2 φ2 IntoPure (P1 P2) (φ1 φ2).
Proof. rewrite /IntoPure pure_or. by intros → →. Qed.
Global Instance into_pure_pure_impl (φ1 φ2 : Prop) P1 P2 :
  FromPure false P1 φ1 IntoPure P2 φ2 IntoPure (P1 P2) (φ1 φ2).
Proof. rewrite /FromPure /IntoPure pure_impl⇒ <- → //. Qed.

Global Instance into_pure_exist {A} (Φ : A PROP) (φ : A Prop) :
  ( x, IntoPure (Φ x) (φ x)) IntoPure ( x, Φ x) ( x, φ x).
Proof. rewrite /IntoPureHx. 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 /IntoPureHx. 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.
Global Instance into_pure_pure_wand a (φ1 φ2 : Prop) P1 P2 :
  FromPure a P1 φ1 IntoPure P2 φ2 IntoPure (P1 -∗ P2) (φ1 φ2).
Proof.
  rewrite /FromPure /IntoPure⇒ <- → /=. rewrite pure_impl.
  apply impl_intro_l, pure_elim_l⇒ ?. rewrite (pure_True φ1) //.
  by rewrite -affinely_affinely_if affinely_True_emp affinely_emp left_id.
Qed.

Global Instance into_pure_affinely P φ : IntoPure P φ IntoPure (<affine> P) φ.
Proof. rewrite /IntoPure⇒ →. apply affinely_elim. Qed.
Global Instance into_pure_intuitionistically P φ :
  IntoPure P φ IntoPure ( P) φ.
Proof. rewrite /IntoPure⇒ →. apply intuitionistically_elim. Qed.
Global Instance into_pure_absorbingly P φ : IntoPure P φ IntoPure (<absorb> P) φ.
Proof. rewrite /IntoPure⇒ →. by rewrite absorbingly_pure. Qed.
Global Instance into_pure_persistently P φ :
  IntoPure P φ IntoPure (<pers> P) φ.
Proof. rewrite /IntoPure⇒ →. apply: persistently_elim. Qed.
Global Instance into_pure_embed `{BiEmbed PROP PROP'} P φ :
  IntoPure P φ IntoPure P φ.
Proof. rewrite /IntoPure⇒ →. by rewrite embed_pure. Qed.

FromPure
Global Instance from_pure_emp : @FromPure PROP true emp True.
Proof. rewrite /FromPure /=. apply (affine _). Qed.
Global Instance from_pure_pure φ : @FromPure PROP false φ φ.
Proof. by rewrite /FromPure /=. Qed.
Global Instance from_pure_pure_and a1 a2 (φ1 φ2 : Prop) P1 P2 :
  FromPure a1 P1 φ1 FromPure a2 P2 φ2
  FromPure (if a1 then true else a2) (P1 P2) (φ1 φ2).
Proof.
  rewrite /FromPure pure_and⇒ <- <- /=. rewrite affinely_if_and.
  f_equiv; apply affinely_if_flag_mono; destruct a1; naive_solver.
Qed.
Global Instance from_pure_pure_or a1 a2 (φ1 φ2 : Prop) P1 P2 :
  FromPure a1 P1 φ1 FromPure a2 P2 φ2
  FromPure (if a1 then true else a2) (P1 P2) (φ1 φ2).
Proof.
  rewrite /FromPure pure_or⇒ <- <- /=. rewrite affinely_if_or.
  f_equiv; apply affinely_if_flag_mono; destruct a1; naive_solver.
Qed.
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 /FromPureHx. 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 /FromPureHx. rewrite pure_forall. setoid_rewrite <-Hx.
  destruct a=>//=. apply affinely_forall.
Qed.

Global Instance from_pure_pure_sep_true a1 a2 (φ1 φ2 : Prop) P1 P2 :
  FromPure a1 P1 φ1 FromPure a2 P2 φ2
  FromPure (if a1 then a2 else false) (P1 P2) (φ1 φ2).
Proof.
  rewrite /FromPure⇒ <- <-. destruct a1; simpl.
  - by rewrite pure_and -persistent_and_affinely_sep_l affinely_if_and_r.
  - by rewrite pure_and -affinely_affinely_if -persistent_and_affinely_sep_r_1.
Qed.
Global Instance from_pure_pure_wand a (φ1 φ2 : Prop) P1 P2 :
  IntoPure P1 φ1 FromPure a P2 φ2
  TCOr (TCEq a false) (Affine P1)
  FromPure a (P1 -∗ P2) (φ1 φ2).
Proof.
  rewrite /FromPure /IntoPureHP1 <- Ha /=. apply wand_intro_l.
  destruct a; simpl.
  - destruct Ha as [Ha|?]; first inversion Ha.
    rewrite -persistent_and_affinely_sep_r -(affine_affinely P1) HP1.
    by rewrite affinely_and_l pure_impl impl_elim_r.
  - by rewrite HP1 sep_and pure_impl impl_elim_r.
Qed.

Global Instance from_pure_persistently P a φ :
  FromPure true P φ FromPure a (<pers> P) φ.
Proof.
  rewrite /FromPure⇒ <- /=.
  by rewrite persistently_affinely_elim affinely_if_elim persistently_pure.
Qed.
Global Instance from_pure_affinely_true a P φ :
  FromPure a P φ FromPure true (<affine> P) φ.
Proof. rewrite /FromPure=><- /=. by rewrite -affinely_affinely_if affinely_idemp. Qed.
Global Instance from_pure_intuitionistically_true a P φ :
  FromPure a P φ FromPure true ( P) φ.
Proof.
  rewrite /FromPure=><- /=.
  rewrite -intuitionistically_affinely_elim -affinely_affinely_if affinely_idemp.
  by rewrite intuitionistic_intuitionistically.
Qed.
Global Instance from_pure_absorbingly a P φ :
  FromPure a P φ FromPure false (<absorb> P) φ.
Proof.
  rewrite /FromPure⇒ <- /=. rewrite -affinely_affinely_if.
  by rewrite -persistent_absorbingly_affinely_2.
Qed.
Global Instance from_pure_embed `{BiEmbed PROP PROP'} a P φ :
  FromPure a P φ FromPure a P φ.
Proof. rewrite /FromPure⇒ <-. by rewrite -embed_pure embed_affinely_if_2. Qed.

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

IntoPersistent
Global Instance into_persistent_persistently p P Q :
  IntoPersistent true P Q IntoPersistent p (<pers> P) Q | 0.
Proof.
  rewrite /IntoPersistent /= ⇒ →.
  destruct p; simpl; auto using persistently_idemp_1.
Qed.
Global Instance into_persistent_affinely p P Q :
  IntoPersistent p P Q IntoPersistent p (<affine> P) Q | 0.
Proof. rewrite /IntoPersistent /= ⇒ <-. by rewrite affinely_elim. Qed.
Global Instance into_persistent_intuitionistically p P Q :
  IntoPersistent true P Q IntoPersistent p ( P) Q | 0.
Proof.
  rewrite /IntoPersistent /= =><-.
  destruct p; simpl;
    eauto using persistently_mono, intuitionistically_elim,
    intuitionistically_into_persistently_1.
Qed.
Global Instance into_persistent_embed `{BiEmbed PROP PROP'} p P Q :
  IntoPersistent p P Q IntoPersistent p P Q | 0.
Proof.
  rewrite /IntoPersistent -embed_persistently -embed_persistently_if⇒ → //.
Qed.
Global Instance into_persistent_here P : IntoPersistent true P P | 1.
Proof. by rewrite /IntoPersistent. Qed.
Global Instance into_persistent_persistent P :
  Persistent P IntoPersistent false P P | 100.
Proof. intros. by rewrite /IntoPersistent. Qed.

FromModal
Global Instance from_modal_affinely P :
  FromModal modality_affinely (<affine> P) (<affine> P) P | 2.
Proof. by rewrite /FromModal. Qed.

Global Instance from_modal_persistently P :
  FromModal modality_persistently (<pers> P) (<pers> P) P | 2.
Proof. by rewrite /FromModal. Qed.
Global Instance from_modal_intuitionistically P :
  FromModal modality_intuitionistically ( P) ( P) P | 1.
Proof. by rewrite /FromModal. Qed.
Global Instance from_modal_intuitionistically_affine_bi P :
  BiAffine PROP FromModal modality_persistently ( P) ( P) P | 0.
Proof.
  intros. by rewrite /FromModal /= intuitionistically_into_persistently.
Qed.

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

Global Instance from_modal_embed `{BiEmbed PROP PROP'} (P : PROP) :
  FromModal (@modality_embed PROP PROP' _) P P P.
Proof. by rewrite /FromModal. Qed.

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

Global Instance from_modal_affinely_embed `{BiEmbed PROP PROP'} `(sel : A) P Q :
  FromModal modality_affinely sel P Q
  FromModal modality_affinely sel P Q | 100.
Proof. rewrite /FromModal /= =><-. by rewrite embed_affinely_2. Qed.
Global Instance from_modal_persistently_embed `{BiEmbed PROP PROP'} `(sel : A) P Q :
  FromModal modality_persistently sel P Q
  FromModal modality_persistently sel P Q | 100.
Proof. rewrite /FromModal /= =><-. by rewrite embed_persistently. Qed.
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.
Proof. rewrite /FromModal /= =><-. by rewrite embed_intuitionistically_2. Qed.

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

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

Global Instance into_wand_wand p q P Q P' :
  FromAssumption q P P' IntoWand p q (P' -∗ Q) P Q.
Proof.
  rewrite /FromAssumption /IntoWandHP. by rewrite HP intuitionistically_if_elim.
Qed.
Global Instance into_wand_impl_false_false P Q P' :
  Absorbing P' Absorbing (P' Q)
  FromAssumption false P P' IntoWand false false (P' Q) P Q.
Proof.
  rewrite /FromAssumption /IntoWand /= ⇒ ?? →. apply wand_intro_r.
  by rewrite sep_and impl_elim_l.
Qed.
Global Instance into_wand_impl_false_true P Q P' :
  Absorbing P' FromAssumption true P P'
  IntoWand false true (P' Q) P Q.
Proof.
  rewrite /IntoWand /FromAssumption /= ⇒ ? HP. apply wand_intro_l.
  rewrite -(intuitionistically_idemp P) HP.
  by rewrite -persistently_and_intuitionistically_sep_l persistently_elim impl_elim_r.
Qed.
Global Instance into_wand_impl_true_false P Q P' :
  Affine P' FromAssumption false P P'
  IntoWand true false (P' Q) P Q.
Proof.
  rewrite /FromAssumption /IntoWand /= ⇒ ? HP. apply wand_intro_r.
  rewrite HP sep_and intuitionistically_elim impl_elim_l //.
Qed.
Global Instance into_wand_impl_true_true P Q P' :
  FromAssumption true P P' IntoWand true true (P' Q) P Q.
Proof.
  rewrite /FromAssumption /IntoWand /= ⇒ <-. apply wand_intro_l.
  rewrite sep_and [( (_ _))%I]intuitionistically_elim impl_elim_r //.
Qed.

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

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.

Global Instance into_wand_forall_prop_true p (φ : Prop) P :
  IntoWand p true ( _ : φ, P) φ P.
Proof.
  rewrite /IntoWand (intuitionistically_if_elim p) /=
          -impl_wand_intuitionistically -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 (intuitionistically_if_elim p) /= pure_wand_forall //.
Qed.

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.

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.

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

Global Instance into_wand_intuitionistically p q R P Q :
  IntoWand true q R P Q IntoWand p q ( R) P Q.
Proof. rewrite /IntoWand /= ⇒ →. by rewrite {1}intuitionistically_if_elim. Qed.
Global Instance into_wand_persistently_true q R P Q :
  IntoWand true q R P Q IntoWand true q (<pers> R) P Q.
Proof. by rewrite /IntoWand /= intuitionistically_persistently_elim. Qed.
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.

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.

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.

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.

FromWand
Global Instance from_wand_wand P1 P2 : FromWand (P1 -∗ P2) P1 P2.
Proof. by rewrite /FromWand. Qed.
Global Instance from_wand_wandM mP1 P2 :
  FromWand (mP1 -∗? P2) (default emp mP1)%I P2.
Proof. by rewrite /FromWand wandM_sound. Qed.
Global Instance from_wand_embed `{BiEmbed PROP PROP'} P Q1 Q2 :
  FromWand P Q1 Q2 FromWand P Q1 Q2.
Proof. by rewrite /FromWand -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 `{BiEmbed PROP PROP'} P Q1 Q2 :
  FromImpl P Q1 Q2 FromImpl P Q1 Q2.
Proof. by rewrite /FromImpl -embed_impl ⇒ <-. Qed.

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 :
  Persistent P1 IntoAbsorbingly P1' P1 FromAnd (P1 P2) P1' P2 | 9.
Proof.
  rewrite /IntoAbsorbingly /FromAnd⇒ ? →.
  rewrite persistent_and_affinely_sep_l_1 {1}(persistent_persistently_2 P1).
  by rewrite absorbingly_elim_persistently -{2}(intuitionistically_elim P1).
Qed.
Global Instance from_and_sep_persistent_r P1 P2 P2' :
  Persistent P2 IntoAbsorbingly P2' P2 FromAnd (P1 P2) P1 P2' | 10.
Proof.
  rewrite /IntoAbsorbingly /FromAnd⇒ ? →.
  rewrite persistent_and_affinely_sep_r_1 {1}(persistent_persistently_2 P2).
  by rewrite absorbingly_elim_persistently -{2}(intuitionistically_elim P2).
Qed.

Global Instance from_and_pure φ ψ : @FromAnd PROP φ ψ φ ψ.
Proof. by rewrite /FromAnd pure_and. Qed.

Global Instance from_and_persistently P Q1 Q2 :
  FromAnd P Q1 Q2
  FromAnd (<pers> P) (<pers> Q1) (<pers> Q2).
Proof. rewrite /FromAnd⇒ <-. by rewrite persistently_and. Qed.
Global Instance from_and_persistently_sep P Q1 Q2 :
  FromSep P Q1 Q2
  FromAnd (<pers> P) (<pers> Q1) (<pers> Q2) | 11.
Proof. rewrite /FromAnd⇒ <-. by rewrite -persistently_and persistently_and_sep. Qed.

Global Instance from_and_embed `{BiEmbed PROP PROP'} P Q1 Q2 :
  FromAnd P Q1 Q2 FromAnd P Q1 Q2.
Proof. by rewrite /FromAnd -embed_and ⇒ <-. Qed.

Global Instance from_and_big_sepL_cons_persistent {A} (Φ : nat A PROP) l x l' :
  IsCons l x l'
  Persistent (Φ 0 x)
  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
  ( k y, Persistent (Φ k y))
  FromAnd ([∗ list] k y l, Φ k y)
    ([∗ list] k y l1, Φ k y) ([∗ list] k y l2, Φ (length l1 + k) y).
Proof. rewrite /IsApp⇒ → ?. by rewrite /FromAnd big_sepL_app persistent_and_sep_1. Qed.

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.

Global Instance from_and_big_sepMS_disj_union_persistent
    `{Countable A} (Φ : A PROP) X1 X2 :
  ( y, Persistent (Φ y))
  FromAnd ([∗ mset] y X1 X2, Φ y) ([∗ mset] y X1, Φ y) ([∗ mset] y X2, Φ y).
Proof. intros. by rewrite /FromAnd big_sepMS_disj_union persistent_and_sep_1. Qed.

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 :
  TCOr (Affine P1) (Absorbing P2) TCOr (Absorbing P1) (Affine P2)
  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.

Global Instance from_sep_affinely P Q1 Q2 :
  FromSep P Q1 Q2 FromSep (<affine> P) (<affine> Q1) (<affine> Q2).
Proof. rewrite /FromSep⇒ <-. by rewrite affinely_sep_2. Qed.
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.
Global Instance from_sep_absorbingly P Q1 Q2 :
  FromSep P Q1 Q2 FromSep (<absorb> P) (<absorb> Q1) (<absorb> Q2).
Proof. rewrite /FromSep⇒ <-. by rewrite absorbingly_sep. Qed.
Global Instance from_sep_persistently P Q1 Q2 :
  FromSep P Q1 Q2
  FromSep (<pers> P) (<pers> Q1) (<pers> Q2).
Proof. rewrite /FromSep⇒ <-. by rewrite persistently_sep_2. Qed.

Global Instance from_sep_embed `{BiEmbed PROP PROP'} P Q1 Q2 :
  FromSep P Q1 Q2 FromSep P Q1 Q2.
Proof. by rewrite /FromSep -embed_sep ⇒ <-. Qed.

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)
    ([∗ list] k y l1, Φ k y) ([∗ list] k y l2, Φ (length l1 + k) y).
Proof. rewrite /IsApp⇒ →. by rewrite /FromSep big_opL_app. Qed.

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.

Global Instance from_sep_big_sepMS_disj_union `{Countable A} (Φ : A PROP) X1 X2 :
  FromSep ([∗ mset] y X1 X2, Φ y) ([∗ mset] y X1, Φ y) ([∗ mset] y X2, Φ y).
Proof. by rewrite /FromSep big_sepMS_disj_union. Qed.

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.

IntoAnd
Global Instance into_and_and p P Q : IntoAnd p (P Q) P Q | 10.
Proof. by rewrite /IntoAnd intuitionistically_if_and. Qed.
Global Instance into_and_and_affine_l P Q Q' :
  Affine P FromAffinely Q' Q IntoAnd false (P Q) P Q'.
Proof.
  intros. rewrite /IntoAnd /=.
  by rewrite -(affine_affinely P) affinely_and_l affinely_and (from_affinely Q').
Qed.
Global Instance into_and_and_affine_r P P' Q :
  Affine Q FromAffinely P' P IntoAnd false (P Q) P' Q.
Proof.
  intros. rewrite /IntoAnd /=.
  by rewrite -(affine_affinely Q) affinely_and_r affinely_and (from_affinely P').
Qed.

Global Instance into_and_sep `{BiPositive PROP} P Q : IntoAnd true (P Q) P Q.
Proof.
  rewrite /IntoAnd /= intuitionistically_sep -and_sep_intuitionistically intuitionistically_and //.
Qed.
Global Instance into_and_sep_affine P Q :
  TCOr (Affine P) (Absorbing Q) TCOr (Absorbing P) (Affine Q)
  IntoAnd true (P Q) P Q.
Proof. intros. by rewrite /IntoAnd /= sep_and. Qed.

Global Instance into_and_pure p φ ψ : @IntoAnd PROP p φ ψ φ ψ.
Proof. by rewrite /IntoAnd pure_and intuitionistically_if_and. Qed.

Global Instance into_and_affinely p P Q1 Q2 :
  IntoAnd p P Q1 Q2 IntoAnd p (<affine> P) (<affine> Q1) (<affine> Q2).
Proof.
  rewrite /IntoAnd. destruct p; simpl.
  - rewrite -affinely_and !intuitionistically_affinely_elim //.
  - intros →. by rewrite affinely_and.
Qed.
Global Instance into_and_intuitionistically p P Q1 Q2 :
  IntoAnd p P Q1 Q2 IntoAnd p ( P) ( Q1) ( Q2).
Proof.
  rewrite /IntoAnd. destruct p; simpl.
  - rewrite -intuitionistically_and !intuitionistically_idemp //.
  - intros →. by rewrite intuitionistically_and.
Qed.
Global Instance into_and_persistently p P Q1 Q2 :
  IntoAnd p P Q1 Q2
  IntoAnd p (<pers> P) (<pers> Q1) (<pers> Q2).
Proof.
  rewrite /IntoAnd /=. destruct p; simpl.
  - rewrite -persistently_and !intuitionistically_persistently_elim //.
  - intros →. by rewrite persistently_and.
Qed.
Global Instance into_and_embed `{BiEmbed PROP PROP'} p P Q1 Q2 :
  IntoAnd p P Q1 Q2 IntoAnd p P Q1 Q2.
Proof.
  rewrite /IntoAnd -embed_andHP. apply intuitionistically_if_intro'.
  by rewrite embed_intuitionistically_if_2 HP intuitionistically_if_elim.
Qed.

IntoSep
Global Instance into_sep_sep P Q : IntoSep (P Q) P Q.
Proof. by rewrite /IntoSep. Qed.

Inductive AndIntoSep : PROP PROP PROP PROP Prop :=
  | and_into_sep_affine P Q Q' : Affine P FromAffinely Q' Q AndIntoSep P P Q Q'
  | and_into_sep P Q : AndIntoSep P (<affine> P)%I Q Q.
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'.
Proof.
  destruct 2 as [P Q Q'|P Q]; rewrite /IntoSep.
  - rewrite -(from_affinely Q' Q) -(affine_affinely P) affinely_and_lr.
    by rewrite persistent_and_affinely_sep_l_1.
  - by rewrite persistent_and_affinely_sep_l_1.
Qed.
Global Instance into_sep_and_persistent_r P P' Q Q' :
  Persistent Q AndIntoSep Q Q' P P' IntoSep (P Q) P' Q'.
Proof.
  destruct 2 as [Q P P'|Q P]; rewrite /IntoSep.
  - rewrite -(from_affinely P' P) -(affine_affinely Q) -affinely_and_lr.
    by rewrite persistent_and_affinely_sep_r_1.
  - by rewrite persistent_and_affinely_sep_r_1.
Qed.

Global Instance into_sep_pure φ ψ : @IntoSep PROP φ ψ φ ψ.
Proof. by rewrite /IntoSep pure_and persistent_and_sep_1. Qed.

Global Instance into_sep_embed `{BiEmbed PROP PROP'} P Q1 Q2 :
  IntoSep P Q1 Q2 IntoSep P Q1 Q2.
Proof. rewrite /IntoSep -embed_sep⇒ → //. Qed.

Global Instance into_sep_affinely `{BiPositive PROP} P Q1 Q2 :
  IntoSep P Q1 Q2 IntoSep (<affine> P) (<affine> Q1) (<affine> Q2) | 0.
Proof. rewrite /IntoSep /= ⇒ →. by rewrite affinely_sep. Qed.
Global Instance into_sep_intuitionistically `{BiPositive PROP} P Q1 Q2 :
  IntoSep P Q1 Q2 IntoSep ( P) ( Q1) ( Q2) | 0.
Proof. rewrite /IntoSep /= ⇒ →. by rewrite intuitionistically_sep. Qed.
Global Instance into_sep_affinely_trim P Q1 Q2 :
  IntoSep P Q1 Q2 IntoSep (<affine> P) Q1 Q2 | 20.
Proof. rewrite /IntoSep /= ⇒ →. by rewrite affinely_elim. Qed.

Global Instance into_sep_persistently `{BiPositive PROP} P Q1 Q2 :
  IntoSep P Q1 Q2
  IntoSep (<pers> P) (<pers> Q1) (<pers> Q2).
Proof. rewrite /IntoSep /= ⇒ →. by rewrite persistently_sep. Qed.
Global Instance into_sep_persistently_affine P Q1 Q2 :
  IntoSep P Q1 Q2
  TCOr (Affine Q1) (Absorbing Q2) TCOr (Absorbing Q1) (Affine Q2)
  IntoSep (<pers> P) (<pers> Q1) (<pers> Q2).
Proof.
  rewrite /IntoSep /= ⇒ → ??.
  by rewrite sep_and persistently_and persistently_and_sep_l_1.
Qed.
Global Instance into_sep_intuitionistically_affine P Q1 Q2 :
  IntoSep P Q1 Q2
  TCOr (Affine Q1) (Absorbing Q2) TCOr (Absorbing Q1) (Affine Q2)
  IntoSep ( P) ( Q1) ( Q2).
Proof.
  rewrite /IntoSep /= ⇒ → ??.
  by rewrite sep_and intuitionistically_and and_sep_intuitionistically.
Qed.

Global Instance into_sep_big_sepL_cons {A} (Φ : nat A PROP) l x l' :
  IsCons l x l'
  IntoSep ([∗ list] k y l, Φ k y)
    (Φ 0 x) ([∗ list] k y l', Φ (S k) y).
Proof. rewrite /IsCons=>->. by rewrite /IntoSep big_sepL_cons. Qed.
Global Instance into_sep_big_sepL_app {A} (Φ : nat A PROP) l l1 l2 :
  IsApp l l1 l2
  IntoSep ([∗ list] k y l, Φ k y)
    ([∗ list] k y l1, Φ k y) ([∗ list] k y l2, Φ (length l1 + k) y).
Proof. rewrite /IsApp=>->. by rewrite /IntoSep big_sepL_app. Qed.

Global Instance into_sep_big_sepL2_cons {A B}
    (Φ : nat A B PROP) l1 x1 l1' l2 x2 l2' :
  IsCons l1 x1 l1' IsCons l2 x2 l2'
  IntoSep ([∗ 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 /IntoSep big_sepL2_cons. Qed.

Global Instance into_sep_big_sepMS_disj_union `{Countable A} (Φ : A PROP) X1 X2 :
  IntoSep ([∗ mset] y X1 X2, Φ y) ([∗ mset] y X1, Φ y) ([∗ mset] y X2, Φ y).
Proof. by rewrite /IntoSep big_sepMS_disj_union. 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.
Global Instance from_or_affinely P Q1 Q2 :
  FromOr P Q1 Q2 FromOr (<affine> P) (<affine> Q1) (<affine> Q2).
Proof. rewrite /FromOr⇒ <-. by rewrite affinely_or. Qed.
Global Instance from_or_intuitionistically P Q1 Q2 :
  FromOr P Q1 Q2 FromOr ( P) ( Q1) ( Q2).
Proof. rewrite /FromOr⇒ <-. by rewrite intuitionistically_or. Qed.
Global Instance from_or_absorbingly P Q1 Q2 :
  FromOr P Q1 Q2 FromOr (<absorb> P) (<absorb> Q1) (<absorb> Q2).
Proof. rewrite /FromOr⇒ <-. by rewrite absorbingly_or. Qed.
Global Instance from_or_persistently P Q1 Q2 :
  FromOr P Q1 Q2
  FromOr (<pers> P) (<pers> Q1) (<pers> Q2).
Proof. rewrite /FromOr⇒ <-. by rewrite persistently_or. Qed.
Global Instance from_or_embed `{BiEmbed PROP PROP'} P Q1 Q2 :
  FromOr P Q1 Q2 FromOr P Q1 Q2.
Proof. by rewrite /FromOr -embed_or ⇒ <-. Qed.

Global Instance from_or_bupd `{BiBUpd 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.

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.
Global Instance into_or_affinely P Q1 Q2 :
  IntoOr P Q1 Q2 IntoOr (<affine> P) (<affine> Q1) (<affine> Q2).
Proof. rewrite /IntoOr=>->. by rewrite affinely_or. Qed.
Global Instance into_or_intuitionistically P Q1 Q2 :
  IntoOr P Q1 Q2 IntoOr ( P) ( Q1) ( Q2).
Proof. rewrite /IntoOr=>->. by rewrite intuitionistically_or. Qed.
Global Instance into_or_absorbingly P Q1 Q2 :
  IntoOr P Q1 Q2 IntoOr (<absorb> P) (<absorb> Q1) (<absorb> Q2).
Proof. rewrite /IntoOr=>->. by rewrite absorbingly_or. Qed.
Global Instance into_or_persistently P Q1 Q2 :
  IntoOr P Q1 Q2
  IntoOr (<pers> P) (<pers> Q1) (<pers> Q2).
Proof. rewrite /IntoOr=>->. by rewrite persistently_or. Qed.
Global Instance into_or_embed `{BiEmbed PROP PROP'} P Q1 Q2 :
  IntoOr P Q1 Q2 IntoOr P Q1 Q2.
Proof. by rewrite /IntoOr -embed_or ⇒ <-. Qed.

FromExist
Global Instance from_exist_exist {A} (Φ : A PROP) : FromExist ( a, Φ a) Φ.
Proof. by rewrite /FromExist. Qed.
Global Instance from_exist_texist {A} (Φ : tele_arg A PROP) :
  FromExist (.. a, Φ a) Φ.
Proof. by rewrite /FromExist bi_texist_exist. Qed.
Global Instance from_exist_pure {A} (φ : A Prop) :
  @FromExist PROP A x, φ x (λ a, φ a)%I.
Proof. by rewrite /FromExist pure_exist. Qed.
Global Instance from_exist_affinely {A} P (Φ : A PROP) :
  FromExist P Φ FromExist (<affine> P) (λ a, <affine> (Φ a))%I.
Proof. rewrite /FromExist⇒ <-. by rewrite affinely_exist. Qed.
Global Instance from_exist_intuitionistically {A} P (Φ : A PROP) :
  FromExist P Φ FromExist ( P) (λ a, (Φ a))%I.
Proof. rewrite /FromExist⇒ <-. by rewrite intuitionistically_exist. Qed.
Global Instance from_exist_absorbingly {A} P (Φ : A PROP) :
  FromExist P Φ FromExist (<absorb> P) (λ a, <absorb> (Φ a))%I.
Proof. rewrite /FromExist⇒ <-. by rewrite absorbingly_exist. Qed.
Global Instance from_exist_persistently {A} P (Φ : A PROP) :
  FromExist P Φ FromExist (<pers> P) (λ a, <pers> (Φ a))%I.
Proof. rewrite /FromExist⇒ <-. by rewrite persistently_exist. Qed.
Global Instance from_exist_embed `{BiEmbed PROP PROP'} {A} P (Φ : A PROP) :
  FromExist P Φ FromExist P (λ a, Φ a%I).
Proof. by rewrite /FromExist -embed_exist ⇒ <-. Qed.

Global Instance from_exist_bupd `{BiBUpd PROP} {A} P (Φ : A PROP) :
  FromExist P Φ FromExist (|==> P) (λ a, |==> Φ a)%I.
Proof.
  rewrite /FromExist=><-. apply exist_elima. by rewrite -(exist_intro a).
Qed.

IntoExist
Global Instance into_exist_exist {A} (Φ : A PROP) : IntoExist ( a, Φ a) Φ.
Proof. by rewrite /IntoExist. Qed.
Global Instance into_exist_texist {A} (Φ : tele_arg A PROP) :
  IntoExist (.. a, Φ a) Φ | 10.
Proof. by rewrite /IntoExist bi_texist_exist. Qed.
Global Instance into_exist_pure {A} (φ : A Prop) :
  @IntoExist PROP A x, φ x (λ a, φ a)%I.
Proof. by rewrite /IntoExist pure_exist. Qed.
Global Instance into_exist_affinely {A} P (Φ : A PROP) :
  IntoExist P Φ IntoExist (<affine> P) (λ a, <affine> (Φ a))%I.
Proof. rewrite /IntoExistHP. by rewrite HP affinely_exist. Qed.
Global Instance into_exist_intuitionistically {A} P (Φ : A PROP) :
  IntoExist P Φ IntoExist ( P) (λ a, (Φ a))%I.
Proof. rewrite /IntoExistHP. by rewrite HP intuitionistically_exist. Qed.
Global Instance into_exist_and_pure P Q φ :
  IntoPureT P φ IntoExist (P Q) (λ _ : φ, Q).
Proof.
  intros (φ'&->&?). rewrite /IntoExist (into_pure P).
  apply pure_elim_lHφ. by rewrite -(exist_intro Hφ).
Qed.
Global Instance into_exist_sep_pure P Q φ :
  IntoPureT P φ TCOr (Affine P) (Absorbing Q) IntoExist (P Q) (λ _ : φ, Q).
Proof.
  intros (φ'&->&?) ?. rewrite /IntoExist.
  eapply (pure_elim φ'); [by rewrite (into_pure P); apply sep_elim_l, _|]=>?.
  rewrite -exist_intro //. apply sep_elim_r, _.
Qed.
Global Instance into_exist_absorbingly {A} P (Φ : A PROP) :
  IntoExist P Φ IntoExist (<absorb> P) (λ a, <absorb> (Φ a))%I.
Proof. rewrite /IntoExistHP. by rewrite HP absorbingly_exist. Qed.
Global Instance into_exist_persistently {A} P (Φ : A PROP) :
  IntoExist P Φ IntoExist (<pers> P) (λ a, <pers> (Φ a))%I.
Proof. rewrite /IntoExistHP. by rewrite HP persistently_exist. Qed.
Global Instance into_exist_embed `{BiEmbed PROP PROP'} {A} P (Φ : A PROP) :
  IntoExist P Φ IntoExist P (λ a, Φ a%I).
Proof. by rewrite /IntoExist -embed_exist ⇒ <-. Qed.

IntoForall
Global Instance into_forall_forall {A} (Φ : A PROP) : IntoForall ( a, Φ a) Φ.
Proof. by rewrite /IntoForall. Qed.
Global Instance into_forall_tforall {A} (Φ : tele_arg A PROP) :
  IntoForall (.. a, Φ a) Φ | 10.
Proof. by rewrite /IntoForall bi_tforall_forall. Qed.
Global Instance into_forall_affinely {A} P (Φ : A PROP) :
  IntoForall P Φ IntoForall (<affine> P) (λ a, <affine> (Φ a))%I.
Proof. rewrite /IntoForallHP. by rewrite HP affinely_forall. Qed.
Global Instance into_forall_intuitionistically {A} P (Φ : A PROP) :
  IntoForall P Φ IntoForall ( P) (λ a, (Φ a))%I.
Proof. rewrite /IntoForallHP. by rewrite HP intuitionistically_forall. Qed.
Global Instance into_forall_persistently {A} P (Φ : A PROP) :
  IntoForall P Φ IntoForall (<pers> P) (λ a, <pers> (Φ a))%I.
Proof. rewrite /IntoForallHP. by rewrite HP persistently_forall. Qed.
Global Instance into_forall_embed `{BiEmbed PROP PROP'} {A} P (Φ : A PROP) :
  IntoForall P Φ IntoForall P (λ a, Φ a%I).
Proof. by rewrite /IntoForall -embed_forall ⇒ <-. Qed.

Global Instance into_forall_impl_pure a φ P Q :
  FromPureT a P φ
  TCOr (TCEq a false) (BiAffine PROP)
  IntoForall (P Q) (λ _ : φ, Q).
Proof.
  rewrite /FromPureT /FromPure /IntoForall⇒ -[φ' [-> <-]] [->|?] /=.
  - by rewrite pure_impl_forall.
  - by rewrite -affinely_affinely_if affine_affinely pure_impl_forall.
Qed.
Global Instance into_forall_wand_pure a φ P Q :
  FromPureT a P φ IntoForall (P -∗ Q) (λ _ : φ, Q).
Proof.
  rewrite /FromPureT /FromPure /IntoForall⇒ -[φ' [-> <-]] /=.
  apply forall_intro=>? /=. rewrite -affinely_affinely_if.
  by rewrite -(pure_intro _ True%I) // /bi_affinely right_id emp_wand.
Qed.

Global Instance into_forall_wand P Q :
  IntoForall (P -∗ Q) (λ _ : bi_emp_valid P, Q) | 10.
Proof. rewrite /IntoForall. apply forall_intro=><-. rewrite emp_wand //. Qed.
Global Instance into_forall_impl `{!BiAffine PROP} P Q :
  IntoForall (P Q) (λ _ : bi_emp_valid P, Q) | 10.
Proof. rewrite /IntoForall. apply forall_intro=><-. rewrite -True_emp True_impl //. Qed.

FromForall
Global Instance from_forall_forall {A} (Φ : A PROP) :
  FromForall ( x, Φ x)%I Φ.
Proof. by rewrite /FromForall. Qed.
Global Instance from_forall_tforall {A} (Φ : tele_arg A PROP) :
  FromForall (.. x, Φ x)%I Φ.
Proof. by rewrite /FromForall bi_tforall_forall. 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.
Global Instance from_forall_pure_not (φ : Prop) :
  @FromForall PROP φ (¬ φ)%I (λ a : φ, False)%I.
Proof. by rewrite /FromForall pure_forall. Qed.
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 φ :
  IntoPureT P φ TCOr (Affine P) (Absorbing Q)
  FromForall (P -∗ Q)%I (λ _ : φ, Q)%I.
Proof.
  intros (φ'&->&?) [|]; rewrite /FromForall; apply wand_intro_r.
  - rewrite -(affine_affinely P) (into_pure P) -persistent_and_affinely_sep_r.
    apply pure_elim_r=>?. by rewrite forall_elim.
  - by rewrite (into_pure P) -pure_wand_forall wand_elim_l.
Qed.

Global Instance from_forall_intuitionistically `{BiAffine PROP} {A} P (Φ : A PROP) :
  FromForall P Φ FromForall ( P) (λ a, (Φ a))%I.
Proof.
  rewrite /FromForall⇒ <-. setoid_rewrite intuitionistically_into_persistently.
  by rewrite persistently_forall.
Qed.
Global Instance from_forall_persistently {A} P (Φ : A PROP) :
  FromForall P Φ FromForall (<pers> P)%I (λ a, <pers> (Φ a))%I.
Proof. rewrite /FromForall⇒ <-. by rewrite persistently_forall. Qed.
Global Instance from_forall_embed `{BiEmbed PROP PROP'} {A} P (Φ : A PROP) :
  FromForall P Φ FromForall P%I (λ a, Φ a%I).
Proof. by rewrite /FromForall -embed_forall ⇒ <-. Qed.

IntoInv
Global Instance into_inv_embed {PROP' : bi} `{BiEmbed PROP PROP'} P N :
  IntoInv P N IntoInv P N := {}.

ElimModal
Global Instance elim_modal_wand φ p p' P P' Q Q' R :
  ElimModal φ p p' P P' Q Q' ElimModal φ p p' P P' (R -∗ Q) (R -∗ Q').
Proof.
  rewrite /ElimModalH Hφ. apply wand_intro_r.
  rewrite wand_curry -assoc (comm _ (□?p' _)%I) -wand_curry wand_elim_l; auto.
Qed.
Global Instance elim_modal_wandM φ p p' P P' Q Q' mR :
  ElimModal φ p p' P P' Q Q'
  ElimModal φ p p' P P' (mR -∗? Q) (mR -∗? Q').
Proof. rewrite /ElimModal !wandM_sound. exact: elim_modal_wand. Qed.
Global Instance elim_modal_forall {A} φ p p' P P' (Φ Ψ : A PROP) :
  ( x, ElimModal φ p p' P P' (Φ x) (Ψ x)) ElimModal φ p p' P P' ( x, Φ x) ( x, Ψ x).
Proof.
  rewrite /ElimModalH ?. apply forall_introa. rewrite (forall_elim a); auto.
Qed.
Global Instance elim_modal_absorbingly_here p P Q :
  Absorbing Q ElimModal True p false (<absorb> P) P Q Q.
Proof.
  rewrite /ElimModal⇒ ? _. by rewrite intuitionistically_if_elim
    absorbingly_sep_l wand_elim_r absorbing_absorbingly.
Qed.

Global Instance elim_modal_bupd `{BiBUpd PROP} p P Q :
  ElimModal True p false (|==> P) P (|==> Q) (|==> Q).
Proof.
  by rewrite /ElimModal
    intuitionistically_if_elim bupd_frame_r wand_elim_r bupd_trans.
Qed.

Global Instance elim_modal_embed_bupd_goal `{BiEmbedBUpd PROP PROP'}
    p p' φ (P P' : PROP') (Q Q' : PROP) :
  ElimModal φ p p' P P' (|==> Q)%I (|==> Q')%I
  ElimModal φ p p' P P' |==> Q |==> Q'.
Proof. by rewrite /ElimModal !embed_bupd. Qed.
Global Instance elim_modal_embed_bupd_hyp `{BiEmbedBUpd PROP PROP'}
    p p' φ (P : PROP) (P' Q Q' : PROP') :
  ElimModal φ p p' (|==> P)%I P' Q Q'
  ElimModal φ p p' |==> P P' Q Q'.
Proof. by rewrite /ElimModal !embed_bupd. Qed.

AddModal
Global Instance add_modal_wand P P' Q R :
  AddModal P P' Q AddModal P P' (R -∗ Q).
Proof.
  rewrite /AddModalH. apply wand_intro_r.
  by rewrite wand_curry -assoc (comm _ P') -wand_curry wand_elim_l.
Qed.
Global Instance add_modal_wandM P P' Q mR :
  AddModal P P' Q AddModal P P' (mR -∗? Q).
Proof. rewrite /AddModal wandM_sound. exact: add_modal_wand. Qed.
Global Instance add_modal_forall {A} P P' (Φ : A PROP) :
  ( x, AddModal P P' (Φ x)) AddModal P P' ( x, Φ x).
Proof.
  rewrite /AddModalH. apply forall_introa. by rewrite (forall_elim a).
Qed.
Global Instance add_modal_embed_bupd_goal `{BiEmbedBUpd PROP PROP'}
       (P P' : PROP') (Q : PROP) :
  AddModal P P' (|==> Q)%I AddModal P P' |==> Q.
Proof. by rewrite /AddModal !embed_bupd. Qed.

Global Instance add_modal_bupd `{BiBUpd PROP} P Q : AddModal (|==> P) P (|==> Q).
Proof. by rewrite /AddModal bupd_frame_r wand_elim_r bupd_trans. Qed.

ElimInv
Global Instance elim_inv_acc_without_close {X : Type}
       φ Pinv Pin
       M1 M2 α β Q (Q' : X PROP) :
  IntoAcc (X:=X) Pinv φ Pin M1 M2 α β
  ElimAcc (X:=X) M1 M2 α β Q Q'
  ElimInv φ Pinv Pin α None Q Q'.
Proof.
  rewrite /ElimAcc /IntoAcc /ElimInv.
  iIntros (Hacc Helim Hφ) "(Hinv & Hin & Hcont)".
  iApply (Helim with "[Hcont]").
  - iIntros (x) "Hα". iApply "Hcont". iSplitL; simpl; done.
  - iApply (Hacc with "Hinv Hin"). done.
Qed.

Global Instance elim_inv_acc_with_close {X : Type}
       φ1 φ2 Pinv Pin
       M1 M2 α β Q Q' :
  IntoAcc Pinv φ1 Pin M1 M2 α β
  ( R, ElimModal φ2 false false (M1 R) R Q Q')
  ElimInv (X:=X) (φ1 φ2) Pinv Pin
          α
          (Some (λ x, β x -∗ M2 (pm_default emp ( x))))%I
          Q (λ _, Q').
Proof.
  rewrite /ElimAcc /IntoAcc /ElimInv.
  iIntros (Hacc Helim [??]) "(Hinv & Hin & Hcont)".
  iMod (Hacc with "Hinv Hin") as (x) "[Hα Hclose]"; first done.
  iApply "Hcont". simpl. iSplitL "Hα"; done.
Qed.

IntoEmbed
Global Instance into_embed_embed {PROP' : bi} `{BiEmbed PROP PROP'} P :
  IntoEmbed P P.
Proof. by rewrite /IntoEmbed. Qed.
Global Instance into_embed_affinely `{BiEmbedBUpd PROP PROP'} (P : PROP') (Q : PROP) :
  IntoEmbed P Q IntoEmbed (<affine> P) (<affine> Q).
Proof. rewrite /IntoEmbed⇒ →. by rewrite embed_affinely_2. Qed.
End bi_instances.