phanerozoic/Coq-Iris huggingface dataset:
(* iris/base_logic/lib/gset_bij.v *)
Instance gset_bij_own_auth_as_fractional γ q L :
    AsFractional (γ ↪●BIJ{#q} L) (λ q, γ ↪●BIJ{#q} L) q.
Proof. split; [auto|apply _]. Qed.
(* iris/base_logic/lib/gset_bij.v *)
Lemma gset_bij_own_auth_agree γ dq1 dq2 L1 L2 :
    γ ↪●BIJ{dq1} L1 -∗ γ ↪●BIJ{dq2} L2 -∗
    ⌜✓ (dq1 ⋅ dq2) ∧ L1 = L2 ∧ gset_bijective L1⌝.
Proof.
    rewrite gset_bij_own_auth_eq. iIntros "H1 H2".
    by iCombine "H1 H2" gives %?%gset_bij_auth_dfrac_op_valid.
  Qed.
(* iris/base_logic/lib/gset_bij.v *)
Lemma gset_bij_own_auth_exclusive γ L1 L2 :
    γ ↪●BIJ L1 -∗ γ ↪●BIJ L2 -∗ False.
Proof.
    iIntros "H1 H2".
    by iDestruct (gset_bij_own_auth_agree with "H1 H2") as %[[] _].
  Qed.
(* iris/base_logic/lib/gset_bij.v *)
Lemma gset_bij_own_valid γ dq L :
    γ ↪●BIJ{dq} L -∗ ⌜✓ dq ∧ gset_bijective L⌝.
Proof.
    rewrite gset_bij_own_auth_eq. iIntros "Hauth".
    by iDestruct (own_valid with "Hauth") as %?%gset_bij_auth_dfrac_valid.
  Qed.
(* iris/base_logic/lib/gset_bij.v *)
Lemma gset_bij_own_elem_agree γ a a' b b' :
    γ ↪◯BIJ ⟨a,b⟩ -∗ γ ↪◯BIJ ⟨a',b'⟩ -∗
    ⌜a = a' ↔ b = b'⌝.
Proof.
    rewrite gset_bij_own_elem_eq. iIntros "Hel1 Hel2".
    by iCombine "Hel1 Hel2" gives %?%gset_bij_elem_agree.
  Qed.
(* iris/base_logic/lib/gset_bij.v *)
Lemma gset_bij_own_elem_get {γ dq L} a b :
    (a, b) ∈ L →
    γ ↪●BIJ{dq} L -∗ γ ↪◯BIJ ⟨a,b⟩.
Proof.
    intros. rewrite gset_bij_own_auth_eq gset_bij_own_elem_eq.
    iApply own_mono. by apply bij_view_included.
  Qed.
(* iris/base_logic/lib/gset_bij.v *)
Lemma gset_bij_elem_of {γ dq L} a b :
    γ ↪●BIJ{dq} L -∗ γ ↪◯BIJ ⟨a,b⟩ -∗ ⌜(a, b) ∈ L⌝.
Proof.
    iIntros "Hauth Helem". rewrite gset_bij_own_auth_eq gset_bij_own_elem_eq.
    iCombine "Hauth Helem" gives "%Ha".
    iPureIntro. revert Ha. rewrite bij_both_dfrac_valid. intros (_ & _ & ?); done.
  Qed.
(* iris/base_logic/lib/gset_bij.v *)
Lemma gset_bij_own_elem_get_big γ dq L :
    γ ↪●BIJ{dq} L -∗ [∗ set] ab ∈ L, γ ↪◯BIJ ⟨ab.1,ab.2⟩.
Proof.
    iIntros "Hauth". iApply big_sepS_forall. iIntros ([a b] ?) "/=".
    by iApply gset_bij_own_elem_get.
  Qed.
(* iris/base_logic/lib/gset_bij.v *)
Lemma gset_bij_own_alloc L :
    gset_bijective L →
    ⊢ |==> ∃ γ, γ ↪●BIJ L ∗ [∗ set] ab ∈ L, γ ↪◯BIJ ⟨ab.1,ab.2⟩.
Proof.
    intro. iAssert (∃ γ, γ ↪●BIJ L)%I with "[>]" as (γ) "Hauth".
    { rewrite gset_bij_own_auth_eq. iApply own_alloc. by apply gset_bij_auth_valid. }
    iExists γ. iModIntro. iSplit; [done|].
    by iApply gset_bij_own_elem_get_big.
  Qed.
(* iris/base_logic/lib/gset_bij.v *)
Lemma gset_bij_own_alloc_empty :
    ⊢ |==> ∃ γ, γ ↪●BIJ (∅ : gset (A * B)).
Proof. iMod (gset_bij_own_alloc ∅) as (γ) "[Hauth _]"; by auto. Qed.
(* iris/base_logic/lib/gset_bij.v *)
Lemma gset_bij_own_extend {γ L} a b :
    (∀ b', (a, b') ∉ L) → (∀ a', (a', b) ∉ L) →
    γ ↪●BIJ L ==∗
    γ ↪●BIJ ({[(a, b)]} ∪ L) ∗ γ ↪◯BIJ ⟨a,b⟩.
