phanerozoic/Coq-Iris huggingface dataset:
(* iris/proofmode/class_instances_later.v *)
Instance into_or_except_0 P Q1 Q2 :
  IntoOr P Q1 Q2 → IntoOr (◇ P) (◇ Q1) (◇ Q2).
Proof. rewrite /IntoOr=>->. by rewrite except_0_or. Qed.
(* iris/proofmode/class_instances_later.v *)
(* FromExist *)
Instance from_exist_later {A} P (Φ : A → PROP) :
  FromExist P Φ → FromExist (▷ P) (λ a, ▷ (Φ a))%I.
Proof.
  rewrite /FromExist=> <-. apply exist_elim=>x. apply later_mono, exist_intro.
Qed.
(* iris/proofmode/class_instances_later.v *)
Instance from_exist_laterN {A} n P (Φ : A → PROP) :
  FromExist P Φ → FromExist (▷^n P) (λ a, ▷^n (Φ a))%I.
Proof.
  rewrite /FromExist=> <-. apply exist_elim=>x. apply laterN_mono, exist_intro.
Qed.
(* iris/proofmode/class_instances_later.v *)
Instance from_exist_except_0 {A} P (Φ : A → PROP) :
  FromExist P Φ → FromExist (◇ P) (λ a, ◇ (Φ a))%I.
Proof. rewrite /FromExist=> <-. by rewrite except_0_exist_2. Qed.
(* iris/proofmode/class_instances_later.v *)
(* IntoExist *)
Instance into_exist_later {A} P (Φ : A → PROP) name :
  IntoExist P Φ name → Inhabited A → IntoExist (▷ P) (λ a, ▷ (Φ a))%I name.
Proof. rewrite /IntoExist=> HP ?. by rewrite HP later_exist. Qed.
(* iris/proofmode/class_instances_later.v *)
Instance into_exist_laterN {A} n P (Φ : A → PROP) name :
  IntoExist P Φ name → Inhabited A → IntoExist (▷^n P) (λ a, ▷^n (Φ a))%I name.
Proof. rewrite /IntoExist=> HP ?. by rewrite HP laterN_exist. Qed.
(* iris/proofmode/class_instances_later.v *)
Instance into_exist_except_0 {A} P (Φ : A → PROP) name :
  IntoExist P Φ name → Inhabited A → IntoExist (◇ P) (λ a, ◇ (Φ a))%I name.
Proof. rewrite /IntoExist=> HP ?. by rewrite HP except_0_exist. Qed.
(* iris/proofmode/class_instances_later.v *)
(* IntoForall *)
Instance into_forall_later {A} P (Φ : A → PROP) :
  IntoForall P Φ → IntoForall (▷ P) (λ a, ▷ (Φ a))%I.
Proof. rewrite /IntoForall=> HP. by rewrite HP later_forall. Qed.
(* iris/proofmode/class_instances_later.v *)
Instance into_forall_laterN {A} P (Φ : A → PROP) n :
  IntoForall P Φ → IntoForall (▷^n P) (λ a, ▷^n (Φ a))%I.
Proof. rewrite /IntoForall=> HP. by rewrite HP laterN_forall. Qed.
(* iris/proofmode/class_instances_later.v *)
Instance into_forall_except_0 {A} P (Φ : A → PROP) :
  IntoForall P Φ → IntoForall (◇ P) (λ a, ◇ (Φ a))%I.
Proof. rewrite /IntoForall=> HP. by rewrite HP except_0_forall. Qed.
(* iris/proofmode/class_instances_later.v *)
(* FromForall *)
Instance from_forall_later {A} P (Φ : A → PROP) name :
  FromForall P Φ name → FromForall (▷ P) (λ a, ▷ (Φ a))%I name.
Proof. rewrite /FromForall=> <-. by rewrite later_forall. Qed.
(* iris/proofmode/class_instances_later.v *)
Instance from_forall_laterN {A} P (Φ : A → PROP) n name :
  FromForall P Φ name → FromForall (▷^n P) (λ a, ▷^n (Φ a))%I name.
