phanerozoic/Coq-Iris huggingface dataset:
(* iris/base_logic/lib/fancy_updates.v *)
(* [invGS_lc] needs to be global in order to enable the use of lemmas like
[lc_split] that require [lcGS], and not [invGS]. [invGS_wsat] also needs to be
global as the lemmas in [invariants.v] require it. *)
Class invGS_gen (hlc : has_lc) (Σ : gFunctors) : Set
:= InvG {
  #[global] invGS_wsat :: wsatGS Σ;
  #[global] invGS_lc :: lcGS hlc Σ;
}.
(* iris/base_logic/lib/fancy_updates.v *)
Notation invGS
:= (invGS_gen HasLc).
(* iris/base_logic/lib/fancy_updates.v *)
Definition invΣ : gFunctors
:= #[wsatΣ; lcΣ].
(* iris/base_logic/lib/fancy_updates.v *)
Instance subG_invΣ {Σ} : subG invΣ Σ → invGpreS Σ.
Proof. solve_inG. Qed.
(* iris/base_logic/lib/fancy_updates.v *)
(* Note that compared to the definition of the fancy update modality in Iris
3.1 ("Iris from the Ground Up") and Iris 4.0 ("Later Credits"), the except-0
modality [◇] is now hidden in the definition of the later-elimination update
[|==£>]. *)
Definition uPred_fupd_def `{!invGS_gen hlc Σ}
    (E1 E2 : coPset) (P : iProp Σ) : iProp Σ
:=
  wsat ∗ ownE E1 -∗ |==£> wsat ∗ ownE E2 ∗ P.
(* iris/base_logic/lib/fancy_updates.v *)
Definition uPred_fupd_aux : seal (@uPred_fupd_def).
Proof. by eexists. Qed.
(* iris/base_logic/lib/fancy_updates.v *)
Definition uPred_fupd
:= uPred_fupd_aux.(unseal).
(* iris/base_logic/lib/fancy_updates.v *)
Lemma uPred_fupd_unseal `{!invGS_gen hlc Σ} :
  @fupd _ uPred_fupd = uPred_fupd_def.
Proof. rewrite -uPred_fupd_aux.(seal_eq) //. Qed.
(* iris/base_logic/lib/fancy_updates.v *)
Lemma uPred_fupd_mixin `{!invGS_gen hlc Σ} :
  BiFUpdMixin (uPredI (iResUR Σ)) uPred_fupd.
Proof.
  split.
  - rewrite uPred_fupd_unseal. solve_proper.
  - intros E1 E2 (E1''&->&?)%subseteq_disjoint_union_L.
    rewrite uPred_fupd_unseal /uPred_fupd_def ownE_op //.
    by iIntros "($ & $ & HE) !> [$ $] !>".
  - rewrite uPred_fupd_unseal.
    iIntros (E1 E2 P) ">H [Hw HE]". iApply "H"; by iFrame.
  - rewrite uPred_fupd_unseal.
    iIntros (E1 E2 P Q HPQ) "HP HwE". rewrite -HPQ. by iApply "HP".
  - rewrite uPred_fupd_unseal. iIntros (E1 E2 E3 P) "HP HwE".
    iMod ("HP" with "HwE") as "(Hw & HE & HP)". iApply "HP"; by iFrame.
  - intros E1 E2 Ef P HE1Ef. rewrite uPred_fupd_unseal /uPred_fupd_def ownE_op //.
    iIntros "Hvs (Hw & HE1 &HEf)".
    iMod ("Hvs" with "[Hw HE1]") as "($ & HE2 & HP)"; first by iFrame.
    iDestruct (ownE_op' with "[HE2 HEf]") as "[? $]"; first by iFrame.
    iIntros "!>". by iApply "HP".
  - rewrite uPred_fupd_unseal /uPred_fupd_def. by iIntros (????) "[HwP $]".
Qed.
(* iris/base_logic/lib/fancy_updates.v *)
Instance uPred_bi_fupd `{!invGS_gen hlc Σ} : BiFUpd (uPredI (iResUR Σ))
:=
  {| bi_fupd_mixin := uPred_fupd_mixin |}.
