phanerozoic/Coq-Iris huggingface dataset:
(* iris/proofmode/class_instances.v *)
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.
(* iris/proofmode/class_instances.v *)
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.
(* iris/proofmode/class_instances.v *)
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.
(* iris/proofmode/class_instances.v *)
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.
(* iris/proofmode/class_instances.v *)
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.
(* iris/proofmode/class_instances.v *)
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.
(* iris/proofmode/class_instances.v *)
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.
(* iris/proofmode/class_instances.v *)
(* FromSep *)
Instance from_sep_sep P1 P2 : FromSep (P1 ∗ P2) P1 P2 | 100.
Proof. by rewrite /FromSep. Qed.
(* iris/proofmode/class_instances.v *)
Instance from_sep_and P1 P2 :
  TCOr (Affine P1) (Absorbing P2) → TCOr (Affine P2) (Absorbing P1) →
  FromSep (P1 ∧ P2) P1 P2 | 101.
Proof. intros. by rewrite /FromSep sep_and. Qed.
(* iris/proofmode/class_instances.v *)
Instance from_sep_pure φ ψ : @FromSep PROP ⌜φ ∧ ψ⌝ ⌜φ⌝ ⌜ψ⌝.
Proof. by rewrite /FromSep pure_and sep_and. Qed.
(* iris/proofmode/class_instances.v *)
(* additional instance for ↔ because it is typeclasses opaque *)
Instance from_sep_pure_iff φ ψ : @FromSep PROP ⌜φ ↔ ψ⌝ ⌜φ → ψ⌝ ⌜ψ → φ⌝.
Proof. rewrite /iff. apply _. Qed.
(* iris/proofmode/class_instances.v *)
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.
(* iris/proofmode/class_instances.v *)
Instance from_sep_intuitionistically P Q1 Q2 :
  FromSep P Q1 Q2 → FromSep (□ P) (□ Q1) (□ Q2).
Proof. rewrite /FromSep=> <-. by rewrite intuitionistically_sep_2. Qed.
(* iris/proofmode/class_instances.v *)
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.
(* iris/proofmode/class_instances.v *)
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.
(* iris/proofmode/class_instances.v *)
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.
(* iris/proofmode/class_instances.v *)
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.
(* iris/proofmode/class_instances.v *)
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.
(* iris/proofmode/class_instances.v *)
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.
(* iris/proofmode/class_instances.v *)
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.
(* iris/proofmode/class_instances.v *)
(* MaybeCombineSepAs *)
Instance maybe_combine_sep_as_affinely Q1 Q2 P progress :
  MaybeCombineSepAs Q1 Q2 P progress →
  MaybeCombineSepAs (<affine> Q1) (<affine> Q2) (<affine> P) progress | 30.
Proof. rewrite /MaybeCombineSepAs =><-. by rewrite affinely_sep_2. Qed.
(* iris/proofmode/class_instances.v *)
Instance maybe_combine_sep_as_intuitionistically Q1 Q2 P progress :
  MaybeCombineSepAs Q1 Q2 P progress →
  MaybeCombineSepAs (□ Q1) (□ Q2) (□ P) progress | 30.
Proof. rewrite /MaybeCombineSepAs =><-. by rewrite intuitionistically_sep_2. Qed.
(* iris/proofmode/class_instances.v *)
Instance maybe_combine_sep_as_absorbingly Q1 Q2 P progress :
  MaybeCombineSepAs Q1 Q2 P progress →
  MaybeCombineSepAs (<absorb> Q1) (<absorb> Q2) (<absorb> P) progress | 30.
Proof. rewrite /MaybeCombineSepAs =><-. by rewrite absorbingly_sep. Qed.
(* iris/proofmode/class_instances.v *)
Instance maybe_combine_sep_as_persistently Q1 Q2 P progress :
  MaybeCombineSepAs Q1 Q2 P progress →
  MaybeCombineSepAs (<pers> Q1) (<pers> Q2) (<pers> P) progress | 30.
