phanerozoic/Coq-Iris huggingface dataset:
(* iris/program_logic/weakestpre.v *)
Lemma wp_frame_step_l' s E e Φ R :
  TCEq (to_val e) None → ▷ R ∗ WP e @ s; E {{ Φ }} ⊢ WP e @ s; E {{ v, R ∗ Φ v }}.
Proof. iIntros (?) "[??]". iApply (wp_frame_step_l s E E); try iFrame; eauto. Qed.
(* iris/program_logic/weakestpre.v *)
Lemma wp_frame_step_r' s E e Φ R :
  TCEq (to_val e) None → WP e @ s; E {{ Φ }} ∗ ▷ R ⊢ WP e @ s; E {{ v, Φ v ∗ R }}.
Proof. iIntros (?) "[??]". iApply (wp_frame_step_r s E E); try iFrame; eauto. Qed.
(* iris/program_logic/weakestpre.v *)
Lemma wp_wand s E e Φ Ψ :
  WP e @ s; E {{ Φ }} -∗ (∀ v, Φ v -∗ Ψ v) -∗ WP e @ s; E {{ Ψ }}.
Proof.
  iIntros "Hwp H". iApply (wp_strong_mono with "Hwp"); auto.
  iIntros (?) "?". by iApply "H".
Qed.
(* iris/program_logic/weakestpre.v *)
Lemma wp_wand_l s E e Φ Ψ :
  (∀ v, Φ v -∗ Ψ v) ∗ WP e @ s; E {{ Φ }} ⊢ WP e @ s; E {{ Ψ }}.
Proof. iIntros "[H Hwp]". iApply (wp_wand with "Hwp H"). Qed.
(* iris/program_logic/weakestpre.v *)
Lemma wp_wand_r s E e Φ Ψ :
  WP e @ s; E {{ Φ }} ∗ (∀ v, Φ v -∗ Ψ v) ⊢ WP e @ s; E {{ Ψ }}.
Proof. iIntros "[Hwp H]". iApply (wp_wand with "Hwp H"). Qed.
(* iris/program_logic/weakestpre.v *)
Lemma wp_frame_wand s E e Φ R :
  R -∗ WP e @ s; E {{ v, R -∗ Φ v }} -∗ WP e @ s; E {{ Φ }}.
Proof.
  iIntros "HR HWP". iApply (wp_wand with "HWP").
  iIntros (v) "HΦ". by iApply "HΦ".
Qed.
(* iris/program_logic/weakestpre.v *)
Instance frame_wp p s E e R Φ Ψ :
    (FrameInstantiateExistDisabled → ∀ v, Frame p R (Φ v) (Ψ v)) →
    Frame p R (WP e @ s; E {{ Φ }}) (WP e @ s; E {{ Ψ }}) | 2.
Proof.
    rewrite /Frame=> HR. rewrite wp_frame_l. apply wp_mono, HR. constructor.
  Qed.
(* iris/program_logic/weakestpre.v *)
Instance is_except_0_wp s E e Φ : IsExcept0 (WP e @ s; E {{ Φ }}).
Proof. by rewrite /IsExcept0 -{2}fupd_wp -except_0_fupd -fupd_intro. Qed.
(* iris/program_logic/weakestpre.v *)
Instance elim_modal_bupd_wp p s E e P Φ :
    ElimModal True p false (|==> P) P (WP e @ s; E {{ Φ }}) (WP e @ s; E {{ Φ }}).
Proof.
    by rewrite /ElimModal intuitionistically_if_elim
      (bupd_fupd E) fupd_frame_r wand_elim_r fupd_wp.
  Qed.
(* iris/program_logic/weakestpre.v *)
Instance elim_modal_fupd_wp p s E e P Φ :
    ElimModal True p false (|={E}=> P) P (WP e @ s; E {{ Φ }}) (WP e @ s; E {{ Φ }}).
Proof.
    by rewrite /ElimModal intuitionistically_if_elim
      fupd_frame_r wand_elim_r fupd_wp.
  Qed.
