phanerozoic/Coq-Iris huggingface dataset:
(* iris/bi/lib/fixpoint_mono.v *)
Lemma least_fixpoint_absorbing :
    (∀ Φ, (∀ x, Absorbing (Φ x)) → (∀ x, Absorbing (F Φ x))) →
    ∀ x, Absorbing (bi_least_fixpoint F x).
Proof using Type*.
    intros ? x. rewrite /Absorbing /bi_absorbingly.
    apply wand_elim_r'. revert x.
    iApply least_fixpoint_iter; first solve_proper.
    iIntros "!> %y HF Htrue". iApply least_fixpoint_unfold.
    iAssert (F (λ x : A, True -∗ bi_least_fixpoint F x) y)%I with "[-]" as "HF".
    { by iClear "Htrue". }
    iApply (bi_mono_pred with "[] HF"); first solve_proper.
    iIntros "!> %x HF". by iApply "HF".
  Qed.
(* iris/bi/lib/fixpoint_mono.v *)
Lemma least_fixpoint_persistent_affine :
    (∀ Φ, (∀ x, Affine (Φ x)) → (∀ x, Affine (F Φ x))) →
    (∀ Φ, (∀ x, Persistent (Φ x)) → (∀ x, Persistent (F Φ x))) →
    ∀ x, Persistent (bi_least_fixpoint F x).
Proof using Type*.
    intros ?? x. rewrite /Persistent -intuitionistically_into_persistently_1.
    revert x. iApply least_fixpoint_iter; first solve_proper.
    iIntros "!> %y #HF !>". iApply least_fixpoint_unfold.
    iApply (bi_mono_pred with "[] HF"); first solve_proper.
    by iIntros "!> %x #?".
  Qed.
(* iris/bi/lib/fixpoint_mono.v *)
Lemma least_fixpoint_persistent_absorbing :
    (∀ Φ, (∀ x, Absorbing (Φ x)) → (∀ x, Absorbing (F Φ x))) →
    (∀ Φ, (∀ x, Persistent (Φ x)) → (∀ x, Persistent (F Φ x))) →
    ∀ x, Persistent (bi_least_fixpoint F x).
Proof using Type*.
    intros ??. pose proof (least_fixpoint_absorbing _). unfold Persistent.
    iApply least_fixpoint_iter; first solve_proper.
    iIntros "!> %y #HF !>". rewrite least_fixpoint_unfold.
    iApply (bi_mono_pred with "[] HF"); first solve_proper.
    by iIntros "!> %x #?".
  Qed.
(* iris/bi/lib/fixpoint_mono.v *)
Lemma least_fixpoint_strong_mono
    {PROP : bi} {A : ofe} (F : (A → PROP) → (A → PROP)) `{!BiMonoPred F}
    (G : (A → PROP) → (A → PROP)) `{!BiMonoPred G} :
  □ (∀ Φ x, F Φ x -∗ G Φ x) -∗
  ∀ x, bi_least_fixpoint F x -∗ bi_least_fixpoint G x.
Proof.
  iIntros "#Hmon". iApply least_fixpoint_iter.
  iIntros "!>" (y) "IH". iApply least_fixpoint_unfold.
  by iApply "Hmon".
Qed.
(* iris/bi/lib/fixpoint_mono.v *)
Lemma Private_wf_pred_mono `{!NonExpansive Φ} :
    BiMonoPred (λ (Ψ : A → PROP) (a : A), Φ a ∧ F Ψ a)%I.
Proof using Type*.
    split; last solve_proper.
    intros Ψ Ψ' Hne Hne'. iIntros "#Mon" (x) "Ha". iSplit; first by iDestruct "Ha" as "[$ _]".
    iDestruct "Ha" as "[_ Hr]". iApply (bi_mono_pred with "[] Hr"). by iModIntro.
  Qed.
(* iris/bi/lib/fixpoint_mono.v *)
Lemma least_fixpoint_ind_wf (Φ : A → PROP) `{!NonExpansive Φ} :
    □ (∀ y, F (bi_least_fixpoint (λ Ψ a, Φ a ∧ F Ψ a)) y -∗ Φ y) -∗
    ∀ x, bi_least_fixpoint F x -∗ Φ x.