(* iris/base_logic/lib/fancy_updates.v *)
Instance uPred_bi_bupd_fupd `{!invGS_gen hlc Σ} : BiBUpdFUpd (uPredI (iResUR Σ)).
Proof. rewrite /BiBUpdFUpd uPred_fupd_unseal. by iIntros (E P) ">? [$ $] !>". Qed.
(* iris/base_logic/lib/fancy_updates.v *)
(* If later credits are disabled, this lemma shows that [fupd] is just the
basic update + except-0 modality, i.e., fancy updates are like Iris 3.0. *)
Lemma fupd_unfold_no_lc `{!invGS_gen HasNoLc Σ} E1 E2 (P : iProp Σ) :
  (|={E1,E2}=> P) ⊣⊢ (wsat ∗ ownE E1 ==∗ ◇ (wsat ∗ ownE E2 ∗ P)).
Proof.
  rewrite uPred_fupd_unseal /uPred_fupd_def.
  by rewrite later_credits.le_upd.le_upd_unfold_no_le.
Qed.
(* iris/base_logic/lib/fancy_updates.v *)
(* [lc_fupd_elim_later] allows to eliminate a later from a hypothesis at an update.
This is typically used as [iMod (lc_fupd_elim_later with "Hcredit HP") as "HP".],
where ["Hcredit"] is a credit available in the context and ["HP"] is the
assumption from which a later should be stripped. *)
Lemma lc_fupd_elim_later `{!invGS_gen HasLc Σ} E P :
   £ 1 -∗ (▷ P) -∗ |={E}=> P.
Proof.
  iIntros "Hf Hupd".
  rewrite uPred_fupd_unseal /uPred_fupd_def.
  iIntros "[$ $]". by iApply (lc_le_upd_elim_later with "Hf").
Qed.
(* iris/base_logic/lib/fancy_updates.v *)
(* If the goal is a fancy update, this lemma can be used to make a later appear
in front of it in exchange for a later credit. This is typically used as
[iApply (lc_fupd_add_later with "Hcredit")], where ["Hcredit"] is a credit
available in the context. *)
Lemma lc_fupd_add_later `{!invGS_gen HasLc Σ} E1 E2 P :
  £ 1 -∗ (▷ |={E1, E2}=> P) -∗ |={E1, E2}=> P.
Proof.
  iIntros "Hf Hupd". iApply (fupd_trans E1 E1).
  iApply (lc_fupd_elim_later with "Hf Hupd").
Qed.
(* iris/base_logic/lib/fancy_updates.v *)
(* Similar to above, but here we are adding [n] laters. *)
Lemma lc_fupd_add_laterN `{!invGS_gen HasLc Σ} E1 E2 P n :
  £ n -∗ (▷^n |={E1, E2}=> P) -∗ |={E1, E2}=> P.
Proof.
  iIntros "Hf Hupd". iInduction n as [|n] "IH"; first done.
  iDestruct "Hf" as "[H1 Hf]".
  iApply (lc_fupd_add_later with "H1"); iNext.
  iApply ("IH" with "[$] [$]").
Qed.
(* iris/base_logic/lib/fancy_updates.v *)
Lemma lc_fupd_add_step_fupdN `{!invGS_gen HasLc Σ} E1 E2 E3 P n :
  £ n -∗ (|={E1}[E2]▷=>^n |={E1,E3}=> P) -∗ |={E1,E3}=> P.
Proof.
  iIntros "Hf Hupd". iInduction n as [|n] "IH"; simpl; first done.
  iMod "Hupd". iDestruct "Hf" as "[H1 Hf]".
  iApply (lc_fupd_add_later with "H1"); iNext.
  iMod "Hupd". iApply ("IH" with "[$] [$]").