Proof. rewrite /MaybeCombineSepAs =><-. by rewrite persistently_sep_2. Qed.
(* iris/proofmode/class_instances.v *)
(* The results of these recursive instances drop the input modalities. This is
fine, because the [P] argument in [CombineSepGives Q1 Q2 P] is by definition
beneath a [<pers>] modality, and we have:
         - [<affine><pers> P ⊢ <pers> P] holds, we have
              [<pers><affine> P ⊣⊢ <pers> P] by [persistently_affinely_elim]
              and the obtained [□ P] in [iCombine] is always [Affine] anyway.
         - [□ <pers> P = <affine><pers> <pers> P], see [<affine>] and [<pers>]
         - [<absorb><pers> P ⊣⊢ <pers> P], see [absorbingly_elim_persistently]
         - [<pers><pers> P ⊣⊢ <pers> P], see [persistently_idemp] *)
Instance combine_sep_as_affinely Q1 Q2 P :
  CombineSepGives Q1 Q2 P → CombineSepGives (<affine> Q1) (<affine> Q2) P | 30.
Proof. by rewrite /CombineSepGives affinely_sep_2 affinely_elim => ->. Qed.
(* iris/proofmode/class_instances.v *)
Instance combine_sep_as_intuitionistically Q1 Q2 P :
  CombineSepGives Q1 Q2 P → CombineSepGives (□ Q1) (□ Q2) P | 30.
Proof. rewrite /CombineSepGives => <-. by rewrite !intuitionistically_elim. Qed.
(* iris/proofmode/class_instances.v *)
Instance combine_sep_as_absorbingly Q1 Q2 P :
  CombineSepGives Q1 Q2 P → CombineSepGives (<absorb> Q1) (<absorb> Q2) P | 30.
Proof.
  rewrite /CombineSepGives -absorbingly_sep =>->.
  by rewrite absorbingly_elim_persistently.
Qed.
(* iris/proofmode/class_instances.v *)
Instance combine_sep_as_persistently Q1 Q2 P :
  CombineSepGives Q1 Q2 P → CombineSepGives (<pers> Q1) (<pers> Q2) P | 30.
Proof.
  rewrite /CombineSepGives persistently_sep_2 => ->.
  by rewrite persistently_idemp.
Qed.
(* iris/proofmode/class_instances.v *)
(* IntoAnd *)
Instance into_and_and p P Q : IntoAnd p (P ∧ Q) P Q | 10.
Proof. by rewrite /IntoAnd intuitionistically_if_and. Qed.
(* iris/proofmode/class_instances.v *)
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.
(* iris/proofmode/class_instances.v *)
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.
(* iris/proofmode/class_instances.v *)
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.
(* iris/proofmode/class_instances.v *)
Instance into_and_sep_affine p P Q :
  TCOr (Affine P) (Absorbing Q) → TCOr (Affine Q) (Absorbing P) →
  IntoAnd p (P ∗ Q) P Q.
Proof. intros. by rewrite /IntoAnd /= sep_and. Qed.
(* iris/proofmode/class_instances.v *)
Instance into_and_pure p φ ψ : @IntoAnd PROP p ⌜φ ∧ ψ⌝ ⌜φ⌝ ⌜ψ⌝.
Proof. by rewrite /IntoAnd pure_and intuitionistically_if_and. Qed.
(* iris/proofmode/class_instances.v *)
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.
(* iris/proofmode/class_instances.v *)
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.
(* iris/proofmode/class_instances.v *)
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.
(* iris/proofmode/class_instances.v *)
(* IntoSep *)
Instance into_sep_sep P Q : IntoSep (P ∗ Q) P Q.
Proof. by rewrite /IntoSep. Qed.
(* iris/proofmode/class_instances.v *)
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) Q Q.
(* iris/proofmode/class_instances.v *)
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.
(* iris/proofmode/class_instances.v *)
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.
(* iris/proofmode/class_instances.v *)
Instance into_sep_pure φ ψ : @IntoSep PROP ⌜φ ∧ ψ⌝ ⌜φ⌝ ⌜ψ⌝.
Proof. by rewrite /IntoSep pure_and persistent_and_sep_1. Qed.
(* iris/proofmode/class_instances.v *)
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.
(* iris/proofmode/class_instances.v *)
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.
(* iris/proofmode/class_instances.v *)
(* 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 higher
cost. *)
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.
(* iris/proofmode/class_instances.v *)
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.
(* iris/proofmode/class_instances.v *)
Instance into_sep_persistently_affine P Q1 Q2 :
  IntoSep P Q1 Q2 →
  TCOr (Affine Q1) (Absorbing Q2) → TCOr (Affine Q2) (Absorbing Q1) →
  IntoSep (<pers> P) (<pers> Q1) (<pers> Q2).