Proof using Type*.
    iIntros "#Hmon" (x). rewrite least_fixpoint_unfold. iIntros "Hx".
    iApply "Hmon". iApply (bi_mono_pred with "[] Hx").
    iModIntro. iApply least_fixpoint_iter.
    iIntros "!> %y Hy". rewrite least_fixpoint_unfold.
    iSplit; last done. by iApply "Hmon".
  Qed.
(* iris/bi/lib/fixpoint_mono.v *)
Lemma least_fixpoint_ind (Φ : A → PROP) `{!NonExpansive Φ} :
    □ (∀ y, F (λ x, Φ x ∧ bi_least_fixpoint F x) y -∗ Φ y) -∗
    ∀ x, bi_least_fixpoint F x -∗ Φ x.
Proof using Type*.
    iIntros "#Hmon". iApply least_fixpoint_ind_wf. iIntros "!> %y Hy".
    iApply "Hmon". iApply (bi_mono_pred with "[] Hy"). { solve_proper. }
    iIntros "!> %x Hx". iSplit.
    - rewrite least_fixpoint_unfold. iDestruct "Hx" as "[$ _]".
    - iApply (least_fixpoint_strong_mono with "[] Hx"). iIntros "!>" (??) "[_ $]".
  Qed.
(* iris/bi/lib/fixpoint_mono.v *)
Lemma greatest_fixpoint_ne_outer {PROP : bi} {A : ofe}
    (F1 : (A → PROP) → (A → PROP)) (F2 : (A → PROP) → (A → PROP)):
  (∀ Φ x n, F1 Φ x ≡{n}≡ F2 Φ x) → ∀ x1 x2 n,
  x1 ≡{n}≡ x2 → bi_greatest_fixpoint F1 x1 ≡{n}≡ bi_greatest_fixpoint F2 x2.
Proof.
  intros HF x1 x2 n Hx. rewrite /bi_greatest_fixpoint /=.
  do 3 f_equiv; last solve_proper. repeat f_equiv. apply HF.
Qed.
(* iris/bi/lib/fixpoint_mono.v *)
(* Both non-expansiveness lemmas do not seem to be interderivable.
  FIXME: is there some lemma that subsumes both? *)
Lemma greatest_fixpoint_ne' {PROP : bi} {A : ofe} (F : (A → PROP) → (A → PROP)):
  (∀ Φ, NonExpansive Φ → NonExpansive (F Φ)) → NonExpansive (bi_greatest_fixpoint F).
Proof. solve_proper. Qed.
(* iris/bi/lib/fixpoint_mono.v *)
Instance greatest_fixpoint_ne {PROP : bi} {A : ofe} n :
  Proper (pointwise_relation (A → PROP) (pointwise_relation A (dist n)) ==>
          dist n ==> dist n) bi_greatest_fixpoint.
Proof. solve_proper. Qed.
(* iris/bi/lib/fixpoint_mono.v *)
Instance greatest_fixpoint_proper {PROP : bi} {A : ofe} :
  Proper (pointwise_relation (A → PROP) (pointwise_relation A (≡)) ==>
          (≡) ==> (≡)) bi_greatest_fixpoint.
Proof. solve_proper. Qed.
(* iris/bi/lib/fixpoint_mono.v *)
Lemma greatest_fixpoint_unfold_1 x :
    bi_greatest_fixpoint F x ⊢ F (bi_greatest_fixpoint F) x.
Proof using Type*.
    iDestruct 1 as (Φ) "[#Hincl HΦ]".
    iApply (bi_mono_pred Φ (bi_greatest_fixpoint F) with "[#]").
    - iIntros "!>" (y) "Hy". iExists Φ. auto.
    - by iApply "Hincl".
  Qed.
(* iris/bi/lib/fixpoint_mono.v *)
Lemma greatest_fixpoint_unfold_2 x :
    F (bi_greatest_fixpoint F) x ⊢ bi_greatest_fixpoint F x.
Proof using Type*.
    iIntros "HF". iExists (OfeMor (F (bi_greatest_fixpoint F))).
    iSplit; last done. iIntros "!>" (y) "Hy /=". iApply (bi_mono_pred with "[#] Hy").
    iIntros "!>" (z) "?". by iApply greatest_fixpoint_unfold_1.
  Qed.
(* iris/bi/lib/fixpoint_mono.v *)
Corollary greatest_fixpoint_unfold x :
    bi_greatest_fixpoint F x ≡ F (bi_greatest_fixpoint F) x.
Proof using Type*.
    apply (anti_symm _); auto using greatest_fixpoint_unfold_1, greatest_fixpoint_unfold_2.
  Qed.
(* iris/bi/lib/fixpoint_mono.v *)
(* The following lemma provides basic coinduction capabilities,
    by requiring to reestablish the coinduction hypothesis after exactly one step. *)
Lemma greatest_fixpoint_coiter (Φ : A → PROP) `{!NonExpansive Φ} :
    □ (∀ y, Φ y -∗ F Φ y) -∗ ∀ x, Φ x -∗ bi_greatest_fixpoint F x.