(* iris/program_logic/weakestpre.v *)
(* Error message instance for non-mask-changing view shifts.
  Also uses a slightly different error: we cannot apply [fupd_mask_subseteq]
  if [e] is not atomic, so we tell the user to first add a leading [fupd]
  and then change the mask of that. *)
Instance elim_modal_fupd_wp_wrong_mask p s E1 E2 e P Φ :
    ElimModal
      (pm_error "Goal and eliminated modality must have the same mask.
Use [iApply fupd_wp; iMod (fupd_mask_subseteq E2)] to adjust the mask of your goal to [E2]")
      p false
      (|={E2}=> P) False (WP e @ s; E1 {{ Φ }}) False | 100.
Proof. intros []. Qed.
(* iris/program_logic/weakestpre.v *)
Instance elim_modal_fupd_wp_atomic p s E1 E2 e P Φ :
    ElimModal (Atomic (stuckness_to_atomicity s) e) p false
            (|={E1,E2}=> P) P
            (WP e @ s; E1 {{ Φ }}) (WP e @ s; E2 {{ v, |={E2,E1}=> Φ v }})%I | 100.
Proof.
    intros ?. by rewrite intuitionistically_if_elim
      fupd_frame_r wand_elim_r wp_atomic.
  Qed.
(* iris/program_logic/weakestpre.v *)
(* Error message instance for mask-changing view shifts. *)
Instance elim_modal_fupd_wp_atomic_wrong_mask p s E1 E2 E2' e P Φ :
    ElimModal
      (pm_error "Goal and eliminated modality must have the same mask.
Use [iMod (fupd_mask_subseteq E2)] to adjust the mask of your goal to [E2]")
      p false
      (|={E2,E2'}=> P) False
      (WP e @ s; E1 {{ Φ }}) False | 200.
Proof. intros []. Qed.
(* iris/program_logic/weakestpre.v *)
Instance add_modal_fupd_wp s E e P Φ :
    AddModal (|={E}=> P) P (WP e @ s; E {{ Φ }}).
Proof. by rewrite /AddModal fupd_frame_r wand_elim_r fupd_wp. Qed.
(* iris/program_logic/weakestpre.v *)
Instance elim_acc_wp_atomic {X} E1 E2 α β γ e s Φ :
    ElimAcc (X:=X) (Atomic (stuckness_to_atomicity s) e)
            (fupd E1 E2) (fupd E2 E1)
            α β γ (WP e @ s; E1 {{ Φ }})
            (λ x, WP e @ s; E2 {{ v, |={E2}=> β x ∗ (γ x -∗? Φ v) }})%I | 100.
Proof.
    iIntros (?) "Hinner >Hacc". iDestruct "Hacc" as (x) "[Hα Hclose]".
    iApply (wp_wand with "(Hinner Hα)").
    iIntros (v) ">[Hβ HΦ]". iApply "HΦ". by iApply "Hclose".
  Qed.
(* iris/program_logic/weakestpre.v *)
Instance elim_acc_wp_nonatomic {X} E α β γ e s Φ :
    ElimAcc (X:=X) True (fupd E E) (fupd E E)
            α β γ (WP e @ s; E {{ Φ }})
            (λ x, WP e @ s; E {{ v, |={E}=> β x ∗ (γ x -∗? Φ v) }})%I.
Proof.
    iIntros (_) "Hinner >Hacc". iDestruct "Hacc" as (x) "[Hα Hclose]".
    iApply wp_fupd.
    iApply (wp_wand with "(Hinner Hα)").
    iIntros (v) ">[Hβ HΦ]". iApply "HΦ". by iApply "Hclose".
  Qed.
(* iris/proofmode/base.v *)
(* The tactics [resolve_tc] and [try_resolve_ground_tc] are used in the proof
mode to obtain fine control over type class search.

The tactic [resolve_tc t] calls type class search on all evars in [t]. The
tactic fails if type class search fails on at least one evar. This tactic is
non-focusing, so when calling [do_stuff; resolve_tc t], the tactic is executed
even if [do_stuff] closes the goal. This is essential to ensure that no
unshelved type classes remain when a proof mode tactic closes the goal. *)
Ltac resolve_tc
:= ltac2:(t |- Std.resolve_tc (Option.get (Ltac1.to_constr t))).
(* iris/proofmode/base.v *)
(* The tactic [try_resolve_ground_tc t] is similar, but has three differences
compared to [resolve_tc t]:

1. The tactic only calls type class search on evars [?x] whose type is ground
   (i.e., contains no evars). For instance, it would solve [?x : Empty nat] but
   not [?x : BiAffine ?PROP].
2. The tactic does not fail.
3. The tactic is focusing, so when calling [do_stuff; try_resolve_ground_tc t],
   the tactic is not executed when [do_stuff] closes the goal.

The typical mode of use in the proof mode is to call [try_resolve_ground_tc] on
all user-input (e.g., arguments/specialization patterns), and call [resolve_tc]
at the very end. Through [try_resolve_ground_tc] we ensure that classes without
modes are not solved too eagerly (resulting in wrong instances or divergence).
The remaining the classes that are not solved through other means (e.g., search
for [IntoWand], unification with hypotheses) are solved in the end using
[resolve_tc]. *)
Ltac try_resolve_ground_tc t
:=
  lazymatch t with
  (* We proceed under applications to solve the arguments of a given lemma one
  by one. We proceed on both the left and the right of the application to handle
  terms like [lem (@gset A ?eqdec ?countable)]. *)
  | ?t1 ?t2 => try_resolve_ground_tc t1; try_resolve_ground_tc t2
  | _ =>
     let T := type of t in
     try ((* call type class search if [t] has an evar and its type [T] is
          ground. *)
          has_evar t; is_ground T;
          (* [t'] is the result of invoking type class search for [T] *)
          let t' := constr:(_ : T) in
          (* instantiate [t] with its instance [t'] *)
          unify t t')
  end.
(* iris/proofmode/base.v *)
(* Ltac1 does not provide primitives to manipulate lists (e.g., [ident_list],
[simple_intropattern_list]), needed for [iIntros], [iDestruct], etc. We can do
that in Ltac2. For most proofmode tactics we only need to iterate over a list
(either in forward or backward direction). The Ltac1 tactics [ltac1_list_iter]
and [ltac1_list_rev_iter] allow us to do that while encapsulating the Ltac2
code. These tactics can be used as:

  Ltac _iTactic xs :=
    ltac1_list_iter ltac:(fun x => /* stuff */) xs.
  Tactic Notation "iTactic" "(" ne_ident_list(xs) ")" :=
    _iTactic xs.

It is important to note that given one n-ary [Tactic Notation] we cannot call
another n-ary [Tactic Notation]. For example, the following does NOT work:

  Tactic Notation "iAnotherTactic" "(" ne_ident_list(xs) ")" :=
    /* stuff */
    iTactic (xs).

Because of this reason, as already shown above, we typically provide an [Ltac]
called [_iTactic] (note the underscore to mark it is "private"), and define the
[Tactic Notation] as a wrapper, allowing us to write:

  Tactic Notation "iAnotherTactic" "(" ne_ident_list(xs) ")" :=
    /* stuff */
    _iTactic xs. *)
Ltac2 of_ltac1_list l
:= Option.get (Ltac1.to_list l).
(* iris/proofmode/base.v *)
Ltac ltac1_list_iter tac l
:=
  let go := ltac2:(tac l |- List.iter (ltac1:(tac x |- tac x) tac)
                                      (of_ltac1_list l)) in
  go tac l.
(* iris/proofmode/base.v *)
Ltac ltac1_list_rev_iter tac l
:=
  let go := ltac2:(tac l |- List.iter (ltac1:(tac x |- tac x) tac)
                                      (List.rev (of_ltac1_list l))) in
  go tac l.
(* iris/proofmode/base.v *)
(* Since the Ltac1-Ltac2 API only supports unit-returning functions, there is
no nice way to produce an empty list in ltac1. We therefore often define a
special version [_iTactic0] for the empty list. This version can be created
using [with_ltac1_nil]:

  Ltac _iTactic0 := with_ltac1_nil ltac:(fun xs => _iTactic xs) *)
Ltac with_ltac1_nil tac
:=
  let go := ltac2:(tac |- ltac1:(tac l |- tac l) tac (Ltac1.of_list [])) in
  go tac.
(* iris/proofmode/base.v *)
(* Directions of rewrites *)
Inductive direction
:= Left | Right.
(* iris/proofmode/base.v *)
(* Some specific versions of operations on strings, booleans, positive for the
proof mode. We need those so that we can make [cbv] unfold just them, but not
the actual operations that may appear in users' proofs. *)
Lemma lazy_andb_true (b1 b2 : bool) : b1 &&& b2 = true ↔ b1 = true ∧ b2 = true.
Proof. destruct b1, b2; intuition congruence. Qed.
(* iris/proofmode/base.v *)
Definition negb (b : bool) : bool
:= if b then false else true.
(* iris/proofmode/base.v *)
Lemma negb_true b : negb b = true ↔ b = false.
Proof. by destruct b. Qed.
(* iris/proofmode/base.v *)
Fixpoint Pos_succ (x : positive) : positive
:=
  match x with
  | (p~1)%positive => ((Pos_succ p)~0)%positive
  | (p~0)%positive => (p~1)%positive
  | 1%positive => 2%positive
  end.
(* iris/proofmode/base.v *)
Definition beq (b1 b2 : bool) : bool
:=
  match b1, b2 with
  | false, false | true, true => true
  | _, _ => false
  end.
(* iris/proofmode/base.v *)
Definition ascii_beq (x y : ascii) : bool
:=
  let 'Ascii x1 x2 x3 x4 x5 x6 x7 x8 := x in
  let 'Ascii y1 y2 y3 y4 y5 y6 y7 y8 := y in
  beq x1 y1 &&& beq x2 y2 &&& beq x3 y3 &&& beq x4 y4 &&&
    beq x5 y5 &&& beq x6 y6 &&& beq x7 y7 &&& beq x8 y8.
(* iris/proofmode/base.v *)
Fixpoint string_beq (s1 s2 : string) : bool
:=
  match s1, s2 with
  | "", "" => true
  | String a1 s1, String a2 s2 => ascii_beq a1 a2 &&& string_beq s1 s2
  | _, _ => false
  end.
(* iris/proofmode/base.v *)
Lemma beq_true b1 b2 : beq b1 b2 = true ↔ b1 = b2.
Proof. destruct b1, b2; simpl; intuition congruence. Qed.
(* iris/proofmode/base.v *)
Lemma ascii_beq_true x y : ascii_beq x y = true ↔ x = y.
Proof.
  destruct x, y; rewrite /= !lazy_andb_true !beq_true. intuition congruence.
Qed.
(* iris/proofmode/base.v *)
Lemma string_beq_true s1 s2 : string_beq s1 s2 = true ↔ s1 = s2.
Proof.
  revert s2. induction s1 as [|x s1 IH]=> -[|y s2] //=.
  rewrite lazy_andb_true ascii_beq_true IH. intuition congruence.
Qed.
(* iris/proofmode/base.v *)
Lemma string_beq_reflect s1 s2 : reflect (s1 = s2) (string_beq s1 s2).
Proof. apply iff_reflect. by rewrite string_beq_true. Qed.
(* iris/proofmode/base.v *)
Inductive ident
:=
  | IAnon : positive → ident
  | INamed :> string → ident.
(* iris/proofmode/base.v *)
Instance maybe_IAnon : Maybe IAnon
:= λ i,
  match i with IAnon n => Some n | _ => None end.
(* iris/proofmode/base.v *)
Instance maybe_INamed : Maybe INamed
:= λ i,
  match i with INamed s => Some s | _ => None end.
(* iris/proofmode/base.v *)
Instance beq_eq_dec : EqDecision ident.
Proof. solve_decision. Defined.
(* iris/proofmode/base.v *)
Definition positive_beq
:= Eval compute in Pos.eqb.
(* iris/proofmode/base.v *)
Lemma positive_beq_true x y : positive_beq x y = true ↔ x = y.
Proof. apply Pos.eqb_eq. Qed.
(* iris/proofmode/base.v *)
Definition ident_beq (i1 i2 : ident) : bool
:=
  match i1, i2 with
  | IAnon n1, IAnon n2 => positive_beq n1 n2
  | INamed s1, INamed s2 => string_beq s1 s2
  | _, _ => false
  end.
(* iris/proofmode/base.v *)
Lemma ident_beq_true i1 i2 : ident_beq i1 i2 = true ↔ i1 = i2.
Proof.
  destruct i1, i2; rewrite /= ?string_beq_true ?positive_beq_true; naive_solver.
Qed.
(* iris/proofmode/base.v *)
Lemma ident_beq_reflect i1 i2 : reflect (i1 = i2) (ident_beq i1 i2).
Proof. apply iff_reflect. by rewrite ident_beq_true. Qed.
(* iris/proofmode/base.v *)
(* Copies of some functions on [list] and [option] for better reduction control. *)
Fixpoint pm_app {A} (l1 l2 : list A) : list A
:=
  match l1 with [] => l2 | x :: l1 => x :: pm_app l1 l2 end.
(* iris/proofmode/base.v *)
Definition pm_option_bind {A B} (f : A → option B) (mx : option A) : option B
:=
  match mx with Some x => f x | None => None end.
(* iris/proofmode/base.v *)
Definition pm_from_option {A B} (f : A → B) (y : B) (mx : option A) : B
:=
  match mx with None => y | Some x => f x end.
(* iris/proofmode/base.v *)
Definition pm_option_fun {A B} (f : option (A → B)) (x : A) : option B
:=
  match f with None => None | Some f => Some (f x) end.
(* iris/proofmode/base.v *)
(* Can't write [id] here as that would not reduce. *)
Notation pm_default
:= (pm_from_option (λ x, x)).
(* iris/proofmode/classes.v *)
(* Use this as precondition on "failing" instances of typeclasses that have
pure preconditions (such as [ElimModal]), if you want a nice error to be shown
when this instances is picked as part of some proof mode tactic. *)
Inductive pm_error (s : string)
:= .
(* iris/proofmode/classes.v *)
Class FromAssumption {PROP : bi} (p : bool) (P Q : PROP)
:=
  from_assumption : □?p P ⊢ Q.
(* iris/proofmode/classes.v *)
Class KnownLFromAssumption {PROP : bi} (p : bool) (P Q : PROP)
:=
  #[global] knownl_from_assumption :: FromAssumption p P Q.
(* iris/proofmode/classes.v *)
Class KnownRFromAssumption {PROP : bi} (p : bool) (P Q : PROP)
:=
  #[global] knownr_from_assumption :: FromAssumption p P Q.
(* iris/proofmode/classes.v *)
Class IntoPure {PROP : bi} (P : PROP) (φ : Prop)
:=
  into_pure : P ⊢ ⌜φ⌝.
(* iris/proofmode/classes.v *)
(* [IntoPureT] is a variant of [IntoPure] with the argument in [Type] to avoid
some shortcoming of unification in Coq's type class search. An example where we
use this workaround is to repair the following instance:

  Global Instance into_exist_and_pure P Q (φ : Prop) :
    IntoPure P φ → IntoExist (P ∧ Q) (λ _ : φ, Q).

Coq is unable to use this instance: [class_apply] -- which is used by type class
search -- fails with the error that it cannot unify [Prop] and [Type]. This is
probably caused because [class_apply] uses an ancient unification algorith. The
[refine] tactic -- which uses a better unification algorithm -- succeeds to
apply the above instance.

Since we do not want to define [Hint Extern] declarations using [refine] for
any instance like [into_exist_and_pure], we factor this out in the class
[IntoPureT]. This way, we only have to declare a [Hint Extern] using [refine]
once, and use [IntoPureT] in any instance like [into_exist_and_pure].

TODO: Report this as a Coq bug, or wait for https://github.com/coq/coq/pull/991
to be finished and merged someday. *)
Class IntoPureT {PROP : bi} (P : PROP) (φ : Type)
:=
  into_pureT : ∃ ψ : Prop, φ = ψ ∧ IntoPure P ψ.
(* iris/proofmode/classes.v *)
Lemma into_pureT_hint {PROP : bi} (P : PROP) (φ : Prop) : IntoPure P φ → IntoPureT P φ.
Proof. by exists φ. Qed.
(* iris/proofmode/classes.v *)
(* [FromPure a P φ] is used when introducing a pure assertion. It is used by
[iPureIntro] and the [[%]] specialization pattern.

The Boolean [a] specifies whether introduction of [P] needs [emp] in addition
to [φ]. Concretely, for the [iPureIntro] tactic, this means it specifies whether
the spatial context should be empty or not.

Note that the Boolean [a] is not needed for the (dual) [IntoPure] class, because
there we can just ask that [P] is [Affine]. *)
Class FromPure {PROP : bi} (a : bool) (P : PROP) (φ : Prop)
:=
  from_pure : <affine>?a ⌜φ⌝ ⊢ P.
(* iris/proofmode/classes.v *)
Class FromPureT {PROP : bi} (a : bool) (P : PROP) (φ : Type)
:=
  from_pureT : ∃ ψ : Prop, φ = ψ ∧ FromPure a P ψ.
(* iris/proofmode/classes.v *)
Lemma from_pureT_hint {PROP : bi} (a : bool) (P : PROP) (φ : Prop) :
  FromPure a P φ → FromPureT a P φ.
Proof. by exists φ. Qed.
(* iris/proofmode/classes.v *)
Class IntoInternalEq `{!Sbi PROP} {A : ofe} (P : PROP) (x y : A)
:=
  into_internal_eq : P ⊢ x ≡ y.
(* iris/proofmode/classes.v *)
Class IntoPersistent {PROP : bi} (p : bool) (P Q : PROP)
:=
  into_persistent : <pers>?p P ⊢ <pers> Q.
(* iris/proofmode/classes.v *)
(* The [FromModal φ M sel P Q] class is used by the [iModIntro] tactic to
transform a goal [P] into a modality [M] and proposition [Q], under additional
pure assumptions [φ].

The inputs are [P] and [sel] and the outputs are [M] and [Q].

The input [sel] can be used to specify which modality to introduce in case there
are multiple choices to turn [P] into a modality. For example, given [⎡|==> R⎤],
[sel] can be either [|==> ?e] or [⎡ ?e ⎤], which turn it into an update modality
or embedding, respectively. In case there is no need to specify the modality to
introduce, [sel] should be an evar.

For modalities [N] that do not need to augment the proof mode environment, one
can define an instance [FromModal True modality_id (N P) P]. Defining such an
instance only imposes the proof obligation [P ⊢ N P]. Examples of such
modalities [N] are [bupd], [fupd], [except_0], [monPred_subjectively] and
[bi_absorbingly]. *)
Class FromModal {PROP1 PROP2 : bi} {A}
    (φ : Prop) (M : modality PROP1 PROP2) (sel : A) (P : PROP2) (Q : PROP1)
:=
  from_modal : φ → M Q ⊢ P.
(* iris/proofmode/classes.v *)
(* The [FromAffinely P Q] class is used to add an [<affine>] modality to the
proposition [Q].

The input is [Q] and the output is [P]. *)
Class FromAffinely {PROP : bi} (P Q : PROP)
:=
  from_affinely : <affine> Q ⊢ P.
(* iris/proofmode/classes.v *)
(* The [IntoAbsorbingly P Q] class is used to add an [<absorb>] modality to
the proposition [Q].

The input is [Q] and the output is [P]. *)
Class IntoAbsorbingly {PROP : bi} (P Q : PROP)
:=
  into_absorbingly : P ⊢ <absorb> Q.
(* iris/proofmode/classes.v *)
(* Converting an assumption [R] into a wand [P -∗ Q] is done in three stages:

- Strip modalities and universal quantifiers of [R] until an arrow or a wand
  has been obtained.
- Balance modalities in the arguments [P] and [Q] to match the goal (which used
  for [iApply]) or the premise (when used with [iSpecialize] and a specific
  hypothesis).
- Instantiate the premise of the wand or implication. *)
Class IntoWand {PROP : bi} (p q : bool) (R P Q : PROP)
:=
  into_wand : □?p R ⊢ □?q P -∗ Q.
(* iris/proofmode/classes.v *)
Class IntoWand' {PROP : bi} (p q : bool) (R P Q : PROP)
:=
  into_wand' : IntoWand p q R P Q.
(* iris/proofmode/classes.v *)
Class FromWand {PROP : bi} (P Q1 Q2 : PROP)
:= from_wand : (Q1 -∗ Q2) ⊢ P.
(* iris/proofmode/classes.v *)
Class FromImpl {PROP : bi} (P Q1 Q2 : PROP)
:= from_impl : (Q1 → Q2) ⊢ P.
(* iris/proofmode/classes.v *)
Class FromSep {PROP : bi} (P Q1 Q2 : PROP)
:= from_sep : Q1 ∗ Q2 ⊢ P.
(* iris/proofmode/classes.v *)
(* For iSplit{L,R} *)
Class FromAnd {PROP : bi} (P Q1 Q2 : PROP)
:= from_and : Q1 ∧ Q2 ⊢ P.
(* iris/proofmode/classes.v *)
(* The [IntoAnd p P Q1 Q2] class is used to handle some [[H1 H2]] intro
patterns:
- [IntoAnd true] is used for such patterns in the intuitionistic context
- [IntoAnd false] is used for such patterns where one of the two sides is
  discarded (e.g. [[_ H]]) or where the left-hand side is pure as in [[% H]]
  (via an [IntoExist] fallback).

The inputs are [p P] and the outputs are [Q1 Q2]. *)
Class IntoAnd {PROP : bi} (p : bool) (P Q1 Q2 : PROP)
:=
  into_and : □?p P ⊢ □?p (Q1 ∧ Q2).
(* iris/proofmode/classes.v *)
(* The [IntoSep P Q1 Q2] class is used to handle [[H1 H2]] intro patterns in
the spatial context, except:
- when one side is [_], then [IntoAnd] is tried first (but [IntoSep] is used as
  fallback)
- when the left-hand side is [%], then [IntoExist] is used)

The input is [P] and the outputs are [Q1 Q2]. *)
Class IntoSep {PROP : bi} (P Q1 Q2 : PROP)
:=
  into_sep : P ⊢ Q1 ∗ Q2.
(* iris/proofmode/classes.v *)
Class FromOr {PROP : bi} (P Q1 Q2 : PROP)
:= from_or : Q1 ∨ Q2 ⊢ P.
(* iris/proofmode/classes.v *)
Class IntoOr {PROP : bi} (P Q1 Q2 : PROP)
:= into_or : P ⊢ Q1 ∨ Q2.
(* iris/proofmode/classes.v *)
Class FromExist {PROP : bi} {A} (P : PROP) (Φ : A → PROP)
:=
  from_exist : (∃ x, Φ x) ⊢ P.
(* iris/proofmode/classes.v *)
Class IntoExist {PROP : bi} {A} (P : PROP) (Φ : A → PROP) (name: ident_name)
:=
  into_exist : P ⊢ ∃ x, Φ x.
(* iris/proofmode/classes.v *)
Class IntoForall {PROP : bi} {A} (P : PROP) (Φ : A → PROP)
:=
  into_forall : P ⊢ ∀ x, Φ x.
(* iris/proofmode/classes.v *)
Class FromForall {PROP : bi} {A} (P : PROP) (Φ : A → PROP) (name : ident_name)
:=
  from_forall : (∀ x, Φ x) ⊢ P.
(* iris/proofmode/classes.v *)
Class IsExcept0 {PROP : bi} (Q : PROP)
:= is_except_0 : ◇ Q ⊢ Q.
(* iris/proofmode/classes.v *)
(* [CombineSepAs], [MaybeCombineSepAs] and [CombineSepGives] are all used for
  the [iCombine] tactic.

These three classes take two hypotheses [P] and [Q] as input, and return a
(possibly simplified) new hypothesis [R]. [CombineSepAs P Q R] means that [R]
may be obtained by deleting both [P] and [Q], and that [R] is not a trivial
combination. [MaybeCombineSepAs P Q R progress] is like [CombineSepAs], but
[R] can be the trivial combination [P ∗ Q], and the [progress] parameter
indicates whether this trivial combination is used. [CombineSepGives P Q R]
means that [□ R] may be obtained 'for free' from [P] and [Q]. The result [R] of
[CombineSepAs] and [MaybeCombineSepAs] will not contain the observations
from [CombineSepGives].

We deliberately use separate typeclasses [CombineSepAs] and [CombineSepGives].
This allows one to (1) combine hypotheses and get additional persistent
information, (2) only combine the hypotheses, without the additional persistent
information, (3) only get the additional persistent information, while keeping
the original hypotheses. A possible alternative would have been something like
[CombineSepAsGives P1 P2 P R := combine_as_gives : P1 ∗ P2 ⊢ P ∗ □ R],
but this was deemed to be harder to use. Specifically, this would force you to
always specify both [P] and [R], even though one might only have a good
candidate for [P], but not [R], or the other way around.

Note that [FromSep] and [CombineSepAs] have nearly the same definition. However,
they have different Hint Modes and are used for different tactics. [FromSep] is
used to compute the two new goals obtained after applying [iSplitL]/[iSplitR],
taking the current goal as input. [CombineSepAs] is used to combine two
hypotheses into one.

In terms of costs, note that the [AsFractional] instance for [CombineSepAs]
has cost 50. If that instance should take priority over yours, make sure to use
a higher cost. *)
Class CombineSepAs {PROP : bi} (P Q R : PROP)
:= combine_sep_as : P ∗ Q ⊢ R.
(* iris/proofmode/classes.v *)
(* The [progress] parameter is of the following [progress_indicator] type: *)
Inductive progress_indicator
:= MadeProgress | NoProgress.
(* iris/proofmode/classes.v *)
(* This aims to make [MaybeCombineSepAs] instances easier to read than if we
had used Booleans. [NoProgress] indicates that the default instance
[maybe_combine_sep_as_default] below has been used, while [MadeProgress]
indicates that a [CombineSepAs] instance was used. *)
Class MaybeCombineSepAs {PROP : bi}
    (P Q R : PROP) (progress : progress_indicator)
:=
  maybe_combine_sep_as : P ∗ Q ⊢ R.
(* iris/proofmode/classes.v *)
Instance maybe_combine_sep_as_combine_sep_as {PROP : bi} (R P Q : PROP) :
  CombineSepAs P Q R → MaybeCombineSepAs P Q R MadeProgress | 20.
Proof. done. Qed.
(* iris/proofmode/classes.v *)
Instance maybe_combine_sep_as_default {PROP : bi} (P Q : PROP) :
  MaybeCombineSepAs P Q (P ∗ Q) NoProgress | 100.
Proof. intros. by rewrite /MaybeCombineSepAs. Qed.