phanerozoic/Coq-Iris huggingface dataset:
(* iris/proofmode/classes.v *)
(* We do not have this Maybe construction for [CombineSepGives], nor do we
provide the trivial [CombineSepGives P Q True]. This is by design: when the user
writes down a 'gives' clause in the [iCombine] tactic, they intend to receive
non-trivial information. If such information cannot be found, we want to
produce an error, instead of the trivial hypothesis [True]. *)
Class CombineSepGives {PROP : bi} (P Q R : PROP)
:=
  combine_sep_gives : P ∗ Q ⊢ <pers> R.
(* iris/proofmode/classes.v *)
(* The [ElimModal φ p p' P P' Q Q'] class is used by the [iMod] tactic.

The inputs are [p], [P] and [Q], and the outputs are [φ], [p'], [P'] and [Q'].

The class is used to transform a hypothesis [P] into a hypothesis [P'], given
a goal [Q], which is simultaneously transformed into [Q']. The Booleans [p]
and [p'] indicate whether the original, respectively, updated hypothesis reside
in the persistent context (iff [true]). The proposition [φ] can be used to
express a side-condition that [iMod] will generate (if not [True]).

An example instance is:

  ElimModal True p false (|={E1,E2}=> P) P (|={E1,E3}=> Q) (|={E2,E3}=> Q).

This instance expresses that to eliminate [|={E1,E2}=> P] the goal is
transformed from [|={E1,E3}=> Q] into [|={E2,E3}=> Q], and the resulting
hypothesis is moved into the spatial context (regardless of where it was
originally). A corresponding [ElimModal] instance for the Iris 1/2-style update
modality, would have a side-condition [φ] on the masks. *)
Class ElimModal {PROP : bi} (φ : Prop) (p p' : bool) (P P' : PROP) (Q Q' : PROP)
:=
  elim_modal : φ → □?p P ∗ (□?p' P' -∗ Q') ⊢ Q.
(* iris/proofmode/classes.v *)
(* Used by the specialization pattern [ > ] in [iSpecialize] and [iAssert] to
add a modality to the goal corresponding to a premise/asserted proposition. *)
Class AddModal {PROP : bi} (P P' : PROP) (Q : PROP)
:=
  add_modal : P ∗ (P' -∗ Q) ⊢ Q.
(* iris/proofmode/classes.v *)
Lemma add_modal_id {PROP : bi} (P Q : PROP) : AddModal P P Q.
Proof. by rewrite /AddModal wand_elim_r. Qed.
(* iris/proofmode/classes.v *)
(* We use the classes [IsCons] and [IsApp] to make sure that instances such as
[frame_big_sepL_cons] and [frame_big_sepL_app] cannot be applied repeatedly
often when having [ [∗ list] k ↦ x ∈ ?e, Φ k x] with [?e] an evar. *)
Class IsCons {A} (l : list A) (x : A) (k : list A)
:= is_cons : l = x :: k.
(* iris/proofmode/classes.v *)
Class IsApp {A} (l k1 k2 : list A)
:= is_app : l = k1 ++ k2.
(* iris/proofmode/classes.v *)
Instance is_cons_cons {A} (x : A) (l : list A) : IsCons (x :: l) x l.
Proof. done. Qed.
(* iris/proofmode/classes.v *)
Instance is_app_app {A} (l1 l2 : list A) : IsApp (l1 ++ l2) l1 l2.
Proof. done. Qed.
(* iris/proofmode/classes.v *)
(* [IsDisjUnion] is similar to [IsCons] and [IsApp] but identifies the
[disj_union] operator. *)
Class IsDisjUnion `{DisjUnion A} (X X1 X2 : A)
:= is_disj_union : X = X1 ⊎ X2.
(* iris/proofmode/classes.v *)
Instance is_disj_union_disj_union `{DisjUnion A} (X1 X2 : A) :
  IsDisjUnion (X1 ⊎ X2) X1 X2.
Proof. done. Qed.
(* iris/proofmode/classes.v *)
Class Frame {PROP : bi} (p : bool) (R P Q : PROP)
:= frame : □?p R ∗ Q ⊢ P.
(* iris/proofmode/classes.v *)
(* The boolean [progress] indicates whether actual framing has been performed.
If it is [false], then the default instance [maybe_frame_default] below has been
used.
[MaybeFrame'] instances should generally _not_ be used directly---instead, use
the [MaybeFrame] notation defined below. *)
Class MaybeFrame' {PROP : bi} (p : bool) (R P Q : PROP) (progress : bool)
:=
  maybe_frame : □?p R ∗ Q ⊢ P.
(* iris/proofmode/classes.v *)
Instance maybe_frame_frame {PROP : bi} p (R P Q : PROP) :
  Frame p R P Q → MaybeFrame' p R P Q true.
Proof. done. Qed.
(* iris/proofmode/classes.v *)
Instance maybe_frame_default_persistent {PROP : bi} (R P : PROP) :
  MaybeFrame' true R P P false | 100.
Proof. intros. rewrite /MaybeFrame' /=. by rewrite sep_elim_r. Qed.
(* iris/proofmode/classes.v *)
Instance maybe_frame_default {PROP : bi} (R P : PROP) :
  TCOr (Affine R) (Absorbing P) → MaybeFrame' false R P P false | 100.
Proof. intros. rewrite /MaybeFrame' /=. apply: sep_elim_r. Qed.
(* iris/proofmode/classes.v *)
(* We never want to backtrack on instances of [MaybeFrame']. We provide
a notation for [MaybeFrame'] wrapped in the [TCNoBackTrack] construct.
For more details, see also iris!989 and the [frame_and] and [frame_or_spatial]
instances in [class_instances_frame.v] *)
Notation MaybeFrame p R P Q progress
:= (TCNoBackTrack (MaybeFrame' p R P Q progress)).
(* iris/proofmode/classes.v *)
(* The [iFrame] tactic is able to instantiate witnesses for existential
quantifiers. We need a way to disable this behavior beneath connectives
like [∀], [-∗] and [→], since it is often unwanted in these cases.
Also see iris#565.

We implement this using two (notations for) type classes:
[FrameInstantiateExistDisabled] and [FrameInstantiateExistEnabled]. These are
essentially 'flags' for type class search, and do not carry any information:
[FrameInstantiateExistDisabled] is equivalent to [True], but does not come with
any instances. Recursive [Frame] instances can disable instantiating
existentials in their recursive search by replacing the recursive [Frame ...]
premise with [(FrameInstantiateExistDisabled → Frame ...)]. This explicitly
adds a [FrameInstantiateExistDisabled] hypothesis to the recursive [Frame]
search, causing [FrameInstantiateExistDisabled] to have instances in that
recursive search. This will disable the 'strong' instance that instantiates
existential quantifiers, and instead enable a weaker instance that looks
for a [Frame] that works for all possible instantiations. The weaker is enabled
since we made [FrameInstantiateExistDisabled] one of its premises. *)
Class FrameInstantiateExistDisabled : Prop
:= frame_instantiate_exist_disabled {}.
(* iris/proofmode/classes.v *)
(* The strong instance also has a new premise: an instance of
the [FrameInstantiateExistEnabled] type class, defined using stdpp's [TCUnless]. *)
Notation FrameInstantiateExistEnabled
:= (TCUnless FrameInstantiateExistDisabled).
(* iris/proofmode/classes.v *)
(* Since [TCUnless P] will only find an instance if no instance of [P] can be
found, the addition of [FrameInstantiateExistDisabled] to the context disables
the instantiation of existential quantifiers. *)
Class IntoExcept0 {PROP : bi} (P Q : PROP)
:= into_except_0 : P ⊢ ◇ Q.
(* iris/proofmode/classes.v *)
(* The class [MaybeIntoLaterN] has only two instances:

- The default instance [MaybeIntoLaterN n P P], i.e. [▷^n P -∗ P]
- The instance [IntoLaterN n P Q → MaybeIntoLaterN n P Q], where [IntoLaterN]
  is identical to [MaybeIntoLaterN], but is supposed to make progress, i.e. it
  should actually strip a later.

The point of using the auxilary class [IntoLaterN] is to ensure that the
default instance is not applied deeply inside a term, which may result in too
many definitions being unfolded (see issue #55).

For binary connectives we have the following instances:

<<
IntoLaterN n P P'       MaybeIntoLaterN n Q Q'
------------------------------------------
     IntoLaterN n (P /\ Q) (P' /\ Q')


      IntoLaterN n Q Q'
-------------------------------
IntoLaterN n (P /\ Q) (P /\ Q')
>>

The Boolean [only_head] indicates whether laters should only be stripped in
head position or also below other logical connectives. For [iNext] it should
strip laters below other logical connectives, but this should not happen while
framing, e.g. the following should succeed:

<<
Lemma test_iFrame_later_1 P Q : P ∗ ▷ Q -∗ ▷ (P ∗ ▷ Q).
Proof. iIntros "H". iFrame "H". Qed.
>> *)
Class MaybeIntoLaterN {PROP : bi} (only_head : bool) (n : nat) (P Q : PROP)
:=
  maybe_into_laterN : P ⊢ ▷^n Q.
(* iris/proofmode/classes.v *)
Class IntoLaterN {PROP : bi} (only_head : bool) (n : nat) (P Q : PROP)
:=
  #[global] into_laterN :: MaybeIntoLaterN only_head n P Q.
(* iris/proofmode/classes.v *)
Instance maybe_into_laterN_default {PROP : bi} only_head n (P : PROP) :
  MaybeIntoLaterN only_head n P P | 1000.
Proof. apply laterN_intro. Qed.
(* iris/proofmode/classes.v *)
(* In the case both parameters are evars and n=0, we have to stop the
   search and unify both evars immediately instead of looping using
   other instances. *)
Instance maybe_into_laterN_default_0 {PROP : bi} only_head (P : PROP) :
  MaybeIntoLaterN only_head 0 P P | 0.
Proof. apply _. Qed.
(* iris/proofmode/classes.v *)
(* The class [IntoEmbed P Q] is used to transform hypotheses while introducing
embeddings using [iModIntro].

Input: the proposition [P], output: the proposition [Q] so that [P ⊢ ⎡Q⎤]. *)
Class IntoEmbed {PROP PROP' : bi} `{BiEmbed PROP PROP'} (P : PROP') (Q : PROP)
:=
  into_embed : P ⊢ ⎡Q⎤.
(* iris/proofmode/classes.v *)
(* We use two type classes for [AsEmpValid], in order to avoid loops in
   typeclass search. Indeed, the [as_emp_valid_embed] instance would try
   to add an arbitrary number of embeddings. To avoid this, the
   [AsEmpValid0] type class cannot handle embeddings, and therefore
   [as_emp_valid_embed] only tries to add one embedding, and we never try
   to insert nested embeddings. This has the additional advantage of
   always trying [as_emp_valid_embed] as a second option, so that this
   instance is never used when the BI is unknown.

   No Hint Modes are declared here. The appropriate one would be
   [Hint Mode - + ! -], but the fact that Coq ignores primitive
   projections for hints modes would make this fail.

   The direction [d] specifies whether [φ] can be converted to resp. from [⊢ P].
   [iPoseProof] requires [AsEmpValid DirectionIntoEmpValid], while [iStartProof]
   requires [AsEmpValid DirectionFromEmpValid]. We nevertheless use a single
   type class to represent both directions since most instances can be parametric
   in the direction. *)
Inductive as_emp_valid_direction
:=
  | DirectionIntoEmpValid
  | DirectionFromEmpValid.
(* iris/proofmode/classes.v *)
(* We define [AsEmpValid] using a conjunction (instead of a [match] or a record
with two fields) to make it possible to "unfold" [AsEmpValid] and handle both
directions in a uniform manner (e.g., using [rewrite]).
See [as_emp_valid_tforall] for an example. *)
Class AsEmpValid {PROP : bi} (d : as_emp_valid_direction) (φ : Prop) (P : PROP)
:=
  as_emp_valid : (d = DirectionIntoEmpValid → φ → ⊢ P) ∧
                 (d = DirectionFromEmpValid → (⊢ P) → φ).
(* iris/proofmode/classes.v *)
Class AsEmpValid0 {PROP : bi} (d : as_emp_valid_direction) (φ : Prop) (P : PROP)
:=
  as_emp_valid_0 : AsEmpValid d φ P.
(* iris/proofmode/classes.v *)
Lemma as_emp_valid_1 (φ : Prop) {PROP : bi} (P : PROP)
    `{!AsEmpValid DirectionIntoEmpValid φ P} :
  φ → ⊢ P.
Proof. by apply as_emp_valid. Qed.
(* iris/proofmode/classes.v *)
Lemma as_emp_valid_2 (φ : Prop) {PROP : bi} (P : PROP)
    `{!AsEmpValid DirectionFromEmpValid φ P} :
  (⊢ P) → φ.
Proof. by apply as_emp_valid. Qed.
(* iris/proofmode/classes.v *)
(* Input: [P]; Outputs: [N],
   Extracts the namespace associated with an invariant assertion. Used for [iInv]. *)
Class IntoInv {PROP : bi} (P: PROP) (N: namespace).
(* iris/proofmode/classes.v *)
(* Accessors.
    This definition only exists for the purpose of the proof mode; a truly
    usable and general form would use telescopes and also allow binders for the
    closing view shift.  [γ] is an [option] to make it easy for ElimAcc
    instances to recognize the [emp] case and make it look nicer. *)
Definition accessor {PROP : bi} {X : Type} (M1 M2 : PROP → PROP)
           (α β : X → PROP) (mγ : X → option PROP) : PROP
:=
  M1 (∃ x, α x ∗ (β x -∗ M2 (default emp (mγ x))))%I.
(* iris/proofmode/classes.v *)
(* Typeclass for assertions around which accessors can be eliminated.
   Inputs: [Q], [E1], [E2], [α], [β], [γ]
   Outputs: [Q'], [φ]

   Elliminates an accessor [accessor E1 E2 α β γ] in goal [Q'], turning the goal
   into [Q'] with a new assumption [α x], where [φ] is a side-condition at the
   Cow level that needs to hold. *)
Class ElimAcc {PROP : bi} {X : Type} (φ : Prop) (M1 M2 : PROP → PROP)
      (α β : X → PROP) (mγ : X → option PROP)
      (Q : PROP) (Q' : X → PROP)
:=
  elim_acc : φ → ((∀ x, α x -∗ Q' x) -∗ accessor M1 M2 α β mγ -∗ Q).
(* iris/proofmode/classes.v *)
(* Turn [P] into an accessor.
   Inputs:
   - [Pacc]: the assertion to be turned into an accessor (e.g. an invariant)
   Outputs:
   - [Pin]: additional logic assertion needed for starting the accessor.
   - [φ]: additional Coq assertion needed for starting the accessor.
   - [X] [α], [β], [γ]: the accessor parameters.
   - [M1], [M2]: the two accessor modalities (they will typically still have
     some evars though, e.g. for the masks) *)
Class IntoAcc {PROP : bi} {X : Type} (Pacc : PROP) (φ : Prop) (Pin : PROP)
      (M1 M2 : PROP → PROP) (α β : X → PROP) (mγ : X → option PROP)
:=
  into_acc : φ → Pacc -∗ Pin -∗ accessor M1 M2 α β mγ.
(* iris/proofmode/classes.v *)
(* The typeclass used for the [iInv] tactic.
   Input: [Pinv]
   Other Arguments:
   - [Pinv] is an invariant assertion
   - [Pin] is an additional logic assertion needed for opening an invariant
   - [φ] is an additional Coq assertion needed for opening an invariant
   - [Pout] is the assertion obtained by opening the invariant
   - [Pclose] is the closing view shift.  It must be (Some _) or None
     when doing typeclass search as instances are allowed to make a
     case distinction on whether the user wants a closing view-shift or not.
   - [Q] is a goal on which iInv may be invoked
   - [Q'] is the transformed goal that must be proved after opening the invariant.

   Most users will never want to instantiate this; there is a general instance
   based on [ElimAcc] and [IntoAcc].  However, logics like Iris 2 that support
   invariants but not mask-changing fancy updates can use this class directly to
   still benefit from [iInv]. *)
Class ElimInv {PROP : bi} {X : Type} (φ : Prop)
      (Pinv Pin : PROP) (Pout : X → PROP) (mPclose : option (X → PROP))
      (Q : PROP) (Q' : X → PROP)
:=
  elim_inv : φ → Pinv ∗ Pin ∗ (∀ x, Pout x ∗ (default (λ _, emp) mPclose) x -∗ Q' x) ⊢ Q.
(* iris/proofmode/classes.v *)
(* We make sure that tactics that perform actions on *specific* hypotheses or
parts of the goal look through the [tc_opaque] connective, which is used to make
definitions opaque for type class search. For example, when using [iDestruct],
an explicit hypothesis is affected, and as such, we should look through opaque
definitions. However, when using [iFrame] or [iNext], arbitrary hypotheses or
parts of the goal are affected, and as such, type class opacity should be
respected.

This means that there are [tc_opaque] instances for all proofmode type classes
with the exception of:

- [FromAssumption] used by [iAssumption]
- [Frame] and [MaybeFrame] used by [iFrame]
- [MaybeIntoLaterN] and [FromLaterN] used by [iNext]
- [IntoPersistent] used by [iIntuitionistic] *)
Instance into_pure_tc_opaque {PROP : bi} (P : PROP) φ :
  IntoPure P φ → IntoPure (tc_opaque P) φ
:= id.
(* iris/proofmode/classes.v *)
Instance from_pure_tc_opaque {PROP : bi} (a : bool) (P : PROP) φ :
  FromPure a P φ → FromPure a (tc_opaque P) φ
:= id.
(* iris/proofmode/classes.v *)
Instance from_wand_tc_opaque {PROP : bi} (P Q1 Q2 : PROP) :
  FromWand P Q1 Q2 → FromWand (tc_opaque P) Q1 Q2
:= id.
(* iris/proofmode/classes.v *)
Instance into_wand_tc_opaque {PROP : bi} p q (R P Q : PROP) :
  IntoWand p q R P Q → IntoWand p q (tc_opaque R) P Q
:= id.
(* iris/proofmode/classes.v *)
(* This instance has a very high cost. The tactic [iCombine] will look for
[FromSep ?P Q1 Q2]. If the cost of this instance is low (and in particular,
lower than the default instance [from_sep_sep], which picks [?P := Q1 * Q2]),
then TC search would diverge. *)
Instance from_sep_tc_opaque {PROP : bi} (P Q1 Q2 : PROP) :
  FromSep P Q1 Q2 → FromSep (tc_opaque P) Q1 Q2 | 102
:= id.
(* iris/proofmode/classes.v *)
Instance from_and_tc_opaque {PROP : bi} (P Q1 Q2 : PROP) :
  FromAnd P Q1 Q2 → FromAnd (tc_opaque P) Q1 Q2
:= id.
(* iris/proofmode/classes.v *)
Instance into_and_tc_opaque {PROP : bi} p (P Q1 Q2 : PROP) :
  IntoAnd p P Q1 Q2 → IntoAnd p (tc_opaque P) Q1 Q2
:= id.
(* iris/proofmode/classes.v *)
Instance into_sep_tc_opaque {PROP : bi} (P Q1 Q2 : PROP) :
  IntoSep P Q1 Q2 → IntoSep (tc_opaque P) Q1 Q2
:= id.
(* iris/proofmode/classes.v *)
Instance from_or_tc_opaque {PROP : bi} (P Q1 Q2 : PROP) :
  FromOr P Q1 Q2 → FromOr (tc_opaque P) Q1 Q2
:= id.
(* iris/proofmode/classes.v *)
Instance into_or_tc_opaque {PROP : bi} (P Q1 Q2 : PROP) :
  IntoOr P Q1 Q2 → IntoOr (tc_opaque P) Q1 Q2
:= id.
(* iris/proofmode/classes.v *)
Instance from_exist_tc_opaque {PROP : bi} {A} (P : PROP) (Φ : A → PROP) :
  FromExist P Φ → FromExist (tc_opaque P) Φ
:= id.
(* iris/proofmode/classes.v *)
Instance into_exist_tc_opaque {PROP : bi} {A} (P : PROP) (Φ : A → PROP) (name: ident_name) :
  IntoExist P Φ name → IntoExist (tc_opaque P) Φ name
:= id.
(* iris/proofmode/classes.v *)
Instance from_forall_tc_opaque {PROP : bi} {A} (P : PROP) (Φ : A → PROP) (name : ident_name) :
  FromForall P Φ name → FromForall (tc_opaque P) Φ name
:= id.
(* iris/proofmode/classes.v *)
Instance into_forall_tc_opaque {PROP : bi} {A} (P : PROP) (Φ : A → PROP) :
  IntoForall P Φ → IntoForall (tc_opaque P) Φ
:= id.
(* iris/proofmode/classes.v *)
Instance from_modal_tc_opaque {PROP1 PROP2 : bi} {A}
    φ M (sel : A) (P : PROP2) (Q : PROP1) :
  FromModal φ M sel P Q → FromModal φ M sel (tc_opaque P) Q
:= id.
(* iris/proofmode/classes.v *)
Instance elim_modal_tc_opaque {PROP : bi} φ p p' (P P' Q Q' : PROP) :
  ElimModal φ p p' P P' Q Q' → ElimModal φ p p' (tc_opaque P) P' Q Q'
:= id.
(* iris/proofmode/classes.v *)
Instance into_inv_tc_opaque {PROP : bi} (P : PROP) N :
  IntoInv P N → IntoInv (tc_opaque P) N
:= id.
(* iris/proofmode/classes.v *)
Instance elim_inv_tc_opaque {PROP : bi} {X} φ Pinv Pin Pout Pclose Q Q' :
  ElimInv (PROP:=PROP) (X:=X) φ Pinv Pin Pout Pclose Q Q' →
  ElimInv φ (tc_opaque Pinv) Pin Pout Pclose Q Q'
:= id.
(* iris/proofmode/classes_make.v *)
(* Aliases for [Affine] and [Absorbing], but the instances are severely
restricted. They only inspect the top-level symbol or check if the whole BI
is affine. *)
Class QuickAffine {PROP : bi} (P : PROP)
:= quick_affine : Affine P.
(* iris/proofmode/classes_make.v *)
Class QuickAbsorbing {PROP : bi} (P : PROP)
:= quick_absorbing : Absorbing P.
(* iris/proofmode/classes_make.v *)
Class MakeEmbed {PROP PROP' : bi} `{BiEmbed PROP PROP'} (P : PROP) (Q : PROP')
:=
  make_embed : ⎡P⎤ ⊣⊢ Q.
(* iris/proofmode/classes_make.v *)
Class KnownMakeEmbed {PROP PROP' : bi} `{BiEmbed PROP PROP'} (P : PROP) (Q : PROP')
:=
  #[global] known_make_embed :: MakeEmbed P Q.
(* iris/proofmode/classes_make.v *)
Class MakeSep {PROP : bi} (P Q PQ : PROP)
:= make_sep : P ∗ Q ⊣⊢ PQ .
(* iris/proofmode/classes_make.v *)
Class KnownLMakeSep {PROP : bi} (P Q PQ : PROP)
:=
  #[global] knownl_make_sep :: MakeSep P Q PQ.
(* iris/proofmode/classes_make.v *)
Class KnownRMakeSep {PROP : bi} (P Q PQ : PROP)
:=
  #[global] knownr_make_sep :: MakeSep P Q PQ.
(* iris/proofmode/classes_make.v *)
Class MakeAnd {PROP : bi} (P Q PQ : PROP)
:=  make_and_l : P ∧ Q ⊣⊢ PQ.
(* iris/proofmode/classes_make.v *)
Class KnownLMakeAnd {PROP : bi} (P Q PQ : PROP)
:=
  #[global] knownl_make_and :: MakeAnd P Q PQ.
(* iris/proofmode/classes_make.v *)
Class KnownRMakeAnd {PROP : bi} (P Q PQ : PROP)
:=
  #[global] knownr_make_and :: MakeAnd P Q PQ.
(* iris/proofmode/classes_make.v *)
Class MakeOr {PROP : bi} (P Q PQ : PROP)
:= make_or_l : P ∨ Q ⊣⊢ PQ.
(* iris/proofmode/classes_make.v *)
Class KnownLMakeOr {PROP : bi} (P Q PQ : PROP)
:=
  #[global] knownl_make_or :: MakeOr P Q PQ.
(* iris/proofmode/classes_make.v *)
Class KnownRMakeOr {PROP : bi} (P Q PQ : PROP)
:= #[global] knownr_make_or :: MakeOr P Q PQ.
(* iris/proofmode/classes_make.v *)
Class MakeAffinely {PROP : bi} (P Q : PROP)
:=
  make_affinely : <affine> P ⊣⊢ Q.
(* iris/proofmode/classes_make.v *)
Class KnownMakeAffinely {PROP : bi} (P Q : PROP)
:=
  #[global] known_make_affinely :: MakeAffinely P Q.
(* iris/proofmode/classes_make.v *)
Class MakeIntuitionistically {PROP : bi} (P Q : PROP)
:=
  make_intuitionistically : □ P ⊣⊢ Q.
(* iris/proofmode/classes_make.v *)
Class KnownMakeIntuitionistically {PROP : bi} (P Q : PROP)
:=
  #[global] known_make_intuitionistically :: MakeIntuitionistically P Q.
(* iris/proofmode/classes_make.v *)
Class MakeAbsorbingly {PROP : bi} (P Q : PROP)
:=
  make_absorbingly : <absorb> P ⊣⊢ Q.
(* iris/proofmode/classes_make.v *)
Class KnownMakeAbsorbingly {PROP : bi} (P Q : PROP)
:=
  #[global] known_make_absorbingly :: MakeAbsorbingly P Q.
(* iris/proofmode/classes_make.v *)
Class MakePersistently {PROP : bi} (P Q : PROP)
:=
  make_persistently : <pers> P ⊣⊢ Q.
(* iris/proofmode/classes_make.v *)
Class KnownMakePersistently {PROP : bi} (P Q : PROP)
:=
  #[global] known_make_persistently :: MakePersistently P Q.
(* iris/proofmode/classes_make.v *)
Class MakeLaterN {PROP : bi} (n : nat) (P lP : PROP)
:=
  make_laterN : ▷^n P ⊣⊢ lP.
(* iris/proofmode/classes_make.v *)
Class KnownMakeLaterN {PROP : bi} (n : nat) (P lP : PROP)
:=
  #[global] known_make_laterN :: MakeLaterN n P lP.
(* iris/proofmode/classes_make.v *)
Class MakeExcept0 {PROP : bi} (P Q : PROP)
:=
  make_except_0 : ◇ P ⊣⊢ Q.
(* iris/proofmode/classes_make.v *)
Class KnownMakeExcept0 {PROP : bi} (P Q : PROP)
:=
  #[global] known_make_except_0 :: MakeExcept0 P Q.
(* iris/proofmode/class_instances.v *)
(* All leaf instances below are defined with [Hint Extern] to use evarconv
([refine]) instead of legacy unification ([apply]). *)
Lemma from_assumption_exact {PROP : bi} p (P : PROP) : FromAssumption p P P.
Proof. by rewrite /FromAssumption /= intuitionistically_if_elim. Qed.
(* iris/proofmode/class_instances.v *)
Lemma into_wand_wand {PROP : bi} p q (P Q P' : PROP) :
  FromAssumption q P P' → IntoWand p q (P' -∗ Q) P Q.
Proof.
  rewrite /FromAssumption /IntoWand=> HP. by rewrite HP intuitionistically_if_elim.
Qed.
(* iris/proofmode/class_instances.v *)
(* See https://gitlab.mpi-sws.org/iris/iris/issues/288 and [test_iExists_unused]
for an example where an ordinary [Instance] fails. *)
Lemma from_exist_exist {PROP : bi} {A} (Φ : A → PROP) : FromExist (∃ a, Φ a) Φ.
Proof. by rewrite /FromExist. Qed.
(* iris/proofmode/class_instances.v *)
(* AsEmpValid *)
Instance as_emp_valid_emp_valid d P : AsEmpValid0 d (⊢ P) P | 0.
Proof. by rewrite /AsEmpValid. Qed.
(* iris/proofmode/class_instances.v *)
Instance as_emp_valid_entails d P Q : AsEmpValid0 d (P ⊢ Q) (P -∗ Q).
Proof. split => _; [ apply bi.entails_wand | apply bi.wand_entails ]. Qed.
(* iris/proofmode/class_instances.v *)
Instance as_emp_valid_equiv d P Q : AsEmpValid0 d (P ≡ Q) (P ∗-∗ Q).
Proof. split => _; [ apply bi.equiv_wand_iff | apply bi.wand_iff_equiv ]. Qed.
(* iris/proofmode/class_instances.v *)
Instance as_emp_valid_forall d {A : Type} (φ : A → Prop) (P : A → PROP) :
  (∀ x, AsEmpValid d (φ x) (P x)) → AsEmpValid d (∀ x, φ x) (∀ x, P x).
Proof.
  move=>H1. split=>? H2.
  - apply bi.forall_intro=>?. by apply H1, H2.
  - intros x. apply H1 => //. revert H2. by rewrite (bi.forall_elim x).
Qed.
(* iris/proofmode/class_instances.v *)
Instance as_emp_valid_tforall d {TT : tele} (φ : TT → Prop) (P : TT → PROP) :
  (∀ x, AsEmpValid d (φ x) (P x)) → AsEmpValid d (∀.. x, φ x) (∀.. x, P x).
Proof.
  rewrite /AsEmpValid !tforall_forall bi_tforall_forall.
  apply as_emp_valid_forall.
Qed.
(* iris/proofmode/class_instances.v *)
(* FromAffinely *)
Instance from_affinely_affine P : Affine P → FromAffinely P P.
Proof. intros. by rewrite /FromAffinely affinely_elim. Qed.
(* iris/proofmode/class_instances.v *)
Instance from_affinely_default P : FromAffinely (<affine> P) P | 100.
Proof. by rewrite /FromAffinely. Qed.
(* iris/proofmode/class_instances.v *)
Instance from_affinely_intuitionistically P :
  FromAffinely (□ P) (<pers> P) | 100.
Proof. by rewrite /FromAffinely. Qed.
(* iris/proofmode/class_instances.v *)
(* IntoAbsorbingly *)
Instance into_absorbingly_True : @IntoAbsorbingly PROP True emp | 0.
Proof. by rewrite /IntoAbsorbingly -absorbingly_emp_True. Qed.
(* iris/proofmode/class_instances.v *)
Instance into_absorbingly_absorbing P : Absorbing P → IntoAbsorbingly P P | 1.
Proof. intros. by rewrite /IntoAbsorbingly absorbing_absorbingly. Qed.