Proof.
  rewrite /IntoSep /= => -> ??.
  by rewrite sep_and persistently_and persistently_and_sep_l_1.
Qed.
(* iris/proofmode/class_instances.v *)
Instance into_sep_intuitionistically_affine P Q1 Q2 :
  IntoSep P Q1 Q2 →
  TCOr (Affine Q1) (Absorbing Q2) → TCOr (Affine Q2) (Absorbing Q1) →
  IntoSep (□ P) (□ Q1) (□ Q2).
Proof.
  rewrite /IntoSep /= => -> ??.
  by rewrite sep_and intuitionistically_and and_sep_intuitionistically.
Qed.
(* iris/proofmode/class_instances.v *)
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.
(* iris/proofmode/class_instances.v *)
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.
(* iris/proofmode/class_instances.v *)
(* No instance for app, since that only works when the LHSs have the same length *)
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.
(* iris/proofmode/class_instances.v *)
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.
(* iris/proofmode/class_instances.v *)
(* FromOr *)
Instance from_or_or P1 P2 : FromOr (P1 ∨ P2) P1 P2.
Proof. by rewrite /FromOr. Qed.
(* iris/proofmode/class_instances.v *)
Instance from_or_pure φ ψ : @FromOr PROP ⌜φ ∨ ψ⌝ ⌜φ⌝ ⌜ψ⌝.
Proof. by rewrite /FromOr pure_or. Qed.
(* iris/proofmode/class_instances.v *)
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.
(* iris/proofmode/class_instances.v *)
Instance from_or_intuitionistically P Q1 Q2 :
  FromOr P Q1 Q2 → FromOr (□ P) (□ Q1) (□ Q2).
Proof. rewrite /FromOr=> <-. by rewrite intuitionistically_or. Qed.
(* iris/proofmode/class_instances.v *)
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.
(* iris/proofmode/class_instances.v *)
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.
(* iris/proofmode/class_instances.v *)
(* IntoOr *)
Instance into_or_or P Q : IntoOr (P ∨ Q) P Q.
Proof. by rewrite /IntoOr. Qed.
(* iris/proofmode/class_instances.v *)
Instance into_or_pure φ ψ : @IntoOr PROP ⌜φ ∨ ψ⌝ ⌜φ⌝ ⌜ψ⌝.
Proof. by rewrite /IntoOr pure_or. Qed.
(* iris/proofmode/class_instances.v *)
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.
(* iris/proofmode/class_instances.v *)
Instance into_or_intuitionistically P Q1 Q2 :
  IntoOr P Q1 Q2 → IntoOr (□ P) (□ Q1) (□ Q2).
Proof. rewrite /IntoOr=>->. by rewrite intuitionistically_or. Qed.
(* iris/proofmode/class_instances.v *)
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.
(* iris/proofmode/class_instances.v *)
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.
(* iris/proofmode/class_instances.v *)
(* FromExist *)
Instance from_exist_texist {TT : tele} (Φ : TT → PROP) :
  FromExist (∃.. a, Φ a) Φ.
