phanerozoic/Coq-Iris huggingface dataset:
(* iris/base_logic/lib/saved_prop.v *)
(* Recover fractional ownership for read-only element. *)
Lemma saved_anything_unpersist γ v :
    saved_anything_own γ DfracDiscarded v ==∗ ∃ q, saved_anything_own γ (DfracOwn q) v.
Proof.
    iIntros "H".
    iMod (own_updateP with "H") as "H";
      first by apply dfrac_agree_unpersist.
    iDestruct "H" as (? (q&->)) "H".
    iIntros "!>". iExists q. done.
  Qed.
(* iris/base_logic/lib/saved_prop.v *)
(* Updates *)
Lemma saved_anything_update y γ x :
    saved_anything_own γ (DfracOwn 1) x ==∗ saved_anything_own γ (DfracOwn 1) y.
Proof.
    iApply own_update. apply cmra_update_exclusive. done.
  Qed.
(* iris/base_logic/lib/saved_prop.v *)
Lemma saved_anything_update_2 y γ q1 q2 x1 x2 :
    (q1 + q2 = 1)%Qp →
    saved_anything_own γ (DfracOwn q1) x1 -∗ saved_anything_own γ (DfracOwn q2) x2 ==∗
    saved_anything_own γ (DfracOwn q1) y ∗ saved_anything_own γ (DfracOwn q2) y.
Proof.
    intros Hq. rewrite -own_op. iApply own_update_2.
    apply dfrac_agree_update_2.
    rewrite dfrac_op_own Hq //.
  Qed.
(* iris/base_logic/lib/saved_prop.v *)
Lemma saved_anything_update_halves y γ x1 x2 :
    saved_anything_own γ (DfracOwn (1/2)) x1 -∗
    saved_anything_own γ (DfracOwn (1/2)) x2 ==∗
    saved_anything_own γ (DfracOwn (1/2)) y ∗ saved_anything_own γ (DfracOwn (1/2)) y.