Proof.
    iIntros (??) "Hauth".
    iAssert (γ ↪●BIJ ({[(a, b)]} ∪ L)) with "[> Hauth]" as "Hauth".
    { rewrite gset_bij_own_auth_eq. iApply (own_update with "Hauth").
      by apply gset_bij_auth_extend. }
    iModIntro. iSplit; [done|].
    iApply (gset_bij_own_elem_get with "Hauth"). set_solver.
  Qed.
(* iris/base_logic/lib/gset_bij.v *)
Lemma gset_bij_own_extend_internal {γ L} a b :
    (∀ b', γ ↪◯BIJ ⟨a,b'⟩ -∗ False) -∗
    (∀ a', γ ↪◯BIJ ⟨a',b⟩ -∗ False) -∗
    γ ↪●BIJ L ==∗
    γ ↪●BIJ ({[(a, b)]} ∪ L) ∗ γ ↪◯BIJ ⟨a,b⟩.
Proof.
    iIntros "Ha Hb HL".
    iAssert ⌜∀ b', (a, b') ∉ L⌝%I as %?.
    { iIntros (b' ?). iApply ("Ha" $! b'). by iApply gset_bij_own_elem_get. }
    iAssert ⌜∀ a', (a', b) ∉ L⌝%I as %?.
    { iIntros (a' ?). iApply ("Hb" $! a'). by iApply gset_bij_own_elem_get. }
    by iApply (gset_bij_own_extend with "HL").
  Qed.
