phanerozoic/Coq-Iris huggingface dataset:
(* iris/algebra/view.v *)
Lemma view_update_dealloc a b a' :
    (∀ n bf, rel n a (b ⋅ bf) → rel n a' bf) →
    ●V a ⋅ ◯V b ~~> ●V a'.
Proof.
    intros Hup. rewrite -(right_id _ _ (●V a')).
    apply view_update=> n bf. rewrite left_id. apply Hup.
  Qed.
(* iris/algebra/view.v *)
Lemma view_update_auth a a' :
    (∀ n bf, rel n a bf → rel n a' bf) →
    ●V a ~~> ●V a'.
Proof.
    intros Hup. rewrite -(right_id _ _ (●V a)) -(right_id _ _ (●V a')).
    apply view_update=> n bf. rewrite !left_id. apply Hup.
  Qed.
(* iris/algebra/view.v *)
Lemma view_updateP_auth_dfrac dq P a :
    dq ~~>: P →
    ●V{dq} a ~~>: λ k, ∃ dq', k = ●V{dq'} a ∧ P dq'.
Proof.
    intros Hupd. apply cmra_total_updateP.
    move=> n [[[dq' ag]|] bf] [Hv ?].
    - destruct (Hupd n (Some dq') Hv) as (dr&Hdr&Heq).
      eexists. split; first by eexists. done.
    - destruct (Hupd n None Hv) as (dr&Hdr&Heq).
      eexists. split; first by eexists. done.
  Qed.
(* iris/algebra/view.v *)
Lemma view_update_auth_persist dq a : ●V{dq} a ~~> ●V□ a.
Proof.
    eapply (cmra_update_lift_updateP (λ dq, view_auth dq a)).
    { intros; by apply view_updateP_auth_dfrac. }
    { apply dfrac_discard_update. }
  Qed.
(* iris/algebra/view.v *)
Lemma view_updateP_auth_unpersist a : ●V□ a ~~>: λ k, ∃ q, k = ●V{#q} a.
Proof.
    eapply cmra_updateP_weaken.
    { eapply view_updateP_auth_dfrac, dfrac_undiscard_update. }
    naive_solver.
  Qed.
(* iris/algebra/view.v *)
Lemma view_updateP_both_unpersist a b : ●V□ a ⋅ ◯V b ~~>: λ k, ∃ q, k = ●V{#q} a ⋅ ◯V b.
Proof.
    eapply cmra_updateP_weaken.
    { eapply cmra_updateP_op'.
      { eapply view_updateP_auth_unpersist. }
      by eapply cmra_update_updateP. }
    naive_solver.
  Qed.
(* iris/algebra/view.v *)
Lemma view_updateP_frag b P :
    (∀ a n bf, rel n a (b ⋅ bf) → ∃ b', P b' ∧ rel n a (b' ⋅ bf)) →
    ◯V b ~~>: λ k, ∃ b', k = ◯V b' ∧ P b'.
Proof.
    rewrite !cmra_total_updateP view_validN_eq=> ? n [[[dq ag]|] bf]; naive_solver.
  Qed.
(* iris/algebra/view.v *)
Lemma view_update_frag b b' :
    (∀ a n bf, rel n a (b ⋅ bf) → rel n a (b' ⋅ bf)) →
    ◯V b ~~> ◯V b'.
Proof.
    rewrite !cmra_total_update view_validN_eq=> ? n [[[dq ag]|] bf]; naive_solver.
  Qed.
(* iris/algebra/view.v *)
Lemma view_update_dfrac_alloc dq a b :
    (∀ n bf, rel n a bf → rel n a (b ⋅ bf)) →
    ●V{dq} a ~~> ●V{dq} a ⋅ ◯V b.
Proof.
    intros Hup. apply cmra_total_update=> n [[[p ag]|] bf] [/=].
    - intros ? (a0 & Hag & Hrel). split; simpl; [done|].
      exists a0; split; [done|]. revert Hrel.
      assert (to_agree a ≼{n} to_agree a0) as <-%to_agree_includedN.
      { by exists ag. }
      rewrite !left_id. apply Hup.
    - intros ? (a0 & <-%(inj to_agree) & Hrel). split; simpl; [done|].
      exists a; split; [done|]. revert Hrel. rewrite !left_id. apply Hup.
  Qed.
(* iris/algebra/view.v *)
Lemma view_local_update a b0 b1 a' b0' b1' :
    (b0, b1) ~l~> (b0', b1') →
    (∀ n, view_rel_holds rel n a b0 → view_rel_holds rel n a' b0') →
    (●V a ⋅ ◯V b0, ●V a ⋅ ◯V b1) ~l~> (●V a' ⋅ ◯V b0', ●V a' ⋅ ◯V b1').
Proof.
    rewrite !local_update_unital.
    move=> Hup Hrel n [[[qd ag]|] bf] /view_both_validN Hrel' [/=].
    - rewrite right_id -Some_op -pair_op => /Some_dist_inj [/= H1q _].
      by destruct (id_free_r (DfracOwn 1) qd).
    - rewrite !left_id=> _ Hb0.
      destruct (Hup n bf) as [? Hb0']; [by eauto using view_rel_validN..|].
      split; [apply view_both_validN; by auto|]. by rewrite -assoc Hb0'.
  Qed.
(* iris/algebra/view.v *)
(* Due to the dependent type [rel] in [view] we cannot actually define
instances of the functor structures [rFunctor] and [urFunctor]. Functors can
only be defined for instances of [view], like [auth]. To make it more convenient
to define functors for instances of [view], we define the map operation
[view_map] and a bunch of lemmas about it. *)
Definition view_map {SI : sidx} {A A' B B'}
    {rel : SI → A → B → Prop} {rel' : SI → A' → B' → Prop}
    (f : A → A') (g : B → B') (x : view rel) : view rel'
:=
  View (prod_map id (agree_map f) <$> view_auth_proj x) (g (view_frag_proj x)).
(* iris/algebra/view.v *)
Lemma view_map_id {SI : sidx} {A B} {rel : SI → A → B → Prop} (x : view rel) :
  view_map id id x = x.
Proof. destruct x as [[[]|] ]; by rewrite // /view_map /= agree_map_id. Qed.
(* iris/algebra/view.v *)
Lemma view_map_compose {SI : sidx} {A A' A'' B B' B''}
    {rel : SI → A → B → Prop} {rel' : SI → A' → B' → Prop}
    {rel'' : SI → A'' → B'' → Prop}
    (f1 : A → A') (f2 : A' → A'') (g1 : B → B') (g2 : B' → B'') (x : view rel) :
  view_map (f2 ∘ f1) (g2 ∘ g1) x
  =@{view rel''} view_map f2 g2 (view_map (rel':=rel') f1 g1 x).
Proof. destruct x as [[[]|] ];  by rewrite // /view_map /= agree_map_compose. Qed.
(* iris/algebra/view.v *)
Lemma view_map_ext {SI : sidx} {A A' B B' : ofe}
    {rel : SI → A → B → Prop} {rel' : SI → A' → B' → Prop}
    (f1 f2 : A → A') (g1 g2 : B → B')
    `{!NonExpansive f1, !NonExpansive g1} (x : view rel) :
  (∀ a, f1 a ≡ f2 a) → (∀ b, g1 b ≡ g2 b) →
  view_map f1 g1 x ≡@{view rel'} view_map f2 g2 x.
Proof.
  intros. constructor; simpl; [|by auto].
  apply option_fmap_equiv_ext=> a; by rewrite /prod_map /= agree_map_ext.
Qed.
(* iris/algebra/view.v *)
Instance view_map_ne {SI : sidx} {A A' B B' : ofe}
    {rel : SI → A → B → Prop} {rel' : SI → A' → B' → Prop}
    (f : A → A') (g : B → B') `{Hf : !NonExpansive f, Hg : !NonExpansive g} :
  NonExpansive (view_map (rel':=rel') (rel:=rel) f g).
Proof.
  intros n [o1 bf1] [o2 bf2] [??]; split; simpl in *; [|by apply Hg].
  apply option_fmap_ne; [|done]=> pag1 pag2 ?.
  apply prod_map_ne; [done| |done]. by apply agree_map_ne.
Qed.
(* iris/algebra/view.v *)
Definition viewO_map {SI : sidx} {A A' B B' : ofe}
    {rel : SI → A → B → Prop} {rel' : SI → A' → B' → Prop}
    (f : A -n> A') (g : B -n> B') : viewO rel -n> viewO rel'
:=
  OfeMor (view_map f g).
(* iris/algebra/view.v *)
Lemma viewO_map_ne {SI : sidx} {A A' B B' : ofe}
    {rel : SI → A → B → Prop} {rel' : SI → A' → B' → Prop} :
  NonExpansive2 (viewO_map (rel:=rel) (rel':=rel')).
Proof.
  intros n f f' Hf g g' Hg [[[p ag]|] bf]; split=> //=.
  do 2 f_equiv. by apply agreeO_map_ne.
Qed.
(* iris/algebra/view.v *)
Lemma view_map_cmra_morphism {SI : sidx} {A A' B B'}
    {rel : view_rel A B} {rel' : view_rel A' B'}
    (f : A → A') (g : B → B') `{!NonExpansive f, !CmraMorphism g} :
  (∀ n a b, rel n a b → rel' n (f a) (g b)) →
  CmraMorphism (view_map (rel:=rel) (rel':=rel') f g).
Proof.
  intros Hrel. split.
  - apply _.
  - rewrite !view_validN_eq=> n [[[p ag]|] bf] /=;
      [|naive_solver eauto using cmra_morphism_validN].
    intros [? [a' [Hag ?]]]. split; [done|]. exists (f a'). split; [|by auto].
    by rewrite -agree_map_to_agree -Hag.
  - intros [o bf]. apply Some_proper; rewrite /view_map /=.
    f_equiv; by rewrite cmra_morphism_core.
  - intros [[[dq1 ag1]|] bf1] [[[dq2 ag2]|] bf2];
      try apply View_proper=> //=; by rewrite cmra_morphism_op.
Qed.
(* iris/algebra/lib/dfrac_agree.v *)
Definition dfrac_agreeR {SI : sidx} (A : ofe) : cmra
:= prodR dfracR (agreeR A).
(* iris/algebra/lib/dfrac_agree.v *)
Definition to_dfrac_agree {SI : sidx} {A : ofe} (d : dfrac) (a : A) : dfrac_agreeR A
:=
  (d, to_agree a).
(* iris/algebra/lib/dfrac_agree.v *)
Instance : Params (@to_dfrac_agree) 3
:= {}.
(* iris/algebra/lib/dfrac_agree.v *)
(* To make it easier to work with the [Qp] version of this, we also provide
    [to_frac_agree] and appropriate lemmas. *)
Definition to_frac_agree {SI : sidx} {A : ofe} (q : Qp) (a : A) : dfrac_agreeR A
:=
  to_dfrac_agree (DfracOwn q) a.
(* iris/algebra/lib/dfrac_agree.v *)
Instance : Params (@to_frac_agree) 3
:= {}.
(* iris/algebra/lib/dfrac_agree.v *)
Instance to_dfrac_agree_ne d : NonExpansive (@to_dfrac_agree SI A d).
Proof. solve_proper. Qed.
(* iris/algebra/lib/dfrac_agree.v *)
Instance to_dfrac_agree_proper d :
    Proper ((≡) ==> (≡)) (@to_dfrac_agree SI A d).
Proof. solve_proper. Qed.
(* iris/algebra/lib/dfrac_agree.v *)
Instance to_dfrac_agree_exclusive a :
    Exclusive (to_dfrac_agree (DfracOwn 1) a).
Proof. apply _. Qed.
(* iris/algebra/lib/dfrac_agree.v *)
Instance to_dfrac_agree_discrete d a : Discrete a → Discrete (to_dfrac_agree d a).
Proof. apply _. Qed.
(* iris/algebra/lib/dfrac_agree.v *)
Instance to_dfrac_agree_injN n :
    Inj2 (dist n) (dist n) (dist n) (@to_dfrac_agree SI A).
Proof. by intros d1 a1 d2 a2 [??%(inj to_agree)]. Qed.
(* iris/algebra/lib/dfrac_agree.v *)
Instance to_dfrac_agree_inj : Inj2 (≡) (≡) (≡) (@to_dfrac_agree SI A).
Proof. by intros d1 a1 d2 a2 [??%(inj to_agree)]. Qed.
(* iris/algebra/lib/dfrac_agree.v *)
Lemma dfrac_agree_op d1 d2 a :
    to_dfrac_agree (d1 ⋅ d2) a ≡ to_dfrac_agree d1 a ⋅ to_dfrac_agree d2 a.
Proof. rewrite /to_dfrac_agree -pair_op agree_idemp //. Qed.
(* iris/algebra/lib/dfrac_agree.v *)
Lemma frac_agree_op q1 q2 a :
    to_frac_agree (q1 + q2) a ≡ to_frac_agree q1 a ⋅ to_frac_agree q2 a.
Proof. rewrite -dfrac_agree_op. done. Qed.
(* iris/algebra/lib/dfrac_agree.v *)
Lemma dfrac_agree_op_valid d1 a1 d2 a2 :
    ✓ (to_dfrac_agree d1 a1 ⋅ to_dfrac_agree d2 a2) ↔
    ✓ (d1 ⋅ d2) ∧ a1 ≡ a2.
Proof.
    rewrite /to_dfrac_agree -pair_op pair_valid to_agree_op_valid. done.
  Qed.
(* iris/algebra/lib/dfrac_agree.v *)
Lemma dfrac_agree_op_valid_L `{!LeibnizEquiv A} d1 a1 d2 a2 :
    ✓ (to_dfrac_agree d1 a1 ⋅ to_dfrac_agree d2 a2) ↔
    ✓ (d1 ⋅ d2) ∧ a1 = a2.
Proof. unfold_leibniz. apply dfrac_agree_op_valid. Qed.
(* iris/algebra/lib/dfrac_agree.v *)
Lemma dfrac_agree_op_validN d1 a1 d2 a2 n :
    ✓{n} (to_dfrac_agree d1 a1 ⋅ to_dfrac_agree d2 a2) ↔
    ✓ (d1 ⋅ d2) ∧ a1 ≡{n}≡ a2.
Proof.
    rewrite /to_dfrac_agree -pair_op pair_validN to_agree_op_validN. done.
  Qed.
(* iris/algebra/lib/dfrac_agree.v *)
Lemma frac_agree_op_valid q1 a1 q2 a2 :
    ✓ (to_frac_agree q1 a1 ⋅ to_frac_agree q2 a2) ↔
    (q1 + q2 ≤ 1)%Qp ∧ a1 ≡ a2.
Proof. apply dfrac_agree_op_valid. Qed.
(* iris/algebra/lib/dfrac_agree.v *)
Lemma frac_agree_op_valid_L `{!LeibnizEquiv A} q1 a1 q2 a2 :
    ✓ (to_frac_agree q1 a1 ⋅ to_frac_agree q2 a2) ↔
    (q1 + q2 ≤ 1)%Qp ∧ a1 = a2.
Proof. apply dfrac_agree_op_valid_L. Qed.
(* iris/algebra/lib/dfrac_agree.v *)
Lemma frac_agree_op_validN q1 a1 q2 a2 n :
    ✓{n} (to_frac_agree q1 a1 ⋅ to_frac_agree q2 a2) ↔
    (q1 + q2 ≤ 1)%Qp ∧ a1 ≡{n}≡ a2.
Proof. apply dfrac_agree_op_validN. Qed.
(* iris/algebra/lib/dfrac_agree.v *)
Lemma dfrac_agree_included d1 a1 d2 a2 :
    to_dfrac_agree d1 a1 ≼ to_dfrac_agree d2 a2 ↔
    (d1 ≼ d2) ∧ a1 ≡ a2.
Proof. by rewrite pair_included to_agree_included. Qed.
(* iris/algebra/lib/dfrac_agree.v *)
Lemma dfrac_agree_included_L `{!LeibnizEquiv A} d1 a1 d2 a2 :
    to_dfrac_agree d1 a1 ≼ to_dfrac_agree d2 a2 ↔
    (d1 ≼ d2) ∧ a1 = a2.
Proof. unfold_leibniz. apply dfrac_agree_included. Qed.
(* iris/algebra/lib/dfrac_agree.v *)
Lemma dfrac_agree_includedN d1 a1 d2 a2 n :
    to_dfrac_agree d1 a1 ≼{n} to_dfrac_agree d2 a2 ↔
    (d1 ≼ d2) ∧ a1 ≡{n}≡ a2.
Proof.
    by rewrite pair_includedN -cmra_discrete_included_iff
               to_agree_includedN.
  Qed.
(* iris/algebra/lib/dfrac_agree.v *)
Lemma frac_agree_included q1 a1 q2 a2 :
    to_frac_agree q1 a1 ≼ to_frac_agree q2 a2 ↔
    (q1 < q2)%Qp ∧ a1 ≡ a2.
Proof. by rewrite dfrac_agree_included dfrac_own_included. Qed.
(* iris/algebra/lib/dfrac_agree.v *)
Lemma frac_agree_included_L `{!LeibnizEquiv A} q1 a1 q2 a2 :
    to_frac_agree q1 a1 ≼ to_frac_agree q2 a2 ↔
    (q1 < q2)%Qp ∧ a1 = a2.
Proof. by rewrite dfrac_agree_included_L dfrac_own_included. Qed.
(* iris/algebra/lib/dfrac_agree.v *)
Lemma frac_agree_includedN q1 a1 q2 a2 n :
    to_frac_agree q1 a1 ≼{n} to_frac_agree q2 a2 ↔
    (q1 < q2)%Qp ∧ a1 ≡{n}≡ a2.
Proof. by rewrite dfrac_agree_includedN dfrac_own_included. Qed.
(* iris/algebra/lib/dfrac_agree.v *)
(* While [cmra_update_exclusive] takes care of most updates, it is not sufficient
      for this one since there is no abstraction-preserving way to rewrite
      [to_dfrac_agree d1 v1 ⋅ to_dfrac_agree d2 v2] into something simpler. *)
Lemma dfrac_agree_update_2 d1 d2 a1 a2 a' :
    d1 ⋅ d2 = DfracOwn 1 →
    to_dfrac_agree d1 a1 ⋅ to_dfrac_agree d2 a2 ~~>
    to_dfrac_agree d1 a' ⋅ to_dfrac_agree d2 a'.
Proof.
    intros Hq. rewrite -pair_op Hq.
    apply cmra_update_exclusive.
    rewrite dfrac_agree_op_valid Hq //.
  Qed.
(* iris/algebra/lib/dfrac_agree.v *)
Lemma frac_agree_update_2 q1 q2 a1 a2 a' :
    (q1 + q2 = 1)%Qp →
    to_frac_agree q1 a1 ⋅ to_frac_agree q2 a2 ~~>
    to_frac_agree q1 a' ⋅ to_frac_agree q2 a'.
Proof. intros Hq. apply dfrac_agree_update_2. rewrite dfrac_op_own Hq //. Qed.
(* iris/algebra/lib/dfrac_agree.v *)
Lemma dfrac_agree_persist d a :
    to_dfrac_agree d a ~~> to_dfrac_agree DfracDiscarded a.
Proof.
    rewrite /to_dfrac_agree. apply prod_update; last done.
    simpl. apply dfrac_discard_update.
  Qed.
(* iris/algebra/lib/dfrac_agree.v *)
Lemma dfrac_agree_unpersist a :
    to_dfrac_agree DfracDiscarded a ~~>: λ k, ∃ q, k = to_dfrac_agree (DfracOwn q) a.
Proof.
    rewrite /to_dfrac_agree. eapply prod_updateP; first apply dfrac_undiscard_update.
    { by eapply cmra_update_updateP. }
    naive_solver.
  Qed.
(* iris/algebra/lib/dfrac_agree.v *)
Definition dfrac_agreeRF {SI : sidx} (F : oFunctor) : rFunctor
:=
  prodRF (constRF dfracR) (agreeRF F).
(* iris/algebra/lib/dfrac_agree.v *)
Instance dfrac_agreeRF_contractive {SI : sidx} F :
  oFunctorContractive F → rFunctorContractive (dfrac_agreeRF F).
Proof. apply _. Qed.
(* iris/algebra/lib/excl_auth.v *)
(* Authoritative CMRA where the fragment is exclusively owned.
This is effectively a single "ghost variable" with two views, the frament [◯E a]
and the authority [●E a]. *)
Definition excl_authR {SI : sidx} (A : ofe) : cmra
:=
  authR (optionUR (exclR A)).
(* iris/algebra/lib/excl_auth.v *)
Definition excl_authUR {SI : sidx} (A : ofe) : ucmra
:=
  authUR (optionUR (exclR A)).
(* iris/algebra/lib/excl_auth.v *)
Definition excl_auth_auth {SI : sidx} {A : ofe} (a : A) : excl_authR A
:=
  ● (Some (Excl a)).
(* iris/algebra/lib/excl_auth.v *)
Definition excl_auth_frag {SI : sidx} {A : ofe} (a : A) : excl_authR A
:=
  ◯ (Some (Excl a)).
(* iris/algebra/lib/excl_auth.v *)
Instance : Params (@excl_auth_auth) 2
:= {}.
(* iris/algebra/lib/excl_auth.v *)
Instance : Params (@excl_auth_frag) 3
:= {}.
(* iris/algebra/lib/excl_auth.v *)
Notation "●E a"
:= (excl_auth_auth a) (at level 10).
(* iris/algebra/lib/excl_auth.v *)
Notation "◯E a"
:= (excl_auth_frag a) (at level 10).
(* iris/algebra/lib/excl_auth.v *)
Instance excl_auth_auth_ne : NonExpansive (@excl_auth_auth SI A).
Proof. solve_proper. Qed.
(* iris/algebra/lib/excl_auth.v *)
Instance excl_auth_auth_proper :
    Proper ((≡) ==> (≡)) (@excl_auth_auth SI A).
Proof. solve_proper. Qed.
(* iris/algebra/lib/excl_auth.v *)
Instance excl_auth_frag_ne : NonExpansive (@excl_auth_frag SI A).
Proof. solve_proper. Qed.
(* iris/algebra/lib/excl_auth.v *)
Instance excl_auth_frag_proper :
    Proper ((≡) ==> (≡)) (@excl_auth_frag SI A).
Proof. solve_proper. Qed.
(* iris/algebra/lib/excl_auth.v *)
Instance excl_auth_auth_discrete a : Discrete a → Discrete (●E a).
Proof. intros; apply auth_auth_discrete; [apply Some_discrete|]; apply _. Qed.
(* iris/algebra/lib/excl_auth.v *)
Instance excl_auth_frag_discrete a : Discrete a → Discrete (◯E a).
Proof. intros; apply auth_frag_discrete, Some_discrete; apply _. Qed.
(* iris/algebra/lib/excl_auth.v *)
Lemma excl_auth_validN n a : ✓{n} (●E a ⋅ ◯E a).
Proof. by rewrite auth_both_validN. Qed.
(* iris/algebra/lib/excl_auth.v *)
Lemma excl_auth_valid a : ✓ (●E a ⋅ ◯E a).
Proof. intros. by apply auth_both_valid_2. Qed.
(* iris/algebra/lib/excl_auth.v *)
Lemma excl_auth_agreeN n a b : ✓{n} (●E a ⋅ ◯E b) → a ≡{n}≡ b.
Proof.
    rewrite auth_both_validN /= => -[Hincl Hvalid].
    move: Hincl=> /Some_includedN_exclusive /(_ I) ?. by apply (inj Excl).
  Qed.
(* iris/algebra/lib/excl_auth.v *)
Lemma excl_auth_agree a b : ✓ (●E a ⋅ ◯E b) → a ≡ b.
Proof.
    intros. apply equiv_dist=> n. by apply excl_auth_agreeN, cmra_valid_validN.
  Qed.
(* iris/algebra/lib/excl_auth.v *)
Lemma excl_auth_agree_L `{!LeibnizEquiv A} a b : ✓ (●E a ⋅ ◯E b) → a = b.
Proof. intros. by apply leibniz_equiv, excl_auth_agree. Qed.
(* iris/algebra/lib/excl_auth.v *)
Lemma excl_auth_auth_op_validN n a b : ✓{n} (●E a ⋅ ●E b) ↔ False.
Proof. apply auth_auth_op_validN. Qed.
(* iris/algebra/lib/excl_auth.v *)
Lemma excl_auth_auth_op_valid a b : ✓ (●E a ⋅ ●E b) ↔ False.
Proof. apply auth_auth_op_valid. Qed.
(* iris/algebra/lib/excl_auth.v *)
Lemma excl_auth_frag_op_validN n a b : ✓{n} (◯E a ⋅ ◯E b) ↔ False.
Proof. by rewrite -auth_frag_op auth_frag_validN. Qed.
(* iris/algebra/lib/excl_auth.v *)
Lemma excl_auth_frag_op_valid a b : ✓ (◯E a ⋅ ◯E b) ↔ False.
Proof. by rewrite -auth_frag_op auth_frag_valid. Qed.
(* iris/algebra/lib/excl_auth.v *)
Lemma excl_auth_update a b a' : ●E a ⋅ ◯E b ~~> ●E a' ⋅ ◯E a'.
Proof.
    intros. by apply auth_update, option_local_update, exclusive_local_update.
  Qed.
(* iris/algebra/lib/excl_auth.v *)
Definition excl_authURF {SI : sidx} (F : oFunctor) : urFunctor
:=
  authURF (optionURF (exclRF F)).
(* iris/algebra/lib/excl_auth.v *)
Instance excl_authURF_contractive {SI : sidx} F :
  oFunctorContractive F → urFunctorContractive (excl_authURF F).
Proof. apply _. Qed.
(* iris/algebra/lib/excl_auth.v *)
Definition excl_authRF {SI : sidx} (F : oFunctor) : rFunctor
:=
  authRF (optionURF (exclRF F)).
(* iris/algebra/lib/excl_auth.v *)
Instance excl_authRF_contractive {SI : sidx} F :
  oFunctorContractive F → rFunctorContractive (excl_authRF F).
Proof. apply _. Qed.
(* iris/algebra/lib/frac_auth.v *)
(* Authoritative CMRA where both parts can be fractional. This CMRA allows the
  original elements [● a] and [◯ a] to be split into fractional parts [●F dq a]
  and [◯F{q} a]. Using  [●F a ≡ ●F{#1} a] or [◯F a ≡ ◯F{1} a] is in effect the
  same as using the original [● a] and [◯ a].

  These fractions don't split the same way, to make the laws more useful. A
  fractional authoritative element [●F dq a] says that the authoritative
  element is actually [a]. Splitting the fraction duplicates this knowledge:
  [●F{#q1+q2} a ≡ ●F{#q1} a ⋅ ●F{#q2} a]. A fractional non-authoritative
  element [◯F{q} a] only says that the authoritative element is *at least* [a],
  and splitting the fraction splits this lower bound:
  [◯F{q1+q2} (a1 ⋅ a2) ≡ ◯F{q1} a1 ⋅ ◯F{q2} a2]. *)
Definition frac_authR {SI : sidx} (A : cmra) : cmra
:=
  authR (optionUR (prodR fracR A)).
(* iris/algebra/lib/frac_auth.v *)
Definition frac_authUR {SI : sidx} (A : cmra) : ucmra
:=
  authUR (optionUR (prodR fracR A)).
(* iris/algebra/lib/frac_auth.v *)
Definition frac_auth_auth {SI : sidx} {A : cmra}
    (dq : dfrac) (x : A) : frac_authR A
:=
  ●{dq} (Some (1%Qp,x)).
(* iris/algebra/lib/frac_auth.v *)
Definition frac_auth_frag {SI : sidx}
    {A : cmra} (q : frac) (x : A) : frac_authR A
:=
  ◯ (Some (q,x)).
(* iris/algebra/lib/frac_auth.v *)
Instance : Params (@frac_auth_auth) 3
:= {}.
(* iris/algebra/lib/frac_auth.v *)
Instance : Params (@frac_auth_frag) 3
:= {}.
(* iris/algebra/lib/frac_auth.v *)
Notation "●F dq a"
:= (frac_auth_auth dq a)
  (at level 10, dq custom dfrac at level 1, format "●F dq  a").
(* iris/algebra/lib/frac_auth.v *)
Notation "◯F{ q } a"
:= (frac_auth_frag q a) (at level 10, format "◯F{ q }  a").
(* iris/algebra/lib/frac_auth.v *)
Notation "◯F a"
:= (frac_auth_frag 1 a) (at level 10).
(* iris/algebra/lib/frac_auth.v *)
Instance frac_auth_auth_ne dq : NonExpansive (@frac_auth_auth SI A dq).
Proof. solve_proper. Qed.
(* iris/algebra/lib/frac_auth.v *)
Instance frac_auth_auth_proper dq :
    Proper ((≡) ==> (≡)) (@frac_auth_auth SI A dq).
Proof. solve_proper. Qed.
(* iris/algebra/lib/frac_auth.v *)
Instance frac_auth_frag_ne q : NonExpansive (@frac_auth_frag SI A q).
Proof. solve_proper. Qed.
(* iris/algebra/lib/frac_auth.v *)
Instance frac_auth_frag_proper q :
    Proper ((≡) ==> (≡)) (@frac_auth_frag SI A q).
Proof. solve_proper. Qed.
(* iris/algebra/lib/frac_auth.v *)
Instance frac_auth_auth_discrete dq a : Discrete a → Discrete (●F{dq} a).
Proof. intros; apply auth_auth_discrete; [apply Some_discrete|]; apply _. Qed.
(* iris/algebra/lib/frac_auth.v *)
Instance frac_auth_frag_discrete q a : Discrete a → Discrete (◯F{q} a).
Proof. intros; apply auth_frag_discrete, Some_discrete; apply _. Qed.
(* iris/algebra/lib/frac_auth.v *)
Lemma frac_auth_dfrac_validN dq n a : ✓ dq → ✓{n} a → ✓{n} (●F{dq} a ⋅ ◯F a).
Proof. by rewrite auth_both_dfrac_validN Some_validN. Qed.
(* iris/algebra/lib/frac_auth.v *)
Lemma frac_auth_validN n a : ✓{n} a → ✓{n} (●F a ⋅ ◯F a).
Proof. by apply frac_auth_dfrac_validN. Qed.
(* iris/algebra/lib/frac_auth.v *)
Lemma frac_auth_dfrac_valid dq a : ✓ dq → ✓ a → ✓ (●F{dq} a ⋅ ◯F a).
Proof. intros. by apply auth_both_dfrac_valid_2. Qed.
(* iris/algebra/lib/frac_auth.v *)
Lemma frac_auth_valid a : ✓ a → ✓ (●F a ⋅ ◯F a).
Proof. by apply frac_auth_dfrac_valid. Qed.
(* iris/algebra/lib/frac_auth.v *)
Lemma frac_auth_agreeN n dq a b : ✓{n} (●F{dq} a ⋅ ◯F b) → a ≡{n}≡ b.
Proof.
    rewrite auth_both_dfrac_validN /= => -[? [Hincl Hvalid]].
    by move: Hincl=> /Some_includedN_exclusive /(_ Hvalid ) [??].
  Qed.
(* iris/algebra/lib/frac_auth.v *)
Lemma frac_auth_agree dq a b : ✓ (●F{dq} a ⋅ ◯F b) → a ≡ b.
Proof.
    intros. apply equiv_dist=> n. by eapply frac_auth_agreeN, cmra_valid_validN.
  Qed.
(* iris/algebra/lib/frac_auth.v *)
Lemma frac_auth_agree_L `{!LeibnizEquiv A} dq a b :
    ✓ (●F{dq} a ⋅ ◯F b) →
    a = b.
Proof. intros. by eapply leibniz_equiv, frac_auth_agree. Qed.
(* iris/algebra/lib/frac_auth.v *)
Lemma frac_auth_includedN n dq q a b :
    ✓{n} (●F{dq} a ⋅ ◯F{q} b) →
    Some b ≼{n} Some a.
Proof.
    by rewrite auth_both_dfrac_validN /= => -[? [/Some_pair_includedN [_ ?] _]].
  Qed.
(* iris/algebra/lib/frac_auth.v *)
Lemma frac_auth_included `{!CmraDiscrete A} dq q a b :
    ✓ (●F{dq} a ⋅ ◯F{q} b) → Some b ≼ Some a.
Proof.
    by rewrite auth_both_dfrac_valid_discrete /=
      => -[? [/Some_pair_included [_ ?] _]].
  Qed.
(* iris/algebra/lib/frac_auth.v *)
Lemma frac_auth_includedN_total `{!CmraTotal A} n dq q a b :
    ✓{n} (●F{dq} a ⋅ ◯F{q} b) → b ≼{n} a.
Proof. intros. by eapply Some_includedN_total, frac_auth_includedN. Qed.
(* iris/algebra/lib/frac_auth.v *)
Lemma frac_auth_included_total `{!CmraDiscrete A, !CmraTotal A} dq q a b :
    ✓ (●F{dq} a ⋅ ◯F{q} b) → b ≼ a.
Proof. intros. by eapply Some_included_total, frac_auth_included. Qed.
(* iris/algebra/lib/frac_auth.v *)
Lemma frac_auth_auth_dfrac_validN n dq a : ✓{n} (●F{dq} a) ↔ ✓ dq ∧ ✓{n} a.
Proof.
    rewrite auth_auth_dfrac_validN Some_validN. split.
    - by intros [?[]].
    - intros [??]; by split.
  Qed.
(* iris/algebra/lib/frac_auth.v *)
Lemma frac_auth_auth_validN n a : ✓{n} (●F a) ↔ ✓{n} a.
Proof.
    rewrite frac_auth_auth_dfrac_validN. split.
    - by intros [_ ?].
    - done.
  Qed.
(* iris/algebra/lib/frac_auth.v *)
Lemma frac_auth_auth_dfrac_valid dq a : ✓ (●F{dq} a) ↔ ✓ dq ∧ ✓ a.
Proof.
    rewrite auth_auth_dfrac_valid Some_valid. split.
    - by intros [?[]].
    - intros [??]; by split.
  Qed.
(* iris/algebra/lib/frac_auth.v *)
Lemma frac_auth_auth_valid a : ✓ (●F a) ↔ ✓ a.
Proof.
    rewrite frac_auth_auth_dfrac_valid. split.
    - by intros [_ ?].
    - done.
  Qed.
(* iris/algebra/lib/frac_auth.v *)
Lemma frac_auth_frag_validN n q a : ✓{n} (◯F{q} a) ↔ (q ≤ 1)%Qp ∧ ✓{n} a.
Proof. by rewrite /frac_auth_frag auth_frag_validN. Qed.
(* iris/algebra/lib/frac_auth.v *)
Lemma frac_auth_frag_valid q a : ✓ (◯F{q} a) ↔ (q ≤ 1)%Qp ∧ ✓ a.
Proof. by rewrite /frac_auth_frag auth_frag_valid. Qed.
(* iris/algebra/lib/frac_auth.v *)
Lemma frac_auth_auth_dfrac_op dq1 dq2 a :
    ●F{dq1⋅dq2} a ≡ ●F{dq1} a ⋅ ●F{dq2} a.
Proof. by rewrite /frac_auth_auth -auth_auth_dfrac_op. Qed.
(* iris/algebra/lib/frac_auth.v *)
Lemma frac_auth_frag_op q1 q2 a1 a2 :
    ◯F{q1+q2} (a1 ⋅ a2) ≡ ◯F{q1} a1 ⋅ ◯F{q2} a2.
Proof. done. Qed.
(* iris/algebra/lib/frac_auth.v *)
Lemma frac_auth_auth_dfrac_op_validN n dq1 dq2 a b :
    ✓{n} (●F{dq1} a ⋅ ●F{dq2} b) → ✓ (dq1 ⋅ dq2)  ∧ a ≡{n}≡ b.
Proof.
    rewrite auth_auth_dfrac_op_validN.
    intros [?[[_?]%Some_dist_inj%pair_dist_inj ?]]; by split.
  Qed.
(* iris/algebra/lib/frac_auth.v *)
Lemma frac_auth_auth_op_validN n a b :
    ✓{n} (●F a ⋅ ●F b) → False.
Proof. by intros [? _]%frac_auth_auth_dfrac_op_validN. Qed.