Proof. rewrite /FromForall => <-. by rewrite laterN_forall. Qed.
(* iris/proofmode/class_instances_later.v *)
Instance from_forall_except_0 {A} P (Φ : A → PROP) name :
  FromForall P Φ name → FromForall (◇ P) (λ a, ◇ (Φ a))%I name.
Proof. rewrite /FromForall=> <-. by rewrite except_0_forall. Qed.
(* iris/proofmode/class_instances_later.v *)
(* IsExcept0 *)
Instance is_except_0_except_0 P : IsExcept0 (◇ P).
Proof. by rewrite /IsExcept0 except_0_idemp. Qed.
(* iris/proofmode/class_instances_later.v *)
Instance is_except_0_later P : IsExcept0 (▷ P).
Proof. by rewrite /IsExcept0 except_0_later. Qed.
(* iris/proofmode/class_instances_later.v *)
(* FromModal *)
Instance from_modal_later P :
  FromModal True (modality_laterN 1) (▷^1 P) (▷ P) P.
Proof. by rewrite /FromModal. Qed.
(* iris/proofmode/class_instances_later.v *)
Instance from_modal_laterN n P :
  FromModal True (modality_laterN n) (▷^n P) (▷^n P) P.
Proof. by rewrite /FromModal. Qed.
(* iris/proofmode/class_instances_later.v *)
Instance from_modal_except_0 P :
  FromModal True modality_id (◇ P) (◇ P) P.
Proof. by rewrite /FromModal /= -except_0_intro. Qed.
(* iris/proofmode/class_instances_later.v *)
(* IntoExcept0 *)
Instance into_except_0_except_0 P : IntoExcept0 (◇ P) P.
Proof. by rewrite /IntoExcept0. Qed.
(* iris/proofmode/class_instances_later.v *)
Instance into_except_0_later P : Timeless P → IntoExcept0 (▷ P) P.
Proof. by rewrite /IntoExcept0. Qed.
(* iris/proofmode/class_instances_later.v *)
Instance into_except_0_later_if p P : Timeless P → IntoExcept0 (▷?p P) P.
Proof. rewrite /IntoExcept0. destruct p; auto using except_0_intro. Qed.
(* iris/proofmode/class_instances_later.v *)
Instance into_except_0_affinely P Q :
  IntoExcept0 P Q → IntoExcept0 (<affine> P) (<affine> Q).
Proof. rewrite /IntoExcept0=> ->. by rewrite except_0_affinely_2. Qed.
(* iris/proofmode/class_instances_later.v *)
Instance into_except_0_intuitionistically P Q :
  IntoExcept0 P Q → IntoExcept0 (□ P) (□ Q).
Proof. rewrite /IntoExcept0=> ->. by rewrite except_0_intuitionistically_2. Qed.
(* iris/proofmode/class_instances_later.v *)
Instance into_except_0_absorbingly P Q :
  IntoExcept0 P Q → IntoExcept0 (<absorb> P) (<absorb> Q).
Proof. rewrite /IntoExcept0=> ->. by rewrite except_0_absorbingly. Qed.
(* iris/proofmode/class_instances_later.v *)
Instance into_except_0_persistently P Q :
  IntoExcept0 P Q → IntoExcept0 (<pers> P) (<pers> Q).
Proof. rewrite /IntoExcept0=> ->. by rewrite except_0_persistently. Qed.
(* iris/proofmode/class_instances_later.v *)
(* ElimModal *)
Instance elim_modal_timeless p P P' Q :
  IntoExcept0 P P' → IsExcept0 Q → ElimModal True p p P P' Q Q.
Proof.
  intros. rewrite /ElimModal (except_0_intro (_ -∗ _)) (into_except_0 P).
  by rewrite except_0_intuitionistically_if_2 -except_0_sep wand_elim_r.
Qed.
(* iris/proofmode/class_instances_later.v *)
(* Low cost to add a [▷] rather than a [◇] when [P] is timeless. *)
Instance add_modal_later_except_0 P Q :
  Timeless P → AddModal (▷ P) P (◇ Q) | 0.
Proof.
  intros. rewrite /AddModal (except_0_intro (_ -∗ _)) (timeless P).
  by rewrite -except_0_sep wand_elim_r except_0_idemp.
