phanerozoic/Coq-Iris huggingface dataset:
(* iris/base_logic/upred.v *)
Lemma bupd_ownM_updateP x (Φ : M → Prop) :
    x ~~>: Φ → uPred_ownM x ⊢ |==> ∃ y, ⌜Φ y⌝ ∧ uPred_ownM y.
Proof.
    unseal; siProp_primitive.unseal=> Hup; split=> n x2 ? [x3 Hx] k yf ??.
    destruct (Hup k (Some (x3 ⋅ yf))) as (y&?&?); simpl in *.
    { rewrite /= assoc -(dist_le _ _ _ _ Hx); auto. }
    exists (y ⋅ x3); split; first by rewrite -assoc.
    exists y; eauto using cmra_includedN_l.
  Qed.
(* iris/base_logic/upred.v *)
Lemma ownM_forall {A} (f : A → M) :
    (∀ a, uPred_ownM (f a)) ⊢ ∃ z, uPred_ownM z ∧
      (∀ a, ∃ xf, <si_pure> siProp_internal_eq z (f a ⋅ xf)).
Proof.
    unseal; siProp_primitive.unseal.
    split=> n y /= Hval Hf. exists y. split; [done|]. intros a.
    destruct (Hf a) as [xf ?]; eauto.
  Qed.
(* iris/base_logic/upred.v *)
Lemma ownM_valid (a : M) : uPred_ownM a ⊢ <si_pure> siProp_cmra_valid a.
Proof.
    unseal; siProp_primitive.unseal.
    split=> n x Hv [a' ?]; ofe_subst; eauto using cmra_validN_op_l.
  Qed.
(* iris/base_logic/lib/boxes.v *)
(* The CMRAs we need. *)
Class boxG Σ
:=
  #[local] boxG_inG :: inG Σ (prodR
    (excl_authR boolO)
    (optionR (agreeR (laterO (iPropO Σ))))).
(* iris/base_logic/lib/boxes.v *)
Definition boxΣ : gFunctors
:= #[ GFunctor (excl_authR boolO *
                                            optionRF (agreeRF (▶ ∙)) ) ].
(* iris/base_logic/lib/boxes.v *)
Instance subG_boxΣ Σ : subG boxΣ Σ → boxG Σ.
Proof. solve_inG. Qed.
(* iris/base_logic/lib/boxes.v *)
Definition slice_name
:= gname.
(* iris/base_logic/lib/boxes.v *)
Definition box_own_auth (γ : slice_name) (a : excl_authR boolO) : iProp Σ
:=
    own γ (a, None).
(* iris/base_logic/lib/boxes.v *)
Definition box_own_prop (γ : slice_name) (P : iProp Σ) : iProp Σ
:=
    own γ (ε, Some (to_agree (Next P))).
(* iris/base_logic/lib/boxes.v *)
Definition slice_inv (γ : slice_name) (P : iProp Σ) : iProp Σ
:=
    ∃ b, box_own_auth γ (●E b) ∗ if b then P else True.
(* iris/base_logic/lib/boxes.v *)
Definition slice (γ : slice_name) (P : iProp Σ) : iProp Σ
:=
    box_own_prop γ P ∗ inv N (slice_inv γ P).
(* iris/base_logic/lib/boxes.v *)
Definition box (f : gmap slice_name bool) (P : iProp Σ) : iProp Σ
:=
    tc_opaque (∃ Φ : slice_name → iProp Σ,
      ▷ (P ≡ [∗ map] γ ↦ _ ∈ f, Φ γ) ∗
      [∗ map] γ ↦ b ∈ f, box_own_auth γ (◯E b) ∗ box_own_prop γ (Φ γ) ∗
                         inv N (slice_inv γ (Φ γ)))%I.
