phanerozoic/Coq-Iris huggingface dataset:
(* iris/proofmode/class_instances.v *)
Instance into_absorbingly_intuitionistically P :
  IntoAbsorbingly (<pers> P) (□ P) | 2.
Proof.
  by rewrite /IntoAbsorbingly -absorbingly_intuitionistically_into_persistently.
Qed.
(* iris/proofmode/class_instances.v *)
Instance into_absorbingly_default P : IntoAbsorbingly (<absorb> P) P | 100.
Proof. by rewrite /IntoAbsorbingly. Qed.
(* iris/proofmode/class_instances.v *)
(* FromAssumption *)
Instance from_assumption_persistently_r P Q :
  FromAssumption true P Q → KnownRFromAssumption true P (<pers> Q).
Proof.
  rewrite /KnownRFromAssumption /FromAssumption /= =><-.
  apply intuitionistically_persistent.
Qed.
(* iris/proofmode/class_instances.v *)
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.
(* iris/proofmode/class_instances.v *)
Instance from_assumption_intuitionistically_r P Q :
  FromAssumption true P Q → KnownRFromAssumption true P (□ Q).
Proof.
  rewrite /KnownRFromAssumption /FromAssumption /= =><-.
  by rewrite intuitionistically_idemp.
Qed.
(* iris/proofmode/class_instances.v *)
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.
(* iris/proofmode/class_instances.v *)
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.
(* iris/proofmode/class_instances.v *)
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.
(* iris/proofmode/class_instances.v *)
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.
(* iris/proofmode/class_instances.v *)
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.
(* iris/proofmode/class_instances.v *)
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.
(* iris/proofmode/class_instances.v *)
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.
(* iris/proofmode/class_instances.v *)
Instance from_assumption_tforall {TT : tele} p (Φ : TT → PROP) Q x :
  FromAssumption p (Φ x) Q → KnownLFromAssumption p (∀.. x, Φ x) Q.
Proof.
  rewrite /KnownLFromAssumption /FromAssumption=> <-.
  by rewrite bi_tforall_forall forall_elim.