Proof. iIntros "#HΦ" (x) "Hx". iExists (OfeMor Φ). auto. Qed.
(* iris/bi/lib/fixpoint_mono.v *)
Lemma greatest_fixpoint_absorbing :
    (∀ Φ, (∀ x, Absorbing (Φ x)) → (∀ x, Absorbing (F Φ x))) →
    ∀ x, Absorbing (bi_greatest_fixpoint F x).
Proof using Type*.
    intros ?. rewrite /Absorbing.
    iApply greatest_fixpoint_coiter; first solve_proper.
    iIntros "!> %y >HF". iDestruct (greatest_fixpoint_unfold with "HF") as "HF".
    iApply (bi_mono_pred with "[] HF"); first solve_proper.
    by iIntros "!> %x HF !>".
  Qed.
(* iris/bi/lib/fixpoint_mono.v *)
Lemma greatest_fixpoint_strong_mono {PROP : bi} {A : ofe}
  (F : (A → PROP) → (A → PROP)) `{!BiMonoPred F}
  (G : (A → PROP) → (A → PROP)) `{!BiMonoPred G} :
  □ (∀ Φ x, F Φ x -∗ G Φ x) -∗
  ∀ x, bi_greatest_fixpoint F x -∗ bi_greatest_fixpoint G x.
Proof using Type*.
  iIntros "#Hmon". iApply greatest_fixpoint_coiter.
  iIntros "!>" (y) "IH". rewrite greatest_fixpoint_unfold.
  by iApply "Hmon".
Qed.
(* iris/bi/lib/fixpoint_mono.v *)
Lemma Private_paco_mono `{!NonExpansive Φ} :
    BiMonoPred (λ (Ψ : A → PROP) (a : A), Φ a ∨ F Ψ a)%I.
Proof using Type*.
    split; last solve_proper.
    intros Ψ Ψ' Hne Hne'. iIntros "#Mon" (x) "[H1|H2]"; first by iLeft.
    iRight. iApply (bi_mono_pred with "[] H2"). by iModIntro.
  Qed.
(* iris/bi/lib/fixpoint_mono.v *)
Lemma greatest_fixpoint_paco (Φ : A → PROP) `{!NonExpansive Φ} :
    □ (∀ y, Φ y -∗ F (bi_greatest_fixpoint (λ Ψ a, Φ a ∨ F Ψ a)) y) -∗
    ∀ x, Φ x -∗ bi_greatest_fixpoint F x.
Proof using Type*.
    iIntros "#Hmon" (x) "HΦ". iDestruct ("Hmon" with "HΦ") as "HF".
    rewrite greatest_fixpoint_unfold. iApply (bi_mono_pred with "[] HF").
    iIntros "!>" (y) "HG". iApply (greatest_fixpoint_coiter with "[] HG").
    iIntros "!>" (z) "Hf". rewrite greatest_fixpoint_unfold.
    iDestruct "Hf" as "[HΦ|$]". by iApply "Hmon".
  Qed.