Qed.
(* iris/base_logic/lib/fancy_updates.v *)
(* The [fupd_finally] modality allows convenient proofs of soundness/adequacy
of a custom modality/program logic. To use it, perform the following steps:
- Apply [pure_soundness] to turn your pure goal into an Iris entailment.
- (Only when *not* using later credits ([HasNoLc]), or proving a theorem generic
  in [hlc : has_lc])
  Apply [laterN_soundness] to add a number of laters.
- Apply [fupd_finally_soundness] to turn the goal into [|={E|}=> ..] and to
  allocate a number of later credits. In addition to the later credits you want
  to supply to the user, you also want to allocate enough later credits to
  eliminate the laters obtained from unfolding a recursive definition (such as
  WP) sufficiently many times.

Next, you can:
- Eliminate update modalities around [|={E|}=> ..] through [fupd_fupd_finally].
  This lemma is used implicitly when using the [iMod] tactic.
- "Duplicate" the context for proving timeless assertions through
  [fupd_finally_keep].
- Introduce foralls below [|={E|}=> ..] through [fupd_finally_forall]. This
  lemma is used implicitly when using the [iIntros] tactic.
- Turn laters below [|={E|}=> ..] into later credits through [fupd_finally_lc]
  or commute them out through [fupd_finally_later].
- Finally introduce the modality using [fupd_finally_intro]. This lemma is used
  implicitly by [iModIntro].

It is important to note that [|={E|}=> P] can only be introduced if [P] is plain
(i.e., it can be proven without resources) due to the [■] modality in the
definition of [|==£|>]. Therefore, rules that have [|={E|}=> P] as a premise
(particularly [fupd_keep]) do not need to require that [P] is plain.

See the proofs of the derived soundness theorems (e.g. [fupd_finally_soundness])
below for examples on how to use the modality. Also see the proofs of adequacy of
WP or total WP. *)
Definition fupd_finally_def `{!invGS_gen hlc Σ}
    (E : coPset) (P : iProp Σ) : iProp Σ
:=
  wsat -∗ ownE E -∗ |==£|> P.
(* iris/base_logic/lib/fancy_updates.v *)
Definition fupd_finally_aux : seal (@fupd_finally_def).
Proof. by eexists. Qed.
(* iris/base_logic/lib/fancy_updates.v *)
Definition fupd_finally
:= fupd_finally_aux.(unseal).
(* iris/base_logic/lib/fancy_updates.v *)
Definition fupd_finally_unseal :
  @fupd_finally = @fupd_finally_def
:= fupd_finally_aux.(seal_eq).
(* iris/base_logic/lib/fancy_updates.v *)
Notation "|={ E |}=> Q"
:= (fupd_finally E Q)
  (at level 20, E at level 50, Q at level 200,
   format "'[  ' |={ E |}=>  '/' Q ']'") : bi_scope.
(* iris/base_logic/lib/fancy_updates.v *)
Notation "P ={ E |}=∗ Q"
:= (P -∗ fupd_finally E Q)%I
  (at level 99, E at level 50, Q at level 200,
   format "'[' P  ={ E |}=∗  '/' '[' Q ']' ']'") : bi_scope.
(* iris/base_logic/lib/fancy_updates.v *)
Notation "P ={ E |}=∗ Q"
:= (P -∗ fupd_finally E Q)
  (at level 99, E at level 50, Q at level 200,
   format "'[' P  ={ E |}=∗  '/' '[' Q ']' ']'") : stdpp_scope.
(* iris/base_logic/lib/fancy_updates.v *)
Instance fupd_finally_ne E : NonExpansive (fupd_finally E).
Proof. rewrite fupd_finally_unseal. solve_proper. Qed.
(* iris/base_logic/lib/fancy_updates.v *)
Lemma fupd_finally_mono E P Q : (P ⊢ Q) → (|={E|}=> P) ⊢ (|={E|}=> Q).
Proof. rewrite fupd_finally_unseal. solve_proper. Qed.
(* iris/base_logic/lib/fancy_updates.v *)
Lemma fupd_finally_intro E P : ■ P ⊢ |={E|}=> P.
Proof.
    rewrite fupd_finally_unseal.
    iIntros "#HP _ _". by iApply le_upd_finally_intro.
  Qed.
(* iris/base_logic/lib/fancy_updates.v *)
Lemma fupd_fupd_finally E1 E2 P : (|={E1,E2}=> |={E2|}=> P) ⊢ |={E1|}=> P.
Proof.
    rewrite fupd_finally_unseal uPred_fupd_unseal.
    iIntros "HP Hw HE1". rewrite /uPred_fupd_def /=.
    iApply le_upd_le_upd_finally.
    iMod ("HP" with "[$Hw $HE1]") as "HP"; iModIntro.
    iDestruct "HP" as "(Hw & HE2 & HP)". iApply ("HP" with "Hw HE2").
  Qed.
(* iris/base_logic/lib/fancy_updates.v *)
(* Generate a later credit by removing a later below the modality. This only
  works if the proposition below the later can be turned into an except-0 [◇]. *)
Lemma fupd_finally_add_lc E P : (£ 1 -∗ |={E|}=> P) ⊢ |={E|}=> ▷ ◇ P.
Proof.
    rewrite fupd_finally_unseal. iIntros "H Hw HE".
    iApply le_upd_finally_add_lc. iIntros "H£". iApply ("H" with "H£ Hw HE").
  Qed.
(* iris/base_logic/lib/fancy_updates.v *)
Lemma fupd_finally_except_0 E P : (|={E|}=> ◇ P) ⊢ |={E|}=> P.
Proof.
    rewrite fupd_finally_unseal. iIntros "H Hw HE".
    iApply le_upd_finally_except_0. iApply ("H" with "Hw HE").
  Qed.
(* iris/base_logic/lib/fancy_updates.v *)
(* Commute a later out of the modality. This only works if the proposition
  below the later can be turned into an except-0 [◇].
  This lemma is derivable from [fupd_finally_lc] with [hlc:=HasLc], but
  not with [hlc:=HasNoLc]. *)
Lemma fupd_finally_later E P : ▷ (|={E|}=> P) ⊢ |={E|}=> ▷ ◇ P.
Proof.
    rewrite fupd_finally_unseal. iIntros "H Hw HE". iApply le_upd_finally_later.
    iNext. iApply ("H" with "Hw HE").
  Qed.
(* iris/base_logic/lib/fancy_updates.v *)
(* [iApply] this lemma to use your current context for proving a (timeless)
  assertion [P] *without* actually using up the context. You can then continue
  the proof in the second conjunct. If later credits are disabled,
  this works for *all* [P], not just timeless assertions. [P] can
  be proven under the [fupd_finally] modality; see above for context. *)
Lemma fupd_keep {E1 E2} P Q `{!TCOr (TCEq hlc HasNoLc) (Timeless P)} :
    (|={E1|}=> P) ∧ (P -∗ |={E1,E2}=> Q) ⊢ |={E1,E2}=> Q.