(* iris/base_logic/lib/invariants.v *)
(* Semantic Invariants *)
Definition inv_def `{!invGS_gen hlc Σ} (N : namespace) (P : iProp Σ) : iProp Σ
:=
  □ ∀ E, ⌜↑N ⊆ E⌝ → |={E,E ∖ ↑N}=> ▷ P ∗ (▷ P ={E ∖ ↑N,E}=∗ True).
(* iris/base_logic/lib/invariants.v *)
Definition inv_aux : seal (@inv_def).
Proof. by eexists. Qed.
(* iris/base_logic/lib/invariants.v *)
Definition inv
:= inv_aux.(unseal).
(* iris/base_logic/lib/invariants.v *)
Definition inv_unseal : @inv = @inv_def
:= inv_aux.(seal_eq).
(* iris/base_logic/lib/invariants.v *)
Instance : Params (@inv) 3
:= {}.
(* iris/base_logic/lib/invariants.v *)
(* ** Internal model of invariants *)
Definition own_inv (N : namespace) (P : iProp Σ) : iProp Σ
:=
    ∃ i, ⌜i ∈@{coPset} ↑N⌝ ∧ ownI i P.
(* iris/base_logic/lib/invariants.v *)
Lemma own_inv_acc E N P :
    ↑N ⊆ E → own_inv N P ={E,E∖↑N}=∗ ▷ P ∗ (▷ P ={E∖↑N,E}=∗ True).
Proof.
    rewrite fancy_updates.uPred_fupd_unseal /fancy_updates.uPred_fupd_def.
    iDestruct 1 as (i) "[Hi #HiP]".
    iDestruct "Hi" as % ?%elem_of_subseteq_singleton.
    rewrite {1 4}(union_difference_L (↑ N) E) // ownE_op; last set_solver.
    rewrite {1 5}(union_difference_L {[ i ]} (↑ N)) // ownE_op; last set_solver.
    iIntros "(Hw & [HE $] & $) !>".
    iDestruct (ownI_open i with "[$Hw $HE $HiP]") as "($ & $ & HD)".
    iIntros "HP [Hw $] !>". iApply (ownI_close _ P). by iFrame.
  Qed.
(* iris/base_logic/lib/invariants.v *)
Lemma fresh_inv_name (E : gset positive) N : ∃ i, i ∉ E ∧ i ∈@{coPset} ↑N.
Proof.
    exists (coPpick (↑ N ∖ gset_to_coPset E)).
    opose proof (coPpick_elem_of (↑ N ∖ gset_to_coPset E) _); last set_solver.
    apply set_infinite_non_empty, difference_infinite, gset_to_coPset_finite.
    apply nclose_infinite.
  Qed.
(* iris/base_logic/lib/invariants.v *)
Lemma own_inv_alloc N E P : ▷ P ={E}=∗ own_inv N P.
Proof.
    rewrite fancy_updates.uPred_fupd_unseal /fancy_updates.uPred_fupd_def.
    iIntros "HP [Hw $]".
    iMod (ownI_alloc (.∈ (↑N : coPset)) P with "[$HP $Hw]")
      as (i ?) "[$ ?]"; auto using fresh_inv_name.
    iModIntro. iExists i. auto.
  Qed.
(* iris/base_logic/lib/invariants.v *)
(* This does not imply [own_inv_alloc] due to the extra assumption [↑N ⊆ E]. *)
Lemma own_inv_alloc_open N E P :
    ↑N ⊆ E → ⊢ |={E, E∖↑N}=> own_inv N P ∗ (▷P ={E∖↑N, E}=∗ True).
Proof.
    rewrite fancy_updates.uPred_fupd_unseal /fancy_updates.uPred_fupd_def.
    iIntros (Sub) "[Hw HE]".
    iMod (ownI_alloc_open (.∈ (↑N : coPset)) P with "Hw")
      as (i ?) "(Hw & #Hi & HD)"; auto using fresh_inv_name.
    iAssert (ownE {[i]} ∗ ownE (↑ N ∖ {[i]}) ∗ ownE (E ∖ ↑ N))%I
      with "[HE]" as "(HEi & HEN\i & HE\N)".
    { rewrite -?ownE_op; [|set_solver..].
      rewrite assoc_L -!union_difference_L //. set_solver. }
    iModIntro. iFrame "HE\N". iSplitL "Hw HEi"; first by iApply "Hw".
    iSplitL "Hi".
    { iExists i. auto. }
    iIntros "HP [Hw HE\N]".
    iDestruct (ownI_close with "[$Hw $Hi $HP $HD]") as "[$ HEi]".
    iModIntro. iSplitL; [|done].
    iCombine "HEi HEN\i HE\N" as "HEN".
    rewrite -?ownE_op; [|set_solver..].
    rewrite assoc_L -!union_difference_L //; set_solver.
  Qed.
(* iris/base_logic/lib/invariants.v *)
Lemma own_inv_to_inv M P: own_inv M P -∗ inv M P.
Proof.
    iIntros "#I". rewrite inv_unseal. iIntros (E H).
    iPoseProof (own_inv_acc with "I") as "H"; eauto.
  Qed.
(* iris/base_logic/lib/invariants.v *)
(* ** Public API of invariants *)
Instance inv_contractive N : Contractive (inv N).
Proof. rewrite inv_unseal. solve_contractive. Qed.
(* iris/base_logic/lib/invariants.v *)
Instance inv_ne N : NonExpansive (inv N).
Proof. apply contractive_ne, _. Qed.
(* iris/base_logic/lib/invariants.v *)
Instance inv_proper N : Proper (equiv ==> equiv) (inv N).
Proof. apply ne_proper, _. Qed.
(* iris/base_logic/lib/invariants.v *)
Instance inv_persistent N P : Persistent (inv N P).
Proof. rewrite inv_unseal. apply _. Qed.
(* iris/base_logic/lib/invariants.v *)
Lemma inv_alter N P Q : inv N P -∗ ▷ □ (P -∗ Q ∗ (Q -∗ P)) -∗ inv N Q.
Proof.
    rewrite inv_unseal. iIntros "#HI #HPQ !>" (E H).
    iMod ("HI" $! E H) as "[HP Hclose]".
    iDestruct ("HPQ" with "HP") as "[$ HQP]".
    iIntros "!> HQ". iApply "Hclose". iApply "HQP". done.
  Qed.
(* iris/base_logic/lib/invariants.v *)
Lemma inv_iff N P Q : inv N P -∗ ▷ □ (P ↔ Q) -∗ inv N Q.
Proof.
    iIntros "#HI #HPQ". iApply (inv_alter with "HI").
    iIntros "!> !> HP". iSplitL "HP".
    - by iApply "HPQ".
    - iIntros "HQ". by iApply "HPQ".
  Qed.
(* iris/base_logic/lib/invariants.v *)
Lemma inv_alloc N E P : ▷ P ={E}=∗ inv N P.
Proof.
    iIntros "HP". iApply own_inv_to_inv.
    iApply (own_inv_alloc N E with "HP").
  Qed.
(* iris/base_logic/lib/invariants.v *)
Lemma inv_alloc_open N E P :
    ↑N ⊆ E → ⊢ |={E, E∖↑N}=> inv N P ∗ (▷P ={E∖↑N, E}=∗ True).
Proof.
    iIntros (?). iMod own_inv_alloc_open as "[HI $]"; first done.
    iApply own_inv_to_inv. done.
  Qed.
(* iris/base_logic/lib/invariants.v *)
Lemma inv_acc E N P :
    ↑N ⊆ E → inv N P ={E,E∖↑N}=∗ ▷ P ∗ (▷ P ={E∖↑N,E}=∗ True).
Proof.
    rewrite inv_unseal /inv_def; iIntros (?) "#HI". by iApply "HI".
  Qed.
(* iris/base_logic/lib/invariants.v *)
Lemma inv_combine N1 N2 N P Q :
    N1 ## N2 →
    ↑N1 ∪ ↑N2 ⊆@{coPset} ↑N →
    inv N1 P -∗ inv N2 Q -∗ inv N (P ∗ Q).
Proof.
    rewrite inv_unseal. iIntros (??) "#HinvP #HinvQ !>"; iIntros (E ?).
    iMod ("HinvP" with "[%]") as "[$ HcloseP]"; first set_solver.
    iMod ("HinvQ" with "[%]") as "[$ HcloseQ]"; first set_solver.
    iApply fupd_mask_intro; first set_solver.
    iIntros "Hclose [HP HQ]".
    iMod "Hclose" as % _. iMod ("HcloseQ" with "HQ") as % _. by iApply "HcloseP".
  Qed.
(* iris/base_logic/lib/invariants.v *)
Lemma inv_combine_dup_l N P Q :
    □ (P -∗ P ∗ P) -∗
    inv N P -∗ inv N Q -∗ inv N (P ∗ Q).
Proof.
    rewrite inv_unseal. iIntros "#HPdup #HinvP #HinvQ !>" (E ?).
    iMod ("HinvP" with "[//]") as "[HP HcloseP]".
    iDestruct ("HPdup" with "HP") as "[$ HP]".
    iMod ("HcloseP" with "HP") as % _.
    iMod ("HinvQ" with "[//]") as "[$ HcloseQ]".
    iIntros "!> [HP HQ]". by iApply "HcloseQ".
  Qed.
(* iris/base_logic/lib/invariants.v *)
Lemma except_0_inv N P : ◇ inv N P ⊢ inv N P.
Proof.
    rewrite inv_unseal /inv_def. iIntros "#H !>" (E ?).
    iMod "H". by iApply "H".
  Qed.
(* iris/base_logic/lib/invariants.v *)
(* ** Proof mode integration *)
Instance is_except_0_inv N P : IsExcept0 (inv N P).
Proof. apply except_0_inv. Qed.
(* iris/base_logic/lib/invariants.v *)
Instance into_inv_inv N P : IntoInv (inv N P) N
:= {}.
(* iris/base_logic/lib/invariants.v *)
Instance into_acc_inv N P E:
    IntoAcc (X := unit) (inv N P)
            (↑N ⊆ E) True (fupd E (E ∖ ↑N)) (fupd (E ∖ ↑N) E)
            (λ _ : (), (▷ P)%I) (λ _ : (), (▷ P)%I) (λ _ : (), None).
Proof.
    rewrite /IntoAcc /accessor bi.exist_unit.
    iIntros (?) "#Hinv _". by iApply inv_acc.
  Qed.
(* iris/base_logic/lib/invariants.v *)
(* ** Derived properties *)
Lemma inv_acc_strong E N P :
    ↑N ⊆ E → inv N P ={E,E∖↑N}=∗ ▷ P ∗ ∀ E', ▷ P ={E',↑N ∪ E'}=∗ True.
Proof.
    iIntros (?) "Hinv".
    iPoseProof (inv_acc (↑ N) N with "Hinv") as "H"; first done.
    rewrite difference_diag_L.
    iPoseProof (fupd_mask_frame_r _ _ (E ∖ ↑ N) with "H") as "H"; first set_solver.
    rewrite left_id_L -union_difference_L //. iMod "H" as "[$ H]"; iModIntro.
    iIntros (E') "HP".
    iPoseProof (fupd_mask_frame_r _ _ E' with "(H HP)") as "H"; first set_solver.
    by rewrite left_id_L.
  Qed.
(* iris/base_logic/lib/invariants.v *)
Lemma inv_acc_timeless E N P `{!Timeless P} :
    ↑N ⊆ E → inv N P ={E,E∖↑N}=∗ P ∗ (P ={E∖↑N,E}=∗ True).