Proof. by rewrite /FromExist bi_texist_exist. Qed.
(* iris/proofmode/class_instances.v *)
Instance from_exist_pure {A} (φ : A → Prop) :
  @FromExist PROP A ⌜∃ x, φ x⌝ (λ a, ⌜φ a⌝)%I.
Proof. by rewrite /FromExist pure_exist. Qed.
(* iris/proofmode/class_instances.v *)
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.
(* iris/proofmode/class_instances.v *)
Instance from_exist_intuitionistically {A} P (Φ : A → PROP) :
  FromExist P Φ → FromExist (□ P) (λ a, □ (Φ a))%I.
Proof. rewrite /FromExist=> <-. by rewrite intuitionistically_exist. Qed.
(* iris/proofmode/class_instances.v *)
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.
(* iris/proofmode/class_instances.v *)
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.
(* iris/proofmode/class_instances.v *)
(* These three instances [into_exist_exist], [into_exist_pure], and
   [into_exist_texist] need to be written without notations, for example
   [bi_exist Φ] and not [∃ a, Φ a], so that [AsIdentName] is always passed the
   entire body of the exists with the binder. *)
Instance into_exist_exist {A} (Φ : A → PROP) name :
  AsIdentName Φ name → IntoExist (bi_exist Φ) Φ name.
Proof. by rewrite /IntoExist. Qed.
(* iris/proofmode/class_instances.v *)
Instance into_exist_pure {A} (φ : A → Prop) name :
  AsIdentName φ name →
  @IntoExist PROP A ⌜ex φ⌝ (λ a, ⌜φ a⌝)%I name.
Proof. by rewrite /IntoExist pure_exist. Qed.
(* iris/proofmode/class_instances.v *)
Instance into_exist_texist {TT : tele} (Φ : TT → PROP) name :
  AsIdentName Φ name → IntoExist (bi_texist Φ) Φ name | 10.
Proof. by rewrite /IntoExist bi_texist_exist. Qed.
(* iris/proofmode/class_instances.v *)
Instance into_exist_affinely {A} P (Φ : A → PROP) name :
  IntoExist P Φ name → IntoExist (<affine> P) (λ a, <affine> (Φ a))%I name.
Proof. rewrite /IntoExist=> HP. by rewrite HP affinely_exist. Qed.
(* iris/proofmode/class_instances.v *)
Instance into_exist_intuitionistically {A} P (Φ : A → PROP) name :
  IntoExist P Φ name → IntoExist (□ P) (λ a, □ (Φ a))%I name.
Proof. rewrite /IntoExist=> HP. by rewrite HP intuitionistically_exist. Qed.
(* iris/proofmode/class_instances.v *)
(* This instance is generalized to let us use [iDestruct as (P) "..."] and
[iIntros "[% ...]"] for conjunctions with a pure left-hand side. There is some
risk of backtracking here, but that should only happen in failing cases
(assuming that appropriate modality commuting instances are provided for both
conjunctions and existential quantification). The alternative of providing
specialized instances for cases like ⌜P ∧ Q⌝ turned out to not be tenable.

[to_ident_name H] makes the default name [H] when [P] is destructed with
[iExistDestruct]. See [IntoPureT] for why [φ] is a [Type]. *)
Instance into_exist_and_pure PQ P Q (φ : Type) :
  IntoAnd false PQ P Q →
  IntoPureT P φ →
  IntoExist PQ (λ _ : φ, Q) (to_ident_name H) | 10.