(* iris/bi/lib/fixpoint_mono.v *)
Lemma greatest_fixpoint_coind (Φ : A → PROP) `{!NonExpansive Φ} :
    □ (∀ y, Φ y -∗ F (λ x, Φ x ∨ bi_greatest_fixpoint F x) y) -∗
    ∀ x, Φ x -∗ bi_greatest_fixpoint F x.
Proof using Type*.
    iIntros "#Ha". iApply greatest_fixpoint_paco. iModIntro.
    iIntros (y) "Hy". iSpecialize ("Ha" with "Hy").
    iApply (bi_mono_pred with "[] Ha"). { solve_proper. }
    iIntros "!> %x [Hphi | Hgfp]".
    - iApply greatest_fixpoint_unfold. eauto.
    - iApply (greatest_fixpoint_strong_mono with "[] Hgfp"); eauto.
  Qed.
(* iris/bi/lib/fractional.v *)
Class Fractional {PROP : bi} (Φ : Qp → PROP)
:=
  fractional p q : Φ (p + q)%Qp ⊣⊢ Φ p ∗ Φ q.
(* iris/bi/lib/fractional.v *)
(* The [AsFractional] typeclass eta-expands a proposition [P] into [Φ q] such
that [Φ] is a fractional predicate. This is needed because higher-order
unification cannot be relied upon to guess the right [Φ].

[AsFractional] should generally be used in APIs that work with fractional
predicates (instead of [Fractional]): when the user provides the original
resource [P], have a premise [AsFractional P Φ 1] to convert that into some
fractional predicate.

The equivalence in [as_fractional] should hold definitionally; various typeclass
instances assume that [Φ q] will un-do the eta-expansion performed by
[AsFractional]. *)
Class AsFractional {PROP : bi} (P : PROP) (Φ : Qp → PROP) (q : Qp)
:= {
  as_fractional : P ⊣⊢ Φ q;
  as_fractional_fractional : Fractional Φ
}.
(* iris/bi/lib/fractional.v *)
(* The class [FrameFractionalQp] is used for fractional framing, it subtracts
the fractional of the hypothesis from the goal: it computes [r := qP - qR].
See [frame_fractional] for how it is used. *)
Class FrameFractionalQp (qR qP r : Qp)
:=
  frame_fractional_qp : qP = (qR + r)%Qp.
(* iris/bi/lib/fractional.v *)
Instance Fractional_proper :
    Proper (pointwise_relation _ (≡) ==> iff) (@Fractional PROP).
Proof.
    rewrite /Fractional.
    intros Φ1 Φ2 Hequiv.
    by setoid_rewrite Hequiv.
  Qed.
(* iris/bi/lib/fractional.v *)
(* Every [Fractional] predicate admits an obvious [AsFractional] instance.

  Ideally, this instance would mean that a user never has to define a manual
  [AsFractional] instance for a [Fractional] predicate (even if it's of the
  form [λ q, Φ a1 ‥ q ‥ an] for some n-ary predicate [Φ].) However, Coq's
  lack of guarantees for higher-order unification mean this instance wouldn't
  guarantee to apply for every [AsFractional] goal.

  Therefore, this instance is not global to avoid conflicts with existing instances
  defined by our users, since we can't ask users to universally delete their
  manually-defined [AsFractional] instances for their own [Fractional] predicates.

  (We could just support this instance for predicates with the fractional argument
  in the final position, but that was felt to be a bit of a foot-gun - users would
  have to remember to *not* define an [AsFractional] some of the time.) *)
Instance fractional_as_fractional Φ q :
    Fractional Φ → AsFractional (Φ q) Φ q.
Proof. done. Qed.
(* iris/bi/lib/fractional.v *)
(* This lemma is meant to be used when [P] is known. But really you should be
   using [iDestruct "H" as "[H1 H2]"], which supports splitting at fractions. *)
Lemma fractional_split P Φ q1 q2 :
    AsFractional P Φ (q1 + q2) →
    P ⊣⊢ Φ q1 ∗ Φ q2.
Proof. by move=>-[-> ->]. Qed.
(* iris/bi/lib/fractional.v *)
(* This lemma is meant to be used when [P] is known. But really you should be
   using [iDestruct "H" as "[H1 H2]"], which supports halving fractions. *)
Lemma fractional_half P Φ q :
    AsFractional P Φ q →
    P ⊣⊢ Φ (q/2)%Qp ∗ Φ (q/2)%Qp.
Proof. by rewrite -{1}(Qp.div_2 q)=>-[->->]. Qed.
(* iris/bi/lib/fractional.v *)
(* This lemma is meant to be used when [P1], [P2] are known. But really you
   should be using [iCombine "H1 H2" as "H"] (for forwards reasoning) or
   [iSplitL]/[iSplitR] (for goal-oriented reasoning), which support merging
   fractions. *)
Lemma fractional_merge P1 P2 Φ q1 q2 `{!Fractional Φ} :
    AsFractional P1 Φ q1 → AsFractional P2 Φ q2 →
    P1 ∗ P2 ⊣⊢ Φ (q1 + q2)%Qp.