Proof.
    iIntros (?) "Hinv". iMod (inv_acc with "Hinv") as "[>HP Hclose]"; auto.
    iIntros "!> {$HP} HP". iApply "Hclose"; auto.
  Qed.
(* iris/base_logic/lib/invariants.v *)
Lemma inv_split_l N P Q : inv N (P ∗ Q) -∗ inv N P.
Proof.
    iIntros "#HI". iApply inv_alter; eauto.
    iIntros "!> !> [$ $] $".
  Qed.
(* iris/base_logic/lib/invariants.v *)
Lemma inv_split_r N P Q : inv N (P ∗ Q) -∗ inv N Q.
Proof.
    rewrite (comm _ P Q). eapply inv_split_l.
  Qed.
(* iris/base_logic/lib/invariants.v *)
Lemma inv_split N P Q : inv N (P ∗ Q) -∗ inv N P ∗ inv N Q.
Proof.
    iIntros "#H".
    iPoseProof (inv_split_l with "H") as "$".
    iPoseProof (inv_split_r with "H") as "$".
  Qed.
(* iris/base_logic/lib/iprop.v *)
(* The type [gFunctor] bundles a functor from the category of COFEs to the
category of CMRAs with a proof that it is locally contractive. *)
Structure gFunctor
:= GFunctor {
  gFunctor_F :> rFunctor;
  gFunctor_map_contractive : rFunctorContractive gFunctor_F;
}.
(* iris/base_logic/lib/iprop.v *)
(* The type [gFunctors] describes the parameters [Σ] of the Iris logic: lists
of [gFunctor]s.

Note that [gFunctors] is isomorphic to [list gFunctor], but defined in an
alternative way to avoid universe inconsistencies with respect to the universe
monomorphic [list] type.

Defining [gFunctors] as a dependent record instead of a [sigT] avoids other
universe inconsistencies. *)
Record gFunctors
:= GFunctors {
  gFunctors_len : nat;
  gFunctors_lookup : fin gFunctors_len → gFunctor
}.
(* iris/base_logic/lib/iprop.v *)
Definition gid (Σ : gFunctors)
:= fin (gFunctors_len Σ).
(* iris/base_logic/lib/iprop.v *)
Definition gname
:= positive.
(* iris/base_logic/lib/iprop.v *)
Canonical gnameO
:= leibnizO gname.
(* iris/base_logic/lib/iprop.v *)
(* The resources functor [iResF Σ A := ∀ i : gid, gname -fin-> (Σ i) A]. *)
Definition iResF (Σ : gFunctors) : urFunctor
:=
  discrete_funURF (λ i, gmapURF gname (gFunctors_lookup Σ i)).
