phanerozoic/Coq-Iris huggingface dataset:
(* iris/algebra/lib/mono_list.v *)
Lemma mono_list_lb_op_valid l1 l2 :
    ✓ (◯ML l1 ⋅ ◯ML l2) ↔ (∃ l, l2 ≡ l1 ++ l) ∨ (∃ l, l1 ≡ l2 ++ l).
Proof. by rewrite auth_frag_op_valid to_max_prefix_list_op_valid. Qed.
(* iris/algebra/lib/mono_list.v *)
Lemma mono_list_lb_op_valid_L `{!LeibnizEquiv A} l1 l2 :
    ✓ (◯ML l1 ⋅ ◯ML l2) ↔ l1 `prefix_of` l2 ∨ l2 `prefix_of` l1.
Proof. rewrite mono_list_lb_op_valid / prefix. naive_solver. Qed.
(* iris/algebra/lib/mono_list.v *)
Lemma mono_list_lb_op_valid_1_L `{!LeibnizEquiv A} l1 l2 :
    ✓ (◯ML l1 ⋅ ◯ML l2) → l1 `prefix_of` l2 ∨ l2 `prefix_of` l1.
Proof. by apply mono_list_lb_op_valid_L. Qed.
(* iris/algebra/lib/mono_list.v *)
Lemma mono_list_lb_op_valid_2_L `{!LeibnizEquiv A} l1 l2 :
    l1 `prefix_of` l2 ∨ l2 `prefix_of` l1 → ✓ (◯ML l1 ⋅ ◯ML l2).
Proof. by apply mono_list_lb_op_valid_L. Qed.
(* iris/algebra/lib/mono_list.v *)
Lemma mono_list_lb_mono l1 l2 : l1 `prefix_of` l2 → ◯ML l1 ≼ ◯ML l2.
Proof. intros. exists (◯ML l2). by rewrite mono_list_lb_op_l. Qed.
(* iris/algebra/lib/mono_list.v *)
Lemma mono_list_included dq l : ◯ML l ≼ ●ML{dq} l.
Proof. apply cmra_included_r. Qed.
(* iris/algebra/lib/mono_list.v *)
(* * Update *)
Lemma mono_list_update {l1} l2 : l1 `prefix_of` l2 → ●ML l1 ~~> ●ML l2.
Proof. intros ?. by apply auth_update, max_prefix_list_local_update. Qed.
(* iris/algebra/lib/mono_list.v *)
Lemma mono_list_auth_persist dq l : ●ML{dq} l ~~> ●ML□ l.
Proof.
    rewrite /mono_list_auth. apply cmra_update_op; [|done].
    by apply auth_update_auth_persist.
  Qed.
(* iris/algebra/lib/mono_list.v *)
Lemma mono_list_auth_unpersist l :
    ●ML□ l ~~>: λ k, ∃ q, k = ●ML{#q} l.
Proof. eapply auth_updateP_both_unpersist. Qed.
(* iris/algebra/lib/mono_list.v *)
Definition mono_listURF {SI : sidx} (F : oFunctor) : urFunctor
:=
  authURF (max_prefix_listURF F).
(* iris/algebra/lib/mono_list.v *)
Instance mono_listURF_contractive {SI : sidx} F :
  oFunctorContractive F → urFunctorContractive (mono_listURF F).
Proof. apply _. Qed.
(* iris/algebra/lib/mono_list.v *)
Definition mono_listRF {SI : sidx} (F : oFunctor) : rFunctor
:=
  authRF (max_prefix_listURF F).
(* iris/algebra/lib/mono_list.v *)
Instance mono_listRF_contractive {SI : sidx} F :
  oFunctorContractive F → rFunctorContractive (mono_listRF F).
Proof. apply _. Qed.
(* iris/algebra/lib/mono_nat.v *)
(* Authoritative CMRA over [max_nat]. The authoritative element is a
monotonically increasing [nat], while a fragment is a lower bound. *)
Definition mono_nat {SI : sidx}
:= auth max_natUR.
(* iris/algebra/lib/mono_nat.v *)
Definition mono_natR {SI : sidx}
:= authR max_natUR.
(* iris/algebra/lib/mono_nat.v *)
Definition mono_natUR {SI : sidx}
:= authUR max_natUR.
(* iris/algebra/lib/mono_nat.v *)
(* [mono_nat_auth] is the authoritative element. The definition includes the
fragment at the same value so that lemma [mono_nat_included], which states that
[mono_nat_lb n ≼ mono_nat_auth dq n], holds. Without this trick, a
frame-preserving update lemma would be required instead. *)
Definition mono_nat_auth {SI : sidx} (dq : dfrac) (n : nat) : mono_nat
:=
  ●{dq} MaxNat n ⋅ ◯ MaxNat n.
(* iris/algebra/lib/mono_nat.v *)
Definition mono_nat_lb {SI : sidx} (n : nat) : mono_nat
:= ◯ MaxNat n.
(* iris/algebra/lib/mono_nat.v *)
Notation "●MN dq a"
:= (mono_nat_auth dq a)
  (at level 20, dq custom dfrac at level 1, format "●MN dq  a").
(* iris/algebra/lib/mono_nat.v *)
Notation "◯MN a"
:= (mono_nat_lb a) (at level 20).
(* iris/algebra/lib/mono_nat.v *)
Instance mono_nat_lb_core_id n : CoreId (◯MN n).
Proof. apply _. Qed.
(* iris/algebra/lib/mono_nat.v *)
Instance mono_nat_auth_core_id l : CoreId (●MN□ l).
Proof. apply _. Qed.
(* iris/algebra/lib/mono_nat.v *)
Lemma mono_nat_auth_dfrac_op dq1 dq2 n :
    ●MN{dq1 ⋅ dq2} n ≡ ●MN{dq1} n ⋅ ●MN{dq2} n.
Proof.
    rewrite /mono_nat_auth auth_auth_dfrac_op.
    rewrite (comm _ (●{dq2} _)) -!assoc (assoc _ (◯ _)).
    by rewrite -core_id_dup (comm _ (◯ _)).
  Qed.
(* iris/algebra/lib/mono_nat.v *)
Lemma mono_nat_lb_op n1 n2 :
    ◯MN (n1 `max` n2) = ◯MN n1 ⋅ ◯MN n2.
Proof. rewrite -auth_frag_op max_nat_op //. Qed.
(* iris/algebra/lib/mono_nat.v *)
Lemma mono_nat_auth_lb_op dq n :
    ●MN{dq} n ≡ ●MN{dq} n ⋅ ◯MN n.
Proof.
    rewrite /mono_nat_auth /mono_nat_lb.
    rewrite -!assoc -auth_frag_op max_nat_op.
    rewrite Nat.max_id //.
  Qed.
(* iris/algebra/lib/mono_nat.v *)
Instance mono_nat_auth_dfrac_is_op dq dq1 dq2 n :
    IsOp dq dq1 dq2 → IsOp' (●MN{dq} n) (●MN{dq1} n) (●MN{dq2} n).
Proof. rewrite /IsOp' /IsOp=> ->. rewrite mono_nat_auth_dfrac_op //. Qed.
(* iris/algebra/lib/mono_nat.v *)
Instance mono_nat_lb_max_is_op n n1 n2 :
    IsOp (MaxNat n) (MaxNat n1) (MaxNat n2) → IsOp' (◯MN n) (◯MN n1) (◯MN n2).
Proof. rewrite /IsOp' /IsOp /mono_nat_lb=> ->. done. Qed.
(* iris/algebra/lib/mono_nat.v *)
(* rephrasing of [mono_nat_lb_op] useful for weakening a fragment to a
  smaller lower-bound *)
Lemma mono_nat_lb_op_le_l n n' :
    n' ≤ n →
    ◯MN n = ◯MN n' ⋅ ◯MN n.
Proof. intros. rewrite -mono_nat_lb_op Nat.max_r //. Qed.
(* iris/algebra/lib/mono_nat.v *)
Lemma mono_nat_auth_dfrac_valid dq n : (✓ ●MN{dq} n) ↔ ✓ dq.
Proof.
    rewrite /mono_nat_auth auth_both_dfrac_valid_discrete /=. naive_solver.
  Qed.
(* iris/algebra/lib/mono_nat.v *)
Lemma mono_nat_auth_valid n : ✓ ●MN n.
Proof. by apply auth_both_valid. Qed.
(* iris/algebra/lib/mono_nat.v *)
Lemma mono_nat_auth_dfrac_op_valid dq1 dq2 n1 n2 :
    ✓ (●MN{dq1} n1 ⋅ ●MN{dq2} n2) ↔ ✓ (dq1 ⋅ dq2) ∧ n1 = n2.
Proof.
    rewrite /mono_nat_auth (comm _ (●{dq2} _)) -!assoc (assoc _ (◯ _)).
    rewrite -auth_frag_op (comm _ (◯ _)) assoc. split.
    - move=> /cmra_valid_op_l /auth_auth_dfrac_op_valid. naive_solver.
    - intros [? ->]. rewrite -core_id_dup -auth_auth_dfrac_op.
      by apply auth_both_dfrac_valid_discrete.
  Qed.
(* iris/algebra/lib/mono_nat.v *)
Lemma mono_nat_auth_op_valid n1 n2 :
    ✓ (●MN n1 ⋅ ●MN n2) ↔ False.
Proof. rewrite mono_nat_auth_dfrac_op_valid. naive_solver. Qed.
(* iris/algebra/lib/mono_nat.v *)
Lemma mono_nat_both_dfrac_valid dq n m :
    ✓ (●MN{dq} n ⋅ ◯MN m) ↔ ✓ dq ∧ m ≤ n.
Proof.
    rewrite /mono_nat_auth /mono_nat_lb -assoc -auth_frag_op.
    rewrite auth_both_dfrac_valid_discrete max_nat_included /=.
    naive_solver lia.
  Qed.
(* iris/algebra/lib/mono_nat.v *)
Lemma mono_nat_both_valid n m :
    ✓ (●MN n ⋅ ◯MN m) ↔ m ≤ n.
Proof. rewrite mono_nat_both_dfrac_valid dfrac_valid_own. naive_solver. Qed.
(* iris/algebra/lib/mono_nat.v *)
Lemma mono_nat_lb_mono n1 n2 : n1 ≤ n2 → ◯MN n1 ≼ ◯MN n2.
Proof. intros. by apply auth_frag_mono, max_nat_included. Qed.
(* iris/algebra/lib/mono_nat.v *)
Lemma mono_nat_included dq n : ◯MN n ≼ ●MN{dq} n.
Proof. apply cmra_included_r. Qed.
(* iris/algebra/lib/mono_nat.v *)
Lemma mono_nat_update {n} n' :
    n ≤ n' → ●MN n ~~> ●MN n'.
Proof.
    intros. rewrite /mono_nat_auth /mono_nat_lb.
    by apply auth_update, max_nat_local_update.
  Qed.
(* iris/algebra/lib/mono_nat.v *)
Lemma mono_nat_auth_persist n dq :
    ●MN{dq} n ~~> ●MN□ n.
Proof.
    intros. rewrite /mono_nat_auth /mono_nat_lb.
    eapply cmra_update_op_proper; last done.
    eapply auth_update_auth_persist.
  Qed.
(* iris/algebra/lib/mono_nat.v *)
Lemma mono_nat_auth_unpersist n :
    ●MN□ n ~~>: λ k, ∃ q, k = ●MN{# q} n.
Proof. eapply auth_updateP_both_unpersist. Qed.
(* iris/algebra/lib/mono_Z.v *)
(* Authoritative CMRA over [max_Z]. The authoritative element is a
monotonically increasing [Z], while a fragment is a lower bound. *)
Definition mono_Z   {SI: sidx}
:= auth (option max_ZR).
(* iris/algebra/lib/mono_Z.v *)
Definition mono_ZR  {SI: sidx}
:= authR (optionUR max_ZR).
(* iris/algebra/lib/mono_Z.v *)
Definition mono_ZUR {SI: sidx}
:= authUR (optionUR max_ZR).
(* iris/algebra/lib/mono_Z.v *)
(* [mono_Z_auth] is the authoritative element. The definition includes the
fragment at the same value so that lemma [mono_Z_included], which states that
[mono_Z_lb n ≼ mono_Z_auth dq n], holds. Without this trick, a frame-preserving
update lemma would be required instead. *)
Definition mono_Z_auth {SI : sidx} (dq : dfrac) (n : Z) : mono_Z
:=
  ●{dq} (Some (MaxZ n)) ⋅ ◯ (Some (MaxZ n)).
(* iris/algebra/lib/mono_Z.v *)
Definition mono_Z_lb {SI : sidx} (n : Z) : mono_Z
:= ◯ (Some (MaxZ n)).
(* iris/algebra/lib/mono_Z.v *)
Notation "●MZ dq a"
:= (mono_Z_auth dq a)
  (at level 20, dq custom dfrac at level 1, format "●MZ dq  a").
(* iris/algebra/lib/mono_Z.v *)
Notation "◯MZ a"
:= (mono_Z_lb a) (at level 20).
(* iris/algebra/lib/mono_Z.v *)
Instance mono_Z_lb_core_id n : CoreId (◯MZ n).
Proof. apply _. Qed.
(* iris/algebra/lib/mono_Z.v *)
Instance mono_Z_auth_core_id l : CoreId (●MZ□ l).
Proof. apply _. Qed.
(* iris/algebra/lib/mono_Z.v *)
Lemma mono_Z_auth_dfrac_op dq1 dq2 n :
    ●MZ{dq1 ⋅ dq2} n ≡ ●MZ{dq1} n ⋅ ●MZ{dq2} n.
Proof.
    rewrite /mono_Z_auth auth_auth_dfrac_op.
    rewrite (comm _ (●{dq2} _)) -!assoc (assoc _ (◯ _)).
    by rewrite -core_id_dup (comm _ (◯ _)).
  Qed.
(* iris/algebra/lib/mono_Z.v *)
Lemma mono_Z_lb_op n1 n2 :
    ◯MZ (n1 `max` n2) = ◯MZ n1 ⋅ ◯MZ n2.
Proof. rewrite -auth_frag_op -Some_op max_Z_op //. Qed.
(* iris/algebra/lib/mono_Z.v *)
Lemma mono_Z_auth_lb_op dq n :
    ●MZ{dq} n ≡ ●MZ{dq} n ⋅ ◯MZ n.
Proof.
    rewrite /mono_Z_auth /mono_Z_lb.
    rewrite -!assoc -auth_frag_op -Some_op max_Z_op.
    rewrite Z.max_id //.
  Qed.
(* iris/algebra/lib/mono_Z.v *)
Instance mono_Z_auth_dfrac_is_op dq dq1 dq2 n :
    IsOp dq dq1 dq2 → IsOp' (●MZ{dq} n) (●MZ{dq1} n) (●MZ{dq2} n).
Proof. rewrite /IsOp' /IsOp=> ->. rewrite mono_Z_auth_dfrac_op //. Qed.
(* iris/algebra/lib/mono_Z.v *)
Instance mono_Z_lb_max_is_op n n1 n2 :
    IsOp (MaxZ n) (MaxZ n1) (MaxZ n2) → IsOp' (◯MZ n) (◯MZ n1) (◯MZ n2).
Proof. rewrite /IsOp' /IsOp /mono_Z_lb=> ->. done. Qed.
(* iris/algebra/lib/mono_Z.v *)
(* rephrasing of [mono_Z_lb_op] useful for weakening a fragment to a
  smaller lower-bound *)
Lemma mono_Z_lb_op_le_l n n' :
    n' ≤ n →
    ◯MZ n = ◯MZ n' ⋅ ◯MZ n.
Proof. intros. rewrite -mono_Z_lb_op Z.max_r //. Qed.
(* iris/algebra/lib/mono_Z.v *)
Lemma mono_Z_auth_dfrac_valid dq n : (✓ ●MZ{dq} n) ↔ ✓ dq.
Proof.
    rewrite /mono_Z_auth auth_both_dfrac_valid_discrete /=. naive_solver.
  Qed.
(* iris/algebra/lib/mono_Z.v *)
Lemma mono_Z_auth_valid n : ✓ ●MZ n.
Proof. by apply auth_both_valid. Qed.
(* iris/algebra/lib/mono_Z.v *)
Lemma mono_Z_auth_dfrac_op_valid dq1 dq2 n1 n2 :
    ✓ (●MZ{dq1} n1 ⋅ ●MZ{dq2} n2) ↔ ✓ (dq1 ⋅ dq2) ∧ n1 = n2.
Proof.
    rewrite /mono_Z_auth (comm _ (●{dq2} _)) -!assoc (assoc _ (◯ _)).
    rewrite -auth_frag_op (comm _ (◯ _)) assoc. split.
    - move=> /cmra_valid_op_l /auth_auth_dfrac_op_valid. naive_solver.
    - intros [? ->]. rewrite -core_id_dup -auth_auth_dfrac_op.
      by apply auth_both_dfrac_valid_discrete.
  Qed.
(* iris/algebra/lib/mono_Z.v *)
Lemma mono_Z_auth_op_valid n1 n2 :
    ✓ (●MZ n1 ⋅ ●MZ n2) ↔ False.
Proof. rewrite mono_Z_auth_dfrac_op_valid. naive_solver. Qed.
(* iris/algebra/lib/mono_Z.v *)
Lemma mono_Z_both_dfrac_valid dq n m :
    ✓ (●MZ{dq} n ⋅ ◯MZ m) ↔ ✓ dq ∧ m ≤ n.
Proof.
    rewrite /mono_Z_auth /mono_Z_lb -assoc -auth_frag_op.
    rewrite auth_both_dfrac_valid_discrete Some_included_total max_Z_included /=.
    naive_solver lia.
  Qed.
(* iris/algebra/lib/mono_Z.v *)
Lemma mono_Z_both_valid n m :
    ✓ (●MZ n ⋅ ◯MZ m) ↔ m ≤ n.
Proof. rewrite mono_Z_both_dfrac_valid dfrac_valid_own. naive_solver. Qed.
(* iris/algebra/lib/mono_Z.v *)
Lemma mono_Z_lb_mono n1 n2 : n1 ≤ n2 → ◯MZ n1 ≼ ◯MZ n2.
Proof.
    intros. by apply auth_frag_mono, Some_included_total, max_Z_included.
  Qed.
(* iris/algebra/lib/mono_Z.v *)
Lemma mono_Z_included dq n : ◯MZ n ≼ ●MZ{dq} n.
Proof. apply: cmra_included_r. Qed.
(* iris/algebra/lib/mono_Z.v *)
Lemma mono_Z_update {n} n' :
    n ≤ n' → ●MZ n ~~> ●MZ n'.
Proof.
    intros. rewrite /mono_Z_auth /mono_Z_lb.
    by apply auth_update, option_local_update, max_Z_local_update.
  Qed.
(* iris/algebra/lib/mono_Z.v *)
Lemma mono_Z_auth_persist n dq :
    ●MZ{dq} n ~~> ●MZ□ n.
Proof.
    intros. rewrite /mono_Z_auth /mono_Z_lb.
    eapply cmra_update_op_proper; last done.
    eapply auth_update_auth_persist.
  Qed.
(* iris/algebra/lib/mono_Z.v *)
Lemma mono_Z_auth_unpersist n :
    ●MZ□ n ~~>: λ k, ∃ q, k = ●MZ{# q} n.
Proof. eapply auth_updateP_both_unpersist. Qed.
(* iris/algebra/lib/ufrac_auth.v *)
Definition ufrac_authR {SI : sidx} (A : cmra) : cmra
:=
  authR (optionUR (prodR ufracR A)).
(* iris/algebra/lib/ufrac_auth.v *)
Definition ufrac_authUR {SI : sidx} (A : cmra) : ucmra
:=
  authUR (optionUR (prodR ufracR A)).
(* iris/algebra/lib/ufrac_auth.v *)
(* Note in the signature of [ufrac_auth_auth] and [ufrac_auth_frag] we use
[q : Qp] instead of [q : ufrac]. This way, the API does not expose that [ufrac]
is used internally. This is quite important, as there are two canonical camera
instances with carrier [Qp], namely [fracR] and [ufracR]. When writing things
like [ufrac_auth_auth q a ∧ ✓ q] we want Coq to infer the type of [q] as [Qp]
such that the [✓] of the default [fracR] camera is used, and not the [✓] of
the [ufracR] camera. *)
Definition ufrac_auth_auth {SI : sidx} {A : cmra}
    (q : Qp) (x : A) : ufrac_authR A
:=
  ● (Some (q : ufracR,x)).
(* iris/algebra/lib/ufrac_auth.v *)
Definition ufrac_auth_frag {SI : sidx} {A : cmra}
    (q : Qp) (x : A) : ufrac_authR A
:=
  ◯ (Some (q : ufracR,x)).
(* iris/algebra/lib/ufrac_auth.v *)
Instance : Params (@ufrac_auth_auth) 3
:= {}.
(* iris/algebra/lib/ufrac_auth.v *)
Instance : Params (@ufrac_auth_frag) 3
:= {}.
(* iris/algebra/lib/ufrac_auth.v *)
Notation "●U_ q a"
:= (ufrac_auth_auth q a) (at level 10, q at level 9, format "●U_ q  a").
(* iris/algebra/lib/ufrac_auth.v *)
Notation "◯U_ q a"
:= (ufrac_auth_frag q a) (at level 10, q at level 9, format "◯U_ q  a").
(* iris/algebra/lib/ufrac_auth.v *)
Instance ufrac_auth_auth_ne q : NonExpansive (@ufrac_auth_auth SI A q).
Proof. solve_proper. Qed.
(* iris/algebra/lib/ufrac_auth.v *)
Instance ufrac_auth_auth_proper q :
    Proper ((≡) ==> (≡)) (@ufrac_auth_auth SI A q).
Proof. solve_proper. Qed.
(* iris/algebra/lib/ufrac_auth.v *)
Instance ufrac_auth_frag_ne q : NonExpansive (@ufrac_auth_frag SI A q).
Proof. solve_proper. Qed.
(* iris/algebra/lib/ufrac_auth.v *)
Instance ufrac_auth_frag_proper q :
    Proper ((≡) ==> (≡)) (@ufrac_auth_frag SI A q).
Proof. solve_proper. Qed.
(* iris/algebra/lib/ufrac_auth.v *)
Instance ufrac_auth_auth_discrete q a : Discrete a → Discrete (●U_q a).
Proof. intros. apply auth_auth_discrete; [apply Some_discrete|]; apply _. Qed.
(* iris/algebra/lib/ufrac_auth.v *)
Instance ufrac_auth_frag_discrete q a : Discrete a → Discrete (◯U_q a).
Proof. intros. apply auth_frag_discrete; apply Some_discrete; apply _. Qed.
(* iris/algebra/lib/ufrac_auth.v *)
Lemma ufrac_auth_validN n a p : ✓{n} a → ✓{n} (●U_p a ⋅ ◯U_p a).
Proof. by rewrite auth_both_validN. Qed.
(* iris/algebra/lib/ufrac_auth.v *)
Lemma ufrac_auth_valid p a : ✓ a → ✓ (●U_p a ⋅ ◯U_p a).
Proof. intros. by apply auth_both_valid_2. Qed.
(* iris/algebra/lib/ufrac_auth.v *)
Lemma ufrac_auth_agreeN n p a b : ✓{n} (●U_p a ⋅ ◯U_p b) → a ≡{n}≡ b.
Proof.
    rewrite auth_both_validN=> -[/Some_includedN [[_ ? //]|Hincl] _].
    move: Hincl=> /pair_includedN=> -[/ufrac_included Hincl _].
    by destruct (irreflexivity (<)%Qp p).
  Qed.
(* iris/algebra/lib/ufrac_auth.v *)
Lemma ufrac_auth_agree p a b : ✓ (●U_p a ⋅ ◯U_p b) → a ≡ b.
Proof.
    intros. apply equiv_dist=> n. by eapply ufrac_auth_agreeN, cmra_valid_validN.
  Qed.
(* iris/algebra/lib/ufrac_auth.v *)
Lemma ufrac_auth_agree_L `{!LeibnizEquiv A} p a b : ✓ (●U_p a ⋅ ◯U_p b) → a = b.
Proof. intros. by eapply leibniz_equiv, ufrac_auth_agree. Qed.
(* iris/algebra/lib/ufrac_auth.v *)
Lemma ufrac_auth_includedN n p q a b : ✓{n} (●U_p a ⋅ ◯U_q b) → Some b ≼{n} Some a.
Proof. by rewrite auth_both_validN=> -[/Some_pair_includedN [_ ?] _]. Qed.
(* iris/algebra/lib/ufrac_auth.v *)
Lemma ufrac_auth_included `{!CmraDiscrete A} q p a b :
    ✓ (●U_p a ⋅ ◯U_q b) → Some b ≼ Some a.
Proof. rewrite auth_both_valid_discrete=> -[/Some_pair_included [_ ?] _] //. Qed.
(* iris/algebra/lib/ufrac_auth.v *)
Lemma ufrac_auth_includedN_total `{!CmraTotal A} n q p a b :
    ✓{n} (●U_p a ⋅ ◯U_q b) → b ≼{n} a.