(* iris/base_logic/lib/boxes.v *)
Instance : Params (@box_own_prop) 3
:= {}.
(* iris/base_logic/lib/boxes.v *)
Instance : Params (@slice_inv) 3
:= {}.
(* iris/base_logic/lib/boxes.v *)
Instance : Params (@slice) 5
:= {}.
(* iris/base_logic/lib/boxes.v *)
Instance : Params (@box) 5
:= {}.
(* iris/base_logic/lib/boxes.v *)
Instance box_own_prop_ne γ : NonExpansive (box_own_prop γ).
Proof. solve_proper. Qed.
(* iris/base_logic/lib/boxes.v *)
Instance box_own_prop_contractive γ : Contractive (box_own_prop γ).
Proof. solve_contractive. Qed.
(* iris/base_logic/lib/boxes.v *)
Instance box_inv_ne γ : NonExpansive (slice_inv γ).
Proof. solve_proper. Qed.
(* iris/base_logic/lib/boxes.v *)
Instance slice_ne γ : NonExpansive (slice N γ).
Proof. solve_proper. Qed.
(* iris/base_logic/lib/boxes.v *)
Instance slice_contractive γ : Contractive (slice N γ).
Proof. solve_contractive. Qed.
(* iris/base_logic/lib/boxes.v *)
Instance slice_proper γ : Proper ((≡) ==> (≡)) (slice N γ).
Proof. apply ne_proper, _. Qed.
(* iris/base_logic/lib/boxes.v *)
Instance slice_persistent γ P : Persistent (slice N γ P).
Proof. apply _. Qed.
(* iris/base_logic/lib/boxes.v *)
Instance box_contractive f : Contractive (box N f).
Proof. solve_contractive. Qed.
(* iris/base_logic/lib/boxes.v *)
Instance box_ne f : NonExpansive (box N f).
Proof. apply (contractive_ne _). Qed.
(* iris/base_logic/lib/boxes.v *)
Instance box_proper f : Proper ((≡) ==> (≡)) (box N f).
Proof. apply ne_proper, _. Qed.
(* iris/base_logic/lib/boxes.v *)
Lemma box_own_auth_agree γ b1 b2 :
  box_own_auth γ (●E b1) ∗ box_own_auth γ (◯E b2) ⊢ ⌜b1 = b2⌝.
Proof.
  rewrite /box_own_prop -own_op own_valid prod_validI /= and_elim_l.
  by iDestruct 1 as %?%excl_auth_agree_L.
Qed.
(* iris/base_logic/lib/boxes.v *)
Lemma box_own_auth_update γ b1 b2 b3 :
  box_own_auth γ (●E b1) ∗ box_own_auth γ (◯E b2)
  ==∗ box_own_auth γ (●E b3) ∗ box_own_auth γ (◯E b3).
Proof.
  rewrite /box_own_auth -!own_op. iApply own_update. apply prod_update; last done.
  apply excl_auth_update.
Qed.
(* iris/base_logic/lib/boxes.v *)
Lemma box_own_agree γ Q1 Q2 :
  box_own_prop γ Q1 ∗ box_own_prop γ Q2 ⊢ ▷ (Q1 ≡ Q2).
Proof.
  rewrite /box_own_prop -own_op own_valid prod_validI /= and_elim_r.
  by rewrite option_validI /= agree_op_invI agree_equivI later_equivI /=.
Qed.
(* iris/base_logic/lib/boxes.v *)
Lemma box_alloc : ⊢ box N ∅ True.
Proof.
  iIntros. iExists (λ _, True)%I. by rewrite !big_opM_empty.
Qed.
(* iris/base_logic/lib/boxes.v *)
Lemma slice_insert_empty E q f Q P :
  ▷?q box N f P ={E}=∗ ∃ γ, ⌜f !! γ = None⌝ ∗
    slice N γ Q ∗ ▷?q box N (<[γ:=false]> f) (Q ∗ P).