Qed.
(* iris/proofmode/class_instances.v *)
(* IntoPure *)
Instance into_pure_pure φ : @IntoPure PROP ⌜φ⌝ φ.
Proof. by rewrite /IntoPure. Qed.
(* iris/proofmode/class_instances.v *)
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.
(* iris/proofmode/class_instances.v *)
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.
(* iris/proofmode/class_instances.v *)
Instance into_pure_pure_impl `{!BiPureForall PROP} (φ1 φ2 : Prop) P1 P2 :
  FromPure false P1 φ1 → IntoPure P2 φ2 → IntoPure (P1 → P2) (φ1 → φ2).
Proof. rewrite /FromPure /IntoPure /= => <- ->. apply pure_impl_2. Qed.
(* iris/proofmode/class_instances.v *)
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.
(* iris/proofmode/class_instances.v *)
Instance into_pure_texist {TT : tele} (Φ : TT → PROP) (φ : TT → Prop) :
  (∀ x, IntoPure (Φ x) (φ x)) → IntoPure (∃.. x, Φ x) (∃.. x, φ x).
Proof. rewrite /IntoPure texist_exist bi_texist_exist. apply into_pure_exist. Qed.
(* iris/proofmode/class_instances.v *)
Instance into_pure_forall `{!BiPureForall PROP}
    {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.
(* iris/proofmode/class_instances.v *)
Instance into_pure_tforall `{!BiPureForall PROP}
    {TT : tele} (Φ : TT → PROP) (φ : TT → Prop) :
  (∀ x, IntoPure (Φ x) (φ x)) → IntoPure (∀.. x, Φ x) (∀.. x, φ x).
Proof.
  rewrite /IntoPure !tforall_forall bi_tforall_forall. apply into_pure_forall.
Qed.
(* iris/proofmode/class_instances.v *)
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.
(* iris/proofmode/class_instances.v *)
Instance into_pure_pure_wand `{!BiPureForall PROP} 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 left_id.
Qed.
(* iris/proofmode/class_instances.v *)
Instance into_pure_affinely P φ : IntoPure P φ → IntoPure (<affine> P) φ.
Proof. rewrite /IntoPure=> ->. apply affinely_elim. Qed.
(* iris/proofmode/class_instances.v *)
Instance into_pure_intuitionistically P φ :
  IntoPure P φ → IntoPure (□ P) φ.
Proof. rewrite /IntoPure=> ->. apply intuitionistically_elim. Qed.
(* iris/proofmode/class_instances.v *)
Instance into_pure_absorbingly P φ : IntoPure P φ → IntoPure (<absorb> P) φ.
Proof. rewrite /IntoPure=> ->. by rewrite absorbingly_pure. Qed.
(* iris/proofmode/class_instances.v *)
Instance into_pure_persistently P φ :
  IntoPure P φ → IntoPure (<pers> P) φ.
Proof. rewrite /IntoPure=> ->. apply: persistently_elim. Qed.
(* iris/proofmode/class_instances.v *)
Instance into_pure_big_sepL {A}
    (Φ : nat → A → PROP) (φ : nat → A → Prop) (l : list A) :
  (∀ k x, IntoPure (Φ k x) (φ k x)) →
  IntoPure ([∗ list] k↦x ∈ l, Φ k x) (∀ k x, l !! k = Some x → φ k x).
Proof.
  rewrite /IntoPure. intros HΦ.
  setoid_rewrite HΦ. rewrite big_sepL_pure_1. done.
Qed.
(* iris/proofmode/class_instances.v *)
Instance into_pure_big_sepM `{Countable K} {A}
    (Φ : K → A → PROP) (φ : K → A → Prop) (m : gmap K A) :
  (∀ k x, IntoPure (Φ k x) (φ k x)) →
  IntoPure ([∗ map] k↦x ∈ m, Φ k x) (map_Forall φ m).
Proof.
  rewrite /IntoPure. intros HΦ.
  setoid_rewrite HΦ. rewrite big_sepM_pure_1. done.
Qed.
(* iris/proofmode/class_instances.v *)
Instance into_pure_big_sepS `{Countable A}
    (Φ : A → PROP) (φ : A → Prop) (X : gset A) :
  (∀ x, IntoPure (Φ x) (φ x)) →
  IntoPure ([∗ set] x ∈ X, Φ x) (set_Forall φ X).
Proof.
  rewrite /IntoPure. intros HΦ.
  setoid_rewrite HΦ. rewrite big_sepS_pure_1. done.
Qed.
(* iris/proofmode/class_instances.v *)
Instance into_pure_big_sepMS `{Countable A}
    (Φ : A → PROP) (φ : A → Prop) (X : gmultiset A) :
  (∀ x, IntoPure (Φ x) (φ x)) →
  IntoPure ([∗ mset] x ∈ X, Φ x) (∀ y : A, y ∈ X → φ y).
Proof.
  rewrite /IntoPure. intros HΦ.
  setoid_rewrite HΦ. rewrite big_sepMS_pure_1. done.
Qed.
(* iris/proofmode/class_instances.v *)
(* FromPure *)
Instance from_pure_emp : @FromPure PROP true emp True.
Proof. rewrite /FromPure /=. apply (affine _). Qed.
(* iris/proofmode/class_instances.v *)
Instance from_pure_pure φ : @FromPure PROP false ⌜φ⌝ φ.
Proof. by rewrite /FromPure /=. Qed.
(* iris/proofmode/class_instances.v *)
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.
(* iris/proofmode/class_instances.v *)
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.
(* iris/proofmode/class_instances.v *)
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_1=> -> <-. destruct a=>//=.
  apply bi.impl_intro_l. by rewrite affinely_and_r bi.impl_elim_r.
Qed.
(* iris/proofmode/class_instances.v *)
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.
(* iris/proofmode/class_instances.v *)
Instance from_pure_texist {TT : tele} a (Φ : TT → PROP) (φ : TT → Prop) :
  (∀ x, FromPure a (Φ x) (φ x)) → FromPure a (∃.. x, Φ x) (∃.. x, φ x).
Proof. rewrite /FromPure texist_exist bi_texist_exist. apply from_pure_exist. Qed.
(* iris/proofmode/class_instances.v *)
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_1. setoid_rewrite <-Hx.
  destruct a=>//=. apply affinely_forall.
Qed.
(* iris/proofmode/class_instances.v *)
Instance from_pure_tforall {TT : tele} a (Φ : TT → PROP) (φ : TT → Prop) :
  (∀ x, FromPure a (Φ x) (φ x)) → FromPure a (∀.. x, Φ x) (∀.. x, φ x).
Proof.
  rewrite /FromPure !tforall_forall bi_tforall_forall. apply from_pure_forall.
Qed.
(* iris/proofmode/class_instances.v *)
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.
(* iris/proofmode/class_instances.v *)
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 /IntoPure=> HP1 <- 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_1 impl_elim_r.
  - by rewrite HP1 sep_and pure_impl_1 impl_elim_r.
Qed.
(* iris/proofmode/class_instances.v *)
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.
(* iris/proofmode/class_instances.v *)
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.
(* iris/proofmode/class_instances.v *)
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.
(* iris/proofmode/class_instances.v *)
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.
(* iris/proofmode/class_instances.v *)
Instance from_pure_big_sepL {A}
    a (Φ : nat → A → PROP) (φ : nat → A → Prop) (l : list A) :
  (∀ k x, FromPure a (Φ k x) (φ k x)) →
  TCOr (TCEq a true) (BiAffine PROP) →
  FromPure a ([∗ list] k↦x ∈ l, Φ k x) (∀ k x, l !! k = Some x → φ k x).
Proof.
  rewrite /FromPure. destruct a; simpl; intros HΦ Haffine.
  - rewrite big_sepL_affinely_pure_2.
    setoid_rewrite HΦ. done.
  - destruct Haffine as [[=]%TCEq_eq|?].
    rewrite -big_sepL_pure. setoid_rewrite HΦ. done.
Qed.
(* iris/proofmode/class_instances.v *)
Instance from_pure_big_sepM `{Countable K} {A}
    a (Φ : K → A → PROP) (φ : K → A → Prop) (m : gmap K A) :
  (∀ k x, FromPure a (Φ k x) (φ k x)) →
  TCOr (TCEq a true) (BiAffine PROP) →
  FromPure a ([∗ map] k↦x ∈ m, Φ k x) (map_Forall φ m).
Proof.
  rewrite /FromPure. destruct a; simpl; intros HΦ Haffine.
  - rewrite big_sepM_affinely_pure_2.
    setoid_rewrite HΦ. done.
  - destruct Haffine as [[=]%TCEq_eq|?].
    rewrite -big_sepM_pure. setoid_rewrite HΦ. done.
Qed.
(* iris/proofmode/class_instances.v *)
Instance from_pure_big_sepS `{Countable A}
    a (Φ : A → PROP) (φ : A → Prop) (X : gset A) :
  (∀ x, FromPure a (Φ x) (φ x)) →
  TCOr (TCEq a true) (BiAffine PROP) →
  FromPure a ([∗ set] x ∈ X, Φ x) (set_Forall φ X).
Proof.
  rewrite /FromPure. destruct a; simpl; intros HΦ Haffine.
  - rewrite big_sepS_affinely_pure_2.
    setoid_rewrite HΦ. done.
  - destruct Haffine as [[=]%TCEq_eq|?].
    rewrite -big_sepS_pure. setoid_rewrite HΦ. done.
Qed.
(* iris/proofmode/class_instances.v *)
Instance from_pure_big_sepMS `{Countable A}
    a (Φ : A → PROP) (φ : A → Prop) (X : gmultiset A) :
  (∀ x, FromPure a (Φ x) (φ x)) →
  TCOr (TCEq a true) (BiAffine PROP) →
  FromPure a ([∗ mset] x ∈ X, Φ x) (∀ y : A, y ∈ X → φ y).
Proof.
  rewrite /FromPure. destruct a; simpl; intros HΦ Haffine.
  - rewrite big_sepMS_affinely_pure_2.
    setoid_rewrite HΦ. done.
  - destruct Haffine as [[=]%TCEq_eq|?].
    rewrite -big_sepMS_pure. setoid_rewrite HΦ. done.
Qed.
(* iris/proofmode/class_instances.v *)
(* IntoPersistent *)
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.
(* iris/proofmode/class_instances.v *)
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.
(* iris/proofmode/class_instances.v *)
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.
(* iris/proofmode/class_instances.v *)
Instance into_persistent_here P : IntoPersistent true P P | 1.
Proof. by rewrite /IntoPersistent. Qed.
(* iris/proofmode/class_instances.v *)
Instance into_persistent_persistent P :
  Persistent P → IntoPersistent false P P | 100.
Proof. intros. by rewrite /IntoPersistent. Qed.
(* iris/proofmode/class_instances.v *)
(* FromModal *)
Instance from_modal_affinely P :
  FromModal True modality_affinely (<affine> P) (<affine> P) P | 2.
Proof. by rewrite /FromModal. Qed.
(* iris/proofmode/class_instances.v *)
Instance from_modal_persistently P :
  FromModal True modality_persistently (<pers> P) (<pers> P) P | 2.
Proof. by rewrite /FromModal. Qed.
(* iris/proofmode/class_instances.v *)
Instance from_modal_intuitionistically P :
  FromModal True modality_intuitionistically (□ P) (□ P) P | 1.
Proof. by rewrite /FromModal. Qed.
(* iris/proofmode/class_instances.v *)
Instance from_modal_intuitionistically_affine_bi P :
  BiAffine PROP → FromModal True modality_persistently (□ P) (□ P) P | 0.
Proof.
  intros. by rewrite /FromModal /= intuitionistically_into_persistently.
Qed.
(* iris/proofmode/class_instances.v *)
Instance from_modal_absorbingly P :
  FromModal True modality_id (<absorb> P) (<absorb> P) P.
Proof. by rewrite /FromModal /= -absorbingly_intro. Qed.
(* iris/proofmode/class_instances.v *)
(* IntoWand *)
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.
(* iris/proofmode/class_instances.v *)
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.
(* iris/proofmode/class_instances.v *)
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.
(* iris/proofmode/class_instances.v *)
(* Implication instances
  For non-affine BIs, generally we assume [P → ...] is written in cases where
  that would be equivalent to [<affine> P -∗ ...], i.e., [P] is absorbing and
  persistent and an affinely modality is added when proving the premise. If the
  implication itself or the premise are taken from the persistent context,
  things become a bit easier and we can drop some of these requirements. We also
  support arbitrary implications for affine BIs via [BiAffine]. *)
Instance into_wand_impl_false_false P Q P' P'' :
  Absorbing P →
  (* Cheap check comes first *)
  TCOr (BiAffine PROP) (Persistent P) →
  MakeAffinely P P' →
  FromAssumption false P'' P' →
  IntoWand false false (P → Q) P'' Q.
Proof.
  rewrite /MakeAffinely /IntoWand /FromAssumption /= => ? Hpers <- ->.
  apply wand_intro_l. destruct Hpers.
  - rewrite impl_wand_1 affinely_elim wand_elim_r //.
  - rewrite persistent_impl_wand_affinely wand_elim_r //.
Qed.
(* iris/proofmode/class_instances.v *)
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 -(persistently_elim P').
  rewrite persistent_impl_wand_affinely.
  rewrite -(intuitionistically_idemp P) HP.
  apply wand_elim_r.
Qed.
(* iris/proofmode/class_instances.v *)
Instance into_wand_impl_true_false P Q P' P'' :
  MakeAffinely P P' →
  FromAssumption false P'' P' →
  IntoWand true false (P → Q) P'' Q.
Proof.
  rewrite /MakeAffinely /IntoWand /FromAssumption /= => <- ->.
  apply wand_intro_r.
  rewrite sep_and intuitionistically_elim affinely_elim impl_elim_l //.
Qed.
(* iris/proofmode/class_instances.v *)
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.
(* iris/proofmode/class_instances.v *)
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.
(* iris/proofmode/class_instances.v *)
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.
(* iris/proofmode/class_instances.v *)
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.
(* iris/proofmode/class_instances.v *)
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.
(* iris/proofmode/class_instances.v *)
Instance into_wand_forall_prop_false p (φ : Prop) Pφ P :
  MakeAffinely ⌜ φ ⌝ Pφ →
  IntoWand p false (∀ _ : φ, P) Pφ P.
Proof.
  rewrite /MakeAffinely /IntoWand=> <-.
  rewrite (intuitionistically_if_elim p) /=.
  by rewrite -pure_impl_forall -persistent_impl_wand_affinely.
Qed.
(* iris/proofmode/class_instances.v *)
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.
(* iris/proofmode/class_instances.v *)
Instance into_wand_tforall {TT : tele} p q (Φ : TT → 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.
(* iris/proofmode/class_instances.v *)
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)) HR. destruct q; simpl in *.
    + rewrite (affinely_elim P) -{2}(affine_affinely (□ P)).
      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)).
      by rewrite affinely_sep_2 wand_elim_l.
    + by rewrite affinely_sep_2 wand_elim_l.
