phanerozoic/Coq-Iris huggingface dataset:
(* iris/bi/lib/laterable.v *)
Lemma make_laterable_except_0 Q :
    make_laterable (◇ Q) ⊢ make_laterable Q.
Proof.
    iIntros "(%P & HP & #HPQ)". iExists P. iFrame.
    iIntros "!# HP". iMod ("HPQ" with "HP"). done.
  Qed.
(* iris/bi/lib/laterable.v *)
Lemma make_laterable_sep Q1 Q2 :
    make_laterable Q1 ∗ make_laterable Q2 ⊢ make_laterable (Q1 ∗ Q2).
Proof.
    iIntros "[HQ1 HQ2]".
    iDestruct "HQ1" as (P1) "[HP1 #HQ1]".
    iDestruct "HQ2" as (P2) "[HP2 #HQ2]".
    iExists (P1 ∗ P2)%I. iFrame. iIntros "!# [HP1 HP2]".
    iDestruct ("HQ1" with "HP1") as ">$".
    iDestruct ("HQ2" with "HP2") as ">$".
    done.
  Qed.
(* iris/bi/lib/laterable.v *)
(* A stronger version of [make_laterable_mono] that lets us keep laterable
  resources. We cannot keep arbitrary resources since that would let us "frame
  in" non-laterable things. *)
Lemma make_laterable_wand Q1 Q2 :
    make_laterable (Q1 -∗ Q2) ⊢ (make_laterable Q1 -∗ make_laterable Q2).
Proof.
    iIntros "HQ HQ1".
    iDestruct (make_laterable_sep with "[$HQ $HQ1 //]") as "HQ".
    iApply make_laterable_mono; last done.
    by rewrite bi.wand_elim_l.
  Qed.
(* iris/bi/lib/laterable.v *)
(* A variant of the above for keeping arbitrary intuitionistic resources.
      Sadly, this is not implied by the above for non-affine BIs. *)
Lemma make_laterable_intuitionistic_wand Q1 Q2 :
    □ (Q1 -∗ Q2) ⊢ (make_laterable Q1 -∗ make_laterable Q2).
Proof.
    iIntros "#HQ HQ1". iDestruct "HQ1" as (P) "[HP #HQ1]".
    iExists P. iFrame. iIntros "!> HP".
    iDestruct ("HQ1" with "HP") as "{HQ1} >HQ1".
    iModIntro. iApply "HQ". done.
  Qed.
(* iris/bi/lib/laterable.v *)
Instance make_laterable_laterable Q :
    Laterable (make_laterable Q).
Proof.
    rewrite /Laterable. iIntros "HQ". iDestruct "HQ" as (P) "[HP #HQ]".
    iExists P. iFrame. iIntros "!> HP !>". iExists P. by iFrame.
  Qed.
(* iris/bi/lib/laterable.v *)
Lemma make_laterable_elim Q :
    make_laterable Q ⊢ ◇ Q.
Proof.
    iIntros "HQ". iDestruct "HQ" as (P) "[HP #HQ]". by iApply "HQ".
  Qed.
(* iris/bi/lib/laterable.v *)
(* Written internally (as an entailment of wands) to reflect
      that persistent assertions can be kept unchanged. *)
Lemma make_laterable_intro P Q :
    Laterable P →
    □ (P -∗ Q) -∗ P -∗ make_laterable Q.
Proof.
    iIntros (?) "#HQ HP".
    iDestruct (laterable with "HP") as (P') "[HP' #HPi]". iExists P'.
    iFrame. iIntros "!> HP'".
    iDestruct ("HPi" with "HP'") as ">HP". iModIntro.
    iApply "HQ". done.
  Qed.
(* iris/bi/lib/laterable.v *)
Lemma make_laterable_intro' Q :
    Laterable Q →
    Q ⊢ make_laterable Q.
Proof.
    intros ?. iApply make_laterable_intro. iIntros "!# $".
  Qed.
(* iris/bi/lib/laterable.v *)
Lemma make_laterable_idemp Q :
    make_laterable (make_laterable Q) ⊣⊢ make_laterable Q.
Proof.
    apply (anti_symm (⊢)).
    - trans (make_laterable (◇ Q)).
      + apply make_laterable_mono, make_laterable_elim.
      + apply make_laterable_except_0.
    - apply make_laterable_intro', _.
  Qed.
(* iris/bi/lib/laterable.v *)
Lemma laterable_alt Q :
    Laterable Q ↔ (Q ⊢ make_laterable Q).
Proof.
    split.
    - intros ?. apply make_laterable_intro'. done.
    - intros ?. done.
  Qed.
(* iris/bi/lib/laterable.v *)
(* * Proofmode integration

      We integrate [make_laterable] with [iModIntro]. All non-laterable
      hypotheses have a ▷ added in front of them to ensure a laterable context. *)
Instance into_laterable_laterable P :
    Laterable P →
    IntoLaterable P P.
Proof. intros ?. constructor; done. Qed.
(* iris/bi/lib/laterable.v *)
Instance into_laterable_fallback P :
    IntoLaterable P (▷ P) | 100.
Proof. constructor; last by apply _. apply bi.later_intro. Qed.
(* iris/bi/lib/laterable.v *)
Lemma modality_make_laterable_mixin `{!Timeless (PROP:=PROP) emp} :
    modality_mixin make_laterable MIEnvId (MIEnvTransform IntoLaterable).
Proof.
    split; simpl; eauto using make_laterable_intro', make_laterable_mono,
      make_laterable_sep, intuitionistic_laterable with typeclass_instances; [].
    intros P Q ?. rewrite (into_laterable P).
    apply make_laterable_intro'. eapply (into_laterable_result_laterable P), _.
  Qed.
(* iris/bi/lib/laterable.v *)
Definition modality_make_laterable `{!Timeless (PROP:=PROP) emp}
:=
    Modality _ modality_make_laterable_mixin.
(* iris/bi/lib/laterable.v *)
Instance from_modal_make_laterable `{!Timeless (PROP:=PROP) emp} P :
    FromModal True modality_make_laterable (make_laterable P) (make_laterable P) P.
Proof. by rewrite /FromModal. Qed.
(* iris/bi/lib/relations.v *)
Definition bi_rtc_pre (R : A → A → PROP)
      (x2 : A) (rec : A → PROP) (x1 : A) : PROP
:=
    <affine> (x1 ≡ x2) ∨ ∃ x', R x1 x' ∗ rec x'.
(* iris/bi/lib/relations.v *)
(* The reflexive transitive closure. *)
Definition bi_rtc (R : A → A → PROP) (x1 x2 : A) : PROP
:=
    bi_least_fixpoint (bi_rtc_pre R x2) x1.
(* iris/bi/lib/relations.v *)
Instance : Params (@bi_rtc) 4
:= {}.
(* iris/bi/lib/relations.v *)
Definition bi_tc_pre (R : A → A → PROP)
      (x2 : A) (rec : A → PROP) (x1 : A) : PROP
:=
    R x1 x2 ∨ ∃ x', R x1 x' ∗ rec x'.
(* iris/bi/lib/relations.v *)
(* The transitive closure. *)
Definition bi_tc (R : A → A → PROP) (x1 x2 : A) : PROP
:=
    bi_least_fixpoint (bi_tc_pre R x2) x1.
(* iris/bi/lib/relations.v *)
Instance : Params (@bi_tc) 4
:= {}.
(* iris/bi/lib/relations.v *)
(* Reductions of exactly [n] steps. *)
Fixpoint bi_nsteps (R : A → A → PROP) (n : nat) (x1 x2 : A) : PROP
:=
    match n with
    | 0    => <affine> (x1 ≡ x2)
    | S n' => ∃ x', R x1 x' ∗ bi_nsteps R n' x' x2
    end.
(* iris/bi/lib/relations.v *)
Instance : Params (@bi_nsteps) 5
:= {}.
(* iris/bi/lib/relations.v *)
Instance bi_rtc_pre_mono {PROP : bi} `{!Sbi PROP}
    {A : ofe} (R : A → A → PROP) `{!NonExpansive2 R} (x : A) :
  BiMonoPred (bi_rtc_pre R x).
Proof.
  constructor; [|solve_proper].
  iIntros (rec1 rec2 ??) "#H". iIntros (x1) "[Hrec | Hrec]".
  { by iLeft. }
  iRight.
  iDestruct "Hrec" as (x') "[HP Hrec]".
  iDestruct ("H" with "Hrec") as "Hrec". eauto with iFrame.
Qed.
(* iris/bi/lib/relations.v *)
Instance bi_rtc_ne {PROP : bi} `{!Sbi PROP} {A : ofe} (R : A → A → PROP) :
  NonExpansive2 (bi_rtc R).
Proof.
  intros n x1 x2 Hx y1 y2 Hy. rewrite /bi_rtc Hx. f_equiv=> rec z.
  solve_proper.
Qed.
(* iris/bi/lib/relations.v *)
Instance bi_rtc_proper {PROP : bi} `{!Sbi PROP} {A : ofe} (R : A → A → PROP)
  : Proper ((≡) ==> (≡) ==> (⊣⊢)) (bi_rtc R).
Proof. apply ne_proper_2. apply _. Qed.
(* iris/bi/lib/relations.v *)
Instance bi_tc_pre_mono `{!Sbi PROP}
    {A : ofe} (R : A → A → PROP) `{NonExpansive2 R} (x : A) :
  BiMonoPred (bi_tc_pre R x).
Proof.
  constructor; [|solve_proper].
  iIntros (rec1 rec2 ??) "#H". iIntros (x1) "Hrec".
  iDestruct "Hrec" as "[Hrec | Hrec]".
  { by iLeft. }
  iDestruct "Hrec" as (x') "[HR Hrec]".
  iRight. iExists x'. iFrame "HR". by iApply "H".
Qed.
(* iris/bi/lib/relations.v *)
Instance bi_tc_ne `{!Sbi PROP} {A : ofe}
    (R : A → A → PROP) `{NonExpansive2 R} :
  NonExpansive2 (bi_tc R).
Proof.
  intros n x1 x2 Hx y1 y2 Hy. rewrite /bi_tc Hx. f_equiv=> rec z.
  solve_proper.
Qed.
(* iris/bi/lib/relations.v *)
Instance bi_tc_proper `{!Sbi PROP} {A : ofe}
    (R : A → A → PROP) `{NonExpansive2 R}
  : Proper ((≡) ==> (≡) ==> (⊣⊢)) (bi_tc R).
Proof. apply ne_proper_2. apply _. Qed.
(* iris/bi/lib/relations.v *)
Instance bi_nsteps_ne {PROP : bi} `{!Sbi PROP}
    {A : ofe} (R : A → A → PROP) `{NonExpansive2 R} (n : nat) :
  NonExpansive2 (bi_nsteps R n).
Proof. induction n; solve_proper. Qed.
(* iris/bi/lib/relations.v *)
Instance bi_nsteps_proper {PROP : bi} `{!Sbi PROP}
    {A : ofe} (R : A → A → PROP) `{NonExpansive2 R} (n : nat)
  : Proper ((≡) ==> (≡) ==> (⊣⊢)) (bi_nsteps R n).
Proof. apply ne_proper_2. apply _. Qed.
(* iris/bi/lib/relations.v *)
(* ** Results about the reflexive-transitive closure [bi_rtc] *)
Lemma bi_rtc_unfold (x1 x2 : A) :
    bi_rtc R x1 x2 ≡ bi_rtc_pre R x2 (λ x1, bi_rtc R x1 x2) x1.
Proof. by rewrite /bi_rtc; rewrite -least_fixpoint_unfold. Qed.
(* iris/bi/lib/relations.v *)
Lemma bi_rtc_strong_ind_l x2 Φ :
    NonExpansive Φ →
    □ (∀ x1, <affine> (x1 ≡ x2) ∨ (∃ x', R x1 x' ∗ (Φ x' ∧ bi_rtc R x' x2)) -∗ Φ x1) -∗
    ∀ x1, bi_rtc R x1 x2 -∗ Φ x1.
Proof.
    iIntros (?) "#IH". rewrite /bi_rtc.
    by iApply (least_fixpoint_ind (bi_rtc_pre R x2) with "IH").
  Qed.
(* iris/bi/lib/relations.v *)
Lemma bi_rtc_ind_l x2 Φ :
    NonExpansive Φ →
    □ (∀ x1, <affine> (x1 ≡ x2) ∨ (∃ x', R x1 x' ∗ Φ x') -∗ Φ x1) -∗
    ∀ x1, bi_rtc R x1 x2 -∗ Φ x1.
Proof.
    iIntros (?) "#IH". rewrite /bi_rtc.
    by iApply (least_fixpoint_iter (bi_rtc_pre R x2) with "IH").
  Qed.
(* iris/bi/lib/relations.v *)
Lemma bi_rtc_refl x : ⊢ bi_rtc R x x.
Proof. rewrite bi_rtc_unfold. by iLeft. Qed.
(* iris/bi/lib/relations.v *)
Lemma bi_rtc_l x1 x2 x3 : R x1 x2 -∗ bi_rtc R x2 x3 -∗ bi_rtc R x1 x3.
Proof.
    iIntros "H1 H2".
    iEval (rewrite bi_rtc_unfold /bi_rtc_pre). iRight.
    iExists x2. iFrame.
  Qed.
(* iris/bi/lib/relations.v *)
Lemma bi_rtc_once x1 x2 : R x1 x2 -∗ bi_rtc R x1 x2.
Proof. iIntros "H". iApply (bi_rtc_l with "H"). iApply bi_rtc_refl. Qed.
(* iris/bi/lib/relations.v *)
Lemma bi_rtc_trans x1 x2 x3 : bi_rtc R x1 x2 -∗ bi_rtc R x2 x3 -∗ bi_rtc R x1 x3.
Proof.
    iRevert (x1).
    iApply bi_rtc_ind_l.
    { solve_proper. }
    iIntros "!>" (x1) "[H | H] H2".
    { by iRewrite "H". }
    iDestruct "H" as (x') "[H IH]".
    iApply (bi_rtc_l with "H").
    by iApply "IH".
  Qed.
(* iris/bi/lib/relations.v *)
Lemma bi_rtc_r x y z : bi_rtc R x y -∗ R y z -∗ bi_rtc R x z.
Proof.
    iIntros "H H'".
    iApply (bi_rtc_trans with "H").
    by iApply bi_rtc_once.
  Qed.
(* iris/bi/lib/relations.v *)
Lemma bi_rtc_inv x z :
    bi_rtc R x z -∗ <affine> (x ≡ z) ∨ ∃ y, R x y ∗ bi_rtc R y z.
Proof. rewrite bi_rtc_unfold. iIntros "[H | H]"; eauto. Qed.
(* iris/bi/lib/relations.v *)
Instance bi_rtc_affine :
    (∀ x y, Affine (R x y)) →
    ∀ x y, Affine (bi_rtc R x y).
Proof. intros. apply least_fixpoint_affine; apply _. Qed.
(* iris/bi/lib/relations.v *)
(* FIXME: It would be nicer to use the least_fixpoint_persistent lemmas,
            but they seem to weak. *)
Instance bi_rtc_persistent :
    (∀ x y, Persistent (R x y)) →
    ∀ x y, Persistent (bi_rtc R x y).
Proof.
    intros ? x y. rewrite /Persistent.
    iRevert (x). iApply bi_rtc_ind_l; first solve_proper.
    iIntros "!>" (x) "[#Heq | (%x' & #Hxx' & #Hx'y)]".
    { iRewrite "Heq". iApply bi_rtc_refl. }
    iApply (bi_rtc_l with "Hxx' Hx'y").
  Qed.
(* iris/bi/lib/relations.v *)
(* ** Results about the transitive closure [bi_tc] *)
Lemma bi_tc_unfold (x1 x2 : A) :
    bi_tc R x1 x2 ≡ bi_tc_pre R x2 (λ x1, bi_tc R x1 x2) x1.
Proof. by rewrite /bi_tc; rewrite -least_fixpoint_unfold. Qed.
(* iris/bi/lib/relations.v *)
Lemma bi_tc_strong_ind_l x2 Φ :
    NonExpansive Φ →
    □ (∀ x1, (R x1 x2 ∨ (∃ x', R x1 x' ∗ (Φ x' ∧ bi_tc R x' x2))) -∗ Φ x1) -∗
    ∀ x1, bi_tc R x1 x2 -∗ Φ x1.
Proof.
    iIntros (?) "#IH". rewrite /bi_tc.
    iApply (least_fixpoint_ind (bi_tc_pre R x2) with "IH").
  Qed.
(* iris/bi/lib/relations.v *)
Lemma bi_tc_ind_l x2 Φ :
    NonExpansive Φ →
    □ (∀ x1, (R x1 x2 ∨ (∃ x', R x1 x' ∗ Φ x')) -∗ Φ x1) -∗
    ∀ x1, bi_tc R x1 x2 -∗ Φ x1.
Proof.
    iIntros (?) "#IH". rewrite /bi_tc.
    iApply (least_fixpoint_iter (bi_tc_pre R x2) with "IH").
  Qed.
(* iris/bi/lib/relations.v *)
Lemma bi_tc_l x1 x2 x3 : R x1 x2 -∗ bi_tc R x2 x3 -∗ bi_tc R x1 x3.
Proof.
    iIntros "H1 H2".
    iEval (rewrite bi_tc_unfold /bi_tc_pre).
    iRight. iExists x2. iFrame.
  Qed.
(* iris/bi/lib/relations.v *)
Lemma bi_tc_once x1 x2 : R x1 x2 -∗ bi_tc R x1 x2.
Proof.
    iIntros "H".
    iEval (rewrite bi_tc_unfold /bi_tc_pre).
    by iLeft.
  Qed.
(* iris/bi/lib/relations.v *)
Lemma bi_tc_trans x1 x2 x3 : bi_tc R x1 x2 -∗ bi_tc R x2 x3 -∗ bi_tc R x1 x3.
Proof.
    iRevert (x1).
    iApply bi_tc_ind_l.
    { solve_proper. }
    iIntros "!>" (x1) "H H2".
    iDestruct "H" as "[H | H]".
    { iApply (bi_tc_l with "H H2"). }
    iDestruct "H" as (x') "[H IH]".
    iApply (bi_tc_l with "H").
    by iApply "IH".
  Qed.
(* iris/bi/lib/relations.v *)
Lemma bi_tc_r x y z : bi_tc R x y -∗ R y z -∗ bi_tc R x z.
Proof.
    iIntros "H H'".
    iApply (bi_tc_trans with "H").
    by iApply bi_tc_once.
  Qed.
(* iris/bi/lib/relations.v *)
Lemma bi_tc_rtc_l x y z : bi_rtc R x y -∗ bi_tc R y z -∗ bi_tc R x z.
Proof.
    iRevert (x).
    iApply bi_rtc_ind_l. { solve_proper. }
    iIntros "!>" (x) "[Heq | H] Hyz".
    { by iRewrite "Heq". }
    iDestruct "H" as (x') "[H IH]".
    iApply (bi_tc_l with "H").
    by iApply "IH".
  Qed.
(* iris/bi/lib/relations.v *)
Lemma bi_tc_rtc_r x y z : bi_tc R x y -∗ bi_rtc R y z -∗ bi_tc R x z.
Proof.
    iIntros "Hxy Hyz".
    iRevert (x) "Hxy". iRevert (y) "Hyz".
    iApply bi_rtc_ind_l. { solve_proper. }
    iIntros "!>" (y) "[Heq | H] %x Hxy".
    { by iRewrite -"Heq". }
    iDestruct "H" as (y') "[H IH]".
    iApply "IH". iApply (bi_tc_r with "Hxy H").
  Qed.
(* iris/bi/lib/relations.v *)
Lemma bi_tc_rtc x y : bi_tc R x y -∗ bi_rtc R x y.
Proof.
    iRevert (x). iApply bi_tc_ind_l. { solve_proper. }
    iIntros "!>" (x) "[Hxy | H]".
    { by iApply bi_rtc_once. }
    iDestruct "H" as (x') "[H H']".
    iApply (bi_rtc_l with "H H'").
  Qed.
(* iris/bi/lib/relations.v *)
Instance bi_tc_affine :
    (∀ x y, Affine (R x y)) →
    ∀ x y, Affine (bi_tc R x y).
Proof. intros. apply least_fixpoint_affine; apply _. Qed.
(* iris/bi/lib/relations.v *)
Instance bi_tc_absorbing :
    (∀ x y, Absorbing (R x y)) →
    ∀ x y, Absorbing (bi_tc R x y).
Proof. intros. apply least_fixpoint_absorbing; apply _. Qed.
(* iris/bi/lib/relations.v *)
(* FIXME: It would be nicer to use the least_fixpoint_persistent lemmas,
            but they seem to weak. *)
Instance bi_tc_persistent :
    (∀ x y, Persistent (R x y)) →
    ∀ x y, Persistent (bi_tc R x y).
Proof.
    intros ? x y. rewrite /Persistent.
    iRevert (x). iApply bi_tc_ind_l; first solve_proper.
    iIntros "!# %x [#H|(%x'&#?&#?)] !>"; first by iApply bi_tc_once.
    by iApply bi_tc_l.
  Qed.
(* iris/bi/lib/relations.v *)
(* ** Results about [bi_nsteps] *)
Lemma bi_nsteps_O x : ⊢ bi_nsteps R 0 x x.
Proof. auto. Qed.
(* iris/bi/lib/relations.v *)
Lemma bi_nsteps_once x y : R x y -∗ bi_nsteps R 1 x y.
Proof. simpl. eauto. Qed.
(* iris/bi/lib/relations.v *)
Lemma bi_nsteps_once_inv x y : bi_nsteps R 1 x y -∗ R x y.
Proof. iDestruct 1 as (x') "[Hxx' Heq]". by iRewrite -"Heq". Qed.
(* iris/bi/lib/relations.v *)
Lemma bi_nsteps_l n x y z : R x y -∗ bi_nsteps R n y z -∗ bi_nsteps R (S n) x z.
Proof. iIntros "? ?". iExists y. iFrame. Qed.
(* iris/bi/lib/relations.v *)
Lemma bi_nsteps_trans n m x y z :
    bi_nsteps R n x y -∗ bi_nsteps R m y z -∗ bi_nsteps R (n + m) x z.
Proof.
    iInduction n as [|n IH] forall (x); simpl.
    - iIntros "Heq". iRewrite "Heq". auto.
    - iDestruct 1 as (x') "[Hxx' Hx'y]". iIntros "Hyz".
      iExists x'. iFrame "Hxx'". iApply ("IH" with "Hx'y Hyz").
  Qed.
(* iris/bi/lib/relations.v *)
Lemma bi_nsteps_r n x y z :
    bi_nsteps R n x y -∗ R y z -∗ bi_nsteps R (S n) x z.
Proof.
    iIntros "Hxy Hyx". rewrite -Nat.add_1_r.
    iApply (bi_nsteps_trans with "Hxy").
    by iApply bi_nsteps_once.
  Qed.
(* iris/bi/lib/relations.v *)
Lemma bi_nsteps_add_inv n m x z :
    bi_nsteps R (n + m) x z ⊢ ∃ y, bi_nsteps R n x y ∗ bi_nsteps R m y z.
Proof.
    iInduction n as [|n IH] forall (x).
    - iIntros "Hxz". iExists x. auto.
    - iDestruct 1 as (y) "[Hxy Hyz]".
      iDestruct ("IH" with "Hyz") as (y') "[Hyy' Hy'z]".
      iExists y'. iFrame "Hy'z".
      iApply (bi_nsteps_l with "Hxy Hyy'").
  Qed.
(* iris/bi/lib/relations.v *)
Lemma bi_nsteps_inv_r n x z :
    bi_nsteps R (S n) x z ⊢ ∃ y, bi_nsteps R n x y ∗ R y z.
Proof.
    rewrite -Nat.add_1_r bi_nsteps_add_inv /=.
    iDestruct 1 as (y) "[Hxy (%x' & Hxx' & Heq)]".
    iExists y. iRewrite -"Heq". iFrame.
  Qed.
(* iris/bi/lib/relations.v *)
(* ** Equivalences between closure operators *)
Lemma bi_rtc_tc x y : bi_rtc R x y ⊣⊢ <affine> (x ≡ y) ∨ bi_tc R x y.
Proof.
    iSplit.
    - iRevert (x). iApply bi_rtc_ind_l. { solve_proper. }
      iIntros "!>" (x) "[Heq | H]".
      { by iLeft. }
      iRight.
      iDestruct "H" as (x') "[H [Heq | IH]]".
      { iRewrite -"Heq". by iApply bi_tc_once. }
      iApply (bi_tc_l with "H IH").
    - iIntros "[Heq | Hxy]".
      { iRewrite "Heq". iApply bi_rtc_refl. }
      by iApply bi_tc_rtc.
  Qed.
(* iris/bi/lib/relations.v *)
Lemma bi_tc_nsteps x y :
    bi_tc R x y ⊣⊢ ∃ n, <affine> ⌜0 < n⌝ ∗ bi_nsteps R n x y.
Proof.
    iSplit.
    - iRevert (x). iApply bi_tc_ind_l. { solve_proper. }
      iIntros "!>" (x) "[Hxy | H]".
      { iExists 1. iSplitR; first auto with lia.
        iApply (bi_nsteps_l with "Hxy"). iApply bi_nsteps_O. }
      iDestruct "H" as (x') "[Hxx' IH]".
      iDestruct "IH" as (n ?) "Hx'y".
      iExists (S n). iSplitR; first auto with lia.
      iApply (bi_nsteps_l with "Hxx' Hx'y").
    - iDestruct 1 as (n ?) "Hxy".
      iInduction n as [|n IH] forall (y). { lia. }
      rewrite bi_nsteps_inv_r.
      iDestruct "Hxy" as (x') "[Hxx' Hx'y]".
      destruct n.
      { simpl. iRewrite "Hxx'". by iApply bi_tc_once. }
      iApply (bi_tc_r with "[Hxx'] Hx'y").
      iApply ("IH" with "[%] Hxx'"). lia.
  Qed.
(* iris/bi/lib/relations.v *)
Lemma bi_rtc_nsteps x y : bi_rtc R x y ⊣⊢ ∃ n, bi_nsteps R n x y.
Proof.
    iSplit.
    - iRevert (x). iApply bi_rtc_ind_l. { solve_proper. }
      iIntros "!>" (x) "[Heq | H]".
      { iExists 0. iRewrite "Heq". iApply bi_nsteps_O. }
      iDestruct "H" as (x') "[Hxx' IH]".
      iDestruct "IH" as (n) "Hx'y".
      iExists (S n). iApply (bi_nsteps_l with "Hxx' Hx'y").
    - iDestruct 1 as (n) "Hxy".
      iInduction n as [|n IH] forall (y).
      { simpl. iRewrite "Hxy". iApply bi_rtc_refl. }
      iDestruct (bi_nsteps_inv_r with "Hxy") as (x') "[Hxx' Hx'y]".
      iApply (bi_rtc_r with "[Hxx'] Hx'y").
      by iApply "IH".
  Qed.
(* iris/bi/lib/relations.v *)
Instance bi_nsteps_timeless n :
    (∀ x y, Timeless (R x y)) →
    ∀ x y, Timeless (bi_nsteps R n x y).
Proof. induction n; apply _. Qed.
(* iris/bi/lib/relations.v *)
Instance bi_rtc_timeless :
    (∀ x y, Timeless (R x y)) →
    ∀ x y, Timeless (bi_rtc R x y).
Proof. intros ? x y. rewrite bi_rtc_nsteps. apply _. Qed.
(* iris/bi/lib/relations.v *)
Instance bi_tc_timeless :
    (∀ x y, Timeless (R x y)) →
    ∀ x y, Timeless (bi_tc R x y).
Proof. intros ? x y. rewrite bi_tc_nsteps. apply _. Qed.
(* iris/prelude/prelude.v *)
(* Iris itself and many dependencies still rely on this coercion. *)
Coercion Z.of_nat : nat >-> Z.
(* iris/program_logic/adequacy.v *)
Notation wptp s t Φs
:= ([∗ list] e;Φ ∈ t;Φs, WP e @ s; ⊤ {{ Φ }})%I.
(* iris/program_logic/adequacy.v *)
Lemma wp_step s e1 σ1 ns κ κs e2 σ2 efs nt Φ :
  prim_step e1 σ1 κ e2 σ2 efs →
  state_interp σ1 ns (κ ++ κs) nt -∗
  £ (S (num_laters_per_step ns)) -∗
  WP e1 @ s; ⊤ {{ Φ }}
    ={⊤,∅}=∗ |={∅}▷=>^(S $ num_laters_per_step ns) |={∅,⊤}=>
    state_interp σ2 (S ns) κs (nt + length efs) ∗ WP e2 @ s; ⊤ {{ Φ }} ∗
    wptp s efs (replicate (length efs) fork_post).
Proof.
  rewrite {1}wp_unfold /wp_pre. iIntros (?) "Hσ Hcred H".
  rewrite (val_stuck e1 σ1 κ e2 σ2 efs) //.
  iMod ("H" $! σ1 ns with "Hσ") as "(_ & H)". iModIntro.
  iApply (step_fupdN_wand with "(H [//] Hcred)"). iIntros ">H".
  by rewrite Nat.add_comm big_sepL2_replicate_r.
Qed.
(* iris/program_logic/adequacy.v *)
Lemma wptp_step s es1 es2 κ κs σ1 ns σ2 Φs nt :
  step (es1,σ1) κ (es2, σ2) →
  state_interp σ1 ns (κ ++ κs) nt -∗
  £ (S (num_laters_per_step ns)) -∗
  wptp s es1 Φs -∗
  ∃ nt', |={⊤,∅}=> |={∅}▷=>^(S $ num_laters_per_step$ ns) |={∅,⊤}=>
         state_interp σ2 (S ns) κs (nt + nt') ∗
         wptp s es2 (Φs ++ replicate nt' fork_post).
Proof.
  iIntros (Hstep) "Hσ Hcred Ht".
  destruct Hstep as [e1' σ1' e2' σ2' efs t2' t3 Hstep]; simplify_eq/=.
  iDestruct (big_sepL2_app_inv_l with "Ht") as (Φs1 Φs2 ->) "[? Ht]".
  iDestruct (big_sepL2_cons_inv_l with "Ht") as (Φ Φs3 ->) "[Ht ?]".
  iExists _. iMod (wp_step with "Hσ Hcred Ht") as "H"; first done. iModIntro.
  iApply (step_fupdN_wand with "H"). iIntros ">($ & He2 & Hefs) !>".
  rewrite -(assoc_L app) -app_comm_cons. iFrame.
Qed.
(* iris/program_logic/adequacy.v *)
(* The total number of laters used between the physical steps number
   [start] (included) to [start+ns] (excluded). *)
Fixpoint steps_sum (num_laters_per_step : nat → nat) (start ns : nat) : nat
:=
  match ns with
  | O => 0
  | S ns =>
    S $ num_laters_per_step start + steps_sum num_laters_per_step (S start) ns
  end.
(* iris/program_logic/adequacy.v *)
Lemma wptp_preservation s n es1 es2 κs κs' σ1 ns σ2 Φs nt :
  nsteps n (es1, σ1) κs (es2, σ2) →
  state_interp σ1 ns (κs ++ κs') nt -∗
  £ (steps_sum num_laters_per_step ns n) -∗
  wptp s es1 Φs
  ={⊤,∅}=∗ |={∅}▷=>^(steps_sum num_laters_per_step ns n) |={∅,⊤}=> ∃ nt',
    state_interp σ2 (n + ns) κs' (nt + nt') ∗
    wptp s es2 (Φs ++ replicate nt' fork_post).
Proof.
  revert nt es1 es2 κs κs' σ1 ns σ2 Φs.
  induction n as [|n IH]=> nt es1 es2 κs κs' σ1 ns σ2 Φs /=.
  { inversion_clear 1; iIntros "? ? ?"; iExists 0=> /=.
    rewrite Nat.add_0_r right_id_L. iFrame. by iApply fupd_mask_subseteq. }
  iIntros (Hsteps) "Hσ Hcred He". inversion_clear Hsteps as [|?? [t1' σ1']].
  rewrite -(assoc_L (++)) Nat.iter_add -{1}plus_Sn_m plus_n_Sm.
  iDestruct "Hcred" as "[Hc1 Hc2]".
  iDestruct (wptp_step with "Hσ Hc1 He") as (nt') ">H"; first eauto; simplify_eq.
  iModIntro. iApply step_fupdN_S_fupd. iApply (step_fupdN_wand with "H").
  iIntros ">(Hσ & He)". iMod (IH with "Hσ Hc2 He") as "IH"; first done. iModIntro.
  iApply (step_fupdN_wand with "IH"). iIntros ">IH".
  iDestruct "IH" as (nt'') "[??]".
  rewrite -Nat.add_assoc -(assoc_L app) -replicate_add. by eauto with iFrame.
Qed.
(* iris/program_logic/adequacy.v *)
Lemma wp_not_stuck κs nt e σ ns Φ :
  state_interp σ ns κs nt -∗ WP e {{ Φ }} ={⊤,∅}=∗ ⌜not_stuck e σ⌝.
Proof.
  rewrite wp_unfold /wp_pre /not_stuck. iIntros "Hσ H".
  destruct (to_val e) as [v|] eqn:?.
  { iMod (fupd_mask_subseteq ∅); first set_solver. iModIntro. eauto. }
  iSpecialize ("H" $! σ ns [] κs with "Hσ"). rewrite sep_elim_l.
  iMod "H" as "%". iModIntro. eauto.
Qed.
(* iris/program_logic/adequacy.v *)
Lemma wptp_postconditions Φs s es :
  wptp s es Φs ={⊤}=∗ [∗ list] e;Φ ∈ es;Φs, from_option Φ True (to_val e).
Proof.
  iIntros "Ht". iApply big_sepL2_fupd. iApply (big_sepL2_impl with "Ht").
  iIntros "!#" (? e Φ ??) "Hwp".
  destruct (to_val e) as [v2|] eqn:He2'; last done.
  apply of_to_val in He2' as <-. simpl. iApply wp_value_fupd'. done.
Qed.
(* iris/program_logic/adequacy.v *)
(* Adequacy when using later credits (the default) *)
Definition wp_strong_adequacy
:= wp_strong_adequacy_gen HasLc.
(* iris/program_logic/adequacy.v *)
(* Since the full adequacy statement is quite a mouthful, we prove some more
intuitive and simpler corollaries. These lemmas are morover stated in terms of
[rtc erased_step] so one does not have to provide the trace. *)
Record adequate {Λ} (s : stuckness) (e1 : expr Λ) (σ1 : state Λ)
    (φ : val Λ → state Λ → Prop)
:= {
  adequate_result t2 σ2 v2 :
   rtc erased_step ([e1], σ1) (of_val v2 :: t2, σ2) → φ v2 σ2;
  adequate_not_stuck t2 σ2 e2 :
   s = NotStuck →
   rtc erased_step ([e1], σ1) (t2, σ2) →
   e2 ∈ t2 → not_stuck e2 σ2
}.
(* iris/program_logic/adequacy.v *)
Lemma adequate_alt {Λ} s e1 σ1 (φ : val Λ → state Λ → Prop) :
  adequate s e1 σ1 φ ↔ ∀ t2 σ2,
    rtc erased_step ([e1], σ1) (t2, σ2) →
      (∀ v2 t2', t2 = of_val v2 :: t2' → φ v2 σ2) ∧
      (∀ e2, s = NotStuck → e2 ∈ t2 → not_stuck e2 σ2).
Proof.
  split.
  - intros []; naive_solver.
  - constructor; naive_solver.
Qed.
(* iris/program_logic/adequacy.v *)
Theorem adequate_tp_safe {Λ} (e1 : expr Λ) t2 σ1 σ2 φ :
  adequate NotStuck e1 σ1 φ →
  rtc erased_step ([e1], σ1) (t2, σ2) →
  Forall (λ e, is_Some (to_val e)) t2 ∨ ∃ t3 σ3, erased_step (t2, σ2) (t3, σ3).
Proof.
  intros Had ?.
  destruct (decide (Forall (λ e, is_Some (to_val e)) t2)) as [|Ht2]; [by left|].
  apply (not_Forall_Exists _), Exists_exists in Ht2; destruct Ht2 as (e2&?&He2).
  destruct (adequate_not_stuck NotStuck e1 σ1 φ Had t2 σ2 e2) as [?|(κ&e3&σ3&efs&?)];
    rewrite ?eq_None_not_Some; auto.
  { exfalso. eauto. }
  destruct (list_elem_of_split t2 e2) as (t2'&t2''&->); auto.
  right; exists (t2' ++ e3 :: t2'' ++ efs), σ3, κ; econstructor; eauto.
Qed.