Proof.
    rewrite fupd_finally_unseal uPred_fupd_unseal. iIntros "H [Hw HE]".
    iApply (le_upd_keep P). iSplit.
    - iDestruct "H" as "[H _]". iApply ("H" with "Hw HE").
    - iIntros "HP". iDestruct "H" as "[_ H]". iApply ("H" with "HP [$Hw $HE]").
  Qed.
(* iris/base_logic/lib/fancy_updates.v *)
Lemma fupd_finally_forall {A} E (Φ : A → iProp Σ) :
    (∀ x, |={E|}=> Φ x) ⊢ |={E|}=> ∀ x, Φ x.
Proof.
    rewrite fupd_finally_unseal. iIntros "H Hw HE".
    iApply le_upd_finally_forall; iIntros (x). iApply ("H" with "Hw HE").
  Qed.
(* iris/base_logic/lib/fancy_updates.v *)
(* Derived *)
Instance fupd_finally_proper E : Proper ((⊣⊢) ==> (⊣⊢)) (fupd_finally E).
Proof. apply: ne_proper. Qed.
(* iris/base_logic/lib/fancy_updates.v *)
Instance fupd_finally_mono' E : Proper ((⊢) ==> (⊢)) (fupd_finally E).
Proof. intros P Q. apply fupd_finally_mono. Qed.
(* iris/base_logic/lib/fancy_updates.v *)
Instance fupd_finally_flip_mono' E :
    Proper (flip (⊢) ==> flip (⊢)) (fupd_finally E).
Proof. intros P Q. apply fupd_finally_mono. Qed.
(* iris/base_logic/lib/fancy_updates.v *)
(* [iApply] this lemma to use your current context for proving a timeless
  assertion [P] *without* actually using up the context. You can then continue
  the proof in the second conjunct. *)