Qed.
(* iris/proofmode/class_instances.v *)
(* In case the argument is affine, but the wand resides in the spatial context,
we can only eliminate the affine modality in the argument. This would lead to
the following instance:

  IntoWand false q R P Q → IntoWand' false q R (<affine> P) Q.

This instance is redundant, however, since the elimination of the affine
modality is already covered by the [IntoAssumption] instances that are used at
the leaves of the instance search for [IntoWand]. *)
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)) HR. destruct q; simpl.
  - rewrite (affinely_elim P) -{2}(affine_affinely (□ P)).
    by rewrite affinely_sep_2 wand_elim_l.
  - by rewrite affinely_sep_2 wand_elim_l.
Qed.
(* iris/proofmode/class_instances.v *)
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.
(* iris/proofmode/class_instances.v *)
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.
(* iris/proofmode/class_instances.v *)
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.
(* iris/proofmode/class_instances.v *)
(* FromWand *)
Instance from_wand_wand P1 P2 : FromWand (P1 -∗ P2) P1 P2.
Proof. by rewrite /FromWand. Qed.
(* iris/proofmode/class_instances.v *)
Instance from_wand_wandM mP1 P2 :
  FromWand (mP1 -∗? P2) (default emp mP1)%I P2.
Proof. by rewrite /FromWand wandM_sound. Qed.
(* iris/proofmode/class_instances.v *)
(* FromImpl *)
Instance from_impl_impl P1 P2 : FromImpl (P1 → P2) P1 P2.
Proof. by rewrite /FromImpl. Qed.
(* iris/proofmode/class_instances.v *)
(* FromAnd *)
Instance from_and_and P1 P2 : FromAnd (P1 ∧ P2) P1 P2 | 100.
Proof. by rewrite /FromAnd. Qed.
(* iris/proofmode/class_instances.v *)
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.
(* iris/proofmode/class_instances.v *)
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.
(* iris/proofmode/class_instances.v *)
Instance from_and_pure φ ψ : @FromAnd PROP ⌜φ ∧ ψ⌝ ⌜φ⌝ ⌜ψ⌝.
Proof. by rewrite /FromAnd pure_and. Qed.
(* iris/proofmode/class_instances.v *)
(* additional instance for ↔ because it is typeclasses opaque *)
Instance from_and_pure_iff φ ψ : @FromAnd PROP ⌜φ ↔ ψ⌝ ⌜φ → ψ⌝ ⌜ψ → φ⌝.
Proof. rewrite /iff. apply _. Qed.