Proof.
  intros HPQ (φ'&->&?). rewrite /IntoAnd /= in HPQ.
  rewrite /IntoExist HPQ (into_pure P).
  apply pure_elim_l=> Hφ. by rewrite -(exist_intro Hφ).
Qed.
(* iris/proofmode/class_instances.v *)
(* [to_ident_name H] makes the default name [H] when [P] is destructed with
[iExistDestruct]. See [IntoPureT] for why [φ] is a [Type]. *)
Instance into_exist_sep_pure P Q (φ : Type) :
  IntoPureT P φ →
  TCOr (Affine P) (Absorbing Q) →
  IntoExist (P ∗ Q) (λ _ : φ, Q) (to_ident_name H).
Proof.
  intros (φ'&->&?) ?. rewrite /IntoExist.
  eapply (pure_elim φ'); [by rewrite (into_pure P); apply sep_elim_l, _|]=>?.
  rewrite -exist_intro //. apply sep_elim_r, _.
Qed.
(* iris/proofmode/class_instances.v *)
Instance into_exist_absorbingly {A} P (Φ : A → PROP) name :
  IntoExist P Φ name → IntoExist (<absorb> P) (λ a, <absorb> (Φ a))%I name.
Proof. rewrite /IntoExist=> HP. by rewrite HP absorbingly_exist. Qed.
(* iris/proofmode/class_instances.v *)
Instance into_exist_persistently {A} P (Φ : A → PROP) name :
  IntoExist P Φ name → IntoExist (<pers> P) (λ a, <pers> (Φ a))%I name.
Proof. rewrite /IntoExist=> HP. by rewrite HP persistently_exist. Qed.
(* iris/proofmode/class_instances.v *)
(* IntoForall *)
Instance into_forall_forall {A} (Φ : A → PROP) : IntoForall (∀ a, Φ a) Φ.
Proof. by rewrite /IntoForall. Qed.
(* iris/proofmode/class_instances.v *)
Instance into_forall_tforall {TT : tele} (Φ : TT → PROP) :
  IntoForall (∀.. a, Φ a) Φ | 10.
Proof. by rewrite /IntoForall bi_tforall_forall. Qed.
(* iris/proofmode/class_instances.v *)
Instance into_forall_affinely {A} P (Φ : A → PROP) :
  IntoForall P Φ → IntoForall (<affine> P) (λ a, <affine> (Φ a))%I.
Proof. rewrite /IntoForall=> HP. by rewrite HP affinely_forall. Qed.
(* iris/proofmode/class_instances.v *)
Instance into_forall_intuitionistically {A} P (Φ : A → PROP) :
  IntoForall P Φ → IntoForall (□ P) (λ a, □ (Φ a))%I.
Proof. rewrite /IntoForall=> HP. by rewrite HP intuitionistically_forall. Qed.
(* iris/proofmode/class_instances.v *)
Instance into_forall_persistently `{!BiPersistentlyForall PROP} {A} P (Φ : A → PROP) :
  IntoForall P Φ → IntoForall (<pers> P) (λ a, <pers> (Φ a))%I.
Proof. rewrite /IntoForall=> HP. by rewrite HP persistently_forall. Qed.
(* iris/proofmode/class_instances.v *)
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.
(* iris/proofmode/class_instances.v *)
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) // /bi_affinely right_id emp_wand.
Qed.
(* iris/proofmode/class_instances.v *)
(* These instances must be used only after [into_forall_wand_pure] and
[into_forall_wand_pure] above. *)
Instance into_forall_wand P Q :
  IntoForall (P -∗ Q) (λ _ : ⊢ P, Q) | 10.
Proof. rewrite /IntoForall. apply forall_intro=><-. rewrite emp_wand //. Qed.
(* iris/proofmode/class_instances.v *)
Instance into_forall_impl `{!BiAffine PROP} P Q :
  IntoForall (P → Q) (λ _ : ⊢ P, Q) | 10.
Proof.
  rewrite /IntoForall. apply forall_intro=><-. rewrite -True_emp True_impl //.
Qed.
(* iris/proofmode/class_instances.v *)
(* FromForall *)
Instance from_forall_forall {A} (Φ : A → PROP) name :
  AsIdentName Φ name → FromForall (bi_forall Φ) Φ name.
Proof. by rewrite /FromForall. Qed.
(* iris/proofmode/class_instances.v *)
Instance from_forall_tforall {TT : tele} (Φ : TT → PROP) name :
  AsIdentName Φ name → FromForall (bi_tforall Φ) Φ name.
Proof. by rewrite /FromForall bi_tforall_forall. Qed.