Proof. intros. by eapply Some_includedN_total, ufrac_auth_includedN. Qed.
(* iris/algebra/lib/ufrac_auth.v *)
Lemma ufrac_auth_included_total `{!CmraDiscrete A, !CmraTotal A} q p a b :
    ✓ (●U_p a ⋅ ◯U_q b) → b ≼ a.
Proof. intros. by eapply Some_included_total, ufrac_auth_included. Qed.
(* iris/algebra/lib/ufrac_auth.v *)
Lemma ufrac_auth_auth_validN n q a : ✓{n} (●U_q a) ↔ ✓{n} a.
Proof.
    rewrite auth_auth_dfrac_validN Some_validN. split.
    - by intros [?[]].
    - intros. by split.
  Qed.
(* iris/algebra/lib/ufrac_auth.v *)
Lemma ufrac_auth_auth_valid q a : ✓ (●U_q a) ↔ ✓ a.
Proof. rewrite !cmra_valid_validN. by setoid_rewrite ufrac_auth_auth_validN. Qed.
(* iris/algebra/lib/ufrac_auth.v *)
Lemma ufrac_auth_frag_validN n q a : ✓{n} (◯U_q a) ↔ ✓{n} a.
Proof.
    rewrite auth_frag_validN. split.
    - by intros [??].
    - by split.
  Qed.
(* iris/algebra/lib/ufrac_auth.v *)
Lemma ufrac_auth_frag_valid q a : ✓ (◯U_q a) ↔ ✓ a.
Proof.
    rewrite auth_frag_valid. split.
    - by intros [??].
    - by split.
  Qed.
(* iris/algebra/lib/ufrac_auth.v *)
Lemma ufrac_auth_frag_op q1 q2 a1 a2 : ◯U_(q1+q2) (a1 ⋅ a2) ≡ ◯U_q1 a1 ⋅ ◯U_q2 a2.
Proof. done. Qed.
(* iris/algebra/lib/ufrac_auth.v *)
Lemma ufrac_auth_frag_op_validN n q1 q2 a b :
    ✓{n} (◯U_q1 a ⋅ ◯U_q2 b) ↔ ✓{n} (a ⋅ b).
Proof. by rewrite -ufrac_auth_frag_op ufrac_auth_frag_validN. Qed.
(* iris/algebra/lib/ufrac_auth.v *)
Lemma ufrac_auth_frag_op_valid q1 q2 a b :
    ✓ (◯U_q1 a ⋅ ◯U_q2 b) ↔ ✓ (a ⋅ b).
Proof. by rewrite -ufrac_auth_frag_op ufrac_auth_frag_valid. Qed.
(* iris/algebra/lib/ufrac_auth.v *)
Instance ufrac_auth_is_op q q1 q2 a a1 a2 :
    IsOp q q1 q2 → IsOp a a1 a2 → IsOp' (◯U_q a) (◯U_q1 a1) (◯U_q2 a2).
Proof. by rewrite /IsOp' /IsOp=> /leibniz_equiv_iff -> ->. Qed.
(* iris/algebra/lib/ufrac_auth.v *)
Instance ufrac_auth_is_op_core_id q q1 q2 a :
    CoreId a → IsOp q q1 q2 → IsOp' (◯U_q a) (◯U_q1 a) (◯U_q2 a).
Proof.
    rewrite /IsOp' /IsOp=> ? /leibniz_equiv_iff ->.
    by rewrite -ufrac_auth_frag_op -core_id_dup.
  Qed.
(* iris/algebra/lib/ufrac_auth.v *)
Lemma ufrac_auth_update p q a b a' b' :
    (a,b) ~l~> (a',b') → ●U_p a ⋅ ◯U_q b ~~> ●U_p a' ⋅ ◯U_q b'.
Proof.
    intros. apply: auth_update.
    apply: option_local_update. by apply: prod_local_update_2.
  Qed.
(* iris/algebra/lib/ufrac_auth.v *)
Lemma ufrac_auth_update_surplus p q a b :
    ✓ (a ⋅ b) → ●U_p a ~~> ●U_(p+q) (a ⋅ b) ⋅ ◯U_q b.
Proof.
    intros Hconsistent. apply: auth_update_alloc. apply local_update_unital.
    intros n mpa; simpl; intros [Hvalid1 Hvalid2] Heq; simplify_eq/=.
    split.
    - split; by apply cmra_valid_validN.
    - rewrite pair_op Some_op Heq comm.
      destruct mpa; simpl; [rewrite left_id | rewrite right_id]; done.
  Qed.
(* iris/algebra/lib/ufrac_auth.v *)
Lemma ufrac_auth_update_surplus_cancel p q a b :
    Cancelable b →
    ●U_(p+q) (a ⋅ b) ⋅ ◯U_q b ~~> ●U_p a.
Proof.
    intros. apply: auth_update_dealloc. apply local_update_unital.
    intros n mpa; simpl; intros [Hvalid1 Hvalid2] Heq; simplify_eq/=.
    split.
    { split; by eapply cmra_validN_op_l. }
    rewrite (comm _ p) (comm _ a) in Heq.
    destruct mpa as [[p' a']|]; simplify_eq/=.
    - rewrite -Some_op in Heq.
      apply (inj _) in Heq as [Hp%leibniz_equiv Ha]; simplify_eq/=.
      apply (inj _) in Hp as ->.
      apply (cancelableN _) in Ha; last by rewrite comm.
      by repeat constructor.
    - rewrite right_id in Heq.
      apply (inj _) in Heq as [Hp%leibniz_equiv _]; simplify_eq/=.
      by apply Qp.add_id_free in Hp.
  Qed.
(* iris/algebra/lib/ufrac_auth.v *)
Definition ufrac_authURF {SI : sidx} (F : rFunctor) : urFunctor
:=
  authURF (optionURF (prodRF (constRF ufracR) F)).
(* iris/algebra/lib/ufrac_auth.v *)
Instance ufrac_authURF_contractive {SI : sidx} F :
  rFunctorContractive F → urFunctorContractive (ufrac_authURF F).
Proof. apply _. Qed.
(* iris/algebra/lib/ufrac_auth.v *)
Definition ufrac_authRF {SI : sidx} (F : rFunctor) : rFunctor
:=
  authRF (optionURF (prodRF (constRF ufracR) F)).
(* iris/algebra/lib/ufrac_auth.v *)
Instance ufrac_authRF_contractive {SI : sidx} F :
  rFunctorContractive F → rFunctorContractive (ufrac_authRF F).
Proof. apply _. Qed.
(* iris/base_logic/bi.v *)
(* [uPred_pure] is a derived notion on [uPred] in terms of [uPred_si_pure].
However, in terms of the BI hierarchy, [bi_pure] it is a primitive notion that
is "below" the concept of an [Sbi], so we cannot use the fact that [uPred] is an
SBI to our advantage here. Below we define [uPred_pure] and derive its laws from
those of [uPred_si_pure]. *)
Definition uPred_pure {M} (φ : Prop) : uPred M
:= uPred_si_pure ⌜ φ ⌝.
(* iris/base_logic/bi.v *)
Definition uPred_emp {M} : uPred M
:= uPred_pure True.
(* iris/base_logic/bi.v *)
Lemma pure_ne {M} n : Proper (iff ==> dist n) (@uPred_pure M).
Proof. intros φ1 φ2 Hφ. apply si_pure_ne. by rewrite Hφ. Qed.
(* iris/base_logic/bi.v *)
Lemma pure_intro {M} (φ : Prop) (P : uPred M) :
  φ → uPred_entails P (uPred_pure φ).
Proof.
  intros. trans (uPred_si_pure (∀ x : False, True) : uPred M).
  - etrans; last apply si_pure_forall_2. by apply forall_intro.
  - by apply si_pure_mono, bi.pure_intro.
Qed.
(* iris/base_logic/bi.v *)
Lemma pure_elim' {M} (φ : Prop) (P : uPred M) :
  (φ → uPred_entails (uPred_pure True) P) →
  uPred_entails (uPred_pure φ) P.
Proof.
  intros HφP. etrans; last apply persistently_elim.
  etrans; last apply si_pure_si_emp_valid.
  apply si_pure_mono. apply bi.pure_elim'=> ?.
  rewrite -(si_emp_valid_si_pure True). by apply si_emp_valid_mono, HφP.
Qed.
(* iris/base_logic/bi.v *)
Lemma uPred_bi_mixin (M : ucmra) :
  BiMixin
    uPred_entails uPred_emp uPred_pure uPred_and uPred_or uPred_impl
    (@uPred_forall M) (@uPred_exist M) uPred_sep uPred_wand.
Proof.
  split.
  - exact: entails_po.
  - exact: equiv_entails.
  - exact: pure_ne.
  - exact: and_ne.
  - exact: or_ne.
  - exact: impl_ne.
  - exact: forall_ne.
  - exact: exist_ne.
  - exact: sep_ne.
  - exact: wand_ne.
  - exact: pure_intro.
  - exact: pure_elim'.
  - exact: and_elim_l.
  - exact: and_elim_r.
  - exact: and_intro.
  - exact: or_intro_l.
  - exact: or_intro_r.
  - exact: or_elim.
  - exact: impl_intro_r.
  - exact: impl_elim_l'.
  - exact: @forall_intro.
  - exact: @forall_elim.
  - exact: @exist_intro.
  - exact: @exist_elim.
  - exact: sep_mono.
  - exact: True_sep_1.
  - exact: True_sep_2.
  - exact: sep_comm'.
  - exact: sep_assoc'.
  - exact: wand_intro_r.
  - exact: wand_elim_l'.
Qed.
(* iris/base_logic/bi.v *)
Lemma uPred_bi_persistently_mixin (M : ucmra) :
  BiPersistentlyMixin
    uPred_entails uPred_emp uPred_and
    (@uPred_exist M) uPred_sep uPred_persistently.
Proof.
  split.
  - exact: persistently_ne.
  - exact: persistently_mono.
  - exact: persistently_idemp_2.
  - (* emp ⊢ <pers> emp (ADMISSIBLE) *)
    trans (uPred_forall (M:=M) (λ _ : False, uPred_persistently uPred_emp)).
    + apply forall_intro=>-[].
    + etrans; first exact: persistently_forall_2.
      by apply persistently_mono, pure_intro.
  - (* ((<pers> P) ∧ (<pers> Q)) ⊢ <pers> (P ∧ Q) (ADMISSIBLE) *)
    intros P Q.
    trans (uPred_forall (M:=M) (λ b : bool, uPred_persistently (if b then P else Q))).
    + apply forall_intro=>[[]].
      * apply and_elim_l.
      * apply and_elim_r.
    + etrans; first exact: persistently_forall_2.
      apply persistently_mono. apply and_intro.
      * etrans; first apply (forall_elim true). done.
      * etrans; first apply (forall_elim false). done.
  - exact: @persistently_exist_1.
  - (* <pers> P ∗ Q ⊢ <pers> P (ADMISSIBLE) *)
    intros. etrans; first exact: sep_comm'.
    etrans; last exact: True_sep_2.
    apply sep_mono; last done. by apply pure_intro.
  - exact: persistently_and_sep_l_1.
Qed.
(* iris/base_logic/bi.v *)
Lemma uPred_bi_later_mixin (M : ucmra) :
  BiLaterMixin
    uPred_entails uPred_pure uPred_or uPred_impl
    (@uPred_forall M) (@uPred_exist M) uPred_sep uPred_persistently uPred_later.
Proof.
  split.
  - apply contractive_ne, later_contractive.
  - exact: later_mono.
  - exact: later_intro.
  - exact: @later_forall_2.
  - exact: @later_exist_false.
  - exact: later_sep_1.
  - exact: later_sep_2.
  - exact: later_persistently_1.
  - exact: later_persistently_2.
  - exact: later_false_em.
Qed.