Lemma fupd_finally_keep {E} P Q `{!TCOr (TCEq hlc HasNoLc) (Timeless P)} :
    (|={E|}=> P) ∧ (P -∗ |={E|}=> Q) ⊢ |={E|}=> Q.
Proof.
    iIntros "H". iApply (fupd_fupd_finally E E). iApply (fupd_keep P).
    by rewrite -fupd_intro.
  Qed.
(* iris/base_logic/lib/fancy_updates.v *)
(* [iApply] this lemma to use your current context for proving a pure
  proposition [φ] *without* actually using up the context and masks. You can
  then continue the proof in the second conjunct. *)
Lemma fupd_keep_pure {E1 E2} φ E2' (Q : iProp Σ) :
    (|={E1,E2'}=> ⌜ φ ⌝) ∧ (⌜ φ ⌝ ={E1,E2}=∗ Q) ⊢ |={E1,E2}=> Q.
Proof.
    iIntros "H". iApply (fupd_keep ⌜ φ ⌝).
    iEval (rewrite -(fupd_fupd_finally E1 E2')).
    by iEval (rewrite -fupd_finally_intro plain_plainly).
  Qed.
(* iris/base_logic/lib/fancy_updates.v *)
Lemma fupd_pure_forall E1 E2 {A} (φ : A → Prop) :
    E2 ⊆ E1 →
    (|={E1,E2}=> ∀ x, ⌜ φ x ⌝) ⊣⊢@{iProp Σ} (∀ x, |={E1,E2}=> ⌜ φ x ⌝).
Proof.
    intros. iSplit; first by iIntros ">H %x !> //".
    iIntros "H". iApply (fupd_keep (∀ x, ⌜ φ x ⌝)). iSplit.
    - iApply fupd_finally_forall; iIntros (x). iApply fupd_fupd_finally.
      iMod ("H" $! x) as "#?". iModIntro. iApply fupd_finally_intro. auto.
    - iIntros "$". by iMod (fupd_mask_subseteq E2).
  Qed.
(* iris/base_logic/lib/fancy_updates.v *)
Lemma fupd_finally_and E P Q : (|={E|}=> P) ∧ (|={E|}=> Q) ⊢ |={E|}=> P ∧ Q.
Proof. rewrite !and_alt -fupd_finally_forall. by f_equiv=> -[]. Qed.
(* iris/base_logic/lib/fancy_updates.v *)
Lemma fupd_finally_wand E P Q : (|={E|}=> P) -∗ ■ (P -∗ Q) -∗ (|={E|}=> Q).
Proof.
    apply entails_wand, wand_intro_r.
    rewrite -plainly_and_sep_r -plainly_idemp.
    rewrite (fupd_finally_intro E) fupd_finally_and.
    by rewrite plainly_and_sep_r plainly_elim wand_elim_r.
  Qed.
(* iris/base_logic/lib/fancy_updates.v *)
Lemma fupd_finally_mask_mono E1 E2 P : E1 ⊆ E2 → (|={E1|}=> P) ⊢ |={E2|}=> P.
Proof.
    iIntros (?) "H". iApply fupd_fupd_finally. by iApply fupd_mask_intro_discard.
  Qed.
(* iris/base_logic/lib/fancy_updates.v *)
(* Introduction of [|={E|}=> P] is the same as introduction of [■]: all
  non-plain propositions are removed from the context. *)
Instance from_modal_fupd_finally E P :
    FromModal True modality_plainly (|={E|}=> P) (|={E|}=> P) P.
Proof. intros _. apply fupd_finally_intro. Qed.
(* iris/base_logic/lib/fancy_updates.v *)
Instance from_pure_fupd_finally a E P φ :
    FromPure a P φ → FromPure a (|={E|}=> P) φ.
Proof.
    rewrite /FromPure=> <-. rewrite -fupd_finally_intro.
    by apply plainly_intro; [destruct a; simpl; apply _|].
  Qed.
(* iris/base_logic/lib/fancy_updates.v *)
Instance from_forall_fupd_finally E {A} P (Φ : A → iProp Σ) name :
    FromForall P Φ name →
    FromForall (|={E|}=> P) (λ a, |={E|}=> Φ a)%I name.
Proof. rewrite /FromForall=> <-. apply fupd_finally_forall. Qed.
(* iris/base_logic/lib/fancy_updates.v *)
Instance is_except_0_fupd_finally E P : IsExcept0 (|={E|}=> P).
Proof.
    by rewrite /IsExcept0 -{2}(fupd_fupd_finally E E) -except_0_fupd -fupd_intro.
  Qed.
(* iris/base_logic/lib/fancy_updates.v *)
Instance elim_modal_bupd_fupd_finally p E P Q :
    ElimModal True p false (|==> P) P (|={E|}=> Q) (|={E|}=> Q).
Proof.
    rewrite /ElimModal intuitionistically_if_elim /= bupd_frame_r wand_elim_r.
    by rewrite (bupd_fupd E) fupd_fupd_finally.
  Qed.
(* iris/base_logic/lib/fancy_updates.v *)
Instance elim_modal_fupd_fupd_finally p E1 E2 P Q :
    ElimModal True p false (|={E1,E2}=> P) P (|={E1|}=> Q) (|={E2|}=> Q).
Proof.
    rewrite /ElimModal intuitionistically_if_elim /= fupd_frame_r wand_elim_r.
    by rewrite fupd_fupd_finally.
  Qed.
(* iris/base_logic/lib/fancy_updates.v *)
Lemma step_fupdN_fupd_finally E1 E2 n P :
    (|={E1}[E2]▷=>^n |={E1|}=> P) ⊢ |={E1|}=> ▷^n ◇ P.
Proof.
    iIntros "HP". iInduction n as [|n] "IH"; simpl.
    { by iEval (rewrite -except_0_intro). }
    iMod "HP". iEval (rewrite -except_0_idemp -except_0_laterN).
    iApply fupd_finally_later; iNext. iMod "HP". by iApply "IH".
  Qed.
(* iris/base_logic/lib/fancy_updates.v *)
Instance from_forall_fupd_pure E {A} P
      (Φ : A → iProp Σ) (φ : A → Prop) name :
    FromForall P Φ name →
    (∀ x, FromPure false (Φ x) (φ x)) →
    FromForall (|={E}=> P) (λ a, |={E}=> ⌜ φ a ⌝)%I name.
Proof.
    rewrite /FromForall /FromPure=> <- /= HΦ. setoid_rewrite <-HΦ.
    rewrite fupd_pure_forall //.
  Qed.
(* iris/base_logic/lib/fancy_updates.v *)
(* The interaction laws with the plainly modality are only supported when we
opt out of the support for later credits. These rules are derived from the rules
of the *finally* modality. *)
Instance uPred_bi_fupd_sbi_no_lc `{!invGS_gen HasNoLc Σ} :
  BiFUpdSbi (uPredI (iResUR Σ)).