Proof. iApply saved_anything_update_2. apply Qp.half_half. Qed.
(* iris/base_logic/lib/saved_prop.v *)
(* Saved propositions. *)
Notation savedPropG Σ
:= (savedAnythingG Σ (▶ ∙)).
(* iris/base_logic/lib/saved_prop.v *)
Notation savedPropΣ
:= (savedAnythingΣ (▶ ∙)).
(* iris/base_logic/lib/saved_prop.v *)
Definition saved_prop_own `{!savedPropG Σ} (γ : gname) (dq : dfrac) (P: iProp Σ)
:=
  saved_anything_own (F := ▶ ∙) γ dq (Next P).
(* iris/base_logic/lib/saved_prop.v *)
Instance : Params (@saved_prop_own) 4
:= {}.
(* iris/base_logic/lib/saved_prop.v *)
Notation "γ ↪PROP dq P"
:= (saved_prop_own γ dq P)
  (at level 20, dq custom dfrac at level 1,
   format "γ  ↪PROP dq  P").
(* iris/base_logic/lib/saved_prop.v *)
Instance saved_prop_own_contractive γ dq :
    Contractive (saved_prop_own γ dq).
Proof. solve_contractive. Qed.
(* iris/base_logic/lib/saved_prop.v *)
Instance saved_prop_discarded_persistent γ P :
    Persistent (γ ↪PROP□ P).
Proof. apply _. Qed.
(* iris/base_logic/lib/saved_prop.v *)
Instance saved_prop_fractional γ P : Fractional (λ q, γ ↪PROP{#q} P).
Proof. apply _. Qed.
(* iris/base_logic/lib/saved_prop.v *)
Instance saved_prop_as_fractional γ P q :
    AsFractional (γ ↪PROP{#q} P) (λ q, γ ↪PROP{#q} P) q.
Proof. apply _. Qed.
(* iris/base_logic/lib/saved_prop.v *)
(* Allocation *)
Lemma saved_prop_alloc_strong (I : gname → Prop) P dq :
    ✓ dq →
    pred_infinite I →
    ⊢ |==> ∃ γ, ⌜I γ⌝ ∗ γ ↪PROP{dq} P.
Proof. intros ??. by apply saved_anything_alloc_strong. Qed.
(* iris/base_logic/lib/saved_prop.v *)
Lemma saved_prop_alloc_cofinite (G : gset gname) P dq :
    ✓ dq →
    ⊢ |==> ∃ γ, ⌜γ ∉ G⌝ ∗ γ ↪PROP{dq} P.
Proof. by apply saved_anything_alloc_cofinite. Qed.
(* iris/base_logic/lib/saved_prop.v *)
Lemma saved_prop_alloc P dq :
    ✓ dq →
    ⊢ |==> ∃ γ, γ ↪PROP{dq} P.
Proof. apply saved_anything_alloc. Qed.
(* iris/base_logic/lib/saved_prop.v *)
(* Validity *)
Lemma saved_prop_valid γ dq P :
    γ ↪PROP{dq} P -∗ ⌜✓ dq⌝.
Proof. apply saved_anything_valid. Qed.
(* iris/base_logic/lib/saved_prop.v *)
Lemma saved_prop_valid_2 γ dq1 dq2 P Q :
    γ ↪PROP{dq1} P -∗ γ ↪PROP{dq2} Q -∗ ⌜✓ (dq1 ⋅ dq2)⌝ ∗ ▷ (P ≡ Q).
Proof.
    iIntros "HP HQ".
    iCombine "HP HQ" gives "($ & Hag)".
    by iApply later_equivI.
  Qed.
(* iris/base_logic/lib/saved_prop.v *)
Lemma saved_prop_agree γ dq1 dq2 P Q :
    γ ↪PROP{dq1} P -∗ γ ↪PROP{dq2} Q -∗ ▷ (P ≡ Q).
Proof. iIntros "HP HQ". iCombine "HP" "HQ" gives "[_ $]". Qed.
(* iris/base_logic/lib/saved_prop.v *)
(* Make an element read-only. *)
Lemma saved_prop_persist γ dq P :
    γ ↪PROP{dq} P ==∗ γ ↪PROP□ P.
Proof. apply saved_anything_persist. Qed.
(* iris/base_logic/lib/saved_prop.v *)
(* Recover fractional ownership for read-only element. *)
Lemma saved_prop_unpersist γ v :
    γ ↪PROP□ v ==∗ ∃ q, γ ↪PROP{#q} v.
Proof. apply saved_anything_unpersist. Qed.
(* iris/base_logic/lib/saved_prop.v *)
(* Updates *)
Lemma saved_prop_update Q γ P :
    γ ↪PROP P ==∗ γ ↪PROP Q.
Proof. apply saved_anything_update. Qed.
(* iris/base_logic/lib/saved_prop.v *)
Lemma saved_prop_update_2 Q γ q1 q2 P1 P2 :
    (q1 + q2 = 1)%Qp →
    γ ↪PROP{#q1} P1 -∗ γ ↪PROP{#q2} P2 ==∗ γ ↪PROP{#q1} Q ∗ γ ↪PROP{#q2} Q.
Proof. apply saved_anything_update_2. Qed.
(* iris/base_logic/lib/saved_prop.v *)
Lemma saved_prop_update_halves Q γ P1 P2 :
    γ ↪PROP{#1/2} P1 -∗ γ ↪PROP{#1/2} P2 ==∗ γ ↪PROP{#1/2} Q ∗ γ ↪PROP{#1/2} Q.
Proof. apply saved_anything_update_halves. Qed.
(* iris/base_logic/lib/saved_prop.v *)
(* Saved predicates. *)
Notation savedPredG Σ A
:= (savedAnythingG Σ (A -d> ▶ ∙)).
(* iris/base_logic/lib/saved_prop.v *)
Notation savedPredΣ A
:= (savedAnythingΣ (A -d> ▶ ∙)).
(* iris/base_logic/lib/saved_prop.v *)
Definition saved_pred_own `{!savedPredG Σ A}
    (γ : gname) (dq : dfrac) (Φ : A → iProp Σ)
:=
  saved_anything_own (F := A -d> ▶ ∙) γ dq (Next ∘ Φ).
(* iris/base_logic/lib/saved_prop.v *)
Notation "γ ↪PRED dq Φ"
:= (saved_pred_own γ dq Φ)
  (at level 20, dq custom dfrac at level 1,
   format "γ  ↪PRED dq  Φ").
(* iris/base_logic/lib/saved_prop.v *)
Instance saved_pred_own_contractive γ dq :
    Contractive (saved_pred_own γ dq : (A -d> iPropO Σ) → iProp Σ).
Proof.
    solve_proper_core ltac:(fun _ =>
      first [ intros ?; progress simpl | by auto | f_contractive | f_equiv ]).
  Qed.
(* iris/base_logic/lib/saved_prop.v *)
Instance saved_pred_discarded_persistent γ Φ :
    Persistent (γ ↪PRED□ Φ).
