phanerozoic/Coq-Iris huggingface dataset:
(* iris/bi/lib/core.v *)
Instance coreP_proper : Proper ((⊣⊢) ==> (⊣⊢)) (coreP (PROP:=PROP)).
Proof. solve_proper. Qed.
(* iris/bi/lib/core.v *)
Instance coreP_mono : Proper ((⊢) ==> (⊢)) (coreP (PROP:=PROP)).
Proof. solve_proper. Qed.
(* iris/bi/lib/core.v *)
Instance coreP_flip_mono :
    Proper (flip (⊢) ==> flip (⊢)) (coreP (PROP:=PROP)).
Proof. solve_proper. Qed.
(* iris/bi/lib/core.v *)
Lemma coreP_wand P Q : <affine> ■ (P -∗ Q) -∗ coreP P -∗ coreP Q.
Proof.
    rewrite /coreP. iIntros "#HPQ HP" (R) "#HR #HQR". iApply ("HP" with "HR").
    iIntros "!> !> HP". iApply "HQR". by iApply "HPQ".
  Qed.
(* iris/bi/lib/core.v *)
Lemma coreP_elim P : Persistent P → coreP P -∗ P.
Proof. rewrite /coreP. iIntros (?) "HCP". iApply "HCP"; auto. Qed.
(* iris/bi/lib/core.v *)
(* The [<affine>] modality is needed for general BIs:
  - The right-to-left direction corresponds to elimination of [<pers>], which
    cannot be done without [<affine>].
  - The left-to-right direction corresponds the introduction of [<pers>]. The
    [<affine>] modality makes it stronger since it appears in the LHS of the
    [⊢] in the premise. As a user, you have to prove [<affine> coreP P ⊢ Q],
    which is weaker than [coreP P ⊢ Q]. *)
Lemma coreP_entails `{!BiPersistentlyForall PROP} P Q :
    (<affine> coreP P ⊢ Q) ↔ (P ⊢ <pers> Q).
Proof.
    split.
    - iIntros (HP) "HP". iDestruct (coreP_intro with "HP") as "#HcP {HP}".
      iIntros "!>". by iApply HP.
    - iIntros (->) "HcQ". by iDestruct (coreP_elim with "HcQ") as "#HQ".
  Qed.
(* iris/bi/lib/core.v *)
(* A more convenient variant of the above lemma for affine [P]. *)
Lemma coreP_entails' `{!BiPersistentlyForall PROP} P Q `{!Affine P} :
    (coreP P ⊢ Q) ↔ (P ⊢ □ Q).
Proof.
    rewrite -(affine_affinely (coreP P)) coreP_entails. split.
    - rewrite -{2}(affine_affinely P). by intros ->.
    - intros ->. apply affinely_elim.
  Qed.
(* iris/bi/lib/counterexamples.v *)
Lemma sep_dup P `{!Affine P} : P -∗ P ∗ P.
Proof.
    iIntros "HP". iDestruct (em P) as "[HP'|HnotP]".
    - iFrame "HP HP'".
    - iExFalso. iApply "HnotP". by iModIntro.
  Qed.
(* iris/bi/lib/counterexamples.v *)
Lemma and_sep `{!BiAffine PROP} P Q : P ∧ Q -∗ P ∗ Q.
Proof.
    iIntros "HPQ". iDestruct (sep_dup with "HPQ") as "[HPQ HPQ']".
    iSplitL "HPQ".
    - by iDestruct "HPQ" as "[HP _]".
    - by iDestruct "HPQ'" as "[_ HQ]".
  Qed.
(* iris/bi/lib/counterexamples.v *)
Lemma later_anything `{!BiLöb PROP} P : ⊢@{PROP} ▷ P.
Proof.
    iDestruct (em (▷ False)) as "#[HP|HnotP]".
    - iNext. done.
    - iExFalso. iLöb as "IH". iSpecialize ("HnotP" with "IH"). done.
  Qed.