Proof.
  split.
  - iIntros (E E' Pi R) "H".
    iApply (fupd_keep (<si_pure> Pi)); iSplit; last by iDestruct "H" as "[_ H]".
    iDestruct "H" as "[>#H _]". by iModIntro.
  - iIntros (E Pi) "H".
    iApply (fupd_keep (▷ ◇ <si_pure> Pi)); iSplit; last by auto.
    iApply fupd_finally_later. iNext. iMod "H" as "#?". by iModIntro.
  - iIntros (E A Φi) "HΦ".
    iApply (fupd_keep (∀ x, <si_pure> Φi x)); iSplit; last by auto.
    iIntros (x). iMod ("HΦ" $! x) as "#?". by iModIntro.
Qed.
(* iris/base_logic/lib/fancy_updates.v *)
Lemma fupd_finally_soundness hlc `{!invGpreS Σ} n E P :
  (∀ `{!invGS_gen hlc Σ}, £ n ⊢ |={E|}=> P) → ⊢ P.
Proof.
  rewrite fupd_finally_unseal=> HP.
  apply (le_upd_finally_soundness hlc n); iIntros (?) "H£".
  iApply le_upd_le_upd_finally. iMod wsat_alloc as (Hw) "[Hw HE]". iModIntro.
  iApply (HP (InvG _ _ _ _) with "H£ Hw").
  rewrite (union_difference_L E ⊤); [|set_solver].
  rewrite ownE_op; [|set_solver]. iDestruct "HE" as "[$ _]".
Qed.
(* iris/base_logic/lib/fancy_updates.v *)
(* Note: the [hlc = HasNoLc] versions also allow generating later credits, but
these cannot be used for anything. They are merely provided to enable making
the adequacy proof generic in whether later credits are used. *)
Lemma fupd_soundness hlc `{!invGpreS Σ} n E1 E2 (P : iProp Σ) `{!Plain P} :
  (∀ `{invGS_gen hlc Σ}, £ n ={E1,E2}=∗ P) →
  ⊢ P.
Proof.
  intros HP. apply (fupd_finally_soundness hlc n E1); iIntros (?) "H£".
  iMod (HP with "H£") as "#?". by iModIntro.
Qed.
(* iris/base_logic/lib/fancy_updates.v *)
Lemma step_fupdN_soundness hlc `{!invGpreS Σ} n m (P : iProp Σ) `{!Plain P} :
  (∀ `{!invGS_gen hlc Σ}, £ m ={⊤,∅}=∗ |={∅}▷=>^n P) →
  ⊢ P.
Proof.
  intros HP. apply (laterN_soundness _  (n + 1)); simpl.
  apply (fupd_finally_soundness hlc m ⊤); iIntros (Hinv) "Hc".
  iMod (HP with "Hc") as "HP".
  rewrite laterN_add /= -except_0_into_later. iApply step_fupdN_fupd_finally.
  iApply (step_fupdN_wand with "HP"); iIntros "#HP !> //".