(* iris/base_logic/lib/iprop.v *)
Definition nil : gFunctors
:= GFunctors 0 (fin_0_inv _).
(* iris/base_logic/lib/iprop.v *)
Definition singleton (F : gFunctor) : gFunctors
:=
    GFunctors 1 (fin_S_inv (λ _, gFunctor) F (fin_0_inv _)).
(* iris/base_logic/lib/iprop.v *)
Definition app (Σ1 Σ2 : gFunctors) : gFunctors
:=
    GFunctors (gFunctors_len Σ1 + gFunctors_len Σ2)
              (fin_add_inv _ (gFunctors_lookup Σ1) (gFunctors_lookup Σ2)).
(* iris/base_logic/lib/iprop.v *)
Coercion gFunctors.singleton : gFunctor >-> gFunctors.
(* iris/base_logic/lib/iprop.v *)
Notation "#[ ]"
:= gFunctors.nil (format "#[ ]").
(* iris/base_logic/lib/iprop.v *)
Notation "#[ Σ1 ; .. ; Σn ]"
:=
  (gFunctors.app Σ1 .. (gFunctors.app Σn gFunctors.nil) ..).
(* iris/base_logic/lib/iprop.v *)
(* In order to make proofs in the Iris logic modular, they are not done with
respect to some concrete list of functors [Σ], but are instead parametrized by
an arbitrary list of functors [Σ] that contains at least certain functors. For
example, the lock library is parameterized by a functor [Σ] that should have
the functors corresponding to the heap and the exclusive monoid to manage to
lock invariant.

The contraints to can be expressed using the type class [subG Σ1 Σ2], which
expresses that the functors [Σ1] are contained in [Σ2]. *)
Class subG (Σ1 Σ2 : gFunctors)
:= in_subG i :
  { j | gFunctors_lookup Σ1 i = gFunctors_lookup Σ2 j }.