(* iris/bi/lib/counterexamples.v *)
Lemma later_inconsistent `{!Sbi PROP} : ⊢@{PROP} False.
Proof. apply later_soundness, later_anything. Qed.
(* iris/bi/lib/counterexamples.v *)
Hypothesis bupd_intro : ∀ P, P ⊢ |==> P.
(* iris/bi/lib/counterexamples.v *)
Hypothesis bupd_mono : ∀ P Q, (P ⊢ Q) → (|==> P) ⊢ |==> Q.
(* iris/bi/lib/counterexamples.v *)
Hypothesis bupd_trans : ∀ P, (|==> |==> P) ⊢ |==> P.
(* iris/bi/lib/counterexamples.v *)
Hypothesis bupd_frame_r : ∀ P R, (|==> P) ∗ R ⊢ |==> (P ∗ R).
(* iris/bi/lib/counterexamples.v *)
Hypothesis sprop_persistent : ∀ i P, Persistent (saved i P).
(* iris/bi/lib/counterexamples.v *)
Hypothesis sprop_alloc_dep :
    ∀ (P : ident → PROP), ⊢ (|==> ∃ i, saved i (P i)).
(* iris/bi/lib/counterexamples.v *)
Hypothesis sprop_agree : ∀ i P Q, saved i P ∧ saved i Q ⊢ □ (P ↔ Q).
(* iris/bi/lib/counterexamples.v *)
(* We assume that we cannot update to false. *)
Hypothesis consistency : ¬(⊢ |==> False).
(* iris/bi/lib/counterexamples.v *)
Instance bupd_mono' : Proper ((⊢) ==> (⊢)) bupd.
Proof. intros P Q ?. by apply bupd_mono. Qed.
(* iris/bi/lib/counterexamples.v *)
Instance elim_modal_bupd p P Q : ElimModal True p false (|==> P) P (|==> Q) (|==> Q).
Proof.
    by rewrite /ElimModal bi.intuitionistically_if_elim
      bupd_frame_r bi.wand_elim_r bupd_trans.
  Qed.
(* iris/bi/lib/counterexamples.v *)
(* A bad recursive reference: "Assertion with name [i] does not hold" *)
Definition A (i : ident) : PROP
:= ∃ P, □ (¬ P ∗ saved i P).
(* iris/bi/lib/counterexamples.v *)
Lemma A_alloc : ⊢ |==> ∃ i, saved i (A i).
Proof. by apply sprop_alloc_dep. Qed.
(* iris/bi/lib/counterexamples.v *)
Lemma saved_NA i : saved i (A i) ⊢ ¬ A i.
Proof.
    iIntros "#Hs #HA". iPoseProof "HA" as "HA'".
    iDestruct "HA'" as (P) "[HNP HsP]". iApply "HNP".
    iDestruct (sprop_agree i P (A i) with "[]") as "#[_ HP]".
    { eauto. }
    iApply "HP". done.
  Qed.
(* iris/bi/lib/counterexamples.v *)
Lemma saved_A i : saved i (A i) ⊢ A i.
Proof.
    iIntros "#Hs". iExists (A i). iFrame "Hs".
    iIntros "!>". by iApply saved_NA.
  Qed.
(* iris/bi/lib/counterexamples.v *)
Lemma contradiction : False.
Proof using All.
    apply consistency.
    iMod A_alloc as (i) "#H".
    iPoseProof (saved_NA with "H") as "HN".
    iApply bupd_intro. iApply "HN". iApply saved_A. done.
  Qed.
(* iris/bi/lib/counterexamples.v *)
(* We have the update modality (two classes: empty/full mask) *)
Inductive mask
:= M0 | M1.
(* iris/bi/lib/counterexamples.v *)
Hypothesis fupd_intro : ∀ E P, P ⊢ fupd E P.
(* iris/bi/lib/counterexamples.v *)
Hypothesis fupd_mono : ∀ E P Q, (P ⊢ Q) → fupd E P ⊢ fupd E Q.
(* iris/bi/lib/counterexamples.v *)
Hypothesis fupd_fupd : ∀ E P, fupd E (fupd E P) ⊢ fupd E P.
(* iris/bi/lib/counterexamples.v *)
Hypothesis fupd_frame_l : ∀ E P Q, P ∗ fupd E Q ⊢ fupd E (P ∗ Q).
(* iris/bi/lib/counterexamples.v *)
Hypothesis fupd_mask_mono : ∀ P, fupd M0 P ⊢ fupd M1 P.
(* iris/bi/lib/counterexamples.v *)
Hypothesis inv_persistent : ∀ i P, Persistent (inv i P).
(* iris/bi/lib/counterexamples.v *)
Hypothesis inv_alloc : ∀ P, P ⊢ fupd M1 (∃ i, inv i P).
(* iris/bi/lib/counterexamples.v *)
Hypothesis inv_fupd :
    ∀ i P Q R, (P ∗ Q ⊢ fupd M0 (P ∗ R)) → (inv i P ∗ Q ⊢ fupd M1 R).
(* iris/bi/lib/counterexamples.v *)
(* We assume that we cannot update to false. *)
Hypothesis consistency : ¬ (⊢ fupd M1 False).
(* iris/bi/lib/counterexamples.v *)
(* This completes the general assumptions shared by both paradoxes. We set up
      some general lemmas and proof mode compatibility before proceeding with
      the paradoxes. *)
Lemma inv_fupd' i P R : inv i P ∗ (P -∗ fupd M0 (P ∗ fupd M1 R)) ⊢ fupd M1 R.
Proof.
    iIntros "(#HiP & HP)". iApply fupd_fupd. iApply inv_fupd; last first.
    { iSplit; first done. iExact "HP". }
    iIntros "(HP & HPw)". by iApply "HPw".
  Qed.
(* iris/bi/lib/counterexamples.v *)
Instance fupd_mono' E : Proper ((⊢) ==> (⊢)) (fupd E).
Proof. intros P Q ?. by apply fupd_mono. Qed.
(* iris/bi/lib/counterexamples.v *)
Instance fupd_proper E : Proper ((⊣⊢) ==> (⊣⊢)) (fupd E).
Proof.
    intros P Q; rewrite !bi.equiv_entails=> -[??]; split; by apply fupd_mono.
  Qed.
(* iris/bi/lib/counterexamples.v *)
Lemma fupd_frame_r E P Q : fupd E P ∗ Q ⊢ fupd E (P ∗ Q).
Proof. by rewrite comm fupd_frame_l comm. Qed.
(* iris/bi/lib/counterexamples.v *)
Instance elim_fupd_fupd p E P Q :
    ElimModal True p false (fupd E P) P (fupd E Q) (fupd E Q).
Proof.
    by rewrite /ElimModal bi.intuitionistically_if_elim
      fupd_frame_r bi.wand_elim_r fupd_fupd.
  Qed.
(* iris/bi/lib/counterexamples.v *)
Instance elim_fupd0_fupd1 p P Q :
    ElimModal True p false (fupd M0 P) P (fupd M1 Q) (fupd M1 Q).
Proof.
    by rewrite /ElimModal bi.intuitionistically_if_elim
      fupd_frame_r bi.wand_elim_r fupd_mask_mono fupd_fupd.
  Qed.
(* iris/bi/lib/counterexamples.v *)
Instance exists_split_fupd0 {A} E P (Φ : A → PROP) :
    FromExist P Φ → FromExist (fupd E P) (λ a, fupd E (Φ a)).
Proof.
    rewrite /FromExist=>HP. apply bi.exist_elim=> a.
    apply fupd_mono. by rewrite -HP -(bi.exist_intro a).
  Qed.
(* iris/bi/lib/counterexamples.v *)
Hypothesis sts_alloc : ⊢ fupd M0 (∃ γ, start γ).
(* iris/bi/lib/counterexamples.v *)
Hypotheses start_finish : ∀ γ, start γ ⊢ fupd M0 (finished γ).
(* iris/bi/lib/counterexamples.v *)
Hypothesis finished_not_start : ∀ γ, start γ ∗ finished γ ⊢ False.
(* iris/bi/lib/counterexamples.v *)
Hypothesis finished_dup : ∀ γ, finished γ ⊢ finished γ ∗ finished γ.
(* iris/bi/lib/counterexamples.v *)
(* Now to the actual counterexample. We start with a weird form of saved propositions. *)
Definition saved (γ : gname) (P : PROP) : PROP
:=
      ∃ i, inv i (start γ ∨ (finished γ ∗ □ P)).
(* iris/bi/lib/counterexamples.v *)
Instance saved_persistent γ P : Persistent (saved γ P)
:= _.
(* iris/bi/lib/counterexamples.v *)
Lemma saved_alloc (P : gname → PROP) : ⊢ fupd M1 (∃ γ, saved γ (P γ)).
Proof.
      iIntros "". iMod (sts_alloc) as (γ) "Hs".
      iMod (inv_alloc (start γ ∨ (finished γ ∗ □ (P γ))) with "[Hs]") as (i) "#Hi".
      { auto. }
      iApply fupd_intro. by iExists γ, i.
    Qed.
(* iris/bi/lib/counterexamples.v *)
Lemma saved_cast γ P Q : saved γ P ∗ saved γ Q ∗ □ P ⊢ fupd M1 (□ Q).
Proof.
      iIntros "(#HsP & #HsQ & #HP)". iDestruct "HsP" as (i) "HiP".
      iApply (inv_fupd' i). iSplit; first done.
      iIntros "HaP". iAssert (fupd M0 (finished γ)) with "[HaP]" as "> Hf".
      { iDestruct "HaP" as "[Hs | [Hf _]]".
        - by iApply start_finish.
        - by iApply fupd_intro. }
      iDestruct (finished_dup with "Hf") as "[Hf Hf']".
      iApply fupd_intro. iSplitL "Hf'"; first by eauto.
      (* Step 2: Open the Q-invariant. *)
      iClear (i) "HiP ". iDestruct "HsQ" as (i) "HiQ".
      iApply (inv_fupd' i). iSplit; first done.
      iIntros "[HaQ | [_ #HQ]]".
      { iExFalso. iApply finished_not_start. by iFrame. }
      iApply fupd_intro. iSplitL "Hf".
      { iRight. by iFrame. }
      by iApply fupd_intro.
    Qed.
(* iris/bi/lib/counterexamples.v *)
(* And now we tie a bad knot. *)
Notation not_fupd P
:= (□ (P -∗ fupd M1 False))%I.
(* iris/bi/lib/counterexamples.v *)
Definition A i : PROP
:= ∃ P, not_fupd P ∗ saved i P.
(* iris/bi/lib/counterexamples.v *)
Instance A_persistent i : Persistent (A i)
:= _.
(* iris/bi/lib/counterexamples.v *)
Lemma A_alloc : ⊢ fupd M1 (∃ i, saved i (A i)).
Proof. by apply saved_alloc. Qed.
(* iris/bi/lib/counterexamples.v *)
Lemma saved_NA i : saved i (A i) ⊢ not_fupd (A i).
Proof.
      iIntros "#Hi !> #HA". iPoseProof "HA" as "HA'".
      iDestruct "HA'" as (P) "#[HNP Hi']".
      iMod (saved_cast i (A i) P with "[]") as "HP".
      { eauto. }
      by iApply "HNP".
    Qed.
(* iris/bi/lib/counterexamples.v *)
Lemma saved_A i : saved i (A i) ⊢ A i.
Proof.
      iIntros "#Hi". iExists (A i). iFrame "#".
      by iApply saved_NA.
    Qed.
(* iris/bi/lib/counterexamples.v *)
Lemma contradiction : False.
Proof using All.
      apply consistency. iIntros "".
      iMod A_alloc as (i) "#H".
      iPoseProof (saved_NA with "H") as "HN".
      iApply "HN". iApply saved_A. done.
    Qed.
(* iris/bi/lib/counterexamples.v *)
Hypothesis finished_persistent : ∀ γ, Persistent (finished γ).
(* iris/bi/lib/counterexamples.v *)
(* A version of ⊥ behind a persistent update. *)
Definition B : PROP
:= □ fupd M1 False.
(* iris/bi/lib/counterexamples.v *)
(* A delayed-initialization invariant storing [B]. *)
Definition P (γ : gname) : PROP
:= start γ ∨ B.
(* iris/bi/lib/counterexamples.v *)
Definition I (i : name) (γ : gname) : PROP
:= inv i (P γ).
(* iris/bi/lib/counterexamples.v *)
(* If we can ever finish initializing the invariant, we have a
     contradiction. *)
Lemma finished_contradiction γ i :
      finished γ ∗ I i γ -∗ B.
Proof.
      iIntros "[#Hfin #HI] !>".
      iApply (inv_fupd' i). iSplit; first done.
      iIntros "[Hstart|#Hfalse]".
      { iDestruct (finished_not_start with "[$Hfin $Hstart]") as %[]. }
      iApply fupd_intro. iSplitR; last done.
      by iRight.
    Qed.
(* iris/bi/lib/counterexamples.v *)
(* If we can even just create the invariant, we can finish initializing it
     using the above lemma, and then get the contradiction. *)
Lemma invariant_contradiction γ i :
      I i γ -∗ B.
Proof.
      iIntros "#HI !>".
      iApply (inv_fupd' i). iSplit; first done.
      iIntros "HP".
      iAssert (fupd M0 B) with "[HP]" as ">#Hfalse".
      { iDestruct "HP" as "[Hstart|#Hfalse]"; last by iApply fupd_intro.
        iMod (start_finish with "Hstart"). iApply fupd_intro.
        (** There's a magic moment here where we have the invariant open,
          but inside [finished_contradiction] we will be proving
          a [fupd M1] and so we can open the invariant *again*.
          Really we are just building up a thunk that can be used
          later when the invariant is closed again. But to build up that
          thunk we can use resources that we just got out of the invariant,
          before closing it again. *)
        iApply finished_contradiction. eauto. }
      iApply fupd_intro. iSplitR; last done.
      by iRight.
    Qed.
(* iris/bi/lib/counterexamples.v *)
(* Of course, creating the invariant is trivial. *)
Lemma contradiction' : False.
Proof using All.
      apply consistency.
      iMod sts_alloc as (γ) "Hstart".
      iMod (inv_alloc (P γ) with "[Hstart]") as (i) "HI".
      { by iLeft. }
      iDestruct (invariant_contradiction with "HI") as "#>[]".
    Qed.
(* iris/bi/lib/counterexamples.v *)
Hypothesis fupd_intro : ∀ E P, P ⊢ fupd E E P.
(* iris/bi/lib/counterexamples.v *)
Hypothesis fupd_mono : ∀ E1 E2 P Q, (P ⊢ Q) → fupd E1 E2 P ⊢ fupd E1 E2 Q.
(* iris/bi/lib/counterexamples.v *)
Hypothesis fupd_fupd : ∀ E1 E2 E3 P, fupd E1 E2 (fupd E2 E3 P) ⊢ fupd E1 E3 P.
(* iris/bi/lib/counterexamples.v *)
Hypothesis fupd_frame_l : ∀ E1 E2 P Q, P ∗ fupd E1 E2 Q ⊢ fupd E1 E2 (P ∗ Q).
(* iris/bi/lib/counterexamples.v *)
Hypothesis cinv_alloc : ∀ E P,
    ▷ P -∗ fupd E E (∃ γ, cinv γ P ∗ cinv_own γ).
(* iris/bi/lib/counterexamples.v *)
Hypothesis cinv_acc : ∀ P γ,
    cinv γ P -∗ cinv_own γ -∗ fupd M1 M0 (▷ P ∗ cinv_own γ ∗ (▷ P -∗ fupd M0 M1 emp)).
(* iris/bi/lib/counterexamples.v *)
(* Some general lemmas and proof mode compatibility. *)
Instance fupd_mono' E1 E2 : Proper ((⊢) ==> (⊢)) (fupd E1 E2).
Proof. intros P Q ?. by apply fupd_mono. Qed.
(* iris/bi/lib/counterexamples.v *)
Instance fupd_proper E1 E2 : Proper ((⊣⊢) ==> (⊣⊢)) (fupd E1 E2).
Proof.
    intros P Q; rewrite !bi.equiv_entails=> -[??]; split; by apply fupd_mono.
  Qed.
(* iris/bi/lib/counterexamples.v *)
Lemma fupd_frame_r E1 E2 P Q : fupd E1 E2 P ∗ Q ⊢ fupd E1 E2 (P ∗ Q).
Proof. by rewrite comm fupd_frame_l comm. Qed.
(* iris/bi/lib/counterexamples.v *)
Instance elim_fupd_fupd p E1 E2 E3 P Q :
    ElimModal True p false (fupd E1 E2 P) P (fupd E1 E3 Q) (fupd E2 E3 Q).
Proof.
    by rewrite /ElimModal bi.intuitionistically_if_elim
      fupd_frame_r bi.wand_elim_r fupd_fupd.
  Qed.
(* iris/bi/lib/counterexamples.v *)
(* Counterexample: now we can make any resource disappear. *)
Lemma leak P : P -∗ fupd M1 M1 emp.
Proof.
    iIntros "HP".
    iMod (cinv_alloc _ True with "[//]") as (γ) "[Hinv Htok]".
    iMod (cinv_acc with "Hinv Htok") as "(Htrue & Htok & Hclose)".
    iApply "Hclose". done.
  Qed.
(* iris/bi/lib/counterexamples.v *)
Hypothesis lc_fupd_elim_later : ∀ E P, lc ∗ ▷ P ⊢ |={E}=> P.
(* iris/bi/lib/counterexamples.v *)
Hypothesis lc_soundness : ∀ P `{!Plain P} E, (lc ⊢ |={E}=> P) → ⊢ P.
(* iris/bi/lib/counterexamples.v *)
(* We have the keep rule for plain propositions taken from [BiFUpdSbi]. *)
Hypothesis fupd_keep_si_pure' : ∀ {E} E' Pi (R : PROP),
    (|={E,E'}=> <si_pure> Pi) ∧ (<si_pure> Pi ={E}=∗ R) ⊢ |={E}=> R.
(* iris/bi/lib/counterexamples.v *)
(* The [fupd_keep_si_pure'] rule lets you keep later credits around later
  elimination. *)
Lemma lc_fupd_elim_later_keep E P `{!Plain P, !Absorbing P} :
    lc -∗ ▷ P ={E}=∗ lc ∗ P.
Proof.
    iIntros "Hlc HP".
    iApply (fupd_keep_si_pure' E (<si_emp_valid> P)). iSplit.
    - iApply lc_fupd_elim_later. iFrame "Hlc".
      iNext. by rewrite -{1}(plain_plainly P).
    - iIntros "HP' !>". iFrame "Hlc".
      by iApply si_pure_si_emp_valid_elim.
  Qed.
(* iris/bi/lib/counterexamples.v *)
Lemma laterN_False : ⊢@{PROP} ∃ n, ▷^n False.
Proof.
    iLöb as "IH".
    iDestruct "IH" as (n) "Hn".
    by iExists (S n).
  Qed.
(* iris/bi/lib/counterexamples.v *)
(* Now we can just apply [lc_fupd_elim_later_keep] [n] times to the
  result of [laterN_False] (because [▷^n False] is plain) to get [False]. *)
Lemma contradiction : False.
Proof using All.
    apply (pure_soundness (PROP:=PROP)).
    apply (lc_soundness _ ⊤).
    iIntros "Hlc".
    iDestruct laterN_False as (n) "-# Hfalse".
    iDestruct (bi.affinely_elim with "Hfalse") as "Hfalse".
    iInduction n as [|n IH]; simpl; first by iFrame.
    iMod (lc_fupd_elim_later_keep with "Hlc Hfalse") as "[Hlc Hfalse]".
    iApply ("IH" with "Hlc Hfalse").
  Qed.
(* iris/bi/lib/fixpoint_banach.v *)
Lemma fixpoint_plain `{!Sbi PROP} {A}
      (F : (A -d> PROP) → A -d> PROP) `{!Contractive F} :
    (∀ Φ, (∀ x, Plain (Φ x)) → (∀ x, Plain (F Φ x))) →
    ∀ x, Plain (fixpoint F x).
Proof.
    intros ?. apply fixpoint_ind.
    - intros Φ1 Φ2 HΦ ??. by rewrite -(HΦ _).
    - exists (λ _, emp%I); apply _.
    - done.
    - apply limit_preserving_forall=> x.
      apply limit_preserving_Plain; solve_proper.
  Qed.
(* iris/bi/lib/fixpoint_banach.v *)
Lemma fixpoint_persistent {A} (F : (A -d> PROP) → A -d> PROP) `{!Contractive F} :
    (∀ Φ, (∀ x, Persistent (Φ x)) → (∀ x, Persistent (F Φ x))) →
    ∀ x, Persistent (fixpoint F x).
Proof.
    intros ?. apply fixpoint_ind.
    - intros Φ1 Φ2 HΦ ??. by rewrite -(HΦ _).
    - exists (λ _, emp%I); apply _.
    - done.
    - apply limit_preserving_forall=> x.
      apply limit_preserving_Persistent; solve_proper.
  Qed.
(* iris/bi/lib/fixpoint_banach.v *)
Lemma fixpoint_absorbing {A} (F : (A -d> PROP) → A -d> PROP) `{!Contractive F} :
    (∀ Φ, (∀ x, Absorbing (Φ x)) → (∀ x, Absorbing (F Φ x))) →
    ∀ x, Absorbing (fixpoint F x).
Proof.
    intros ?. apply fixpoint_ind.
    - intros Φ1 Φ2 HΦ ??. by rewrite -(HΦ _).
    - exists (λ _, True%I); apply _.
    - done.
    - apply limit_preserving_forall=> x.
      apply limit_preserving_entails; solve_proper.
  Qed.
(* iris/bi/lib/fixpoint_banach.v *)
Lemma fixpoint_affine {A} (F : (A -d> PROP) → A -d> PROP) `{!Contractive F} :
    (∀ Φ, (∀ x, Affine (Φ x)) → (∀ x, Affine (F Φ x))) →
    ∀ x, Affine (fixpoint F x).
Proof.
    intros ?. apply fixpoint_ind.
    - intros Φ1 Φ2 HΦ ??. by rewrite -(HΦ _).
    - exists (λ _, emp%I); apply _.
    - done.
    - apply limit_preserving_forall=> x.
      apply limit_preserving_entails; solve_proper.
  Qed.
(* iris/bi/lib/fixpoint_banach.v *)
Lemma fixpoint_persistent_absoring {A}
      (F : (A -d> PROP) → A -d> PROP) `{!Contractive F} :
    (∀ Φ, (∀ x, Persistent (Φ x)) → (∀ x, Absorbing (Φ x)) →
          (∀ x, Persistent (F Φ x) ∧ Absorbing (F Φ x))) →
    ∀ x, Persistent (fixpoint F x) ∧ Absorbing (fixpoint F x).
Proof.
    intros ?. apply fixpoint_ind.
    - intros Φ1 Φ2 HΦ ??. by rewrite -(HΦ _).
    - exists (λ _, True%I); split; apply _.
    - naive_solver.
    - apply limit_preserving_forall=> x.
      apply limit_preserving_and; apply limit_preserving_entails; solve_proper.
  Qed.
(* iris/bi/lib/fixpoint_banach.v *)
Lemma fixpoint_persistent_affine {A}
      (F : (A -d> PROP) → A -d> PROP) `{!Contractive F} :
    (∀ Φ, (∀ x, Persistent (Φ x)) → (∀ x, Affine (Φ x)) →
          (∀ x, Persistent (F Φ x) ∧ Affine (F Φ x))) →
    ∀ x, Persistent (fixpoint F x) ∧ Affine (fixpoint F x).
Proof.
    intros ?. apply fixpoint_ind.
    - intros Φ1 Φ2 HΦ ??. by rewrite -(HΦ _).
    - exists (λ _, emp%I); split; apply _.
    - naive_solver.
    - apply limit_preserving_forall=> x.
      apply limit_preserving_and; apply limit_preserving_entails; solve_proper.
  Qed.
(* iris/bi/lib/fixpoint_banach.v *)
Lemma fixpoint_plain_absoring `{!Sbi PROP} {A}
      (F : (A -d> PROP) → A -d> PROP) `{!Contractive F} :
    (∀ Φ, (∀ x, Plain (Φ x)) → (∀ x, Absorbing (Φ x)) →
          (∀ x, Plain (F Φ x) ∧ Absorbing (F Φ x))) →
    ∀ x, Plain (fixpoint F x) ∧ Absorbing (fixpoint F x).
Proof.
    intros ?. apply fixpoint_ind.
    - intros Φ1 Φ2 HΦ ??. by rewrite -(HΦ _).
    - exists (λ _, True%I); split; apply _.
    - naive_solver.
    - apply limit_preserving_forall=> x.
      apply limit_preserving_and; apply limit_preserving_entails; solve_proper.
  Qed.
(* iris/bi/lib/fixpoint_banach.v *)
Lemma fixpoint_plain_affine `{!Sbi PROP} {A}
      (F : (A -d> PROP) → A -d> PROP) `{!Contractive F} :
    (∀ Φ, (∀ x, Plain (Φ x)) → (∀ x, Affine (Φ x)) →
          (∀ x, Plain (F Φ x) ∧ Affine (F Φ x))) →
    ∀ x, Plain (fixpoint F x) ∧ Affine (fixpoint F x).
Proof.
    intros ?. apply fixpoint_ind.
    - intros Φ1 Φ2 HΦ ??. by rewrite -(HΦ _).
    - exists (λ _, emp%I); split; apply _.
    - naive_solver.
    - apply limit_preserving_forall=> x.
      apply limit_preserving_and; apply limit_preserving_entails; solve_proper.
  Qed.
(* iris/bi/lib/fixpoint_mono.v *)
(* Least and greatest fixpoint of a monotone function, defined entirely inside
    the logic. *)
Class BiMonoPred {PROP : bi} {A : ofe} (F : (A → PROP) → (A → PROP))
:= {
  bi_mono_pred Φ Ψ :
    NonExpansive Φ →
    NonExpansive Ψ →
    □ (∀ x, Φ x -∗ Ψ x) -∗ ∀ x, F Φ x -∗ F Ψ x;
  bi_mono_pred_ne Φ : NonExpansive Φ → NonExpansive (F Φ)
}.
(* iris/bi/lib/fixpoint_mono.v *)
Definition bi_least_fixpoint {PROP : bi} {A : ofe}
    (F : (A → PROP) → (A → PROP)) (x : A) : PROP
:=
  tc_opaque (∀ Φ : A -n> PROP, □ (∀ x, F Φ x -∗ Φ x) -∗ Φ x)%I.
(* iris/bi/lib/fixpoint_mono.v *)
Definition bi_greatest_fixpoint {PROP : bi} {A : ofe}
    (F : (A → PROP) → (A → PROP)) (x : A) : PROP
:=
  tc_opaque (∃ Φ : A -n> PROP, □ (∀ x, Φ x -∗ F Φ x) ∗ Φ x)%I.
(* 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 least_fixpoint_ne' {PROP : bi} {A : ofe} (F : (A → PROP) → (A → PROP)):
  (∀ Φ, NonExpansive Φ → NonExpansive (F Φ)) → NonExpansive (bi_least_fixpoint F).
Proof. solve_proper. Qed.
(* iris/bi/lib/fixpoint_mono.v *)
Instance least_fixpoint_ne {PROP : bi} {A : ofe} n :
  Proper (pointwise_relation (A → PROP) (pointwise_relation A (dist n)) ==>
          dist n ==> dist n) bi_least_fixpoint.
Proof. solve_proper. Qed.
(* iris/bi/lib/fixpoint_mono.v *)
Instance least_fixpoint_proper {PROP : bi} {A : ofe} :
  Proper (pointwise_relation (A → PROP) (pointwise_relation A (≡)) ==>
          (≡) ==> (≡)) bi_least_fixpoint.
Proof. solve_proper. Qed.
(* iris/bi/lib/fixpoint_mono.v *)
Lemma least_fixpoint_unfold_2 x : F (bi_least_fixpoint F) x ⊢ bi_least_fixpoint F x.
Proof using Type*.
    rewrite /bi_least_fixpoint /=. iIntros "HF" (Φ) "#Hincl".
    iApply "Hincl". iApply (bi_mono_pred _ Φ with "[#] HF"); [solve_proper|].
    iIntros "!>" (y) "Hy". iApply ("Hy" with "[# //]").
  Qed.
(* iris/bi/lib/fixpoint_mono.v *)
Lemma least_fixpoint_unfold_1 x :
    bi_least_fixpoint F x ⊢ F (bi_least_fixpoint F) x.
Proof using Type*.
    iIntros "HF". iApply ("HF" $! (OfeMor (F (bi_least_fixpoint F))) with "[#]").
    iIntros "!>" (y) "Hy /=". iApply (bi_mono_pred with "[#] Hy").
    iIntros "!>" (z) "?". by iApply least_fixpoint_unfold_2.
  Qed.
(* iris/bi/lib/fixpoint_mono.v *)
Corollary least_fixpoint_unfold x :
    bi_least_fixpoint F x ≡ F (bi_least_fixpoint F) x.
Proof using Type*.
    apply (anti_symm _); auto using least_fixpoint_unfold_1, least_fixpoint_unfold_2.
  Qed.
(* iris/bi/lib/fixpoint_mono.v *)
(* The basic induction principle for least fixpoints: as inductive hypothesis,
    it allows to assume the statement to prove below exactly one application of [F]. *)
Lemma least_fixpoint_iter (Φ : A → PROP) `{!NonExpansive Φ} :
    □ (∀ y, F Φ y -∗ Φ y) -∗ ∀ x, bi_least_fixpoint F x -∗ Φ x.
Proof.
    iIntros "#HΦ" (x) "HF". by iApply ("HF" $! (OfeMor Φ) with "[#]").
  Qed.
(* iris/bi/lib/fixpoint_mono.v *)
Lemma least_fixpoint_affine :
    (∀ x, Affine (F (λ _, emp%I) x)) →
    ∀ x, Affine (bi_least_fixpoint F x).
Proof.
    intros ?. rewrite /Affine. iApply least_fixpoint_iter.
    by iIntros "!> %y HF".
  Qed.