Proof. apply _. Qed.
(* iris/base_logic/lib/saved_prop.v *)
Instance saved_pred_fractional γ Φ : Fractional (λ q, γ ↪PRED{#q} Φ).
Proof. apply _. Qed.
(* iris/base_logic/lib/saved_prop.v *)
Instance saved_pred_as_fractional γ Φ q :
    AsFractional (γ ↪PRED{#q} Φ) (λ q, γ ↪PRED{#q} Φ) q.
Proof. apply _. Qed.
(* iris/base_logic/lib/saved_prop.v *)
(* Allocation *)
Lemma saved_pred_alloc_strong (I : gname → Prop) Φ dq :
    ✓ dq →
    pred_infinite I →
    ⊢ |==> ∃ γ, ⌜I γ⌝ ∗ γ ↪PRED{dq} Φ.
Proof. intros ??. by apply saved_anything_alloc_strong. Qed.
(* iris/base_logic/lib/saved_prop.v *)
Lemma saved_pred_alloc_cofinite (G : gset gname) Φ dq :
    ✓ dq →
    ⊢ |==> ∃ γ, ⌜γ ∉ G⌝ ∗ γ ↪PRED{dq} Φ.
Proof. by apply saved_anything_alloc_cofinite. Qed.
(* iris/base_logic/lib/saved_prop.v *)
Lemma saved_pred_alloc Φ dq :
    ✓ dq →
    ⊢ |==> ∃ γ, γ ↪PRED{dq} Φ.
Proof. apply saved_anything_alloc. Qed.
(* iris/base_logic/lib/saved_prop.v *)
(* Validity *)
Lemma saved_pred_valid γ dq Φ :
    γ ↪PRED{dq} Φ -∗ ⌜✓ dq⌝.
Proof. apply saved_anything_valid. Qed.
(* iris/base_logic/lib/saved_prop.v *)
Lemma saved_pred_valid_2 γ dq1 dq2 Φ Ψ x :
    γ ↪PRED{dq1} Φ -∗ γ ↪PRED{dq2} Ψ -∗ ⌜✓ (dq1 ⋅ dq2)⌝ ∗ ▷ (Φ x ≡ Ψ x).
Proof.
    iIntros "HΦ HΨ".
    iCombine "HΦ HΨ" gives "($ & Hag)".
    iApply later_equivI. by iApply (discrete_fun_equivI with "Hag").
  Qed.
(* iris/base_logic/lib/saved_prop.v *)
Lemma saved_pred_agree γ dq1 dq2 Φ Ψ x :
    γ ↪PRED{dq1} Φ -∗ γ ↪PRED{dq2} Ψ -∗ ▷ (Φ x ≡ Ψ x).
Proof. iIntros "HΦ HΨ". iPoseProof (saved_pred_valid_2 with "HΦ HΨ") as "[_ $]". Qed.
(* iris/base_logic/lib/saved_prop.v *)
(* Make an element read-only. *)
Lemma saved_pred_persist γ dq Φ :
    γ ↪PRED{dq} Φ ==∗ γ ↪PRED□ Φ.
Proof. apply saved_anything_persist. Qed.
(* iris/base_logic/lib/saved_prop.v *)
(* Recover fractional ownership for read-only element. *)
Lemma saved_pred_unpersist γ Φ:
    γ ↪PRED□ Φ ==∗ ∃ q, γ ↪PRED{#q} Φ.
Proof. apply saved_anything_unpersist. Qed.
(* iris/base_logic/lib/saved_prop.v *)
(* Updates *)
Lemma saved_pred_update Ψ γ Φ :
    γ ↪PRED Φ ==∗ γ ↪PRED Ψ.
Proof. apply saved_anything_update. Qed.
(* iris/base_logic/lib/saved_prop.v *)
Lemma saved_pred_update_2 Ψ γ q1 q2 Φ1 Φ2 :
    (q1 + q2 = 1)%Qp →
    γ ↪PRED{#q1} Φ1 -∗ γ ↪PRED{#q2} Φ2 ==∗ γ ↪PRED{#q1} Ψ ∗ γ ↪PRED{#q2} Ψ.
Proof. apply saved_anything_update_2. Qed.
(* iris/base_logic/lib/saved_prop.v *)
Lemma saved_pred_update_halves Ψ γ Φ1 Φ2 :
    γ ↪PRED{#1/2} Φ1 -∗ γ ↪PRED{#1/2} Φ2 ==∗ γ ↪PRED{#1/2} Ψ ∗ γ ↪PRED{#1/2} Ψ.
Proof. apply saved_anything_update_halves. Qed.
(* iris/base_logic/lib/token.v *)
(* The CMRA we need. *)
Class tokenG Σ
:= TokenG {
  #[local] token_inG :: inG Σ (exclR unitO);
}.
(* iris/base_logic/lib/token.v *)
Definition tokenΣ : gFunctors
:=
  #[ GFunctor (exclR unitO) ].
(* iris/base_logic/lib/token.v *)
Instance subG_tokenΣ Σ : subG tokenΣ Σ → tokenG Σ.
Proof. solve_inG. Qed.
(* iris/base_logic/lib/token.v *)
Definition token_def `{!tokenG Σ} (γ : gname) : iProp Σ
:=
  own γ (Excl ()).
(* iris/base_logic/lib/token.v *)
Definition token_aux : seal (@token_def).
Proof. by eexists. Qed.
(* iris/base_logic/lib/token.v *)
Definition token
:= token_aux.(unseal).
(* iris/base_logic/lib/token.v *)
Definition token_unseal :
  @token = @token_def
:= token_aux.(seal_eq).
(* iris/base_logic/lib/token.v *)
Ltac unseal
:= rewrite ?token_unseal /token_def.
(* iris/base_logic/lib/token.v *)
Instance token_timeless γ : Timeless (token γ).
Proof. unseal. apply _. Qed.
(* iris/base_logic/lib/token.v *)
Lemma token_alloc_strong (P : gname → Prop) :
    pred_infinite P →
    ⊢ |==> ∃ γ, ⌜P γ⌝ ∗ token γ.
Proof. unseal. intros. iApply own_alloc_strong; done. Qed.
(* iris/base_logic/lib/token.v *)
Lemma token_alloc :
    ⊢ |==> ∃ γ, token γ.
Proof. unseal. iApply own_alloc. done. Qed.
(* iris/base_logic/lib/token.v *)
Lemma token_exclusive γ :
    token γ -∗ token γ -∗ False.
Proof.
    unseal. iIntros "Htok1 Htok2".
    iCombine "Htok1 Htok2" gives %[].
  Qed.
(* iris/base_logic/lib/token.v *)
Instance token_combine_gives γ :
    CombineSepGives (token γ) (token γ) ⌜False⌝.
Proof.
    rewrite /CombineSepGives. iIntros "[H1 H2]".
    iDestruct (token_exclusive with "H1 H2") as %[].
  Qed.
(* iris/base_logic/lib/wsat.v *)
Class wsatGpreS (Σ : gFunctors) : Set
:= WsatGpreS {
    wsatGpreS_inv : inG Σ (gmap_viewR positive (agreeR $ laterO (iPropO Σ)));
    wsatGpreS_enabled : inG Σ coPset_disjR;
    wsatGpreS_disabled : inG Σ (gset_disjR positive);
  }.
(* iris/base_logic/lib/wsat.v *)
Class wsatGS (Σ : gFunctors) : Set
:= WsatG {
    wsat_inG : wsatGpreS Σ;
    invariant_name : gname;
    enabled_name : gname;
    disabled_name : gname;
  }.
(* iris/base_logic/lib/wsat.v *)
Definition wsatΣ : gFunctors
:=
    #[GFunctor (gmap_viewRF positive (agreeRF $ laterOF idOF));
      GFunctor coPset_disjR;
      GFunctor (gset_disjR positive)].
(* iris/base_logic/lib/wsat.v *)
Instance subG_wsatΣ {Σ} : subG wsatΣ Σ → wsatGpreS Σ.
Proof. solve_inG. Qed.
(* iris/base_logic/lib/wsat.v *)
Definition invariant_unfold {Σ} (P : iProp Σ) : later (iProp Σ)
:=
  Next P.
(* iris/base_logic/lib/wsat.v *)
Definition ownI `{!wsatGS Σ} (i : positive) (P : iProp Σ) : iProp Σ
:=
  own invariant_name
    (gmap_view_frag i DfracDiscarded (to_agree $ invariant_unfold P)).
(* iris/base_logic/lib/wsat.v *)
Instance : Params (@invariant_unfold) 1
:= {}.
(* iris/base_logic/lib/wsat.v *)
Instance : Params (@ownI) 3
:= {}.
(* iris/base_logic/lib/wsat.v *)
Definition ownE `{!wsatGS Σ} (E : coPset) : iProp Σ
:=
  own enabled_name (CoPset E).
(* iris/base_logic/lib/wsat.v *)
Instance : Params (@ownE) 3
:= {}.
(* iris/base_logic/lib/wsat.v *)
Definition ownD `{!wsatGS Σ} (E : gset positive) : iProp Σ
:=
  own disabled_name (GSet E).
(* iris/base_logic/lib/wsat.v *)
Instance : Params (@ownD) 3
:= {}.
(* iris/base_logic/lib/wsat.v *)
Definition wsat `{!wsatGS Σ} : iProp Σ
:=
  locked (∃ I : gmap positive (iProp Σ),
    own invariant_name
      (gmap_view_auth (DfracOwn 1) (to_agree <$> (invariant_unfold <$> I))) ∗
    [∗ map] i ↦ Q ∈ I, ▷ Q ∗ ownD {[i]} ∨ ownE {[i]})%I.
(* iris/base_logic/lib/wsat.v *)
(* Invariants *)
Instance invariant_unfold_contractive : Contractive (@invariant_unfold Σ).
Proof. solve_contractive. Qed.
(* iris/base_logic/lib/wsat.v *)
Instance ownI_contractive i : Contractive (@ownI Σ _ i).
Proof. solve_contractive. Qed.
(* iris/base_logic/lib/wsat.v *)
Instance ownI_persistent i P : Persistent (ownI i P).
Proof. rewrite /ownI. apply _. Qed.
(* iris/base_logic/lib/wsat.v *)
Lemma ownE_empty : ⊢ |==> ownE ∅.
Proof.
  rewrite /bi_emp_valid.
  by rewrite (own_unit (coPset_disjUR) enabled_name).
Qed.
(* iris/base_logic/lib/wsat.v *)
Lemma ownE_op E1 E2 : E1 ## E2 → ownE (E1 ∪ E2) ⊣⊢ ownE E1 ∗ ownE E2.
Proof. intros. by rewrite /ownE -own_op coPset_disj_union. Qed.
(* iris/base_logic/lib/wsat.v *)
Lemma ownE_disjoint E1 E2 : ownE E1 ∗ ownE E2 ⊢ ⌜E1 ## E2⌝.
Proof. rewrite /ownE -own_op own_valid. by iIntros (?%coPset_disj_valid_op). Qed.
(* iris/base_logic/lib/wsat.v *)
Lemma ownE_op' E1 E2 : ⌜E1 ## E2⌝ ∧ ownE (E1 ∪ E2) ⊣⊢ ownE E1 ∗ ownE E2.
Proof.
  iSplit; [iIntros "[% ?]"; by iApply ownE_op|].
  iIntros "HE". iDestruct (ownE_disjoint with "HE") as %?.
  iSplit; first done. iApply ownE_op; by try iFrame.
Qed.
(* iris/base_logic/lib/wsat.v *)
Lemma ownE_singleton_twice i : ownE {[i]} ∗ ownE {[i]} ⊢ False.
Proof. rewrite ownE_disjoint. iIntros (?); set_solver. Qed.
(* iris/base_logic/lib/wsat.v *)
Lemma ownD_empty : ⊢ |==> ownD ∅.
Proof.
  rewrite /bi_emp_valid.
  by rewrite (own_unit (gset_disjUR positive) disabled_name).
Qed.
(* iris/base_logic/lib/wsat.v *)
Lemma ownD_op E1 E2 : E1 ## E2 → ownD (E1 ∪ E2) ⊣⊢ ownD E1 ∗ ownD E2.
Proof. intros. by rewrite /ownD -own_op gset_disj_union. Qed.
(* iris/base_logic/lib/wsat.v *)
Lemma ownD_disjoint E1 E2 : ownD E1 ∗ ownD E2 ⊢ ⌜E1 ## E2⌝.
Proof. rewrite /ownD -own_op own_valid. by iIntros (?%gset_disj_valid_op). Qed.
(* iris/base_logic/lib/wsat.v *)
Lemma ownD_op' E1 E2 : ⌜E1 ## E2⌝ ∧ ownD (E1 ∪ E2) ⊣⊢ ownD E1 ∗ ownD E2.
Proof.
  iSplit; [iIntros "[% ?]"; by iApply ownD_op|].
  iIntros "HE". iDestruct (ownD_disjoint with "HE") as %?.
  iSplit; first done. iApply ownD_op; by try iFrame.
Qed.
(* iris/base_logic/lib/wsat.v *)
Lemma ownD_singleton_twice i : ownD {[i]} ∗ ownD {[i]} ⊢ False.
Proof. rewrite ownD_disjoint. iIntros (?); set_solver. Qed.
(* iris/base_logic/lib/wsat.v *)
Lemma invariant_lookup (I : gmap positive (iProp Σ)) i P :
  own invariant_name (gmap_view_auth (DfracOwn 1) (to_agree <$> (invariant_unfold <$> I))) ∗
  own invariant_name (gmap_view_frag i DfracDiscarded (to_agree $ invariant_unfold P)) ⊢
  ∃ Q, ⌜I !! i = Some Q⌝ ∗ ▷ (Q ≡ P).
Proof.
  rewrite -own_op own_valid gmap_view_both_validI_total.
  iIntros "[%Q' (_& _ & HQ' & Hval & Hincl)]". rewrite !lookup_fmap.
  case: (I !! i)=> [Q|] /=; last first.
  { iDestruct "HQ'" as %?. done. }
  iDestruct "HQ'" as %[= <-]. iExists Q; iSplit; first done.
  rewrite to_agree_includedI internal_eq_sym -later_equivI. done.
Qed.
(* iris/base_logic/lib/wsat.v *)
Lemma ownI_open i P : wsat ∗ ownI i P ∗ ownE {[i]} ⊢ wsat ∗ ▷ P ∗ ownD {[i]}.
Proof.
  rewrite /ownI /wsat -!lock.
  iIntros "(Hw & Hi & HiE)". iDestruct "Hw" as (I) "[Hw HI]".
  iDestruct (invariant_lookup I i P with "[$]") as (Q ?) "#HPQ".
  iDestruct (big_sepM_delete _ _ i with "HI") as "[[[HQ $]|HiE'] HI]"; eauto.
  - iSplitR "HQ"; last by iNext; iRewrite -"HPQ".
    iExists I. iFrame "Hw". iApply (big_sepM_delete _ _ i); eauto.
    iFrame "HI"; eauto.
  - iDestruct (ownE_singleton_twice with "[$HiE $HiE']") as %[].
Qed.
(* iris/base_logic/lib/wsat.v *)
Lemma ownI_close i P : wsat ∗ ownI i P ∗ ▷ P ∗ ownD {[i]} ⊢ wsat ∗ ownE {[i]}.
Proof.
  rewrite /ownI /wsat -!lock.
  iIntros "(Hw & Hi & HP & HiD)". iDestruct "Hw" as (I) "[Hw HI]".
  iDestruct (invariant_lookup with "[$]") as (Q ?) "#HPQ".
  iDestruct (big_sepM_delete _ _ i with "HI") as "[[[HQ ?]|$] HI]"; eauto.
  - iDestruct (ownD_singleton_twice with "[$]") as %[].
  - iExists I. iFrame "Hw". iApply (big_sepM_delete _ _ i); eauto.
    iFrame "HI". iLeft. iFrame "HiD". by iNext; iRewrite "HPQ".
Qed.
(* iris/base_logic/lib/wsat.v *)
Lemma ownI_alloc φ P :
  (∀ E : gset positive, ∃ i, i ∉ E ∧ φ i) →
  wsat ∗ ▷ P ==∗ ∃ i, ⌜φ i⌝ ∗ wsat ∗ ownI i P.
Proof.
  iIntros (Hfresh) "[Hw HP]". rewrite /wsat -!lock.
  iDestruct "Hw" as (I) "[Hw HI]".
  iMod (own_unit (gset_disjUR positive) disabled_name) as "HE".
  iMod (own_updateP with "[$]") as "HE".
  { apply (gset_disj_alloc_empty_updateP_strong' (λ i, I !! i = None ∧ φ i)).
    intros E. destruct (Hfresh (E ∪ dom I))
      as (i & [? HIi%not_elem_of_dom]%not_elem_of_union & ?); eauto. }
  iDestruct "HE" as (X) "[Hi HE]"; iDestruct "Hi" as %(i & -> & HIi & ?).
  iMod (own_update with "Hw") as "[Hw HiP]".
  { eapply (gmap_view_alloc _ i DfracDiscarded (to_agree _)); [|done..].
    by rewrite /= !lookup_fmap HIi. }
  iModIntro; iExists i;  iSplit; [done|]. rewrite /ownI; iFrame "HiP".
  iExists (<[i:=P]>I); iSplitL "Hw".
  { by rewrite !fmap_insert. }
  iApply (big_sepM_insert _ I); first done.
  iFrame "HI". iLeft. by rewrite /ownD; iFrame.
Qed.
(* iris/base_logic/lib/wsat.v *)
Lemma ownI_alloc_open φ P :
  (∀ E : gset positive, ∃ i, i ∉ E ∧ φ i) →
  wsat ==∗ ∃ i, ⌜φ i⌝ ∗ (ownE {[i]} -∗ wsat) ∗ ownI i P ∗ ownD {[i]}.
Proof.
  iIntros (Hfresh) "Hw". rewrite /wsat -!lock. iDestruct "Hw" as (I) "[Hw HI]".
  iMod (own_unit (gset_disjUR positive) disabled_name) as "HD".
  iMod (own_updateP with "[$]") as "HD".
  { apply (gset_disj_alloc_empty_updateP_strong' (λ i, I !! i = None ∧ φ i)).
    intros E. destruct (Hfresh (E ∪ dom I))
      as (i & [? HIi%not_elem_of_dom]%not_elem_of_union & ?); eauto. }
  iDestruct "HD" as (X) "[Hi HD]"; iDestruct "Hi" as %(i & -> & HIi & ?).
  iMod (own_update with "Hw") as "[Hw HiP]".
  { eapply (gmap_view_alloc _ i DfracDiscarded (to_agree _)); [|done..].
    by rewrite /= !lookup_fmap HIi. }
  iModIntro; iExists i;  iSplit; [done|]. rewrite /ownI; iFrame "HiP".
  rewrite -/(ownD _). iFrame "HD".
  iIntros "HE". iExists (<[i:=P]>I); iSplitL "Hw".
  { by rewrite !fmap_insert. }
  iApply (big_sepM_insert _ I); first done.
  iFrame "HI". by iRight.
Qed.
(* iris/base_logic/lib/wsat.v *)
(* Allocation of an initial world *)
Lemma wsat_alloc `{!wsatGpreS Σ} : ⊢ |==> ∃ _ : wsatGS Σ, wsat ∗ ownE ⊤.
Proof.
  iIntros.
  iMod (own_alloc (gmap_view_auth (DfracOwn 1) ∅)) as (γI) "HI";
    first by apply gmap_view_auth_valid.
  iMod (own_alloc (CoPset ⊤)) as (γE) "HE"; first done.
  iMod (own_alloc (GSet ∅)) as (γD) "HD"; first done.
  iModIntro; iExists (WsatG _ _ γI γE γD).
  rewrite /wsat /ownE -lock; iFrame.
  iExists ∅. rewrite fmap_empty big_opM_empty. by iFrame.
Qed.
(* iris/bi/algebra.v *)
(* Force implicit argument [PROP] *)
Notation "P ⊢ Q"
:= (bi_entails (PROP:=PROP) P Q).
(* iris/bi/algebra.v *)
Notation "P ⊣⊢ Q"
:= (equiv (A:=PROP) P%I Q%I).
(* iris/bi/algebra.v *)
Notation "⊢ Q"
:= (bi_emp_valid (PROP:=PROP) Q).
(* iris/bi/algebra.v *)
Lemma ucmra_unit_validI {A : ucmra} : ⊢ ✓ (ε : A).
Proof. sbi_unfold. apply ucmra_unit_validN. Qed.
(* iris/bi/algebra.v *)
Lemma cmra_validI_op_r {A : cmra} (x y : A) : ✓ (x ⋅ y) ⊢ ✓ y.
Proof. sbi_unfold=> n. apply cmra_validN_op_r. Qed.
(* iris/bi/algebra.v *)
Lemma cmra_validI_op_l {A : cmra} (x y : A) : ✓ (x ⋅ y) ⊢ ✓ x.
Proof. sbi_unfold=> n. apply cmra_validN_op_l. Qed.
(* iris/bi/algebra.v *)
Lemma cmra_later_opI `{!CmraTotal A} (x y1 y2 : A) :
    ▷ (✓ x ∧ x ≡ y1 ⋅ y2) ⊢ ∃ z1 z2, x ≡ z1 ⋅ z2 ∧ ▷ (z1 ≡ y1) ∧ ▷ (z2 ≡ y2).
Proof.
    sbi_unfold=> -[|n].
    - intros _. exists x, (core x). by rewrite cmra_core_r.
    - intros [??].
      destruct (cmra_extend n x y1 y2) as (z1 & z2 & ? & ? & ?); [done..|].
      exists z1, z2. auto using equiv_dist.
  Qed.
(* iris/bi/algebra.v *)
Lemma cmra_morphism_validI {A B : cmra} (f : A → B) `{!CmraMorphism f} x :
    ✓ x ⊢ ✓ (f x).
Proof. sbi_unfold=> n. by apply cmra_morphism_validN. Qed.
(* iris/bi/algebra.v *)
Lemma prod_validI {A B : cmra} (x : A * B) : ✓ x ⊣⊢ ✓ x.1 ∧ ✓ x.2.
Proof. by sbi_unfold. Qed.
(* iris/bi/algebra.v *)
Lemma prod_includedI {A B : cmra} (x y : A * B) :
    x ≼ y ⊣⊢ x.1 ≼ y.1 ∧ x.2 ≼ y.2.
Proof. sbi_unfold=> n. apply prod_includedN. Qed.
(* iris/bi/algebra.v *)
Lemma option_validI {A : cmra} (mx : option A) :
    ✓ mx ⊣⊢ match mx with Some x => ✓ x | None => True end.
Proof. sbi_unfold=> n. by destruct mx. Qed.
(* iris/bi/algebra.v *)
Lemma option_includedI {A : cmra} (mx my : option A) :
    mx ≼ my ⊣⊢ match mx, my with
               | Some x, Some y => (x ≼ y) ∨ (x ≡ y)
               | None, _ => True
               | Some x, None => False
               end.
Proof.
    sbi_unfold=> n. destruct mx, my; rewrite ?option_includedN; naive_solver.
  Qed.
(* iris/bi/algebra.v *)
Lemma option_included_totalI `{!CmraTotal A} (mx my : option A) :
    mx ≼ my ⊣⊢ match mx, my with
               | Some x, Some y => x ≼ y
               | None, _ => True
               | Some x, None => False
               end.
Proof.
    sbi_unfold=> n; destruct mx, my;
      rewrite ?Some_includedN_total ?option_includedN; naive_solver.
  Qed.
(* iris/bi/algebra.v *)
Lemma Some_included_totalI `{!CmraTotal A} (x y : A) :
    Some x ≼ Some y ⊣⊢ x ≼ y.
Proof. by rewrite option_included_totalI. Qed.
(* iris/bi/algebra.v *)
Lemma discrete_fun_validI {A} {B : A → ucmra} (g : discrete_fun B) :
    ✓ g ⊣⊢ ∀ i, ✓ g i.
Proof. by sbi_unfold. Qed.
(* iris/bi/algebra.v *)
Lemma f_homom_includedI {A B : cmra} (x y : A) (f : A → B) `{!NonExpansive f} :
    (* This is a slightly weaker condition than being a [CmraMorphism] *)
    (∀ c, f x ⋅ f c ≡ f (x ⋅ c)) →
    (x ≼ y ⊢ f x ≼ f y).
Proof. intros Hf. sbi_unfold=> n. intros [z ->]. rewrite -Hf. by eexists. Qed.
(* iris/bi/algebra.v *)
(* Analogues of [id_freeN_l] and [id_freeN_r] in the logic, stated in a way
    that allows us to do [iDestruct (id_freeI_r with "H✓ H≡") as %[]] *)
Lemma id_freeI_r {A : cmra} (x y : A) :
    IdFree x → ⊢@{PROP} ✓ x -∗ (x ⋅ y) ≡ x -∗ False.
Proof. intros. sbi_unfold. eauto using id_freeN_r. Qed.
(* iris/bi/algebra.v *)
Lemma id_freeI_l {A : cmra} (x y : A) :
    IdFree x → ⊢ ✓ x -∗ (y ⋅ x) ≡ x -∗ False.
Proof. intros. sbi_unfold. eauto using id_freeN_l. Qed.
(* iris/bi/algebra.v *)
Lemma gmap_equivI m1 m2 : m1 ≡ m2 ⊣⊢ ∀ i, m1 !! i ≡ m2 !! i.
Proof. by sbi_unfold. Qed.
(* iris/bi/algebra.v *)
Lemma gmap_union_equiv_eqI m m1 m2 :
      m ≡ m1 ∪ m2 ⊣⊢ ∃ m1' m2', ⌜ m = m1' ∪ m2' ⌝ ∧ m1' ≡ m1 ∧ m2' ≡ m2.
Proof. sbi_unfold=> n. apply gmap_union_dist_eq. Qed.
(* iris/bi/algebra.v *)
Lemma gmap_validI m : ✓ m ⊣⊢ ∀ i, ✓ (m !! i).
Proof. by sbi_unfold. Qed.
(* iris/bi/algebra.v *)
Lemma singleton_validI i x : ✓ ({[ i := x ]} : gmap K A) ⊣⊢ ✓ x.
Proof. sbi_unfold=> n. apply singleton_validN. Qed.
(* iris/bi/algebra.v *)
Lemma list_equivI l1 l2 : l1 ≡ l2 ⊣⊢ ∀ i, l1 !! i ≡ l2 !! i.
Proof. sbi_unfold. intros n. apply list_dist_lookup. Qed.
(* iris/bi/algebra.v *)
Lemma excl_equivI x y :
      x ≡ y ⊣⊢ match x, y with
                          | Excl a, Excl b => a ≡ b
                          | ExclInvalid, ExclInvalid => True
                          | _, _ => False
                          end.
Proof.
      sbi_unfold; split; [by destruct 1|destruct x, y; by repeat constructor].
    Qed.
(* iris/bi/algebra.v *)
Lemma excl_validI x :
      ✓ x ⊣⊢ if x is ExclInvalid then False else True.
Proof. by sbi_unfold. Qed.
(* iris/bi/algebra.v *)
Lemma excl_includedI (x y : excl A) :
      x ≼ y ⊣⊢ ⌜ y = ExclInvalid ⌝.
Proof. sbi_unfold=> n; apply excl_includedN. Qed.
(* iris/bi/algebra.v *)
Lemma agree_equivI a b : to_agree a ≡ to_agree b ⊣⊢ (a ≡ b).
Proof. sbi_unfold=> n. apply: inj_iff. Qed.
(* iris/bi/algebra.v *)
Lemma agree_op_invI x y : ✓ (x ⋅ y) ⊢ x ≡ y.
Proof. sbi_unfold=> n. apply agree_op_invN. Qed.
(* iris/bi/algebra.v *)
Lemma to_agree_validI a : ⊢ ✓ to_agree a.
Proof. by sbi_unfold. Qed.
(* iris/bi/algebra.v *)
Lemma to_agree_op_validI a b : ✓ (to_agree a ⋅ to_agree b) ⊣⊢ a ≡ b.
Proof. sbi_unfold. apply to_agree_op_validN. Qed.
(* iris/bi/algebra.v *)
Lemma to_agree_uninjI x : ✓ x ⊢ ∃ a, to_agree a ≡ x.
Proof. sbi_unfold=> n. exact: to_agree_uninjN. Qed.