phanerozoic/Coq-Iris huggingface dataset:
(* iris/proofmode/class_instances_frame.v *)
(* Framing a spatial resource [R] under [∨] is done only when:
  - [R] can be framed on both sides of the [∨]; or
  - [R] completely solves one side of the [∨], reducing it to [True].
This instance does _not_ framing spatial resources when they can be framed in
exactly one side, since that can make your goal unprovable. *)
Instance frame_or_spatial progress1 progress2 R P1 P2 Q1 Q2 Q :
  MaybeFrame false R P1 Q1 progress1 →
  MaybeFrame false R P2 Q2 progress2 →
  (** Below [TCOr] encodes the condition described above. If this condition
    cannot be satisfied, the [frame_or_spatial] instance is immediately
    abandoned: the [TCNoBackTrack]s present in the [MaybeFrame] notation
    prevent Coq from considering other ways to construct [MaybeFrame']
    instances. *)
  TCOr (TCEq (progress1 && progress2) true) (TCOr
    (TCAnd (TCEq progress1 true) (TCEq Q1 True%I))
    (TCAnd (TCEq progress2 true) (TCEq Q2 True%I))) →
  MakeOr Q1 Q2 Q →
  Frame false R (P1 ∨ P2) Q | 9.
Proof. rewrite /Frame /MakeOr => [[<-]] [<-] _ <-. by rewrite -sep_or_l. Qed.
(* iris/proofmode/class_instances_frame.v *)
(* Framing a persistent resource [R] under [∨] is done when [R] can be framed
on _at least_ one side. This does not affect provability of your goal,
since you can keep the resource after framing. *)
Instance frame_or_persistent progress1 progress2 R P1 P2 Q1 Q2 Q :
  MaybeFrame true R P1 Q1 progress1 →
  MaybeFrame true R P2 Q2 progress2 →
  (** If below [TCEq] fails, the [frame_or_persistent] instance is immediately
    abandoned: the [TCNoBackTrack]s present in the [MaybeFrame] notation
    prevent Coq from considering other ways to construct [MaybeFrame']
    instances. *)
  TCEq (progress1 || progress2) true →
  MakeOr Q1 Q2 Q → Frame true R (P1 ∨ P2) Q | 9.
Proof. rewrite /Frame /MakeOr => [[<-]] [<-] _ <-. by rewrite -sep_or_l. Qed.
(* iris/proofmode/class_instances_frame.v *)
Instance frame_wand p R P1 P2 Q2 :
  (FrameInstantiateExistDisabled → Frame p R P2 Q2) →
  Frame p R (P1 -∗ P2) (P1 -∗ Q2) | 2.
Proof.
  rewrite /Frame=> /(_ ltac:(constructor)) ?. apply wand_intro_l.
  by rewrite assoc (comm _ P1) -assoc wand_elim_r.
Qed.
(* iris/proofmode/class_instances_frame.v *)
Instance frame_affinely p R P Q Q' :
  TCOr (TCEq p true) (QuickAffine R) →
  Frame p R P Q → MakeAffinely Q Q' →
  Frame p R (<affine> P) Q'.
(* Default cost > 1 *)
Proof.
  rewrite /QuickAffine /Frame /MakeAffinely=> -[->|?] <- <- /=;
    by rewrite -{1}(affine_affinely (_ R)) affinely_sep_2.
Qed.
(* iris/proofmode/class_instances_frame.v *)
Instance frame_intuitionistically R P Q Q' :
  Frame true R P Q → MakeIntuitionistically Q Q' →
  Frame true R (□ P) Q' | 2.
(* Same cost as default. *)
Proof.
  rewrite /Frame /MakeIntuitionistically=> <- <- /=.
  rewrite -intuitionistically_sep_2 intuitionistically_idemp //.
Qed.
(* iris/proofmode/class_instances_frame.v *)
Instance frame_absorbingly p R P Q Q' :
  Frame p R P Q → MakeAbsorbingly Q Q' →
  Frame p R (<absorb> P) Q' | 2.
(* Same cost as default. *)
Proof.
  rewrite /Frame /MakeAbsorbingly=> <- <- /=. by rewrite absorbingly_sep_r.
Qed.
(* iris/proofmode/class_instances_frame.v *)
Instance frame_persistently R P Q Q' :
  Frame true R P Q → MakePersistently Q Q' →
  Frame true R (<pers> P) Q' | 2.
(* Same cost as default. *)
Proof.
  rewrite /Frame /MakePersistently=> <- <- /=.
  rewrite -persistently_and_intuitionistically_sep_l.
  by rewrite -persistently_sep_2 -persistently_and_sep_l_1
    persistently_affinely_elim persistently_idemp.
Qed.
(* iris/proofmode/class_instances_frame.v *)
(* We construct an instance for [Frame]ing under existentials that can both
instantiate the existential and leave it untouched:

- If we have [H : P a] and goal [∃ b, P b ∗ Q b], framing [H] turns the goal
  into [Q a], i.e., instantiates the existential.
- If we have [H : P] and goal [∃ b, P ∗ Q b], framing [H] turns the goal
  into [∃ b, Q b], i.e., leaves the existential untouched.

Below we describe the instances. More information can be found in the paper
https://doi.org/10.1145/3636501.3636950 The general lemma is: *)
Lemma frame_exist_helper {A} p R (Φ : A → PROP)
    {C} (g : C → A) (Ψ : C → PROP) :
  (∀ c, Frame p R (Φ $ g c) (Ψ c)) →
  Frame p R (∃ a, Φ a) (∃ c, Ψ c).
Proof.
  rewrite /Frame=> HΨ. rewrite sep_exist_l.
  apply bi.exist_elim=> c. rewrite HΨ. apply exist_intro.
Qed.
(* iris/proofmode/class_instances_frame.v *)
(* To perform above inference, we introduce a separate equality type class. *)
Inductive GatherEvarsEq {A} (x : A) : A → Prop
:= 
  GatherEvarsEq_refl : GatherEvarsEq x x.
(* iris/proofmode/class_instances_frame.v *)
(* We are now able to state a lemma for building [Frame] instances directly:

[Lemma frame_exist_slow {A} p R (Φ : A → PROP)
    (TT : tele) (g : TT → A) (Ψ : TT → PROP) :
  (∀ c, ∃ a' G,
    Frame p R (Φ a') G ∧
    GatherEvarsEq a' (g c) ∧
    TCEq G (Ψ c)) →
  Frame p R (∃ a, Φ a) (∃.. c, Ψ c)%I.]

Although this would function as intended, the two inner [ex] and [conj]s
repeat terms in the implicit arguments; in particular, they repeat the
quantified goal [Φ] a bunch of times. This means the term size can get quite
big, and make type checking slower than need. We therefore make an effort to
reduce term size and type-checking time by creating a tailored [Class], which
furthermore can be solved automatically by type class search. *)
Class FrameExistRequirements
    (p : bool) (R : PROP) {A} (Φ : A → PROP) (a' : A) (G' : PROP)
:= {
  frame_exist_witness : A;
  frame_exist_resource : PROP;
  frame_exist_proof : Frame p R (Φ frame_exist_witness) frame_exist_resource;
  frame_exist_witness_eq : GatherEvarsEq frame_exist_witness a';
  frame_exist_resource_eq : TCEq frame_exist_resource G'
}.
(* iris/proofmode/class_instances_frame.v *)
(* This class is used so that we can [cbn] away the [bi_texist] in the result
of framing. This is done by the [Hint Extern] at the bottom of the file. *)
Inductive TCCbnTele {A} (x : A) : A → Prop
:=
  TCCbnTele_refl : TCCbnTele x x.
(* iris/proofmode/class_instances_frame.v *)
(* We include a dependency on [FrameInstantiateExistEnabled] so as to disable
this instance when framing beneath [∀], [-∗] and [→] *)
Instance frame_exist {A} p R (Φ : A → PROP)
    (TT : tele) (g : TT → A) (Ψ : TT → PROP) Q :
  FrameInstantiateExistEnabled →
  (∀ c, FrameExistRequirements p R Φ (g c) (Ψ c)) →
  TCCbnTele (∃.. c, Ψ c)%I Q →
  Frame p R (∃ a, Φ a) Q.
Proof.
  move=> _ H <-. rewrite /Frame bi_texist_exist.
  eapply frame_exist_helper=> c.
  by specialize (H c) as [a G HG -> ->].
Qed.
(* iris/proofmode/class_instances_frame.v *)
(* If [FrameInstantiateExistDisabled] holds we are not allowed to instantiate
existentials, so we just frame below the quantifier without instantiating
anything. *)
Instance frame_exist_no_instantiate {A} p R (Φ Ψ : A → PROP) :
  FrameInstantiateExistDisabled →
  (∀ a, Frame p R (Φ a) (Ψ a)) →
  Frame p R (∃ a, Φ a) (∃ a, Ψ a).
Proof. move=> _ H. eapply frame_exist_helper, H. Qed.
(* iris/proofmode/class_instances_frame.v *)
Instance frame_texist {TT : tele} p R (Φ Ψ : TT → PROP) :
  (∀ x, Frame p R (Φ x) (Ψ x)) → Frame p R (∃.. x, Φ x) (∃.. x, Ψ x) | 2.
Proof. rewrite /Frame !bi_texist_exist. apply frame_exist_helper. Qed.
(* iris/proofmode/class_instances_frame.v *)
Instance frame_forall {A} p R (Φ Ψ : A → PROP) :
  (FrameInstantiateExistDisabled → ∀ a, Frame p R (Φ a) (Ψ a)) →
  Frame p R (∀ x, Φ x) (∀ x, Ψ x) | 2.
Proof.
  rewrite /Frame=> /(_ ltac:(constructor)) ?.
  by rewrite sep_forall_l; apply forall_mono.
Qed.
(* iris/proofmode/class_instances_frame.v *)
Instance frame_tforall {TT : tele} p R (Φ Ψ : TT → PROP) :
  (FrameInstantiateExistDisabled → (∀ x, Frame p R (Φ x) (Ψ x))) →
  Frame p R (∀.. x, Φ x) (∀.. x, Ψ x) | 2.
Proof. rewrite /Frame !bi_tforall_forall. apply frame_forall. Qed.
(* iris/proofmode/class_instances_frame.v *)
Instance frame_impl_persistent R P1 P2 Q2 :
  (FrameInstantiateExistDisabled → Frame true R P2 Q2) →
  Frame true R (P1 → P2) (P1 → Q2) | 2.
Proof.
  rewrite /Frame /= => /(_ ltac:(constructor)) ?. apply impl_intro_l.
  by rewrite -persistently_and_intuitionistically_sep_l assoc (comm _ P1) -assoc impl_elim_r
             persistently_and_intuitionistically_sep_l.
Qed.
(* iris/proofmode/class_instances_frame.v *)
(* You may wonder why this uses [Persistent] and not [QuickPersistent].
The reason is that [QuickPersistent] is not needed anywhere else, and
even without [QuickPersistent], this instance avoids quadratic complexity:
we usually use the [Quick*] classes to not traverse the same term over and over
again, but here [P1] is encountered at most once. It is hence not worth adding
a new typeclass just for this extremely rarely used instance. *)
Instance frame_impl R P1 P2 Q2 :
  Persistent P1 → QuickAbsorbing P1 →
  (FrameInstantiateExistDisabled → Frame false R P2 Q2) →
  Frame false R (P1 → P2) (P1 → Q2).
(* Default cost > 1 *)
Proof.
  rewrite /Frame /QuickAbsorbing /==> ?? /(_ ltac:(constructor)) ?.
  apply impl_intro_l.
  rewrite {1}(persistent P1) persistently_and_intuitionistically_sep_l assoc.
  rewrite (comm _ (□ P1)%I) -assoc -persistently_and_intuitionistically_sep_l.
  rewrite persistently_elim impl_elim_r //.
Qed.
(* iris/proofmode/class_instances_frame.v *)
Instance frame_eq_embed `{!BiEmbed PROP PROP', !Sbi PROP,
    !Sbi PROP', !BiEmbedSbi PROP PROP'}
    p P Q (Q' : PROP') {A : ofe} (a b : A) :
  Frame p (a ≡ b) P Q → MakeEmbed Q Q' →
  Frame p (a ≡ b) ⎡P⎤ Q'.
(* Default cost > 1 *)
Proof. rewrite /Frame /MakeEmbed -embed_internal_eq. apply (frame_embed p P Q). Qed.
(* iris/proofmode/class_instances_frame.v *)
Instance frame_later p R R' P Q Q' :
  TCNoBackTrack (MaybeIntoLaterN true 1 R' R) →
  Frame p R P Q → MakeLaterN 1 Q Q' →
  Frame p R' (▷ P) Q'.
(* Default cost > 1 *)
Proof.
  rewrite /Frame /MakeLaterN /MaybeIntoLaterN=>-[->] <- <-.
  by rewrite later_intuitionistically_if_2 later_sep.
Qed.
(* iris/proofmode/class_instances_frame.v *)
Instance frame_laterN p n R R' P Q Q' :
  TCNoBackTrack (MaybeIntoLaterN true n R' R) →
  Frame p R P Q → MakeLaterN n Q Q' →
  Frame p R' (▷^n P) Q'.
(* Default cost > 1 *)
Proof.
  rewrite /Frame /MakeLaterN /MaybeIntoLaterN=>-[->] <- <-.
  by rewrite laterN_intuitionistically_if_2 laterN_sep.
Qed.
(* iris/proofmode/class_instances_frame.v *)
Instance frame_bupd `{!BiBUpd PROP} p R P Q :
  Frame p R P Q → Frame p R (|==> P) (|==> Q) | 2.
Proof. rewrite /Frame=><-. by rewrite bupd_frame_l. Qed.
(* iris/proofmode/class_instances_frame.v *)
Instance frame_fupd `{!BiFUpd PROP} p E1 E2 R P Q :
  Frame p R P Q → Frame p R (|={E1,E2}=> P) (|={E1,E2}=> Q) | 2.
Proof. rewrite /Frame=><-. by rewrite fupd_frame_l. Qed.
(* iris/proofmode/class_instances_frame.v *)
Instance frame_except_0 p R P Q Q' :
  Frame p R P Q → MakeExcept0 Q Q' →
  Frame p R (◇ P) Q' | 2.
(* Same cost as default *)
Proof.
  rewrite /Frame /MakeExcept0=><- <-.
  by rewrite except_0_sep -(except_0_intro (□?p R)).
Qed.
(* iris/proofmode/class_instances_frame.v *)
(* We now write the tactic for constructing [GatherEvarsEq] instances.
We want to prove goals of shape [GatherEvarsEq a (?g c)] with [a : A],
and [g : ?C → A]. We need to infer both the function [g] and [C : tele]. *)
Ltac solve_gather_evars_eq
:=
  lazymatch goal with
  | |- GatherEvarsEq ?a (?g ?c) =>
    let rec retcon_tele T arg :=
      (* [retcon_tele] takes two arguments:
      - [T], an evar that has type [tele]
      - [arg], a term that has type [tele_arg T]
        (recall that [tele_arg] is the [tele → Type] coercion)
      [retcon_tele] will find all the evars occurring in [a], and unify [T]
      to be the telescope with types for all these evars. These evars will be
      unified with projections of [arg].
      In effect, it ensures 'retro-active continuity', namely that the
      telescope [T] was appropriately chosen all along. *)
      match a with
      | context [?term] =>
        is_evar term;
        let X := type of term in
        lazymatch X with
        | tele => fail (* Shortcircuit, since nesting telescopes is a bad idea *)
        | _ => idtac
        end;
        let T' := open_constr:(_) in (* creates a new evar *)
        unify T (TeleS (λ _ : X, T')); 
        (* The evar telescope [T'] is used for any remaining evars *)
        unify term (tele_arg_head (λ _ : X, T') arg);
        (* [tele_arg_head] is the first projection of [arg] *)
        retcon_tele T' (tele_arg_tail (λ _ : X, T') arg)
        (* recurse with the tail projection of [arg] *)
      | _ => 
        (* no more evars: unify [T] with the empty telescope *)
        unify T TeleO
      end
    in
    let T' := lazymatch (type of c) with tele_arg ?T => T end in
    retcon_tele T' c;
    notypeclasses refine (GatherEvarsEq_refl _)
  end.
(* iris/proofmode/class_instances_internal_eq.v *)
(* When a user calls [iPureIntro] on [⊢ a ≡ b], the following instance turns
  turns this into the pure goal [a ≡ b : Prop].
  If [a, b : A] with [LeibnizEquiv A], another candidate would be [a = b]. While
  this does not lead to information loss, [=] is harder to prove than [≡]. We thus
  leave such simplifications to the user (e.g. they can call [fold_leibniz]). *)
Instance from_pure_internal_eq {A : ofe} (a b : A) :
  @FromPure PROP false (a ≡ b) (a ≡ b).
Proof. by rewrite /FromPure pure_internal_eq. Qed.
(* iris/proofmode/class_instances_internal_eq.v *)
(* On the other hand, when a user calls [iIntros "%H"] on [⊢ (a ≡ b) -∗ P],
  it is most convenient if [H] is as strong as possible---meaning, the user would
  rather get [H : a = b] than [H : a ≡ b]. This is only possible if the
  equivalence on [A] implies Leibniz equality (i.e., we have [LeibnizEquiv A]).
  If the equivalence on [A] does not imply Leibniz equality, we cannot simplify
  [a ≡ b] any further.
  The following instance implements above logic, while avoiding a double search
  for [Discrete a]. *)
Instance into_pure_eq {A : ofe} (a b : A) (P : Prop) :
  TCOr (Discrete a) (Discrete b) →
  TCOr (TCAnd (LeibnizEquiv A) (TCEq P (a = b)))
       (TCEq P (a ≡ b)) →
  @IntoPure PROP (a ≡ b) P.
Proof.
  move=> ? [[? ->]|->]; rewrite /IntoPure discrete_eq; last done.
  by rewrite leibniz_equiv_iff.
Qed.
(* iris/proofmode/class_instances_internal_eq.v *)
Instance from_modal_Next {A : ofe} (x y : A) :
  FromModal (PROP1:=PROP) (PROP2:=PROP) True (modality_laterN 1)
    (▷^1 (x ≡ y) : PROP)%I (Next x ≡ Next y) (x ≡ y).
Proof. by rewrite /FromModal /= later_equivI. Qed.
(* iris/proofmode/class_instances_internal_eq.v *)
Instance into_laterN_Next {A : ofe} only_head n n' (x y : A) :
  NatCancel n 1 n' 0 →
  IntoLaterN (PROP:=PROP) only_head n (Next x ≡ Next y) (x ≡ y) | 2.
Proof.
  rewrite /IntoLaterN /MaybeIntoLaterN /NatCancel Nat.add_0_r.
  move=> <-. rewrite later_equivI. by rewrite Nat.add_comm /= -laterN_intro.
Qed.
(* iris/proofmode/class_instances_internal_eq.v *)
Instance into_internal_eq_internal_eq {A : ofe} (x y : A) :
  @IntoInternalEq PROP _ A (x ≡ y) x y.
Proof. by rewrite /IntoInternalEq. Qed.
(* iris/proofmode/class_instances_internal_eq.v *)
Instance into_internal_eq_affinely {A : ofe} (x y : A) P :
  IntoInternalEq P x y → IntoInternalEq (<affine> P) x y.
Proof. rewrite /IntoInternalEq=> ->. by rewrite affinely_elim. Qed.
(* iris/proofmode/class_instances_internal_eq.v *)
Instance into_internal_eq_intuitionistically {A : ofe} (x y : A) P :
  IntoInternalEq P x y → IntoInternalEq (□ P) x y.
Proof. rewrite /IntoInternalEq=> ->. by rewrite intuitionistically_elim. Qed.
(* iris/proofmode/class_instances_internal_eq.v *)
Instance into_internal_eq_absorbingly {A : ofe} (x y : A) P :
  IntoInternalEq P x y → IntoInternalEq (<absorb> P) x y.
Proof. rewrite /IntoInternalEq=> ->. by rewrite absorbingly_internal_eq. Qed.
(* iris/proofmode/class_instances_internal_eq.v *)
Instance into_internal_eq_plainly `{!BiPlainly PROP} {A : ofe} (x y : A) P :
  IntoInternalEq P x y → IntoInternalEq (■ P) x y.
Proof. rewrite /IntoInternalEq=> ->. by rewrite plainly_elim. Qed.
(* iris/proofmode/class_instances_internal_eq.v *)
Instance into_internal_eq_persistently {A : ofe} (x y : A) P :
  IntoInternalEq P x y → IntoInternalEq (<pers> P) x y.
Proof. rewrite /IntoInternalEq=> ->. by rewrite persistently_elim. Qed.
(* iris/proofmode/class_instances_later.v *)
(* FromAssumption *)
Instance from_assumption_later p P Q :
  FromAssumption p P Q → KnownRFromAssumption p P (▷ Q).
Proof. rewrite /KnownRFromAssumption /FromAssumption=>->. apply later_intro. Qed.
(* iris/proofmode/class_instances_later.v *)
Instance from_assumption_laterN n p P Q :
  FromAssumption p P Q → KnownRFromAssumption p P (▷^n Q).
Proof. rewrite /KnownRFromAssumption /FromAssumption=>->. apply laterN_intro. Qed.
(* iris/proofmode/class_instances_later.v *)
Instance from_assumption_except_0 p P Q :
  FromAssumption p P Q → KnownRFromAssumption p P (◇ Q).
Proof. rewrite /KnownRFromAssumption /FromAssumption=>->. apply except_0_intro. Qed.
(* iris/proofmode/class_instances_later.v *)
(* FromPure *)
Instance from_pure_later a P φ : FromPure a P φ → FromPure a (▷ P) φ.
Proof. rewrite /FromPure=> ->. apply later_intro. Qed.
(* iris/proofmode/class_instances_later.v *)
Instance from_pure_laterN a n P φ : FromPure a P φ → FromPure a (▷^n P) φ.
Proof. rewrite /FromPure=> ->. apply laterN_intro. Qed.
(* iris/proofmode/class_instances_later.v *)
Instance from_pure_except_0 a P φ : FromPure a P φ → FromPure a (◇ P) φ.
Proof. rewrite /FromPure=> ->. apply except_0_intro. Qed.
(* iris/proofmode/class_instances_later.v *)
(* IntoWand *)
Instance into_wand_later p q R P Q :
  IntoWand p q R P Q → IntoWand p q (▷ R) (▷ P) (▷ Q).
Proof.
  rewrite /IntoWand /= => HR.
  by rewrite !later_intuitionistically_if_2 -later_wand HR.
Qed.
(* iris/proofmode/class_instances_later.v *)
Instance into_wand_later_args p q R P Q :
  IntoWand p q R P Q → IntoWand' p q R (▷ P) (▷ Q).
Proof.
  rewrite /IntoWand' /IntoWand /= => HR.
  by rewrite !later_intuitionistically_if_2
             (later_intro (□?p R)) -later_wand HR.
Qed.
(* iris/proofmode/class_instances_later.v *)
Instance into_wand_laterN n p q R P Q :
  IntoWand p q R P Q → IntoWand p q (▷^n R) (▷^n P) (▷^n Q).
Proof.
  rewrite /IntoWand /= => HR.
  by rewrite !laterN_intuitionistically_if_2 -laterN_wand HR.
Qed.
(* iris/proofmode/class_instances_later.v *)
Instance into_wand_laterN_args n p q R P Q :
  IntoWand p q R P Q → IntoWand' p q R (▷^n P) (▷^n Q).
Proof.
  rewrite /IntoWand' /IntoWand /= => HR.
  by rewrite !laterN_intuitionistically_if_2
             (laterN_intro _ (□?p R)) -laterN_wand HR.
Qed.
(* iris/proofmode/class_instances_later.v *)
(* FromAnd *)
Instance from_and_later P Q1 Q2 :
  FromAnd P Q1 Q2 → FromAnd (▷ P) (▷ Q1) (▷ Q2).
Proof. rewrite /FromAnd=> <-. by rewrite later_and. Qed.
(* iris/proofmode/class_instances_later.v *)
Instance from_and_laterN n P Q1 Q2 :
  FromAnd P Q1 Q2 → FromAnd (▷^n P) (▷^n Q1) (▷^n Q2).
Proof. rewrite /FromAnd=> <-. by rewrite laterN_and. Qed.
(* iris/proofmode/class_instances_later.v *)
Instance from_and_except_0 P Q1 Q2 :
  FromAnd P Q1 Q2 → FromAnd (◇ P) (◇ Q1) (◇ Q2).
Proof. rewrite /FromAnd=><-. by rewrite except_0_and. Qed.
(* iris/proofmode/class_instances_later.v *)
(* FromSep *)
Instance from_sep_later P Q1 Q2 :
  FromSep P Q1 Q2 → FromSep (▷ P) (▷ Q1) (▷ Q2).
Proof. rewrite /FromSep=> <-. by rewrite later_sep. Qed.
(* iris/proofmode/class_instances_later.v *)
Instance from_sep_laterN n P Q1 Q2 :
  FromSep P Q1 Q2 → FromSep (▷^n P) (▷^n Q1) (▷^n Q2).
Proof. rewrite /FromSep=> <-. by rewrite laterN_sep. Qed.
(* iris/proofmode/class_instances_later.v *)
Instance from_sep_except_0 P Q1 Q2 :
  FromSep P Q1 Q2 → FromSep (◇ P) (◇ Q1) (◇ Q2).
Proof. rewrite /FromSep=><-. by rewrite except_0_sep. Qed.
(* iris/proofmode/class_instances_later.v *)
(* MaybeCombineSepAs *)
Instance maybe_combine_sep_as_later Q1 Q2 P progress :
  MaybeCombineSepAs Q1 Q2 P progress →
  MaybeCombineSepAs (▷ Q1) (▷ Q2) (▷ P) progress.
Proof. by rewrite /MaybeCombineSepAs -later_sep => <-. Qed.
(* iris/proofmode/class_instances_later.v *)
Instance maybe_combine_sep_as_laterN n Q1 Q2 P progress :
  MaybeCombineSepAs Q1 Q2 P progress →
  MaybeCombineSepAs (▷^n Q1) (▷^n Q2) (▷^n P) progress.
Proof. by rewrite /MaybeCombineSepAs -laterN_sep => <-. Qed.
(* iris/proofmode/class_instances_later.v *)
Instance maybe_combine_sep_as_except_0 Q1 Q2 P progress :
  MaybeCombineSepAs Q1 Q2 P progress →
  MaybeCombineSepAs (◇ Q1) (◇ Q2) (◇ P) progress.
Proof. by rewrite /MaybeCombineSepAs -except_0_sep => <-. Qed.
(* iris/proofmode/class_instances_later.v *)
(* MaybeCombineSepGives *)
Instance maybe_combine_sep_gives_later Q1 Q2 P :
  CombineSepGives Q1 Q2 P →
  CombineSepGives (▷ Q1) (▷ Q2) (▷ P).
Proof. by rewrite /CombineSepGives -later_sep -later_persistently => ->. Qed.
(* iris/proofmode/class_instances_later.v *)
Instance maybe_combine_sep_gives_laterN n Q1 Q2 P :
  CombineSepGives Q1 Q2 P →
  CombineSepGives (▷^n Q1) (▷^n Q2) (▷^n P).
Proof. by rewrite /CombineSepGives -laterN_sep -laterN_persistently => ->. Qed.
(* iris/proofmode/class_instances_later.v *)
Instance maybe_combine_sep_gives_except_0 Q1 Q2 P :
  CombineSepGives Q1 Q2 P →
  CombineSepGives (◇ Q1) (◇ Q2) (◇ P).
Proof.
  by rewrite /CombineSepGives -except_0_sep -except_0_persistently => ->.
Qed.
(* iris/proofmode/class_instances_later.v *)
(* IntoAnd *)
Instance into_and_later p P Q1 Q2 :
  IntoAnd p P Q1 Q2 → IntoAnd p (▷ P) (▷ Q1) (▷ Q2).
Proof.
  rewrite /IntoAnd=> HP. apply intuitionistically_if_intro'.
  by rewrite later_intuitionistically_if_2 HP
             intuitionistically_if_elim later_and.
Qed.
(* iris/proofmode/class_instances_later.v *)
Instance into_and_laterN n p P Q1 Q2 :
  IntoAnd p P Q1 Q2 → IntoAnd p (▷^n P) (▷^n Q1) (▷^n Q2).
Proof.
  rewrite /IntoAnd=> HP. apply intuitionistically_if_intro'.
  by rewrite laterN_intuitionistically_if_2 HP
             intuitionistically_if_elim laterN_and.
Qed.
(* iris/proofmode/class_instances_later.v *)
Instance into_and_except_0 p P Q1 Q2 :
  IntoAnd p P Q1 Q2 → IntoAnd p (◇ P) (◇ Q1) (◇ Q2).
Proof.
  rewrite /IntoAnd=> HP. apply intuitionistically_if_intro'.
  by rewrite except_0_intuitionistically_if_2 HP
             intuitionistically_if_elim except_0_and.
Qed.
(* iris/proofmode/class_instances_later.v *)
(* IntoSep *)
Instance into_sep_later P Q1 Q2 :
  IntoSep P Q1 Q2 → IntoSep (▷ P) (▷ Q1) (▷ Q2).
Proof. rewrite /IntoSep=> ->. by rewrite later_sep. Qed.
(* iris/proofmode/class_instances_later.v *)
Instance into_sep_laterN n P Q1 Q2 :
  IntoSep P Q1 Q2 → IntoSep (▷^n P) (▷^n Q1) (▷^n Q2).
Proof. rewrite /IntoSep=> ->. by rewrite laterN_sep. Qed.
(* iris/proofmode/class_instances_later.v *)
Instance into_sep_except_0 P Q1 Q2 :
  IntoSep P Q1 Q2 → IntoSep (◇ P) (◇ Q1) (◇ Q2).
Proof. rewrite /IntoSep=> ->. by rewrite except_0_sep. Qed.
(* iris/proofmode/class_instances_later.v *)
(* FIXME: This instance is overly specific, generalize it. *)
Instance into_sep_affinely_later `{!Timeless (PROP:=PROP) emp} P Q1 Q2 :
  IntoSep P Q1 Q2 → Affine Q1 → Affine Q2 →
  IntoSep (<affine> ▷ P) (<affine> ▷ Q1) (<affine> ▷ Q2).
Proof.
  rewrite /IntoSep /= => -> ??.
  rewrite -{1}(affine_affinely Q1) -{1}(affine_affinely Q2) later_sep !later_affinely_1.
  rewrite -except_0_sep /bi_except_0 affinely_or. apply or_elim, affinely_elim.
  rewrite -(idemp bi_and (<affine> ▷ False)%I) persistent_and_sep_1.
  by rewrite -(False_elim Q1) -(False_elim Q2).
Qed.
(* iris/proofmode/class_instances_later.v *)
(* FromOr *)
Instance from_or_later P Q1 Q2 :
  FromOr P Q1 Q2 → FromOr (▷ P) (▷ Q1) (▷ Q2).
Proof. rewrite /FromOr=><-. by rewrite later_or. Qed.
(* iris/proofmode/class_instances_later.v *)
Instance from_or_laterN n P Q1 Q2 :
  FromOr P Q1 Q2 → FromOr (▷^n P) (▷^n Q1) (▷^n Q2).
Proof. rewrite /FromOr=><-. by rewrite laterN_or. Qed.
(* iris/proofmode/class_instances_later.v *)
Instance from_or_except_0 P Q1 Q2 :
  FromOr P Q1 Q2 → FromOr (◇ P) (◇ Q1) (◇ Q2).
Proof. rewrite /FromOr=><-. by rewrite except_0_or. Qed.
(* iris/proofmode/class_instances_later.v *)
(* IntoOr *)
Instance into_or_later P Q1 Q2 :
  IntoOr P Q1 Q2 → IntoOr (▷ P) (▷ Q1) (▷ Q2).
Proof. rewrite /IntoOr=>->. by rewrite later_or. Qed.
(* iris/proofmode/class_instances_later.v *)
Instance into_or_laterN n P Q1 Q2 :
  IntoOr P Q1 Q2 → IntoOr (▷^n P) (▷^n Q1) (▷^n Q2).
Proof. rewrite /IntoOr=>->. by rewrite laterN_or. Qed.