(* iris/base_logic/lib/iprop.v *)
Lemma subG_inv Σ1 Σ2 Σ : subG (gFunctors.app Σ1 Σ2) Σ → subG Σ1 Σ * subG Σ2 Σ.
Proof.
  move=> H; split.
  - move=> i; move: H=> /(_ (Fin.L _ i)) [j] /=. rewrite fin_add_inv_l; eauto.
  - move=> i; move: H=> /(_ (Fin.R _ i)) [j] /=. rewrite fin_add_inv_r; eauto.
Qed.
(* iris/base_logic/lib/iprop.v *)
Instance subG_refl Σ : subG Σ Σ.
Proof. move=> i; by exists i. Qed.
(* iris/base_logic/lib/iprop.v *)
Instance subG_app_l Σ Σ1 Σ2 : subG Σ Σ1 → subG Σ (gFunctors.app Σ1 Σ2).
Proof.
  move=> H i; move: H=> /(_ i) [j ?].
  exists (Fin.L _ j). by rewrite /= fin_add_inv_l.
Qed.
(* iris/base_logic/lib/iprop.v *)
Instance subG_app_r Σ Σ1 Σ2 : subG Σ Σ2 → subG Σ (gFunctors.app Σ1 Σ2).
Proof.
  move=> H i; move: H=> /(_ i) [j ?].
  exists (Fin.R _ j). by rewrite /= fin_add_inv_r.
Qed.
(* iris/base_logic/lib/iprop.v *)
Parameter iPrePropO : gFunctors → ofe.
(* iris/base_logic/lib/iprop.v *)
Definition iResUR (Σ : gFunctors) : ucmra
:=
    discrete_funUR (λ i,
      gmapUR gname (rFunctor_apply (gFunctors_lookup Σ i) (iPrePropO Σ))).
(* iris/base_logic/lib/iprop.v *)
Notation iProp Σ
:= (uPred (iResUR Σ)).
(* iris/base_logic/lib/iprop.v *)
Notation iPropO Σ
:= (uPredO (iResUR Σ)).
(* iris/base_logic/lib/iprop.v *)
Notation iPropI Σ
:= (uPredI (iResUR Σ)).
(* iris/base_logic/lib/iprop.v *)
Parameter iProp_unfold: ∀ {Σ}, iPropO Σ -n> iPrePropO Σ.
(* iris/base_logic/lib/iprop.v *)
Parameter iProp_fold: ∀ {Σ}, iPrePropO Σ -n> iPropO Σ.
(* iris/base_logic/lib/iprop.v *)
Parameter iProp_fold_unfold: ∀ {Σ} (P : iProp Σ),
    iProp_fold (iProp_unfold P) ≡ P.
(* iris/base_logic/lib/iprop.v *)
Parameter iProp_unfold_fold: ∀ {Σ} (P : iPrePropO Σ),
    iProp_unfold (iProp_fold P) ≡ P.
(* iris/base_logic/lib/iprop.v *)
Definition iProp_result (Σ : gFunctors) :
    solution (uPredOF (iResF Σ))
:= solver.result _.
(* iris/base_logic/lib/iprop.v *)
Definition iPrePropO (Σ : gFunctors) : ofe
:= iProp_result Σ.
(* iris/base_logic/lib/iprop.v *)
Instance iPreProp_cofe {Σ} : Cofe (iPrePropO Σ)
:= _.
(* iris/base_logic/lib/iprop.v *)
Definition iProp_unfold {Σ} : iPropO Σ -n> iPrePropO Σ
:=
    ofe_iso_1 (iProp_result Σ).
(* iris/base_logic/lib/iprop.v *)
Definition iProp_fold {Σ} : iPrePropO Σ -n> iPropO Σ
:=
    ofe_iso_2 (iProp_result Σ).
(* iris/base_logic/lib/iprop.v *)
Lemma iProp_fold_unfold {Σ} (P : iProp Σ) : iProp_fold (iProp_unfold P) ≡ P.
Proof. apply ofe_iso_21. Qed.
(* iris/base_logic/lib/iprop.v *)
Lemma iProp_unfold_fold {Σ} (P : iPrePropO Σ) : iProp_unfold (iProp_fold P) ≡ P.
Proof. apply ofe_iso_12. Qed.
(* iris/base_logic/lib/iprop.v *)
(* * Properties of the solution to the recursive domain equation *)
Lemma iProp_unfold_equivI {Σ} (P Q : iProp Σ) :
  iProp_unfold P ≡ iProp_unfold Q ⊢@{iPropI Σ} P ≡ Q.