Qed.
(* iris/base_logic/lib/fancy_updates.v *)
Lemma step_fupdN_soundness' hlc `{!invGpreS Σ} n m (P : iProp Σ) `{!Plain P} :
  (∀ `{!invGS_gen hlc Σ}, £ m ={⊤}[∅]▷=∗^n P) →
  ⊢ P.
Proof.
  intros HP. apply (laterN_soundness _  (n + 1)); simpl.
  apply (fupd_finally_soundness hlc m ⊤); iIntros (Hinv) "Hc".
  iPoseProof (HP with "Hc") as "HP".
  rewrite laterN_add /= -except_0_into_later. iApply step_fupdN_fupd_finally.
  iApply (step_fupdN_wand with "HP"); iIntros "#HP !> //".
Qed.
(* iris/base_logic/lib/fancy_updates.v *)
(* This theorem exposes that when initializing the [invGS_gen], we can provide
a general lemma that lets one unfold a [|={E1, E2}=> P] into a basic update
while also carrying around some frame [ω E] that tracks the current mask.
We also provide a bunch of later credits for consistency, but there is no way to
use them since this is a [HasNoLc] lemma. *)
Lemma fupd_soundness_no_lc_unfold `{!invGpreS Σ} m E :
  ⊢ |==> ∃ `(Hws: invGS_gen HasNoLc Σ) (ω : coPset → iProp Σ),
    £ m ∗ ω E ∗ □ (∀ E1 E2 P, (|={E1, E2}=> P) -∗ ω E1 ==∗ ◇ (ω E2 ∗ P)).
Proof.
  iMod wsat_alloc as (Hw) "[Hw HE]".
  (* We don't actually want any credits, but we need the [lcGS]. *)
  iDestruct (later_credits.le_upd.lc_alloc_no_lc m) as (Hc) "[_ Hlc]".
  set (Hi := InvG HasNoLc _ Hw Hc).
  iExists Hi, (λ E, wsat ∗ ownE E)%I.
  rewrite (union_difference_L E ⊤); [|set_solver].
  rewrite ownE_op; [|set_solver].
  iDestruct "HE" as "[HE _]". iFrame "Hw HE Hlc".
  iIntros "!>!>" (E1 E2 P) "HP HwE".
  rewrite fancy_updates.uPred_fupd_unseal
          /fancy_updates.uPred_fupd_def -assoc /=.
  iApply later_credits.le_upd.le_upd_unfold_no_le. by iApply ("HP" with "HwE").
Qed.
(* iris/base_logic/lib/fancy_updates.v *)
(* * Now the Rocq-level tactic [iNext credit:H] *)
Lemma tac_lc_add_laterN_split `{!invGS_gen HasLc Σ} Δ Δ' Δ'' E i n m m' P :
  envs_lookup i Δ = Some (false, £ m) →
  (* Ensure that the goal [P] that be turned into a [fupd], i.e. the goal is a
  WP or a (possibly mask-changing) fancy update *)
  AddModal (|={E}=> P) P P →
  NatCancel m n m' 0 →
  envs_replace i false false (Esnoc Enil i (£ m')) Δ = Some Δ' →
  MaybeIntoLaterNEnvs n Δ' Δ'' →
  (m' = 0 ∧
   match envs_lookup_delete false i Δ'' with
   | Some (_, _, Δ''') => envs_entails Δ''' P
   | None => False
   end
   ∨ envs_entails Δ'' P) →
  envs_entails Δ P.
Proof.
  rewrite envs_entails_unseal /NatCancel /AddModal right_id.
  intros Hi HP <- HΔ HΔ' HΔ''. rewrite -HP -wand_refl right_id.
  rewrite envs_replace_sound //. simpl.
  rewrite Nat.add_comm lc_split. rewrite right_id -assoc wand_elim_r.
  rewrite into_laterN_env_sound.
  destruct HΔ'' as [[-> HΔ'']|<-].
  - destruct (envs_lookup_delete _ _) as [[[p Pi] Δ''']|] eqn:HΔ'''; [|done].
    rewrite envs_lookup_delete_sound // HΔ''.
    iIntros "[H£ [_ H]]".
    iApply (lc_fupd_add_laterN with "H£"). by iIntros "!> !>".
  - iIntros "[H£ H]". iApply (lc_fupd_add_laterN with "H£"). by iIntros "!> !>".
Qed.
(* iris/base_logic/lib/fancy_updates_from_vs.v *)
Notation "P ={ E1 , E2 }=> Q"
:= (vs E1 E2 P Q)
  (at level 99, E1,E2 at level 50, Q at level 200,
   format "P  ={ E1 , E2 }=>  Q") : bi_scope.
(* iris/base_logic/lib/fancy_updates_from_vs.v *)
Definition fupd (E1 E2 : coPset) (P : uPred M) : uPred M
:=
  ∃ R, R ∗ vs E1 E2 R P.
(* iris/base_logic/lib/fancy_updates_from_vs.v *)
Notation "|={ E1 , E2 }=> Q"
:= (fupd E1 E2 Q) : bi_scope.
(* iris/base_logic/lib/fancy_updates_from_vs.v *)
Instance fupd_ne E1 E2 : NonExpansive (@fupd E1 E2).
Proof. solve_proper. Qed.
(* iris/base_logic/lib/fancy_updates_from_vs.v *)
Lemma fupd_intro E P : P ⊢ |={E,E}=> P.
Proof. iIntros "HP". iExists P. iFrame "HP". iApply vs_impl; auto. Qed.
(* iris/base_logic/lib/fancy_updates_from_vs.v *)
Lemma fupd_mono E1 E2 P Q : (P ⊢ Q) → (|={E1,E2}=> P) ⊢ |={E1,E2}=> Q.
Proof.
  iIntros (HPQ); iDestruct 1 as (R) "[HR Hvs]".
  iExists R; iFrame "HR". iApply (vs_trans with "[$Hvs]").
  iApply vs_impl. iIntros "!> HP". by iApply HPQ.
Qed.
(* iris/base_logic/lib/fancy_updates_from_vs.v *)
Lemma fupd_trans E1 E2 E3 P : (|={E1,E2}=> |={E2,E3}=> P) ⊢ |={E1,E3}=> P.
Proof.
  iDestruct 1 as (R) "[HR Hvs]". iExists R. iFrame "HR".
  iApply (vs_trans with "[$Hvs]"). clear R.
  iApply vs_exists; iIntros (R). iApply vs_persistent_intro_r; iIntros "Hvs".
  iApply (vs_trans with "[$Hvs]"). iApply vs_impl; auto.
Qed.
(* iris/base_logic/lib/fancy_updates_from_vs.v *)
Lemma fupd_mask_frame_r E1 E2 Ef P :
  E1 ## Ef → (|={E1,E2}=> P) ⊢ |={E1 ∪ Ef,E2 ∪ Ef}=> P.
Proof.
  iIntros (HE); iDestruct 1 as (R) "[HR Hvs]". iExists R; iFrame "HR".
  by iApply vs_mask_frame_r.
Qed.
(* iris/base_logic/lib/fancy_updates_from_vs.v *)
Lemma fupd_frame_r E1 E2 P Q : (|={E1,E2}=> P) ∗ Q ⊢ |={E1,E2}=> P ∗ Q.
Proof.
  iIntros "[Hvs HQ]". iDestruct "Hvs" as (R) "[HR Hvs]".
  iExists (R ∗ Q)%I. iFrame "HR HQ". by iApply vs_frame_r.
Qed.
(* iris/base_logic/lib/gen_heap.v *)
(* The CMRAs we need, and the global ghost names we are using. *)
Class gen_heapGpreS (L V : Type) (Σ : gFunctors) `{Countable L}
:= {
  #[local] gen_heapGpreS_heap :: ghost_mapG Σ L V;
  #[local] gen_heapGpreS_meta :: ghost_mapG Σ L gname;
  #[local] gen_heapGpreS_meta_data :: inG Σ (reservation_mapR (agreeR positiveO));
}.
(* iris/base_logic/lib/gen_heap.v *)
Class gen_heapGS (L V : Type) (Σ : gFunctors) `{Countable L}
:= GenHeapGS {
  #[local] gen_heap_inG :: gen_heapGpreS L V Σ;
  gen_heap_name : gname;
  gen_meta_name : gname
}.
(* iris/base_logic/lib/gen_heap.v *)
Definition gen_heapΣ (L V : Type) `{Countable L} : gFunctors
:= #[
  ghost_mapΣ L V;
  ghost_mapΣ L gname;
  GFunctor (reservation_mapR (agreeR positiveO))
].
(* iris/base_logic/lib/gen_heap.v *)
Instance subG_gen_heapGpreS {Σ L V} `{Countable L} :
  subG (gen_heapΣ L V) Σ → gen_heapGpreS L V Σ.
Proof. solve_inG. Qed.