Proof.
  iDestruct 1 as (Φ) "[#HeqP Hf]".
  iMod (own_alloc_cofinite (●E false ⋅ ◯E false,
    Some (to_agree (Next Q))) (dom f))
    as (γ) "[Hdom Hγ]"; first by (split; [apply auth_both_valid_discrete|]).
  rewrite pair_split. iDestruct "Hγ" as "[[Hγ Hγ'] #HγQ]".
  iDestruct "Hdom" as % ?%not_elem_of_dom.
  iMod (inv_alloc N _ (slice_inv γ Q) with "[Hγ]") as "#Hinv".
  { iNext. iExists false; eauto. }
  iModIntro; iExists γ; repeat iSplit; auto.
  iNext. iExists (<[γ:=Q]> Φ); iSplit.
  - iNext. iRewrite "HeqP". by rewrite big_opM_fn_insert'.
  - rewrite (big_opM_fn_insert (λ _ _ P',  _ ∗ _ _ P' ∗ _ _ (_ _ P')))%I //.
    iFrame; eauto.
Qed.
(* iris/base_logic/lib/boxes.v *)
Lemma slice_delete_empty E q f P Q γ :
  ↑N ⊆ E →
  f !! γ = Some false →
  slice N γ Q -∗ ▷?q box N f P ={E}=∗ ∃ P',
    ▷?q (▷ (P ≡ (Q ∗ P')) ∗ box N (delete γ f) P').
Proof.
  iIntros (??) "[#HγQ Hinv] H". iDestruct "H" as (Φ) "[#HeqP Hf]".
  iExists ([∗ map] γ'↦_ ∈ delete γ f, Φ γ')%I.
  iInv N as (b) "[>Hγ _]".
  iDestruct (big_sepM_delete _ f _ false with "Hf")
    as "[[>Hγ' #[HγΦ ?]] ?]"; first done.
  iDestruct (box_own_auth_agree γ b false with "[-]") as %->; first by iFrame.
  iModIntro. iSplitL "Hγ"; first iExists false; eauto.
  iModIntro. iNext. iSplit.
  - iDestruct (box_own_agree γ Q (Φ γ) with "[#]") as "HeqQ"; first by eauto.
    iNext. iRewrite "HeqP". iRewrite "HeqQ". by rewrite -big_opM_delete.
  - iExists Φ; eauto.
Qed.
(* iris/base_logic/lib/boxes.v *)
Lemma slice_fill E q f γ P Q :
  ↑N ⊆ E →
  f !! γ = Some false →
  slice N γ Q -∗ ▷ Q -∗ ▷?q box N f P ={E}=∗ ▷?q box N (<[γ:=true]> f) P.
Proof.
  iIntros (??) "#[HγQ Hinv] HQ H"; iDestruct "H" as (Φ) "[#HeqP Hf]".
  iInv N as (b') "[>Hγ _]".
  iDestruct (big_sepM_delete _ f _ false with "Hf")
    as "[[>Hγ' #[HγΦ Hinv']] ?]"; first done.
  iMod (box_own_auth_update γ b' false true with "[$Hγ $Hγ']") as "[Hγ Hγ']".
  iModIntro. iSplitL "Hγ HQ"; first (iNext; iExists true; by iFrame).
  iModIntro; iNext; iExists Φ; iSplit.
  - by rewrite big_opM_insert_override.
  - rewrite -insert_delete_eq big_opM_insert ?lookup_delete_eq //.
    iFrame; eauto.
Qed.
(* iris/base_logic/lib/boxes.v *)
Lemma slice_empty E q f P Q γ :
  ↑N ⊆ E →
  f !! γ = Some true →
  slice N γ Q -∗ ▷?q box N f P ={E}=∗ ▷ Q ∗ ▷?q box N (<[γ:=false]> f) P.
Proof.
  iIntros (??) "#[HγQ Hinv] H"; iDestruct "H" as (Φ) "[#HeqP Hf]".
  iInv N as (b) "[>Hγ HQ]".
  iDestruct (big_sepM_delete _ f with "Hf")
    as "[[>Hγ' #[HγΦ Hinv']] ?]"; first done.
  iDestruct (box_own_auth_agree γ b true with "[-]") as %->; first by iFrame.
  iFrame "HQ".
  iMod (box_own_auth_update γ with "[$Hγ $Hγ']") as "[Hγ Hγ']".
  iModIntro. iSplitL "Hγ"; first (iNext; iExists false; by repeat iSplit).
  iModIntro; iNext; iExists Φ; iSplit.
  - by rewrite big_opM_insert_override.
  - rewrite -insert_delete_eq big_opM_insert ?lookup_delete_eq //.
    iFrame; eauto.
Qed.
(* iris/base_logic/lib/boxes.v *)
Lemma slice_insert_full E q f P Q :
  ↑N ⊆ E →
  ▷ Q -∗ ▷?q box N f P ={E}=∗ ∃ γ, ⌜f !! γ = None⌝ ∗
    slice N γ Q ∗ ▷?q box N (<[γ:=true]> f) (Q ∗ P).
Proof.
  iIntros (?) "HQ Hbox".
  iMod (slice_insert_empty with "Hbox") as (γ ?) "[#Hslice Hbox]".
  iExists γ. iFrame "%#". iMod (slice_fill with "Hslice HQ Hbox"); first done.
  - by apply lookup_insert_eq.
  - by rewrite insert_insert_eq.
Qed.
(* iris/base_logic/lib/boxes.v *)
Lemma slice_delete_full E q f P Q γ :
  ↑N ⊆ E →
  f !! γ = Some true →
  slice N γ Q -∗ ▷?q box N f P ={E}=∗
  ∃ P', ▷ Q ∗ ▷?q ▷ (P ≡ (Q ∗ P')) ∗ ▷?q box N (delete γ f) P'.
Proof.
  iIntros (??) "#Hslice Hbox".
  iMod (slice_empty with "Hslice Hbox") as "[$ Hbox]"; try done.
  iMod (slice_delete_empty with "Hslice Hbox") as (P') "[Heq Hbox]"; first done.
  { by apply lookup_insert_eq. }
  iExists P'. iFrame. rewrite -insert_delete_eq delete_insert_id ?lookup_delete_eq //.
Qed.
(* iris/base_logic/lib/boxes.v *)
Lemma box_fill E f P :
  ↑N ⊆ E →
  box N f P -∗ ▷ P ={E}=∗ box N (const true <$> f) P.
Proof.
  iIntros (?) "H HP"; iDestruct "H" as (Φ) "[#HeqP Hf]".
  iExists Φ; iSplitR; first by rewrite big_opM_fmap.
  iEval (rewrite internal_eq_iff later_iff big_sepM_later) in "HeqP".
  iDestruct ("HeqP" with "HP") as "HP".
  iCombine "Hf" "HP" as "Hf".
  rewrite -big_sepM_sep big_opM_fmap; iApply (big_sepM_fupd _ _ f).
  iApply (@big_sepM_impl with "Hf").
  iIntros "!>" (γ b' ?) "[(Hγ' & #$ & #$) HΦ]".
  iInv N as (b) "[>Hγ _]".
  iMod (box_own_auth_update γ with "[Hγ Hγ']") as "[Hγ $]"; first by iFrame.
  iModIntro. iSplitL; last done. iNext; iExists true. iFrame.
Qed.
(* iris/base_logic/lib/boxes.v *)
Lemma box_empty E f P :
  ↑N ⊆ E →
  map_Forall (λ _, (true =.)) f →
  box N f P ={E}=∗ ▷ P ∗ box N (const false <$> f) P.
Proof.
  iDestruct 1 as (Φ) "[#HeqP Hf]".
  iAssert (([∗ map] γ↦b ∈ f, ▷ Φ γ) ∗
    [∗ map] γ↦b ∈ f, box_own_auth γ (◯E false) ∗  box_own_prop γ (Φ γ) ∗
      inv N (slice_inv γ (Φ γ)))%I with "[> Hf]" as "[HΦ ?]".
  { rewrite -big_sepM_sep -big_sepM_fupd. iApply (@big_sepM_impl with "[$Hf]").
    iIntros "!>" (γ b ?) "(Hγ' & #HγΦ & #Hinv)".
    assert (true = b) as <- by eauto.
    iInv N as (b) "[>Hγ HΦ]".
    iDestruct (box_own_auth_agree γ b true with "[-]") as %->; first by iFrame.
    iMod (box_own_auth_update γ true true false with "[$Hγ $Hγ']") as "[Hγ $]".
    iModIntro. iSplitL "Hγ"; first (iNext; iExists false; iFrame; eauto).
    iFrame "HγΦ Hinv". by iApply "HΦ". }
  iModIntro; iSplitL "HΦ".
  - rewrite internal_eq_iff later_iff big_sepM_later. by iApply "HeqP".
  - iExists Φ; iSplit; by rewrite big_opM_fmap.
Qed.
(* iris/base_logic/lib/boxes.v *)
Lemma slice_iff E q f P Q Q' γ b :
  ↑N ⊆ E → f !! γ = Some b →
  ▷ □ (Q ↔ Q') -∗ slice N γ Q -∗ ▷?q box N f P ={E}=∗ ∃ γ' P',
    ⌜delete γ f !! γ' = None⌝ ∗ ▷?q ▷ □ (P ↔ P') ∗
    slice N γ' Q' ∗ ▷?q box N (<[γ' := b]>(delete γ f)) P'.
Proof.
  iIntros (??) "#HQQ' #Hs Hb". destruct b.
  - iMod (slice_delete_full with "Hs Hb") as (P') "(HQ & Heq & Hb)"; try done.
    iDestruct ("HQQ'" with "HQ") as "HQ'".
    iMod (slice_insert_full with "HQ' Hb") as (γ' ?) "[#Hs' Hb]"; try done.
    iExists γ', _. iIntros "{$∗ $# $%} !>". do 2 iNext. iRewrite "Heq".
    iIntros "!>". by iSplit; iIntros "[? $]"; iApply "HQQ'".
  - iMod (slice_delete_empty with "Hs Hb") as (P') "(Heq & Hb)"; try done.
    iMod (slice_insert_empty with "Hb") as (γ' ?) "[#Hs' Hb]"; try done.
    iExists γ', (Q' ∗ P')%I. iIntros "{$∗ $# $%} !>".  do 2 iNext. iRewrite "Heq".
    iIntros "!>". by iSplit; iIntros "[? $]"; iApply "HQQ'".
Qed.
(* iris/base_logic/lib/boxes.v *)
Lemma slice_split E q f P Q1 Q2 γ b :
  ↑N ⊆ E → f !! γ = Some b →
  slice N γ (Q1 ∗ Q2) -∗ ▷?q box N f P ={E}=∗ ∃ γ1 γ2,
    ⌜delete γ f !! γ1 = None⌝ ∗ ⌜delete γ f !! γ2 = None⌝ ∗ ⌜γ1 ≠ γ2⌝ ∗
    slice N γ1 Q1 ∗ slice N γ2 Q2 ∗ ▷?q box N (<[γ2 := b]>(<[γ1 := b]>(delete γ f))) P.
Proof.
  iIntros (??) "#Hslice Hbox". destruct b.
  - iMod (slice_delete_full with "Hslice Hbox") as (P') "([HQ1 HQ2] & Heq & Hbox)"; try done.
    iMod (slice_insert_full with "HQ1 Hbox") as (γ1 ?) "[#Hslice1 Hbox]"; first done.
    iMod (slice_insert_full with "HQ2 Hbox") as (γ2 ?) "[#Hslice2 Hbox]"; first done.
    iExists γ1, γ2. iIntros "{$% $#} !>". iSplit; last iSplit; try iPureIntro.
    { by eapply lookup_insert_None. }
    { by apply (lookup_insert_None (delete γ f) γ1 γ2 true). }
    iNext. iApply (internal_eq_rewrite_contractive _ _ (box _ _) with "[Heq] Hbox").
    iNext. iRewrite "Heq". iPureIntro. by rewrite assoc (comm _ Q2).
  - iMod (slice_delete_empty with "Hslice Hbox") as (P') "[Heq Hbox]"; try done.
    iMod (slice_insert_empty with "Hbox") as (γ1 ?) "[#Hslice1 Hbox]".
    iMod (slice_insert_empty with "Hbox") as (γ2 ?) "[#Hslice2 Hbox]".
    iExists γ1, γ2. iIntros "{$% $#} !>". iSplit; last iSplit; try iPureIntro.
    { by eapply lookup_insert_None. }
    { by apply (lookup_insert_None (delete γ f) γ1 γ2 false). }
    iNext. iApply (internal_eq_rewrite_contractive _ _ (box _ _) with "[Heq] Hbox").
    iNext. iRewrite "Heq". iPureIntro. by rewrite assoc (comm _ Q2).
Qed.
(* iris/base_logic/lib/boxes.v *)
Lemma slice_combine E q f P Q1 Q2 γ1 γ2 b :
  ↑N ⊆ E → γ1 ≠ γ2 → f !! γ1 = Some b → f !! γ2 = Some b →
  slice N γ1 Q1 -∗ slice N γ2 Q2 -∗ ▷?q box N f P ={E}=∗ ∃ γ,
    ⌜delete γ2 (delete γ1 f) !! γ = None⌝ ∗ slice N γ (Q1 ∗ Q2) ∗
    ▷?q box N (<[γ := b]>(delete γ2 (delete γ1 f))) P.
Proof.
  iIntros (????) "#Hslice1 #Hslice2 Hbox". destruct b.
  - iMod (slice_delete_full with "Hslice1 Hbox") as (P1) "(HQ1 & Heq1 & Hbox)"; try done.
    iMod (slice_delete_full with "Hslice2 Hbox") as (P2) "(HQ2 & Heq2 & Hbox)"; first done.
    { by simplify_map_eq. }
    iMod (slice_insert_full _ _ _ _ (Q1 ∗ Q2) with "[$HQ1 $HQ2] Hbox")
      as (γ ?) "[#Hslice Hbox]"; first done.
    iExists γ. iIntros "{$% $#} !>". iNext.
    iApply (internal_eq_rewrite_contractive _ _ (box _ _) with "[Heq1 Heq2] Hbox").
    iNext. iRewrite "Heq1". iRewrite "Heq2". by rewrite assoc.
  - iMod (slice_delete_empty with "Hslice1 Hbox") as (P1) "(Heq1 & Hbox)"; try done.
    iMod (slice_delete_empty with "Hslice2 Hbox") as (P2) "(Heq2 & Hbox)"; first done.
    { by simplify_map_eq. }
    iMod (slice_insert_empty with "Hbox") as (γ ?) "[#Hslice Hbox]".
    iExists γ. iIntros "{$% $#} !>". iNext.
    iApply (internal_eq_rewrite_contractive _ _ (box _ _) with "[Heq1 Heq2] Hbox").
    iNext. iRewrite "Heq1". iRewrite "Heq2". by rewrite assoc.
Qed.
(* iris/base_logic/lib/cancelable_invariants.v *)
(* This is using a pair of options to represent two pieces of ghost state (the
 * fractional invariant token and an internal exclusive token) using one ghost
 * name. The exclusive token is used to prove `cinv_acc_1`. *)
Class cinvG Σ
:= { 
  #[local] cinv_inG :: inG Σ (prodR (optionR (exclR unitO)) (optionR dfracR)) ;
}.
(* iris/base_logic/lib/cancelable_invariants.v *)
Definition cinvΣ : gFunctors
:=
  #[GFunctor (prodR (optionR (exclR unitO)) (optionR dfracR))].
(* iris/base_logic/lib/cancelable_invariants.v *)
Instance subG_cinvΣ {Σ} : subG cinvΣ Σ → cinvG Σ.
Proof. solve_inG. Qed.
(* iris/base_logic/lib/cancelable_invariants.v *)
Definition cinv_own (γ : gname) (p : frac) : iProp Σ
:=
    own γ (None, Some (DfracOwn p)).
(* iris/base_logic/lib/cancelable_invariants.v *)
Definition cinv_excl γ : iProp Σ
:= own γ (Some (Excl ()), None).
(* iris/base_logic/lib/cancelable_invariants.v *)
Definition cinv (N : namespace) (γ : gname) (P : iProp Σ) : iProp Σ
:=
    inv N (cinv_own γ 1 ∨ P ∗ cinv_excl γ).
(* iris/base_logic/lib/cancelable_invariants.v *)
Instance : Params (@cinv) 5
:= {}.
(* iris/base_logic/lib/cancelable_invariants.v *)
Instance cinv_own_timeless γ p : Timeless (cinv_own γ p).
Proof. rewrite /cinv_own; apply _. Qed.
(* iris/base_logic/lib/cancelable_invariants.v *)
Instance cinv_contractive N γ : Contractive (cinv N γ).
Proof. solve_contractive. Qed.
(* iris/base_logic/lib/cancelable_invariants.v *)
Instance cinv_ne N γ : NonExpansive (cinv N γ).
Proof. exact: contractive_ne. Qed.
(* iris/base_logic/lib/cancelable_invariants.v *)
Instance cinv_proper N γ : Proper ((≡) ==> (≡)) (cinv N γ).
Proof. exact: ne_proper. Qed.
(* iris/base_logic/lib/cancelable_invariants.v *)
Instance cinv_persistent N γ P : Persistent (cinv N γ P).
Proof. rewrite /cinv; apply _. Qed.
(* iris/base_logic/lib/cancelable_invariants.v *)
Instance cinv_own_fractional γ : Fractional (cinv_own γ).
Proof. intros ??. by rewrite /cinv_own -own_op. Qed.
(* iris/base_logic/lib/cancelable_invariants.v *)
Instance cinv_own_as_fractional γ q :
    AsFractional (cinv_own γ q) (cinv_own γ) q.
Proof. split; [done|]. apply _. Qed.
(* iris/base_logic/lib/cancelable_invariants.v *)
Lemma cinv_own_valid γ q1 q2 : cinv_own γ q1 -∗ cinv_own γ q2 -∗ ⌜q1 + q2 ≤ 1⌝%Qp.
Proof.
    rewrite bi.wand_curry -own_op own_valid.
    iIntros "%H !%". apply H.
  Qed.
(* iris/base_logic/lib/cancelable_invariants.v *)
Lemma cinv_own_excl_alloc P :
    pred_infinite P → ⊢ |==> ∃ γ, ⌜P γ⌝ ∗ cinv_excl γ ∗ cinv_own γ 1.
Proof.
    intros HP. setoid_rewrite <-own_op. apply own_alloc_strong; done.
  Qed.
(* iris/base_logic/lib/cancelable_invariants.v *)
Lemma cinv_own_1_l γ q : cinv_own γ 1 -∗ cinv_own γ q -∗ False.
Proof.
    iIntros "H1 H2".
    iDestruct (cinv_own_valid with "H1 H2") as %[]%(exclusive_l 1%Qp).
  Qed.
(* iris/base_logic/lib/cancelable_invariants.v *)
Lemma cinv_excl_excl γ : cinv_excl γ -∗ cinv_excl γ -∗ False.
Proof.
    rewrite bi.wand_curry -own_op own_valid -pair_op.
    iIntros "%H !%". apply H.
  Qed.
(* iris/base_logic/lib/cancelable_invariants.v *)
Lemma cinv_iff N γ P Q : cinv N γ P -∗ ▷ □ (P ↔ Q) -∗ cinv N γ Q.
Proof.
    iIntros "HI #HPQ". iApply (inv_iff with "HI"). iIntros "!> !>".
    iSplit; iIntros "[$|[? ?]]"; iRight; iFrame; by iApply "HPQ".
  Qed.
(* iris/base_logic/lib/cancelable_invariants.v *)
(* The "strong" variants permit any infinite [I], and choosing [P] is delayed
  until after [γ] was chosen. *)
Lemma cinv_alloc_strong (I : gname → Prop) E N :
    pred_infinite I →
    ⊢ |={E}=> ∃ γ, ⌜ I γ ⌝ ∗ cinv_own γ 1 ∗ ∀ P, ▷ P ={E}=∗ cinv N γ P.
Proof.
    iIntros (?). iMod cinv_own_excl_alloc as (γ) "[$ [Hexcl $]]"; first done.
    iIntros "!>" (P) "P". iApply inv_alloc. iRight. iFrame.
  Qed.
(* iris/base_logic/lib/cancelable_invariants.v *)
(* The "open" variants create the invariant in the open state, and delay
  having to prove [P].
  These do not imply the other variants because of the extra assumption [↑N ⊆ E]. *)
Lemma cinv_alloc_strong_open (I : gname → Prop) E N :
    pred_infinite I →
    ↑N ⊆ E →
    ⊢ |={E}=> ∃ γ, ⌜ I γ ⌝ ∗ cinv_own γ 1 ∗ ∀ P,
      |={E,E∖↑N}=> cinv N γ P ∗ (▷ P ={E∖↑N,E}=∗ True).
Proof.
    iIntros (??). iMod (cinv_own_excl_alloc I) as (γ) "[$ [Hexcl $]]"; first done.
    iIntros "!>" (P). iMod inv_alloc_open as "[$ Hclose]"; first done.
    iIntros "!> P". iApply "Hclose". iRight. iFrame.
  Qed.
(* iris/base_logic/lib/cancelable_invariants.v *)
Lemma cinv_alloc_cofinite (G : gset gname) E N :
    ⊢ |={E}=> ∃ γ, ⌜ γ ∉ G ⌝ ∗ cinv_own γ 1 ∗ ∀ P, ▷ P ={E}=∗ cinv N γ P.
Proof.
    apply cinv_alloc_strong. apply (pred_infinite_set (C:=gset gname))=> E'.
    exists (fresh (G ∪ E')). apply not_elem_of_union, is_fresh.
  Qed.
(* iris/base_logic/lib/cancelable_invariants.v *)
Lemma cinv_alloc E N P : ▷ P ={E}=∗ ∃ γ, cinv N γ P ∗ cinv_own γ 1.
Proof.
    iIntros "HP". iMod (cinv_alloc_cofinite ∅ E N) as (γ _) "[Hγ Halloc]".
    iExists γ. iFrame "Hγ". by iApply "Halloc".
  Qed.
(* iris/base_logic/lib/cancelable_invariants.v *)
Lemma cinv_alloc_open E N P :
    ↑N ⊆ E → ⊢ |={E,E∖↑N}=> ∃ γ, cinv N γ P ∗ cinv_own γ 1 ∗ (▷ P ={E∖↑N,E}=∗ True).
Proof.
    iIntros (?). iMod (cinv_alloc_strong_open (λ _, True)) as (γ) "(_ & Htok & Hmake)"; [|done|].
    { apply pred_infinite_True. }
    iMod ("Hmake" $! P) as "[Hinv Hclose]". iIntros "!>". iExists γ. iFrame.
  Qed.
(* iris/base_logic/lib/cancelable_invariants.v *)
(* If we any fraction of the invariant token, then we can open the invariant
  * atomically. *)
Lemma cinv_acc_strong E N γ p P :
    ↑N ⊆ E →
    cinv N γ P -∗ (cinv_own γ p ={E,E∖↑N}=∗
    ▷ P ∗ cinv_own γ p ∗ (∀ E' : coPset, ▷ P ∨ cinv_own γ 1 ={E',↑N ∪ E'}=∗ True)).
Proof.
    iIntros (?) "Hinv Hown".
    iMod (inv_acc_strong with "Hinv") as "[[>Hown'|[$ >Hexcl]] H]"; first done.
    { iDestruct (cinv_own_1_l with "Hown' Hown") as %[]. }
    iIntros "{$Hown} !>" (E') "[P|Hown]"; iApply "H"; eauto with iFrame.
  Qed.
(* iris/base_logic/lib/cancelable_invariants.v *)
Lemma cinv_acc E N γ p P :
    ↑N ⊆ E →
    cinv N γ P -∗ cinv_own γ p ={E,E∖↑N}=∗ ▷ P ∗ cinv_own γ p ∗ (▷ P ={E∖↑N,E}=∗ True).
Proof.
    iIntros (?) "#Hinv Hγ".
    iMod (cinv_acc_strong with "Hinv Hγ") as "($ & $ & H)"; first done.
    iIntros "!> HP".
    iMod ("H" with "[$HP]") as "_".
    rewrite -union_difference_L //.
  Qed.
(* iris/base_logic/lib/cancelable_invariants.v *)
(* If we temporarily give up the invariant token at fraction 1, then we can
   * open the invariant non-atomically. *)
Lemma cinv_acc_1 E N γ P :
    ↑N ⊆ E →
    cinv N γ P -∗ 
    cinv_own γ 1 ={E}=∗ 
    ▷ P ∗ (∀ E', ⌜↑N ⊆ E'⌝ -∗ ▷P ={E'}=∗ cinv_own γ 1).
Proof.
    iIntros (?) "#Hinv Hγ".
    iInv "Hinv" as "[>Hγ'|[$ >Hexcl]]" "Hclose".
    { iDestruct (cinv_own_1_l with "Hγ Hγ'") as %[]. }
    iMod ("Hclose" with "[$Hγ]") as "_". iIntros "!>" (E' HE') "HP".
    iInv "Hinv" as "[>$|[_ >Hexcl']]" "Hclose".
    - iApply "Hclose". eauto with iFrame.
    - iDestruct (cinv_excl_excl with "Hexcl Hexcl'") as %[].
  Qed.
(* iris/base_logic/lib/cancelable_invariants.v *)
(* Other *)
Lemma cinv_cancel E N γ P :
    ↑N ⊆ E → cinv N γ P -∗ cinv_own γ 1 ={E}=∗ ▷ P.
Proof.
    iIntros (?) "#Hinv Hγ".
    by iDestruct (cinv_acc_1 with "[$] [$]") as "[$ _]".
  Qed.
(* iris/base_logic/lib/cancelable_invariants.v *)
Lemma cinv_inv N γ q P :
    cinv N γ P -∗ cinv_own γ q ==∗ inv N P.
Proof.
    iIntros "#Hinv Htok".
    iAssert (own γ (None, Some DfracDiscarded)) with "[> Htok]" as "#Htok".
    { iApply (own_update with "Htok").
      apply prod_update; simpl; first done.
      apply option_update.
      apply dfrac_discard_update. }
    iModIntro. iApply (inv_alter with "Hinv").
    iIntros "!> !> [Htok2|[$ Hexcl]]".
    { iExFalso. iCombine "Htok Htok2" gives %[_ ?]. done. }
    iIntros "HP". iRight. by iFrame.
  Qed.
(* iris/base_logic/lib/cancelable_invariants.v *)
Instance into_inv_cinv N γ P : IntoInv (cinv N γ P) N
:= {}.
(* iris/base_logic/lib/cancelable_invariants.v *)
Instance into_acc_cinv E N γ P p :
    IntoAcc (X:=unit) (cinv N γ P)
            (↑N ⊆ E) (cinv_own γ p) (fupd E (E∖↑N)) (fupd (E∖↑N) E)
            (λ _, ▷ P ∗ cinv_own γ p)%I (λ _, ▷ P)%I (λ _, None)%I.
Proof.
    rewrite /IntoAcc /accessor bi.exist_unit -assoc.
    iIntros (?) "#Hinv Hown". by iApply cinv_acc.
  Qed.
(* iris/base_logic/lib/fancy_updates.v *)
(* The definition of fancy updates (and in turn the logic built on top of it)
is parameterized by whether it supports elimination of laters via later credits
or not. This choice is necessary as the fancy update *with* later credits does
*not* support the interaction laws with the plainly modality in [BiFUpdPlainly].
While these laws are seldomly used, support for them is required for backwards
compatibility. More precisely:

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

The [invGS_gen] typeclass ("gen" for "generalized") is parameterized by a
parameter of type [has_lc] that determines whether later credits are available
or not. [invGS] is provided as a convenient notation for the default [HasLc].
We don't use that notation in this file to avoid confusion. *)
Class invGpreS (Σ : gFunctors) : Set
:= InvGpreS {
  #[local] invGpreS_wsat :: wsatGpreS Σ;
  #[local] invGpreS_lc :: lcGpreS Σ;
}.