phanerozoic/Coq-Iris huggingface dataset:
(* iris/base_logic/lib/own.v *)
(* TODO: This also holds if we just have ✓ a at the current step-idx, as Iris
   assertion. However, the map_updateP_alloc does not suffice to show this. *)
Lemma own_alloc_strong_dep (f : gname → A) (P : gname → Prop) :
  pred_infinite P →
  (∀ γ, P γ → ✓ (f γ)) →
  ⊢ |==> ∃ γ, ⌜P γ⌝ ∗ own γ (f γ).
Proof.
  intros HPinf Hf.
  rewrite -(bupd_mono (∃ m, ⌜∃ γ, P γ ∧ m = iRes_singleton γ (f γ)⌝ ∧ uPred_ownM m)%I).
  - rewrite /bi_emp_valid (ownM_unit emp).
    apply bupd_ownM_updateP, (discrete_fun_singleton_updateP_empty _ (λ m, ∃ γ,
      m = {[ γ := inG_unfold (cmra_transport inG_prf (f γ)) ]} ∧ P γ));
      [|naive_solver].
    apply (alloc_updateP_strong_dep _ P _ (λ γ,
      inG_unfold (cmra_transport inG_prf (f γ)))); [done| |naive_solver].
    intros γ _ ?.
    by apply (cmra_morphism_valid inG_unfold), cmra_transport_valid, Hf.
  - apply exist_elim=>m; apply pure_elim_l=>-[γ [Hfresh ->]].
    by rewrite !own_eq /own_def -(exist_intro γ) pure_True // left_id.
Qed.
(* iris/base_logic/lib/own.v *)
Lemma own_alloc_cofinite_dep (f : gname → A) (G : gset gname) :
  (∀ γ, γ ∉ G → ✓ (f γ)) → ⊢ |==> ∃ γ, ⌜γ ∉ G⌝ ∗ own γ (f γ).
Proof.
  intros Ha.
  apply (own_alloc_strong_dep f (λ γ, γ ∉ G))=> //.
  apply (pred_infinite_set (C:=gset gname)).
  intros E. set (γ := fresh (G ∪ E)).
  exists γ. apply not_elem_of_union, is_fresh.
Qed.
(* iris/base_logic/lib/own.v *)
Lemma own_alloc_dep (f : gname → A) :
  (∀ γ, ✓ (f γ)) → ⊢ |==> ∃ γ, own γ (f γ).
Proof.
  intros Ha. rewrite /bi_emp_valid (own_alloc_cofinite_dep f ∅) //; [].
  apply bupd_mono, exist_mono=>?. apply: sep_elim_r.
Qed.
(* iris/base_logic/lib/own.v *)
Lemma own_alloc_strong a (P : gname → Prop) :
  pred_infinite P →
  ✓ a → ⊢ |==> ∃ γ, ⌜P γ⌝ ∗ own γ a.
Proof. intros HP Ha. eapply (own_alloc_strong_dep (λ _, a)); eauto. Qed.
(* iris/base_logic/lib/own.v *)
Lemma own_alloc_cofinite a (G : gset gname) :
  ✓ a → ⊢ |==> ∃ γ, ⌜γ ∉ G⌝ ∗ own γ a.