Qed.
(* iris/proofmode/class_instances_later.v *)
Instance add_modal_later P Q :
  Timeless P → AddModal (▷ P) P (▷ Q) | 0.
Proof.
  intros. rewrite /AddModal (except_0_intro (_ -∗ _)) (timeless P).
  by rewrite -except_0_sep wand_elim_r except_0_later.
Qed.
(* iris/proofmode/class_instances_later.v *)
Instance add_modal_except_0 P Q : AddModal (◇ P) P (◇ Q) | 1.
Proof.
  intros. rewrite /AddModal (except_0_intro (_ -∗ _)).
  by rewrite -except_0_sep wand_elim_r except_0_idemp.
Qed.
(* iris/proofmode/class_instances_later.v *)
Instance add_modal_except_0_later P Q : AddModal (◇ P) P (▷ Q) | 1.
Proof.
  intros. rewrite /AddModal (except_0_intro (_ -∗ _)).
  by rewrite -except_0_sep wand_elim_r except_0_later.
Qed.
(* iris/proofmode/class_instances_later.v *)
(* IntoLater *)
Instance into_laterN_0 only_head P : IntoLaterN only_head 0 P P.
Proof. by rewrite /IntoLaterN /MaybeIntoLaterN. Qed.
(* iris/proofmode/class_instances_later.v *)
Instance into_laterN_later only_head n n' m' P Q lQ :
  NatCancel n 1 n' m' →
  (** If canceling has failed (i.e. [1 = m']), we should make progress deeper
  into [P], as such, we continue with the [IntoLaterN] class, which is required
  to make progress. If canceling has succeeded, we do not need to make further
  progress, but there may still be a left-over (i.e. [n']) to cancel more deeply
  into [P], as such, we continue with [MaybeIntoLaterN]. *)
  TCIf (TCEq 1 m') (IntoLaterN only_head n' P Q) (MaybeIntoLaterN only_head n' P Q) →
  (* Similar to [iFrame], the [iNext] tactic also performs a traversal through a
  term (a hypothesis) to find laters to strip. And like [iFrame] we don't want
  this to be excessively smart. So we use the same typeclass as [iFrame] here.
  *)
  MakeLaterN m' Q lQ →
  IntoLaterN only_head n (▷ P) lQ | 2.
Proof.
  rewrite /MakeLaterN /IntoLaterN /MaybeIntoLaterN /NatCancel.
  move=> Hn [_ ->|->] <-;
    by rewrite -later_laterN -laterN_add -Hn Nat.add_comm.
Qed.
(* iris/proofmode/class_instances_later.v *)
Instance into_laterN_laterN only_head n m n' m' P Q lQ :
  NatCancel n m n' m' →
  TCIf (TCEq m m') (IntoLaterN only_head n' P Q) (MaybeIntoLaterN only_head n' P Q) →
  MakeLaterN m' Q lQ →
  IntoLaterN only_head n (▷^m P) lQ | 1.
Proof.
  rewrite /MakeLaterN /IntoLaterN /MaybeIntoLaterN /NatCancel.
  move=> Hn [_ ->|->] <-; by rewrite -!laterN_add -Hn Nat.add_comm.
Qed.
(* iris/proofmode/class_instances_later.v *)
(* When considering [▷?p] where we do not know the value of [p] (0 or 1 laters),
this instance considers the worst case ([p = true]) and cancels a later too much.
Hence this instance has higher cost than [into_laterN_laterN], which does not
cause information loss. See [test_iNext_laterN_bool_later_2]. *)
Instance into_laterN_laterN_bool only_head n p n' m' P Q lQ :
  NatCancel n 1 n' m' →
  TCIf (TCEq 1 m') (IntoLaterN only_head n' P Q) (MaybeIntoLaterN only_head n' P Q) →
  MakeLaterN m' Q lQ →
  IntoLaterN only_head n (▷?p P) lQ | 3.
Proof.
  destruct p; simpl; [apply into_laterN_later|].
  rewrite /MakeLaterN /IntoLaterN /MaybeIntoLaterN /NatCancel.
  move=> Hn [_ ->|->] <-; rewrite -!laterN_add -Hn Nat.add_comm /= -later_intro //.
Qed.
(* iris/proofmode/class_instances_later.v *)
Instance into_laterN_and_l n P1 P2 Q1 Q2 :
  IntoLaterN false n P1 Q1 → MaybeIntoLaterN false n P2 Q2 →
  IntoLaterN false n (P1 ∧ P2) (Q1 ∧ Q2) | 10.
Proof. rewrite /IntoLaterN /MaybeIntoLaterN=> -> ->. by rewrite laterN_and. Qed.
(* iris/proofmode/class_instances_later.v *)
Instance into_laterN_and_r n P P2 Q2 :
  IntoLaterN false n P2 Q2 → IntoLaterN false n (P ∧ P2) (P ∧ Q2) | 11.
Proof.
  rewrite /IntoLaterN /MaybeIntoLaterN=> ->. by rewrite laterN_and -(laterN_intro _ P).
Qed.
(* iris/proofmode/class_instances_later.v *)
Instance into_laterN_forall {A} n (Φ Ψ : A → PROP) :
  (∀ x, IntoLaterN false n (Φ x) (Ψ x)) →
  IntoLaterN false n (∀ x, Φ x) (∀ x, Ψ x).
Proof. rewrite /IntoLaterN /MaybeIntoLaterN laterN_forall=> ?. by apply forall_mono. Qed.
(* iris/proofmode/class_instances_later.v *)
Instance into_laterN_exist {A} n (Φ Ψ : A → PROP) :
  (∀ x, IntoLaterN false n (Φ x) (Ψ x)) →
  IntoLaterN false n (∃ x, Φ x) (∃ x, Ψ x).
Proof. rewrite /IntoLaterN /MaybeIntoLaterN -laterN_exist_2=> ?. by apply exist_mono. Qed.
(* iris/proofmode/class_instances_later.v *)
Instance into_laterN_or_l n P1 P2 Q1 Q2 :
  IntoLaterN false n P1 Q1 → MaybeIntoLaterN false n P2 Q2 →
  IntoLaterN false n (P1 ∨ P2) (Q1 ∨ Q2) | 10.
Proof. rewrite /IntoLaterN /MaybeIntoLaterN=> -> ->. by rewrite laterN_or. Qed.
(* iris/proofmode/class_instances_later.v *)
Instance into_laterN_or_r n P P2 Q2 :
  IntoLaterN false n P2 Q2 →
  IntoLaterN false n (P ∨ P2) (P ∨ Q2) | 11.
Proof.
  rewrite /IntoLaterN /MaybeIntoLaterN=> ->. by rewrite laterN_or -(laterN_intro _ P).
Qed.
(* iris/proofmode/class_instances_later.v *)
Instance into_later_affinely n P Q :
  IntoLaterN false n P Q → IntoLaterN false n (<affine> P) (<affine> Q).
Proof. rewrite /IntoLaterN /MaybeIntoLaterN=> ->. by rewrite laterN_affinely_2. Qed.
(* iris/proofmode/class_instances_later.v *)
Instance into_later_intuitionistically n P Q :
  IntoLaterN false n P Q → IntoLaterN false n (□ P) (□ Q).
Proof. rewrite /IntoLaterN /MaybeIntoLaterN=> ->. by rewrite laterN_intuitionistically_2. Qed.
(* iris/proofmode/class_instances_later.v *)
Instance into_later_absorbingly n P Q :
  IntoLaterN false n P Q → IntoLaterN false n (<absorb> P) (<absorb> Q).
Proof. rewrite /IntoLaterN /MaybeIntoLaterN=> ->. by rewrite laterN_absorbingly. Qed.
(* iris/proofmode/class_instances_later.v *)
Instance into_later_persistently n P Q :
  IntoLaterN false n P Q → IntoLaterN false n (<pers> P) (<pers> Q).
Proof. rewrite /IntoLaterN /MaybeIntoLaterN=> ->. by rewrite laterN_persistently. Qed.
(* iris/proofmode/class_instances_later.v *)
Instance into_laterN_sep_l n P1 P2 Q1 Q2 :
  IntoLaterN false n P1 Q1 → MaybeIntoLaterN false n P2 Q2 →
  IntoLaterN false n (P1 ∗ P2) (Q1 ∗ Q2) | 10.
Proof. rewrite /IntoLaterN /MaybeIntoLaterN=> -> ->. by rewrite laterN_sep. Qed.
(* iris/proofmode/class_instances_later.v *)
Instance into_laterN_sep_r n P P2 Q2 :
  IntoLaterN false n P2 Q2 →
  IntoLaterN false n (P ∗ P2) (P ∗ Q2) | 11.
Proof.
  rewrite /IntoLaterN /MaybeIntoLaterN=> ->. by rewrite laterN_sep -(laterN_intro _ P).
Qed.
(* iris/proofmode/class_instances_later.v *)
Instance into_laterN_big_sepL n {A} (Φ Ψ : nat → A → PROP) (l: list A) :
  (∀ x k, IntoLaterN false n (Φ k x) (Ψ k x)) →
  IntoLaterN false n ([∗ list] k ↦ x ∈ l, Φ k x) ([∗ list] k ↦ x ∈ l, Ψ k x).
Proof.
  rewrite /IntoLaterN /MaybeIntoLaterN=> ?.
  rewrite big_opL_commute. by apply big_sepL_mono.
Qed.
(* iris/proofmode/class_instances_later.v *)
Instance into_laterN_big_sepL2 n {A B} (Φ Ψ : nat → A → B → PROP) l1 l2 :
  (∀ x1 x2 k, IntoLaterN false n (Φ k x1 x2) (Ψ k x1 x2)) →
  IntoLaterN false n ([∗ list] k ↦ y1;y2 ∈ l1;l2, Φ k y1 y2)
    ([∗ list] k ↦ y1;y2 ∈ l1;l2, Ψ k y1 y2).
Proof.
  rewrite /IntoLaterN /MaybeIntoLaterN=> ?.
  rewrite -big_sepL2_laterN_2. by apply big_sepL2_mono.
Qed.
(* iris/proofmode/class_instances_later.v *)
Instance into_laterN_big_sepM n `{Countable K} {A}
    (Φ Ψ : K → A → PROP) (m : gmap K A) :
  (∀ x k, IntoLaterN false n (Φ k x) (Ψ k x)) →
  IntoLaterN false n ([∗ map] k ↦ x ∈ m, Φ k x) ([∗ map] k ↦ x ∈ m, Ψ k x).
Proof.
  rewrite /IntoLaterN /MaybeIntoLaterN=> ?.
  rewrite big_opM_commute. by apply big_sepM_mono.
Qed.
(* iris/proofmode/class_instances_later.v *)
Instance into_laterN_big_sepM2 n `{Countable K} {A B}
    (Φ Ψ : K → A → B → PROP) (m1 : gmap K A) (m2 : gmap K B) :
  (∀ x1 x2 k, IntoLaterN false n (Φ k x1 x2) (Ψ k x1 x2)) →
  IntoLaterN false n ([∗ map] k ↦ x1;x2 ∈ m1;m2, Φ k x1 x2) ([∗ map] k ↦ x1;x2 ∈ m1;m2, Ψ k x1 x2).
Proof.
  rewrite /IntoLaterN /MaybeIntoLaterN=> HΦΨ.
  rewrite -big_sepM2_laterN_2. by apply big_sepM2_mono.
Qed.
(* iris/proofmode/class_instances_later.v *)
Instance into_laterN_big_sepS n `{Countable A}
    (Φ Ψ : A → PROP) (X : gset A) :
  (∀ x, IntoLaterN false n (Φ x) (Ψ x)) →
  IntoLaterN false n ([∗ set] x ∈ X, Φ x) ([∗ set] x ∈ X, Ψ x).
Proof.
  rewrite /IntoLaterN /MaybeIntoLaterN=> ?.
  rewrite big_opS_commute. by apply big_sepS_mono.
Qed.
(* iris/proofmode/class_instances_later.v *)
Instance into_laterN_big_sepMS n `{Countable A}
    (Φ Ψ : A → PROP) (X : gmultiset A) :
  (∀ x, IntoLaterN false n (Φ x) (Ψ x)) →
  IntoLaterN false n ([∗ mset] x ∈ X, Φ x) ([∗ mset] x ∈ X, Ψ x).
Proof.
  rewrite /IntoLaterN /MaybeIntoLaterN=> ?.
  rewrite big_opMS_commute. by apply big_sepMS_mono.
Qed.
(* iris/proofmode/class_instances_make.v *)
(* Affine *)
Instance bi_affine_quick_affine P : BiAffine PROP → QuickAffine P.
Proof. rewrite /QuickAffine. apply _. Qed.
(* iris/proofmode/class_instances_make.v *)
Instance False_quick_affine : @QuickAffine PROP False.
Proof. rewrite /QuickAffine. apply _. Qed.
(* iris/proofmode/class_instances_make.v *)
Instance emp_quick_affine : @QuickAffine PROP emp.
Proof. rewrite /QuickAffine. apply _. Qed.
(* iris/proofmode/class_instances_make.v *)
Instance affinely_quick_affine P : QuickAffine (<affine> P).
Proof. rewrite /QuickAffine. apply _. Qed.
(* iris/proofmode/class_instances_make.v *)
Instance intuitionistically_quick_affine P : QuickAffine (□ P).
Proof. rewrite /QuickAffine. apply _. Qed.
(* iris/proofmode/class_instances_make.v *)
(* Absorbing *)
Instance bi_affine_quick_absorbing P : BiAffine PROP → QuickAbsorbing P.
Proof. rewrite /QuickAbsorbing. apply _. Qed.
(* iris/proofmode/class_instances_make.v *)
Instance pure_quick_absorbing φ : @QuickAbsorbing PROP ⌜ φ ⌝.
Proof. rewrite /QuickAbsorbing. apply _. Qed.
(* iris/proofmode/class_instances_make.v *)
Instance absorbingly_quick_absorbing P : QuickAbsorbing (<absorb> P).
Proof. rewrite /QuickAbsorbing. apply _. Qed.
(* iris/proofmode/class_instances_make.v *)
Instance persistently_quick_absorbing P : QuickAbsorbing (<pers> P).
Proof. rewrite /QuickAbsorbing. apply _. Qed.
(* iris/proofmode/class_instances_make.v *)
(* Embed *)
Instance make_embed_pure {PROP'} `{!BiEmbed PROP PROP'} φ :
  KnownMakeEmbed (PROP:=PROP) ⌜φ⌝ ⌜φ⌝.
Proof. apply embed_pure. Qed.
(* iris/proofmode/class_instances_make.v *)
Instance make_embed_emp {PROP'} `{!BiEmbed PROP PROP'} `{!BiEmbedEmp PROP PROP'} :
  KnownMakeEmbed (PROP:=PROP) emp emp.
Proof. apply embed_emp. Qed.
(* iris/proofmode/class_instances_make.v *)
Instance make_embed_default {PROP'} `{!BiEmbed PROP PROP'} P :
  MakeEmbed P ⎡P⎤ | 100.
Proof. by rewrite /MakeEmbed. Qed.
(* iris/proofmode/class_instances_make.v *)
(* Sep *)
Instance make_sep_emp_l P : KnownLMakeSep emp P P.
Proof. apply left_id, _. Qed.
(* iris/proofmode/class_instances_make.v *)
Instance make_sep_emp_r P : KnownRMakeSep P emp P.
Proof. apply right_id, _. Qed.
(* iris/proofmode/class_instances_make.v *)
Instance make_sep_true_l P : QuickAbsorbing P → KnownLMakeSep True P P.
Proof. rewrite /QuickAbsorbing /KnownLMakeSep /MakeSep=> ?. by apply True_sep. Qed.
(* iris/proofmode/class_instances_make.v *)
Instance make_sep_true_r P : QuickAbsorbing P →  KnownRMakeSep P True P.
Proof. rewrite /QuickAbsorbing /KnownLMakeSep /MakeSep=> ?. by apply sep_True. Qed.
(* iris/proofmode/class_instances_make.v *)
Instance make_sep_default P Q : MakeSep P Q (P ∗ Q) | 100.
Proof. by rewrite /MakeSep. Qed.
(* iris/proofmode/class_instances_make.v *)
(* And *)
Instance make_and_true_l P : KnownLMakeAnd True P P.
Proof. apply left_id, _. Qed.
(* iris/proofmode/class_instances_make.v *)
Instance make_and_true_r P : KnownRMakeAnd P True P.
Proof. by rewrite /KnownRMakeAnd /MakeAnd right_id. Qed.
(* iris/proofmode/class_instances_make.v *)
Instance make_and_emp_l P : QuickAffine P → KnownLMakeAnd emp P P.
Proof. apply emp_and. Qed.
(* iris/proofmode/class_instances_make.v *)
Instance make_and_emp_r P : QuickAffine P → KnownRMakeAnd P emp P.
Proof. apply and_emp. Qed.
(* iris/proofmode/class_instances_make.v *)
Instance make_and_false_l P : KnownLMakeAnd False P False.
Proof. apply left_absorb, _. Qed.
(* iris/proofmode/class_instances_make.v *)
Instance make_and_false_r P : KnownRMakeAnd P False False.
Proof. by rewrite /KnownRMakeAnd /MakeAnd right_absorb. Qed.
(* iris/proofmode/class_instances_make.v *)
Instance make_and_default P Q : MakeAnd P Q (P ∧ Q) | 100.
Proof. by rewrite /MakeAnd. Qed.
(* iris/proofmode/class_instances_make.v *)
(* Or *)
Instance make_or_true_l P : KnownLMakeOr True P True.
Proof. apply left_absorb, _. Qed.
(* iris/proofmode/class_instances_make.v *)
Instance make_or_true_r P : KnownRMakeOr P True True.
Proof. by rewrite /KnownRMakeOr /MakeOr right_absorb. Qed.
(* iris/proofmode/class_instances_make.v *)
Instance make_or_emp_l P : QuickAffine P → KnownLMakeOr emp P emp.
Proof. apply emp_or. Qed.
(* iris/proofmode/class_instances_make.v *)
Instance make_or_emp_r P : QuickAffine P → KnownRMakeOr P emp emp.
Proof. apply or_emp. Qed.
(* iris/proofmode/class_instances_make.v *)
Instance make_or_false_l P : KnownLMakeOr False P P.
Proof. apply left_id, _. Qed.
(* iris/proofmode/class_instances_make.v *)
Instance make_or_false_r P : KnownRMakeOr P False P.
Proof. by rewrite /KnownRMakeOr /MakeOr right_id. Qed.
(* iris/proofmode/class_instances_make.v *)
Instance make_or_default P Q : MakeOr P Q (P ∨ Q) | 100.
Proof. by rewrite /MakeOr. Qed.
(* iris/proofmode/class_instances_make.v *)
(* Affinely

- [make_affinely_affine] adds no modality, but only if the argument is affine.
- [make_affinely_True] turns [True] into [emp]. For an affine BI this instance
  overlaps with [make_affinely_affine], since [True] is affine. Since we prefer
  to avoid [emp] in goals involving affine BIs, we give [make_affinely_affine]
  a lower cost than [make_affinely_True].
- [make_affinely_default] adds the modality. This is the default instance since
  it can always be used, and thus has the highest cost.
  (For this last point, the cost of the [KnownMakeAffinely] instances does not
  actually matter, since this is a [MakeAffinely] instance, i.e. an instance of
  a different class. What really matters is that the [known_make_affinely]
  instance has a lower cost than [make_affinely_default].) *)
Instance make_affinely_affine P :
  QuickAffine P → KnownMakeAffinely P P | 0.
Proof. apply affine_affinely. Qed.
(* iris/proofmode/class_instances_make.v *)
Instance make_affinely_True : @KnownMakeAffinely PROP True emp | 1.
Proof. by rewrite /KnownMakeAffinely /MakeAffinely affinely_True_emp. Qed.
(* iris/proofmode/class_instances_make.v *)
Instance make_affinely_default P : MakeAffinely P (<affine> P) | 100.
Proof. by rewrite /MakeAffinely. Qed.
(* iris/proofmode/class_instances_make.v *)
(* Absorbingly

- [make_absorbingly_absorbing] adds no modality, but only if the argument is
  absorbing.
- [make_absorbingly_emp] turns [emp] into [True]. For an affine BI this instance
  overlaps with [make_absorbingly_absorbing], since [emp] is absorbing. For
  consistency, we give this instance the same cost as [make_affinely_True], but
  it does not really matter since goals in affine BIs typically do not contain
  occurrences of [emp] to start with.
- [make_absorbingly_default] adds the modality. This is the default instance
  since it can always be used, and thus has the highest cost.
  (For this last point, the cost of the [KnownMakeAbsorbingly] instances does not
  actually matter, since this is a [MakeAbsorbingly] instance, i.e. an instance of
  a different class. What really matters is that the [known_make_absorbingly]
  instance has a lower cost than [make_absorbingly_default].) *)
Instance make_absorbingly_absorbing P :
  QuickAbsorbing P → KnownMakeAbsorbingly P P | 0.
Proof. apply absorbing_absorbingly. Qed.
(* iris/proofmode/class_instances_make.v *)
Instance make_absorbingly_emp : @KnownMakeAbsorbingly PROP emp True | 1.
Proof.
  by rewrite /KnownMakeAbsorbingly /MakeAbsorbingly -absorbingly_emp_True.
Qed.
(* iris/proofmode/class_instances_make.v *)
Instance make_absorbingly_default P : MakeAbsorbingly P (<absorb> P) | 100.
Proof. by rewrite /MakeAbsorbingly. Qed.
(* iris/proofmode/class_instances_make.v *)
(* Persistently *)
Instance make_persistently_emp :
  @KnownMakePersistently PROP emp True | 0.
Proof.
  by rewrite /KnownMakePersistently /MakePersistently
     -persistently_True_emp persistently_pure.
Qed.
(* iris/proofmode/class_instances_make.v *)
Instance make_persistently_True :
  @KnownMakePersistently PROP True True | 0.
Proof. by rewrite /KnownMakePersistently /MakePersistently persistently_pure. Qed.
(* iris/proofmode/class_instances_make.v *)
Instance make_persistently_default P :
  MakePersistently P (<pers> P) | 100.
Proof. by rewrite /MakePersistently. Qed.
(* iris/proofmode/class_instances_make.v *)
(* Intuitionistically *)
Instance make_intuitionistically_emp :
  @KnownMakeIntuitionistically PROP emp emp | 0.
Proof.
  by rewrite /KnownMakeIntuitionistically /MakeIntuitionistically
    intuitionistically_emp.
Qed.
(* iris/proofmode/class_instances_make.v *)
(* For affine BIs, we would prefer [□ True] to become [True] rather than [emp],
so we have this instance with lower cost than the next. *)
Instance make_intuitionistically_True_affine :
  BiAffine PROP →
  @KnownMakeIntuitionistically PROP True True | 0.
Proof.
  intros. rewrite /KnownMakeIntuitionistically /MakeIntuitionistically
    intuitionistically_True_emp True_emp //.
Qed.
(* iris/proofmode/class_instances_make.v *)
Instance make_intuitionistically_True :
  @KnownMakeIntuitionistically PROP True emp | 1.
Proof.
  by rewrite /KnownMakeIntuitionistically /MakeIntuitionistically
    intuitionistically_True_emp.
Qed.
(* iris/proofmode/class_instances_make.v *)
Instance make_intuitionistically_default P :
  MakeIntuitionistically P (□ P) | 100.
Proof. by rewrite /MakeIntuitionistically. Qed.
(* iris/proofmode/class_instances_make.v *)
(* Later *)
Instance make_laterN_true n : @KnownMakeLaterN PROP n True True | 0.
Proof. by rewrite /KnownMakeLaterN /MakeLaterN laterN_True. Qed.
(* iris/proofmode/class_instances_make.v *)
Instance make_laterN_emp `{!BiAffine PROP} n :
  @KnownMakeLaterN PROP n emp emp | 0.
Proof. by rewrite /KnownMakeLaterN /MakeLaterN laterN_emp. Qed.
(* iris/proofmode/class_instances_make.v *)
Instance make_laterN_default n P : MakeLaterN n P (▷^n P) | 100.
Proof. by rewrite /MakeLaterN. Qed.
(* iris/proofmode/class_instances_make.v *)
(* Except-0 *)
Instance make_except_0_True : @KnownMakeExcept0 PROP True True.
Proof. by rewrite /KnownMakeExcept0 /MakeExcept0 except_0_True. Qed.