Proof. move=>-[-> _] [-> _]. rewrite fractional //. Qed.
(* iris/bi/lib/fractional.v *)
(* Fractional and logical connectives *)
Instance persistent_fractional (P : PROP) :
    Persistent P → TCOr (Affine P) (Absorbing P) → Fractional (λ _, P).
Proof. intros ?? q q'. apply: bi.persistent_sep_dup. Qed.
(* iris/bi/lib/fractional.v *)
(* We do not have [AsFractional] instances for [∗] and the big operators
  because the [iDestruct] tactic already turns [P ∗ Q] into [P] and [Q],
  [[∗ list] k↦x ∈ y :: l, Φ k x] into [Φ 0 i] and [[∗ list] k↦x ∈ l, Φ (S k) x],
  etc. Hence, an [AsFractional] instance would cause ambiguity because for
  example [l ↦{1} v ∗ l' ↦{1} v'] could be turned into [l ↦{1} v] and
  [l' ↦{1} v'], or into two times [l ↦{1/2} v ∗ l' ↦{1/2} v'].

  We do provide the [Fractional] instances so that when one defines a derived
  connection in terms of [∗] or a big operator (and makes that opaque in some
  way), one could choose to split along the [∗] or along the fraction. *)
Instance fractional_sep Φ Ψ :
    Fractional Φ → Fractional Ψ → Fractional (λ q, Φ q ∗ Ψ q)%I.
Proof.
    intros ?? q q'. rewrite !fractional -!assoc. f_equiv.
    rewrite !assoc. f_equiv. by rewrite comm.
  Qed.