Proof. intros Ha. eapply (own_alloc_cofinite_dep (λ _, a)); eauto. Qed.
(* iris/base_logic/lib/own.v *)
Lemma own_alloc a : ✓ a → ⊢ |==> ∃ γ, own γ a.
Proof. intros Ha. eapply (own_alloc_dep (λ _, a)); eauto. Qed.
(* iris/base_logic/lib/own.v *)
(* ** Frame preserving updates *)
Lemma own_updateP P γ a : a ~~>: P → own γ a ⊢ |==> ∃ a', ⌜P a'⌝ ∗ own γ a'.
Proof.
  intros Hupd. rewrite !own_eq.
  rewrite -(bupd_mono (∃ m,
    ⌜ ∃ a', m = iRes_singleton γ a' ∧ P a' ⌝ ∧ uPred_ownM m)%I).
  - apply bupd_ownM_updateP, (discrete_fun_singleton_updateP _ (λ m, ∃ x,
      m = {[ γ := x ]} ∧ ∃ x',
      x = inG_unfold x' ∧ ∃ a',
      x' = cmra_transport inG_prf a' ∧ P a')); [|naive_solver].
    apply singleton_updateP', (iso_cmra_updateP' inG_fold).
    { apply inG_unfold_fold. }
    { apply (cmra_morphism_op _). }
    { apply inG_unfold_validN. }
    by apply cmra_transport_updateP'.
  - apply exist_elim=> m; apply pure_elim_l=> -[a' [-> HP]].
    rewrite -(exist_intro a'). rewrite -persistent_and_sep.
    by apply and_intro; [apply pure_intro|].
Qed.
(* iris/base_logic/lib/own.v *)
Lemma own_update γ a a' : a ~~> a' → own γ a ⊢ |==> own γ a'.
Proof.
  intros. iIntros "?".
  iMod (own_updateP (a' =.) with "[$]") as (a'') "[-> $]".
  { by apply cmra_update_updateP. }
  done.
Qed.
(* iris/base_logic/lib/own.v *)
Lemma own_update_2 γ a1 a2 a' :
  a1 ⋅ a2 ~~> a' → own γ a1 -∗ own γ a2 ==∗ own γ a'.
Proof. intros. apply entails_wand, wand_intro_r. rewrite -own_op. by iApply own_update. Qed.
(* iris/base_logic/lib/own.v *)
Lemma own_update_3 γ a1 a2 a3 a' :
  a1 ⋅ a2 ⋅ a3 ~~> a' → own γ a1 -∗ own γ a2 -∗ own γ a3 ==∗ own γ a'.
Proof. intros. apply entails_wand. do 2 apply wand_intro_r. rewrite -!own_op. by iApply own_update. Qed.
(* iris/base_logic/lib/own.v *)
Lemma own_unit A `{i : !inG Σ (A:ucmra)} γ : ⊢ |==> own γ (ε:A).
Proof.
  rewrite /bi_emp_valid (ownM_unit emp) !own_eq /own_def.
  apply bupd_ownM_update, discrete_fun_singleton_update_empty.
  apply (alloc_unit_singleton_update (inG_unfold (cmra_transport inG_prf ε))).
  - apply (cmra_morphism_valid _), cmra_transport_valid, ucmra_unit_valid.
  - intros x. rewrite -(inG_unfold_fold x) -(cmra_morphism_op inG_unfold).
    f_equiv. generalize (inG_fold x)=> x'.
    destruct inG_prf=> /=. by rewrite left_id.
  - done.
Qed.
(* iris/base_logic/lib/own.v *)
Instance own_cmra_sep_homomorphism γ :
    WeakMonoidHomomorphism op uPred_sep (≡) (own γ).
Proof. split; try apply _. apply own_op. Qed.
(* iris/base_logic/lib/own.v *)
Lemma big_opL_own {B} γ (f : nat → B → A) (l : list B) :
    l ≠ [] →
    own γ ([^op list] k↦x ∈ l, f k x) ⊣⊢ [∗ list] k↦x ∈ l, own γ (f k x).
Proof. apply (big_opL_commute1 _). Qed.
(* iris/base_logic/lib/own.v *)
Lemma big_opM_own `{Countable K} {B} γ (g : K → B → A) (m : gmap K B) :
    m ≠ ∅ →
    own γ ([^op map] k↦x ∈ m, g k x) ⊣⊢ [∗ map] k↦x ∈ m, own γ (g k x).
Proof. apply (big_opM_commute1 _). Qed.
(* iris/base_logic/lib/own.v *)
Lemma big_opS_own `{Countable B} γ (g : B → A) (X : gset B) :
    X ≠ ∅ →
    own γ ([^op set] x ∈ X, g x) ⊣⊢ [∗ set] x ∈ X, own γ (g x).
Proof. apply (big_opS_commute1 _). Qed.
(* iris/base_logic/lib/own.v *)
Lemma big_opMS_own `{Countable B} γ (g : B → A) (X : gmultiset B) :
    X ≠ ∅ →
    own γ ([^op mset] x ∈ X, g x) ⊣⊢ [∗ mset] x ∈ X, own γ (g x).
Proof. apply (big_opMS_commute1 _). Qed.
(* iris/base_logic/lib/own.v *)
Instance own_cmra_sep_entails_homomorphism γ :
    MonoidHomomorphism op uPred_sep (⊢) (own γ).
Proof.
    split; [split|]; try apply _.
    - intros. by rewrite own_op.
    - apply (affine _).
  Qed.
(* iris/base_logic/lib/own.v *)
Lemma big_opL_own_1 {B} γ (f : nat → B → A) (l : list B) :
    own γ ([^op list] k↦x ∈ l, f k x) ⊢ [∗ list] k↦x ∈ l, own γ (f k x).
Proof. apply (big_opL_commute _). Qed.
(* iris/base_logic/lib/own.v *)
Lemma big_opM_own_1 `{Countable K} {B} γ (g : K → B → A) (m : gmap K B) :
    own γ ([^op map] k↦x ∈ m, g k x) ⊢ [∗ map] k↦x ∈ m, own γ (g k x).
Proof. apply (big_opM_commute _). Qed.
(* iris/base_logic/lib/own.v *)
Lemma big_opS_own_1 `{Countable B} γ (g : B → A) (X : gset B) :
    own γ ([^op set] x ∈ X, g x) ⊢ [∗ set] x ∈ X, own γ (g x).
Proof. apply (big_opS_commute _). Qed.
(* iris/base_logic/lib/own.v *)
Lemma big_opMS_own_1 `{Countable B} γ (g : B → A) (X : gmultiset B) :
    own γ ([^op mset] x ∈ X, g x) ⊢ [∗ mset] x ∈ X, own γ (g x).
Proof. apply (big_opMS_commute _). Qed.
(* iris/base_logic/lib/own.v *)
Instance into_sep_own γ a b1 b2 :
    IsOp a b1 b2 → IntoSep (own γ a) (own γ b1) (own γ b2).
Proof. intros. by rewrite /IntoSep (is_op a) own_op. Qed.
(* iris/base_logic/lib/own.v *)
Instance into_and_own p γ a b1 b2 :
    IsOp a b1 b2 → IntoAnd p (own γ a) (own γ b1) (own γ b2).
Proof. intros. by rewrite /IntoAnd (is_op a) own_op sep_and. Qed.
(* iris/base_logic/lib/own.v *)
Instance from_sep_own γ a b1 b2 :
    IsOp a b1 b2 → FromSep (own γ a) (own γ b1) (own γ b2).
Proof. intros. by rewrite /FromSep -own_op -is_op. Qed.
(* iris/base_logic/lib/own.v *)
(* Cost > 50 to give priority to [combine_sep_as_fractional]. *)
Instance combine_sep_as_own γ a b1 b2 :
    IsOp a b1 b2 → CombineSepAs (own γ b1) (own γ b2) (own γ a) | 60.
Proof. intros. by rewrite /CombineSepAs -own_op -is_op. Qed.
(* iris/base_logic/lib/own.v *)
(* TODO: Improve this instance with generic own validity simplification
  machinery once https://gitlab.mpi-sws.org/iris/iris/-/issues/460 is fixed *)
Instance combine_sep_gives_own γ b1 b2 :
    CombineSepGives (own γ b1) (own γ b2) (✓ (b1 ⋅ b2)).
Proof.
    intros. rewrite /CombineSepGives -own_op own_valid.
    by apply: bi.persistently_intro.
  Qed.
(* iris/base_logic/lib/own.v *)
Instance from_and_own_persistent γ a b1 b2 :
    IsOp a b1 b2 → TCOr (CoreId b1) (CoreId b2) →
    FromAnd (own γ a) (own γ b1) (own γ b2).
Proof.
    intros ? Hb. rewrite /FromAnd (is_op a) own_op.
    destruct Hb; by rewrite persistent_and_sep.
  Qed.
(* iris/base_logic/lib/own.v *)
(* Our main goal in this section is to prove [own_forall]:

    (∀ b, own γ (f b)) ⊢ ∃ c : A, own γ c ∗ (∀ b, Some (f b) ≼ Some c)

  We have the analogue in the global ucmra, from [ownM_forall]:

    (∀ a, uPred_ownM (f a)) ⊢ ∃ z : iRes Σ, uPred_ownM z ∧ (∀ a, f a ≼ z)

  We need to relate [uPred_ownM (iRes_singleton γ _)] to [own γ _] so that we
  can bring this theorem from the global ucmra world to the [A] world.
  In particular, [ownM_forall] gives us some [z] in the ucmra world, but to prove
  the theorem in the end, we need to supply a witness [z'] in the [A] world.
  We start by defining the [iRes_project] function to map from the ucmra world
  to the [A] world, basically an inverse of [iRes_singleton]: *)
Definition iRes_project (γ : gname) (x : iResUR Σ) : option A
:=
    cmra_transport (eq_sym inG_prf) ∘ inG_fold <$> x (inG_id i) !! γ.
(* iris/base_logic/lib/own.v *)
(* Now we prove some properties about [iRes_project] *)
Lemma iRes_project_op γ x y :
    iRes_project γ (x ⋅ y) ≡@{option A} iRes_project γ x ⋅ iRes_project γ y.
Proof.
    rewrite /iRes_project lookup_op.
    case: (x (inG_id i) !! γ)=> [x1|]; case: (y (inG_id i) !! γ)=> [y1|] //=.
    rewrite -Some_op -cmra_transport_op. do 2 f_equiv. apply: cmra_morphism_op.
  Qed.
(* iris/base_logic/lib/own.v *)
Instance iRes_project_ne γ : NonExpansive (iRes_project γ).
Proof. intros n x1 x2 Hx. rewrite /iRes_project. do 2 f_equiv. apply Hx. Qed.
(* iris/base_logic/lib/own.v *)
Lemma iRes_project_singleton γ a :
    iRes_project γ (iRes_singleton γ a) ≡ Some a.
Proof.
    rewrite /iRes_project /iRes_singleton discrete_fun_lookup_singleton.
    rewrite lookup_singleton_eq /= inG_fold_unfold.
    by rewrite cmra_transport_trans eq_trans_sym_inv_r.
  Qed.
(* iris/base_logic/lib/own.v *)
(* The singleton result [c] of [iRes_project γ z] is below [z] *)
Lemma iRes_project_below γ z c :
    iRes_project γ z = Some c → iRes_singleton γ c ≼ z.
Proof.
    rewrite /iRes_project /iRes_singleton fmap_Some.
    intros (a' & Hγ & ->). rewrite cmra_transport_trans eq_trans_sym_inv_l /=.
    exists (discrete_fun_insert (inG_id i) (delete γ (z (inG_id i))) z).
    intros j. rewrite discrete_fun_lookup_op.
    destruct (decide (j = inG_id i)) as [->|]; last first.
    { rewrite discrete_fun_lookup_singleton_ne //.
      rewrite discrete_fun_lookup_insert_ne //. by rewrite left_id. }
    rewrite discrete_fun_lookup_singleton discrete_fun_lookup_insert.
    intros γ'. rewrite lookup_op. destruct (decide (γ' = γ)) as [->|].
    - by rewrite lookup_singleton_eq lookup_delete_eq Hγ inG_unfold_fold.
    - by rewrite lookup_singleton_ne // lookup_delete_ne // left_id.
  Qed.
(* iris/base_logic/lib/own.v *)
(* If another singleton [c] is below [z], [iRes_project] is above [c]. *)
Lemma iRes_project_above γ z c :
    iRes_singleton γ c ≼ z ⊢@{iProp Σ} Some c ≼ iRes_project γ z.
Proof.
    iIntros "#[%x Hincl]". iExists (iRes_project γ x).
    rewrite -(iRes_project_singleton γ) -iRes_project_op.
    by iRewrite "Hincl".
  Qed.
(* iris/base_logic/lib/own.v *)
(* Finally we tie it all together.
  As usual, we use [Some a ≼ Some c] for the reflexive closure of [a ≼ c]. *)
Lemma own_forall `{!Inhabited B} γ (f : B → A) :
    (∀ b, own γ (f b)) ⊢ ∃ c, own γ c ∗ (∀ b, Some (f b) ≼ Some c).
Proof.
    rewrite own_eq /own_def. iIntros "Hown".
    iDestruct (ownM_forall with "Hown") as (z) "[Hown Hincl]".
    destruct (iRes_project γ z) as [c|] eqn:Hc.
    - iExists c. iSplitL "Hown".
      { iApply (ownM_mono with "Hown"). by apply iRes_project_below. }
      iIntros (b). rewrite -Hc. by iApply iRes_project_above.
    - iDestruct ("Hincl" $! inhabitant) as "Hincl".
      iDestruct (iRes_project_above with "Hincl") as "Hincl".
      rewrite Hc. iDestruct "Hincl" as (mx) "H".
      rewrite option_equivI. by destruct mx.
  Qed.
(* iris/base_logic/lib/own.v *)
(* Now some corollaries. *)
Lemma own_forall_total `{!CmraTotal A, !Inhabited B} γ (f : B → A) :
    (∀ b, own γ (f b)) ⊢ ∃ c, own γ c ∗ (∀ b, f b ≼ c).
Proof. setoid_rewrite <-Some_included_totalI. apply own_forall. Qed.
(* iris/base_logic/lib/own.v *)
Lemma own_and γ a1 a2 :
    own γ a1 ∧ own γ a2 ⊢ ∃ c, own γ c ∗ Some a1 ≼ Some c ∗ Some a2 ≼ Some c.
Proof.
    iIntros "Hown". iDestruct (own_forall γ (λ b, if b : bool then a1 else a2)
      with "[Hown]") as (c) "[$ Hincl]".
    { rewrite and_alt.
      iIntros ([]); [iApply ("Hown" $! true)|iApply ("Hown" $! false)]. }
    iSplit; [iApply ("Hincl" $! true)|iApply ("Hincl" $! false)].
  Qed.
(* iris/base_logic/lib/own.v *)
Lemma own_and_total `{!CmraTotal A} γ a1 a2 :
    own γ a1 ∧ own γ a2 ⊢ ∃ c, own γ c ∗ a1 ≼ c ∗ a2 ≼ c.
Proof. setoid_rewrite <-Some_included_totalI. apply own_and. Qed.
(* iris/base_logic/lib/own.v *)
(* A version of [own_forall] for bounded quantification. Here [φ : B → Prop]
  is a pure predicate that restricts the elements of [B]. *)
Lemma own_forall_pred {B} γ (φ : B → Prop) (f : B → A) :
    (∃ b, φ b) → (* [φ] is non-empty *)
    (∀ b, ⌜ φ b ⌝ -∗ own γ (f b)) ⊢
    ∃ c, own γ c ∗ (∀ b, ⌜ φ b ⌝ -∗ Some (f b) ≼ Some c).
Proof.
    iIntros ([b0 pb0]) "Hown".
    iAssert (∀ b : { b | φ b }, own γ (f (`b)))%I with "[Hown]" as "Hown".
    { iIntros ([b pb]). by iApply ("Hown" $! b). }
    iDestruct (@own_forall _ with "Hown") as (c) "[$ Hincl]".
    { split. apply (b0 ↾ pb0). }
    iIntros (b pb). iApply ("Hincl" $! (b ↾ pb)).
  Qed.
(* iris/base_logic/lib/own.v *)
Lemma own_forall_pred_total `{!CmraTotal A} {B} γ (φ : B → Prop) (f : B → A) :
    (∃ b, φ b) →
    (∀ b, ⌜ φ b ⌝ -∗ own γ (f b)) ⊢ ∃ c, own γ c ∗ (∀ b, ⌜ φ b ⌝ -∗ f b ≼ c).
Proof. setoid_rewrite <-Some_included_totalI. apply own_forall_pred. Qed.
(* iris/base_logic/lib/own.v *)
Lemma own_and_discrete_total `{!CmraDiscrete A, !CmraTotal A} γ a1 a2 c :
    (∀ c', ✓ c' → a1 ≼ c' → a2 ≼ c' → c ≼ c') →
    own γ a1 ∧ own γ a2 ⊢ own γ c.
Proof.
    iIntros (Hvalid) "Hown".
    iDestruct (own_and_total with "Hown") as (c') "[Hown [%Ha1 %Ha2]]".
    iDestruct (own_valid with "Hown") as %?.
    iApply (own_mono with "Hown"); eauto.
  Qed.
(* iris/base_logic/lib/own.v *)
Lemma own_and_discrete_total_False `{!CmraDiscrete A, !CmraTotal A} γ a1 a2 :
    (∀ c', ✓ c' → a1 ≼ c' → a2 ≼ c' → False) →
    own γ a1 ∧ own γ a2 ⊢ False.
Proof.
    iIntros (Hvalid) "Hown".
    iDestruct (own_and_total with "Hown") as (c) "[Hown [%Ha1 %Ha2]]".
    iDestruct (own_valid with "Hown") as %?; eauto.
  Qed.
(* iris/base_logic/lib/proph_map.v *)
Notation proph_map P V
:= (gmap P (list V)).
(* iris/base_logic/lib/proph_map.v *)
Definition proph_val_list (P V : Type)
:= list (P * V).
(* iris/base_logic/lib/proph_map.v *)
(* The CMRA we need. *)
Class proph_mapGpreS (P V : Type) (Σ : gFunctors) `{Countable P}
:= {
  #[local] proph_map_GpreS_inG :: ghost_mapG Σ P (list V)
}.
(* iris/base_logic/lib/proph_map.v *)
Class proph_mapGS (P V : Type) (Σ : gFunctors) `{Countable P}
:= ProphMapGS {
  #[local] proph_map_inG :: proph_mapGpreS P V Σ;
  proph_map_name : gname
}.
(* iris/base_logic/lib/proph_map.v *)
Definition proph_mapΣ (P V : Type) `{Countable P} : gFunctors
:=
  #[ghost_mapΣ P (list V)].
(* iris/base_logic/lib/proph_map.v *)
Instance subG_proph_mapGpreS {Σ P V} `{Countable P} :
  subG (proph_mapΣ P V) Σ → proph_mapGpreS P V Σ.
Proof. solve_inG. Qed.
(* iris/base_logic/lib/proph_map.v *)
(* The list of resolves for [p] in [pvs]. *)
Fixpoint proph_list_resolves pvs p : list V
:=
    match pvs with
    | []         => []
    | (q,v)::pvs => if decide (p = q) then v :: proph_list_resolves pvs p
                    else proph_list_resolves pvs p
    end.
(* iris/base_logic/lib/proph_map.v *)
Definition proph_resolves_in_list R pvs
:=
    map_Forall (λ p vs, vs = proph_list_resolves pvs p) R.
(* iris/base_logic/lib/proph_map.v *)
Definition proph_map_interp pvs (ps : gset P) : iProp Σ
:=
    ∃ R, ⌜proph_resolves_in_list R pvs ∧
         dom R ⊆ ps⌝ ∗ proph_map_name pG ↪●MAP R.
(* iris/base_logic/lib/proph_map.v *)
Definition proph_def (p : P) (vs : list V) : iProp Σ
:=
    proph_map_name pG ↪◯MAP[p] vs.
(* iris/base_logic/lib/proph_map.v *)
Definition proph_aux : seal (@proph_def).
Proof. by eexists. Qed.
(* iris/base_logic/lib/proph_map.v *)
Definition proph
:= proph_aux.(unseal).
(* iris/base_logic/lib/proph_map.v *)
Definition proph_unseal : @proph = @proph_def
:= proph_aux.(seal_eq).
(* iris/base_logic/lib/proph_map.v *)
Lemma resolves_insert pvs p R :
    proph_resolves_in_list R pvs →
    p ∉ dom R →
    proph_resolves_in_list (<[p := proph_list_resolves pvs p]> R) pvs.
Proof.
    intros Hinlist Hp q vs HEq.
    destruct (decide (p = q)) as [->|NEq].
    - rewrite lookup_insert_eq in HEq. by inversion HEq.
    - rewrite lookup_insert_ne in HEq; last done. by apply Hinlist.
  Qed.
(* iris/base_logic/lib/proph_map.v *)
Lemma proph_map_init `{Countable P, !proph_mapGpreS P V Σ} pvs ps :
  ⊢ |==> ∃ _ : proph_mapGS P V Σ, proph_map_interp pvs ps ∗
    [∗ set] p ∈ ps, proph p (proph_list_resolves pvs p).
Proof.
  pose (R := set_to_map (proph_list_resolves pvs) ps : gmap P (list V)).
  iMod (ghost_map_alloc R) as (γ) "[Hh Hps]".
  iModIntro. iExists (ProphMapGS P V _ _ _ _ γ). iFrame "Hh". repeat iSplit.
  - by iIntros "!%" (p vs [??]%lookup_set_to_map_Some).
  - by rewrite /R dom_set_to_map.
  - by rewrite /R big_sepM_set_to_map proph_unseal.
Qed.
(* iris/base_logic/lib/proph_map.v *)
(* General properties of pointsto *)
Instance proph_timeless p vs : Timeless (proph p vs).
Proof. rewrite proph_unseal /proph_def. apply _. Qed.
(* iris/base_logic/lib/proph_map.v *)
Lemma proph_exclusive p vs1 vs2 :
    proph p vs1 -∗ proph p vs2 -∗ False.
Proof.
    rewrite proph_unseal /proph_def. iIntros "Hp1 Hp2".
    by iDestruct (ghost_map_elem_ne with "Hp1 Hp2") as %?.
  Qed.
(* iris/base_logic/lib/proph_map.v *)
Lemma proph_map_new_proph p ps pvs :
    p ∉ ps →
    proph_map_interp pvs ps ==∗
    proph_map_interp pvs ({[p]} ∪ ps) ∗ proph p (proph_list_resolves pvs p).
Proof.
    iIntros (Hp) "HR". iDestruct "HR" as (R) "[[% %] H●]".
    rewrite proph_unseal /proph_def.
    iMod (ghost_map_insert p (proph_list_resolves pvs p) with "H●") as "[H● H◯]".
    { apply not_elem_of_dom. set_solver. }
    iFrame. iPureIntro. split.
    - apply resolves_insert; first done. set_solver.
    - rewrite dom_insert_L. set_solver.
  Qed.
(* iris/base_logic/lib/proph_map.v *)
Lemma proph_map_resolve_proph p v pvs ps vs :
    proph_map_interp ((p,v) :: pvs) ps ∗ proph p vs ==∗
    ∃vs', ⌜vs = v::vs'⌝ ∗ proph_map_interp pvs ps ∗ proph p vs'.
Proof.
    iIntros "[HR Hp]". iDestruct "HR" as (R) "[HP H●]". iDestruct "HP" as %[Hres Hdom].
    rewrite /proph_map_interp proph_unseal /proph_def.
    iCombine "H● Hp" gives %HR.
    assert (vs = v :: proph_list_resolves pvs p) as ->.
    { rewrite (Hres p vs HR). simpl. by rewrite decide_True. }
    iMod (ghost_map_update (proph_list_resolves pvs p) with "H● Hp") as "[H● H◯]".
    iModIntro. iExists (proph_list_resolves pvs p). iFrame. iSplitR.
    - iPureIntro. done.
    - iPureIntro. split.
      + intros q ws HEq. destruct (decide (p = q)) as [<-|NEq].
        * rewrite lookup_insert_eq in HEq. by inversion HEq.
        * rewrite lookup_insert_ne in HEq; last done.
          rewrite (Hres q ws HEq).
          simpl. rewrite decide_False; done.
      + assert (p ∈ dom R) by exact: elem_of_dom_2.
        rewrite dom_insert_L. set_solver.
  Qed.
(* iris/base_logic/lib/proph_map.v *)
Lemma proph_map_agree pvs ps p vs :
    proph_map_interp pvs ps -∗ proph p vs -∗ ⌜p ∈ ps ∧ vs = proph_list_resolves pvs p⌝.
Proof.
    iIntros "(%R & [%Hres %Hdom] & H●) Hp".
    rewrite /proph_map_interp proph_unseal /proph_def.
    iCombine "H● Hp" gives %Hlookup.
    iPureIntro. split; last by auto.
    eapply Hdom, elem_of_dom_2. done.
  Qed.
(* iris/base_logic/lib/saved_prop.v *)
(* "Saved anything" -- this can give you saved propositions, saved predicates,
   saved whatever-you-like. *)
Class savedAnythingG (Σ : gFunctors) (F : oFunctor)
:= SavedAnythingG {
  #[local] saved_anything_inG :: inG Σ (dfrac_agreeR (oFunctor_apply F (iPropO Σ)));
  saved_anything_contractive : oFunctorContractive F (* NOT an instance to avoid cycles with [subG_savedAnythingΣ]. *)
}.
(* iris/base_logic/lib/saved_prop.v *)
Definition savedAnythingΣ (F : oFunctor) `{!oFunctorContractive F} : gFunctors
:=
  #[ GFunctor (dfrac_agreeRF F) ].
(* iris/base_logic/lib/saved_prop.v *)
Instance subG_savedAnythingΣ {Σ F} `{!oFunctorContractive F} :
  subG (savedAnythingΣ F) Σ → savedAnythingG Σ F.
Proof. solve_inG. Qed.
(* iris/base_logic/lib/saved_prop.v *)
Definition saved_anything_own `{!savedAnythingG Σ F}
    (γ : gname) (dq : dfrac) (x : oFunctor_apply F (iPropO Σ)) : iProp Σ
:=
  own γ (to_dfrac_agree dq x).
(* iris/base_logic/lib/saved_prop.v *)
Instance : Params (@saved_anything_own) 4
:= {}.
(* iris/base_logic/lib/saved_prop.v *)
Instance saved_anything_discarded_persistent γ x :
    Persistent (saved_anything_own γ DfracDiscarded x).
Proof. rewrite /saved_anything_own; apply _. Qed.
(* iris/base_logic/lib/saved_prop.v *)
Instance saved_anything_ne γ dq : NonExpansive (saved_anything_own γ dq).
Proof. solve_proper. Qed.
(* iris/base_logic/lib/saved_prop.v *)
Instance saved_anything_proper γ dq : Proper ((≡) ==> (≡)) (saved_anything_own γ dq).
Proof. solve_proper. Qed.
(* iris/base_logic/lib/saved_prop.v *)
Instance saved_anything_fractional γ x : Fractional (λ q, saved_anything_own γ (DfracOwn q) x).
Proof. intros q1 q2. rewrite /saved_anything_own -own_op -dfrac_agree_op //. Qed.
(* iris/base_logic/lib/saved_prop.v *)
Instance saved_anything_as_fractional γ x q :
    AsFractional (saved_anything_own γ (DfracOwn q) x) (λ q, saved_anything_own γ (DfracOwn q) x) q.
Proof. split; [done|]. apply _. Qed.
(* iris/base_logic/lib/saved_prop.v *)
(* Allocation *)
Lemma saved_anything_alloc_strong x (I : gname → Prop) dq :
    ✓ dq →
    pred_infinite I →
    ⊢ |==> ∃ γ, ⌜I γ⌝ ∗ saved_anything_own γ dq x.
Proof. intros ??. by apply own_alloc_strong. Qed.
(* iris/base_logic/lib/saved_prop.v *)
Lemma saved_anything_alloc_cofinite x (G : gset gname) dq :
    ✓ dq →
    ⊢ |==> ∃ γ, ⌜γ ∉ G⌝ ∗ saved_anything_own γ dq x.
Proof. intros ?. by apply own_alloc_cofinite. Qed.
(* iris/base_logic/lib/saved_prop.v *)
Lemma saved_anything_alloc x dq :
    ✓ dq →
    ⊢ |==> ∃ γ, saved_anything_own γ dq x.
Proof. intros ?. by apply own_alloc. Qed.
(* iris/base_logic/lib/saved_prop.v *)
(* Validity *)
Lemma saved_anything_valid γ dq x :
    saved_anything_own γ dq x -∗ ⌜✓ dq⌝.
Proof.
    rewrite /saved_anything_own own_valid dfrac_agree_validI //. eauto.
  Qed.
(* iris/base_logic/lib/saved_prop.v *)
Lemma saved_anything_valid_2 γ dq1 dq2 x y :
    saved_anything_own γ dq1 x -∗ saved_anything_own γ dq2 y -∗ ⌜✓ (dq1 ⋅ dq2)⌝ ∗ x ≡ y.
Proof.
    iIntros "Hx Hy". rewrite /saved_anything_own.
    iCombine "Hx Hy" gives "Hv".
    rewrite dfrac_agree_validI_2. iDestruct "Hv" as "[$ $]".
  Qed.
(* iris/base_logic/lib/saved_prop.v *)
Lemma saved_anything_agree γ dq1 dq2 x y :
    saved_anything_own γ dq1 x -∗ saved_anything_own γ dq2 y -∗ x ≡ y.
Proof. iIntros "Hx Hy". iPoseProof (saved_anything_valid_2 with "Hx Hy") as "[_ $]". Qed.
(* iris/base_logic/lib/saved_prop.v *)
Instance saved_anything_combine_gives γ dq1 dq2 x y :
    CombineSepGives (saved_anything_own γ dq1 x) (saved_anything_own γ dq2 y)
      (⌜✓ (dq1 ⋅ dq2)⌝ ∗ x ≡ y).
Proof.
    rewrite /CombineSepGives. iIntros "[Hx Hy]".
    iPoseProof (saved_anything_valid_2 with "Hx Hy") as "[% #$]". eauto.
  Qed.
(* iris/base_logic/lib/saved_prop.v *)
Instance saved_anything_combine_as γ dq1 dq2 x y :
    CombineSepAs (saved_anything_own γ dq1 x) (saved_anything_own γ dq2 y)
      (saved_anything_own γ (dq1 ⋅ dq2) x).
(* higher cost than the Fractional instance, which kicks in for #qs *)
  Proof.
    rewrite /CombineSepAs. iIntros "[Hx Hy]".
    iCombine "Hx Hy" gives "[_ #H]".
    iRewrite -"H" in "Hy". rewrite /saved_anything_own.
    iCombine "Hx Hy" as "Hxy". by rewrite -dfrac_agree_op.
  Qed.
(* iris/base_logic/lib/saved_prop.v *)
(* Make an element read-only. *)
Lemma saved_anything_persist γ dq v :
    saved_anything_own γ dq v ==∗ saved_anything_own γ DfracDiscarded v.
Proof.
    iApply own_update. apply dfrac_agree_persist.
  Qed.