Proof.
  rewrite -{2}(iProp_fold_unfold P) -{2}(iProp_fold_unfold Q). apply: f_equivI.
Qed.
(* iris/base_logic/lib/later_credits.v *)
(* The [hlc : has_lc] parameter indicates whether later credits are enabled
or not. From a user's point of view there are two differences:

- If later credits are enabled ([hlc = HasLc]), we obtain the rule
  [lc_le_upd_elim_later : £ 1 -∗ (▷ P) -∗ |==£> P], which allows us strip a
  later by spending a credit. This rule is used to prove the similar rule for
  the fancy update modality.
- If later credits are disabled ([hlc = HasNoLc]), we obtain the rule
  [le_upd_keep : (|==£|> P) ∧ (P -∗ |==£> Q) ⊢ |==£> Q] without the
  side-condition that [P] should be timeless (the "finally" modality [|==£|>]
  is described further below in this file). This rule is used to derive the
  plain interaction rules [BiFUpdSbi] of the fancy update modality.

In the model, if later credits are disabled ([hlc = HasNoLc]), we simply define
the credit [£ n] as [True] and the supply [lc_supply n] as [n = 0]. This choice
gives uniform proofs, where we do not have to case split on [hlc] for nearly all
rules. *)
Inductive has_lc
:= HasLc | HasNoLc.
(* iris/base_logic/lib/later_credits.v *)
(* The ghost state for later credits *)
Class lcGpreS (Σ : gFunctors)
:= LcGpreS {
  #[local] lcGpreS_inG :: inG Σ (authR natUR)
}.
(* iris/base_logic/lib/later_credits.v *)
Class lcGS (hlc : has_lc) (Σ : gFunctors)
:= LcGS {
  #[local] lcGS_inG :: inG Σ (authR natUR);
  lcGS_name : gname;
}.
(* iris/base_logic/lib/later_credits.v *)
Definition lcΣ
:= #[GFunctor (authR (natUR))].
(* iris/base_logic/lib/later_credits.v *)
Instance subG_lcΣ {Σ} : subG lcΣ Σ → lcGpreS Σ.
Proof. solve_inG. Qed.
(* iris/base_logic/lib/later_credits.v *)
(* The user-facing credit resource, denoting ownership of [n] credits
(but only if later credits are enabled). *)
Definition lc_def `{!lcGS hlc Σ} (n : nat) : iProp Σ
:=
  if hlc is HasLc then own lcGS_name (◯ n) else True.
(* iris/base_logic/lib/later_credits.v *)
Definition lc_aux : seal (@lc_def).
Proof. by eexists. Qed.
(* iris/base_logic/lib/later_credits.v *)
Definition lc
:= lc_aux.(unseal).
(* iris/base_logic/lib/later_credits.v *)
Definition lc_unseal : @lc = @lc_def
:= lc_aux.(seal_eq).
(* iris/base_logic/lib/later_credits.v *)
Notation "'£'  n"
:= (lc n) (at level 1).
(* iris/base_logic/lib/later_credits.v *)
(* The internal authoritative part of the credit ghost state, tracking how many
credits are available in total. Users should not directly interface with this. *)
Definition lc_supply_def `{!lcGS hlc Σ} (n : nat) : iProp Σ
:=
  if hlc is HasLc then own lcGS_name (● n) else ⌜ n = 0 ⌝.
(* iris/base_logic/lib/later_credits.v *)
Definition lc_supply_aux : seal (@lc_supply_def).
Proof. by eexists. Qed.
(* iris/base_logic/lib/later_credits.v *)
Definition lc_supply
:= lc_supply_aux.(unseal).
(* iris/base_logic/lib/later_credits.v *)
Definition lc_supply_unseal :
  @lc_supply = @lc_supply_def
:= lc_supply_aux.(seal_eq).
(* iris/base_logic/lib/later_credits.v *)
Lemma lc_no_lc `{!lcGS HasNoLc Σ} n : £ n ⊣⊢ True.
Proof. by rewrite lc_unseal. Qed.
(* iris/base_logic/lib/later_credits.v *)
Lemma lc_supply_no_lc `{!lcGS HasNoLc Σ} n : lc_supply n ⊣⊢ ⌜ n = 0 ⌝.
Proof. by rewrite lc_supply_unseal. Qed.
(* iris/base_logic/lib/later_credits.v *)
Lemma lc_split n m : £ (n + m) ⊣⊢ £ n ∗ £ m.
Proof.
    rewrite lc_unseal /lc_def. destruct hlc; [|by iSplit; auto].
    rewrite -own_op auth_frag_op //=.
  Qed.