(* iris/bi/lib/fractional.v *)
Instance fractional_embed `{!BiEmbed PROP PROP'} Φ :
    Fractional Φ → Fractional (λ q, ⎡ Φ q ⎤ : PROP')%I.
Proof. intros ???. by rewrite fractional embed_sep. Qed.
(* iris/bi/lib/fractional.v *)
Instance as_fractional_embed `{!BiEmbed PROP PROP'} P Φ q :
    AsFractional P Φ q → AsFractional (⎡ P ⎤) (λ q, ⎡ Φ q ⎤)%I q.
Proof. intros [??]; split; [by f_equiv|apply _]. Qed.
(* iris/bi/lib/fractional.v *)
Instance fractional_big_sepL {A} (l : list A) Ψ :
    (∀ k x, Fractional (Ψ k x)) →
    Fractional (PROP:=PROP) (λ q, [∗ list] k↦x ∈ l, Ψ k x q)%I.
Proof. intros ? q q'. rewrite -big_sepL_sep. by setoid_rewrite fractional. Qed.
(* iris/bi/lib/fractional.v *)
Instance fractional_big_sepL2 {A B} (l1 : list A) (l2 : list B) Ψ :
    (∀ k x1 x2, Fractional (Ψ k x1 x2)) →
    Fractional (PROP:=PROP) (λ q, [∗ list] k↦x1; x2 ∈ l1; l2, Ψ k x1 x2 q)%I.
Proof. intros ? q q'. rewrite -big_sepL2_sep. by setoid_rewrite fractional. Qed.
(* iris/bi/lib/fractional.v *)
Instance fractional_big_sepM `{Countable K} {A} (m : gmap K A) Ψ :
    (∀ k x, Fractional (Ψ k x)) →
    Fractional (PROP:=PROP) (λ q, [∗ map] k↦x ∈ m, Ψ k x q)%I.
Proof. intros ? q q'. rewrite -big_sepM_sep. by setoid_rewrite fractional. Qed.
(* iris/bi/lib/fractional.v *)
Instance fractional_big_sepS `{Countable A} (X : gset A) Ψ :
    (∀ x, Fractional (Ψ x)) →
    Fractional (PROP:=PROP) (λ q, [∗ set] x ∈ X, Ψ x q)%I.
Proof. intros ? q q'. rewrite -big_sepS_sep. by setoid_rewrite fractional. Qed.
(* iris/bi/lib/fractional.v *)
Instance fractional_big_sepMS `{Countable A} (X : gmultiset A) Ψ :
    (∀ x, Fractional (Ψ x)) →
    Fractional (PROP:=PROP) (λ q, [∗ mset] x ∈ X, Ψ x q)%I.
Proof. intros ? q q'. rewrite -big_sepMS_sep. by setoid_rewrite fractional. Qed.
(* iris/bi/lib/fractional.v *)
(* Proof mode instances *)
Instance from_sep_fractional P Φ q1 q2 :
    AsFractional P Φ (q1 + q2) → FromSep P (Φ q1) (Φ q2).
Proof. rewrite /FromSep=>-[-> ->] //. Qed.
(* iris/bi/lib/fractional.v *)
Instance combine_sep_as_fractional P1 P2 Φ q1 q2 :
    AsFractional P1 Φ q1 → AsFractional P2 Φ q2 →
    CombineSepAs P1 P2 (Φ (q1 + q2)%Qp) | 50.
(* Explicit cost, to make it easier to provide instances with higher or
     lower cost. Higher-cost instances exist to combine (for example)
     [l ↦{q1} v1] with [l ↦{q2} v2] where [v1] and [v2] are not unifiable. *)
  Proof. rewrite /CombineSepAs =>-[-> _] [-> <-] //. Qed.
(* iris/bi/lib/fractional.v *)
Instance from_sep_fractional_half P Φ q :
    AsFractional P Φ q → FromSep P (Φ (q / 2)%Qp) (Φ (q / 2)%Qp) | 10.
Proof. rewrite /FromSep -{1}(Qp.div_2 q). intros [-> <-]. rewrite Qp.div_2 //. Qed.
(* iris/bi/lib/fractional.v *)
Instance combine_sep_as_fractional_half P Φ q :
    AsFractional P Φ (q/2) → CombineSepAs P P (Φ q) | 50.
(* Explicit cost, to make it easier to provide instances with higher or
     lower cost. Higher-cost instances exist to combine (for example)
     [l ↦{q1} v1] with [l ↦{q2} v2] where [v1] and [v2] are not unifiable. *)
  Proof. rewrite /CombineSepAs=>-[-> <-]. by rewrite Qp.div_2. Qed.
(* iris/bi/lib/fractional.v *)
Instance into_sep_fractional P Φ q1 q2 :
    AsFractional P Φ (q1 + q2) → IntoSep P (Φ q1) (Φ q2).
Proof. intros [??]. rewrite /IntoSep [P]fractional_split //. Qed.
(* iris/bi/lib/fractional.v *)
Instance into_sep_fractional_half P Φ q :
    AsFractional P Φ q → IntoSep P (Φ (q / 2)%Qp) (Φ (q / 2)%Qp) | 100.
Proof. intros [??]. rewrite /IntoSep [P]fractional_half //. Qed.
(* iris/bi/lib/fractional.v *)
Instance frame_fractional_qp_add_l q q' : FrameFractionalQp q (q + q') q'.
Proof. by rewrite /FrameFractionalQp. Qed.
(* iris/bi/lib/fractional.v *)
Instance frame_fractional_qp_add_r q q' : FrameFractionalQp q' (q + q') q.
Proof. by rewrite /FrameFractionalQp Qp.add_comm. Qed.
(* iris/bi/lib/fractional.v *)
Instance frame_fractional_qp_half q : FrameFractionalQp (q/2) q (q/2).
Proof. by rewrite /FrameFractionalQp Qp.div_2. Qed.
(* iris/bi/lib/fractional.v *)
(* Not an instance because of performance; you can locally add it if you are
  willing to pay the cost. We have concrete instances for certain fractional
  assertions such as ↦.

  Coq is sometimes unable to infer the [Φ], hence it might be useful to write
  [apply: (frame_fractional (λ q, ...))] when using the lemma to prove your
  custom instance. See also https://github.com/coq/coq/issues/17688 *)
Lemma frame_fractional Φ p R P qR qP r :
    AsFractional R Φ qR →
    AsFractional P Φ qP →
    FrameFractionalQp qR qP r →
    Frame p R P (Φ r).
Proof.
    rewrite /Frame /FrameFractionalQp=> -[-> _] [-> ?] ->.
    by rewrite bi.intuitionistically_if_elim fractional.
  Qed.
(* iris/bi/lib/fractional.v *)
(* Marked [tc_opaque] instead [Typeclasses Opaque] so that you can use
[iDestruct] to eliminate and [iModIntro] to introduce [internal_fractional],
while still preventing [iFrame] and [iNext] from unfolding. *)
Definition internal_fractional {PROP : bi} (Φ : Qp → PROP) : PROP
:=
  tc_opaque (□ ∀ p q, Φ (p + q)%Qp ∗-∗ Φ p ∗ Φ q)%I.
(* iris/bi/lib/fractional.v *)
Instance : Params (@internal_fractional) 1
:= {}.
(* iris/bi/lib/fractional.v *)
Instance internal_fractional_ne n :
    Proper (pointwise_relation _ (dist n) ==> dist n) (@internal_fractional PROP).
Proof. solve_proper. Qed.
(* iris/bi/lib/fractional.v *)
Instance internal_fractional_proper :
    Proper (pointwise_relation _ (≡) ==> (≡)) (@internal_fractional PROP).
Proof. solve_proper. Qed.
(* iris/bi/lib/fractional.v *)
Instance internal_fractional_affine Φ : Affine (internal_fractional Φ).
Proof. rewrite /internal_fractional /=. apply _. Qed.
(* iris/bi/lib/fractional.v *)
Instance internal_fractional_persistent Φ :
    Persistent (internal_fractional Φ).
Proof. rewrite /internal_fractional /=. apply _. Qed.
(* iris/bi/lib/fractional.v *)
Lemma fractional_internal_fractional Φ :
    Fractional Φ → ⊢ internal_fractional Φ.
Proof.
    intros. iIntros "!>" (q1 q2).
    rewrite [Φ (q1 + q2)%Qp]fractional //=; auto.
  Qed.
(* iris/bi/lib/fractional.v *)
Lemma internal_fractional_iff Φ Ψ:
    □ (∀ q, Φ q ∗-∗ Ψ q) ⊢ internal_fractional Φ -∗ internal_fractional Ψ.
Proof.
    iIntros "#Hiff #HΦdup !>" (p q).
    iSplit.
    - iIntros "H".
      iDestruct ("Hiff" with "H") as "HΦ".
      iDestruct ("HΦdup" with "HΦ") as "[H1 ?]".
      iSplitL "H1"; iApply "Hiff"; iFrame.
    - iIntros "[H1 H2]".
      iDestruct ("Hiff" with "H1") as "HΦ1".
      iDestruct ("Hiff" with "H2") as "HΦ2".
      iApply "Hiff".
      iApply "HΦdup".
      iFrame.
  Qed.
(* iris/bi/lib/laterable.v *)
(* The class of laterable assertions *)
Class Laterable {PROP : bi} (P : PROP)
:= laterable :
  P ⊢ ∃ Q, ▷ Q ∗ □ (▷ Q -∗ ◇ P).
(* iris/bi/lib/laterable.v *)
(* Proofmode class for turning [P] into a laterable [Q].
    Will be the identity if [P] already is laterable, and add
    [▷] otherwise. *)
Class IntoLaterable {PROP : bi} (P Q : PROP) : Prop
:= {
  (** This is non-standard; usually we would just demand
      [P ⊢ make_laterable Q]. However, we need these stronger properties for
      the [make_laterable_id] hack in [atomic.v]. *)
  into_laterable : P ⊢ Q;
  into_laterable_result_laterable : Laterable Q;
}.
(* iris/bi/lib/laterable.v *)
Instance laterable_proper : Proper ((⊣⊢) ==> (↔)) (@Laterable PROP).
Proof. solve_proper. Qed.
(* iris/bi/lib/laterable.v *)
Instance later_laterable P : Laterable (▷ P).
Proof.
    rewrite /Laterable. iIntros "HP". iExists P. iFrame.
    iIntros "!> HP !>". done.
  Qed.
(* iris/bi/lib/laterable.v *)
Instance timeless_laterable P :
    Timeless P → Laterable P.
Proof.
    rewrite /Laterable. iIntros (?) "HP". iExists P%I. iFrame.
    iSplitR; first by iNext. iIntros "!> >HP !>". done.
  Qed.
(* iris/bi/lib/laterable.v *)
(* This lemma is not very useful: It needs a strange assumption about
      emp, and most of the time intuitionistic propositions can be just kept
      around anyway and don't need to be "latered".  The lemma exists
      because the fact that it needs the side-condition is interesting;
      it is not an instance because it won't usually get used. *)
Lemma intuitionistic_laterable P :
    Timeless (PROP:=PROP) emp → Affine P → Persistent P → Laterable P.
Proof.
    rewrite /Laterable. iIntros (???) "#HP".
    iExists emp%I. iSplitL; first by iNext.
    iIntros "!> >_". done.
  Qed.
(* iris/bi/lib/laterable.v *)
(* This instance, together with the one below, can lead to massive
      backtracking, but only when searching for [Laterable]. In the future, it
      should be rewritten using [Hint Immediate] or [Hint Cut], where the latter
      is preferred once we figure out how to use it. *)
Instance persistent_laterable `{!BiAffine PROP} P :
    Persistent P → Laterable P.
Proof.
    intros ?. apply intuitionistic_laterable; apply _.
  Qed.
(* iris/bi/lib/laterable.v *)
Instance sep_laterable P Q :
    Laterable P → Laterable Q → Laterable (P ∗ Q).
Proof.
    rewrite /Laterable. iIntros (LP LQ) "[HP HQ]".
    iDestruct (LP with "HP") as (P') "[HP' #HP]".
    iDestruct (LQ with "HQ") as (Q') "[HQ' #HQ]".
    iExists (P' ∗ Q')%I. iSplitL; first by iFrame.
    iIntros "!> [HP' HQ']". iSplitL "HP'".
    - iApply "HP". done.
    - iApply "HQ". done.
  Qed.
(* iris/bi/lib/laterable.v *)
Instance exist_laterable {A} (Φ : A → PROP) :
    (∀ x, Laterable (Φ x)) → Laterable (∃ x, Φ x).
Proof.
    rewrite /Laterable. iIntros (LΦ). iDestruct 1 as (x) "H".
    iDestruct (LΦ with "H") as (Q) "[HQ #HΦ]".
    iExists Q. iIntros "{$HQ} !> HQ". iExists x. by iApply "HΦ".
  Qed.
(* iris/bi/lib/laterable.v *)
Lemma big_sep_sepL_laterable Q Ps :
    Laterable Q →
    TCForall Laterable Ps →
    Laterable (Q ∗ [∗] Ps).
Proof.
    intros HQ HPs. revert Q HQ. induction HPs as [|P Ps ?? IH]; intros Q HQ.
    { simpl. rewrite right_id. done. }
    simpl. rewrite assoc. apply IH; by apply _.
  Qed.
(* iris/bi/lib/laterable.v *)
Instance big_sepL_laterable Ps :
    Laterable (PROP:=PROP) emp →
    TCForall Laterable Ps →
    Laterable ([∗] Ps).
Proof.
    intros. assert (Laterable (emp ∗ [∗] Ps)) as Hlater.
    { apply big_sep_sepL_laterable; done. }
    rewrite ->left_id in Hlater; last by apply _. done.
  Qed.
(* iris/bi/lib/laterable.v *)
(* A wrapper to obtain a weaker, laterable form of any assertion.
     Alternatively: the modality corresponding to [Laterable].
     The ◇ is required to make [make_laterable_intro'] hold.
   TODO: Define [Laterable] in terms of this (see [laterable_alt] below). *)
Definition make_laterable (Q : PROP) : PROP
:=
    ∃ P, ▷ P ∗ □ (▷ P -∗ ◇ Q).
(* iris/bi/lib/laterable.v *)
Instance make_laterable_ne : NonExpansive make_laterable.
Proof. solve_proper. Qed.
(* iris/bi/lib/laterable.v *)
Instance make_laterable_proper : Proper ((≡) ==> (≡)) make_laterable
:= ne_proper _.
(* iris/bi/lib/laterable.v *)
Instance make_laterable_mono' : Proper ((⊢) ==> (⊢)) make_laterable.
Proof. solve_proper. Qed.
(* iris/bi/lib/laterable.v *)
Instance make_laterable_flip_mono' :
    Proper (flip (⊢) ==> flip (⊢)) make_laterable.
Proof. solve_proper. Qed.
(* iris/bi/lib/laterable.v *)
Lemma make_laterable_mono Q1 Q2 :
    (Q1 ⊢ Q2) → (make_laterable Q1 ⊢ make_laterable Q2).
Proof. by intros ->. Qed.