(* iris/base_logic/lib/later_credits.v *)
Lemma lc_zero : ⊢ |==> £ 0.
Proof.
    rewrite lc_unseal /lc_def. destruct hlc; [|by auto]. iApply own_unit.
  Qed.
(* iris/base_logic/lib/later_credits.v *)
Lemma lc_succ n : £ (S n) ⊣⊢ £ 1 ∗ £ n.
Proof. rewrite -lc_split //=. Qed.
(* iris/base_logic/lib/later_credits.v *)
Lemma lc_weaken {n} m : m ≤ n → £ n -∗ £ m.
Proof. intros [k ->]%Nat.le_sum. rewrite lc_split. iIntros "[$ _]". Qed.
(* iris/base_logic/lib/later_credits.v *)
Instance lc_timeless n : Timeless (£ n).
Proof. rewrite lc_unseal /lc_def. apply _. Qed.
(* iris/base_logic/lib/later_credits.v *)
Instance lc_0_persistent : Persistent (£ 0).
Proof. rewrite lc_unseal /lc_def. apply _. Qed.
(* iris/base_logic/lib/later_credits.v *)
(* Make sure that the rule for [+] is used before [S], otherwise Coq's
  unification applies the [S] hint too eagerly. See Iris issue #470. *)
Instance from_sep_lc_add n m : FromSep (£ (n + m)) (£ n) (£ m) | 0.
Proof. by rewrite /FromSep lc_split. Qed.
(* iris/base_logic/lib/later_credits.v *)
Instance from_sep_lc_S n : FromSep (£ (S n)) (£ 1) (£ n) | 1.
Proof. by rewrite /FromSep (lc_succ n). Qed.
(* iris/base_logic/lib/later_credits.v *)
(* When combining later credits with [iCombine], the priorities are
  reversed when compared to [FromSep] and [IntoSep]. This causes
  [£ n] and [£ 1] to be combined as [£ (S n)], not as [£ (n + 1)]. *)
Instance combine_sep_lc_add n m :
    CombineSepAs (£ n) (£ m) (£ (n + m)) | 1.
Proof. by rewrite /CombineSepAs lc_split. Qed.
(* iris/base_logic/lib/later_credits.v *)
Instance combine_sep_lc_S_l n :
    CombineSepAs (£ n) (£ 1) (£ (S n)) | 0.
Proof. by rewrite /CombineSepAs comm (lc_succ n). Qed.
(* iris/base_logic/lib/later_credits.v *)
Instance into_sep_lc_add n m : IntoSep (£ (n + m)) (£ n) (£ m) | 0.
Proof. by rewrite /IntoSep lc_split. Qed.
(* iris/base_logic/lib/later_credits.v *)
Instance into_sep_lc_S n : IntoSep (£ (S n)) (£ 1) (£ n) | 1.
Proof. by rewrite /IntoSep (lc_succ n). Qed.
(* iris/base_logic/lib/later_credits.v *)
Lemma lc_supply_bound n m : lc_supply m -∗ £ n -∗ ⌜n ≤ m⌝.
Proof.
    rewrite lc_unseal /lc_def lc_supply_unseal /lc_supply_def.
    iIntros "H1 H2". iCombine "H1 H2" gives %Hop.
    iPureIntro. eapply auth_both_valid_discrete in Hop as [Hlt _].
    by eapply nat_included.
  Qed.
(* iris/base_logic/lib/later_credits.v *)
Lemma lc_decrease_supply n m :
    lc_supply (n + m) -∗ £ n ==∗ lc_supply m.
Proof.
    rewrite lc_unseal /lc_def lc_supply_unseal /lc_supply_def.
    iIntros "H1 H2". iMod (own_update_2 with "H1 H2") as "Hown".
    { eapply auth_update. eapply (nat_local_update _ _ m 0). lia. }
    by iDestruct "Hown" as "[Hm _]".
  Qed.
(* iris/base_logic/lib/later_credits.v *)
Lemma lc_increase_supply n m :
    lc_supply m ==∗ lc_supply (n + m) ∗ £ n.
Proof.
    rewrite lc_unseal /lc_def lc_supply_unseal /lc_supply_def.
    iIntros "H"; iMod (own_update with "H") as "Hown".
    { eapply auth_update_alloc. eapply (nat_local_update m 0 (n + m) n). lia. }
    iDestruct "Hown" as "[Hm ?]"; by iFrame.
  Qed.