phanerozoic/Coq-Iris huggingface dataset:
(* iris/algebra/agree.v *)
(* Note that the projection [agree_car] is not non-expansive, so it cannot be
used in the logic. If you need to get a witness out, you should use the
lemma [to_agree_uninjN] instead. In general, [agree_car] should ONLY be used
internally in this file. *)
Record agree (A : Type) : Type
:= {
  agree_car : list A;
  agree_not_nil : bool_decide (agree_car = []) = false
}.
(* iris/algebra/agree.v *)
Coercion agree_car : agree >-> list.
(* iris/algebra/agree.v *)
Definition to_agree {A} (a : A) : agree A
:=
  {| agree_car := [a]; agree_not_nil := eq_refl |}.
(* iris/algebra/agree.v *)
Lemma elem_of_agree {A} (x : agree A) : ∃ a, a ∈ agree_car x.
Proof. destruct x as [[|a ?] ?]; set_solver+. Qed.
(* iris/algebra/agree.v *)
Lemma agree_eq {A} (x y : agree A) : agree_car x = agree_car y → x = y.
Proof.
  destruct x as [a ?], y as [b ?]; simpl.
  intros ->; f_equal. apply (proof_irrel _).
Qed.
(* iris/algebra/agree.v *)
(* OFE *)
Instance agree_dist : Dist (agree A)
:= λ n x y,
  (∀ a, a ∈ agree_car x → ∃ b, b ∈ agree_car y ∧ a ≡{n}≡ b) ∧
  (∀ b, b ∈ agree_car y → ∃ a, a ∈ agree_car x ∧ a ≡{n}≡ b).
(* iris/algebra/agree.v *)
Instance agree_equiv : Equiv (agree A)
:= λ x y, ∀ n, x ≡{n}≡ y.
(* iris/algebra/agree.v *)
Definition agree_ofe_mixin : OfeMixin (agree A).
Proof.
  split.
  - done.
  - intros n; split; rewrite /dist /agree_dist.
    + intros x; split; eauto.
    + intros x y [??]. naive_solver eauto.
    + intros x y z [H1 H1'] [H2 H2']; split.
      * intros a ?. destruct (H1 a) as (b&?&?); auto.
        destruct (H2 b) as (c&?&?); eauto. by exists c; split; last etrans.
      * intros a ?. destruct (H2' a) as (b&?&?); auto.
        destruct (H1' b) as (c&?&?); eauto. by exists c; split; last etrans.
  - intros n m x y [??]; split; naive_solver eauto using dist_le.
Qed.
(* iris/algebra/agree.v *)
Canonical agreeO
:= Ofe (agree A) agree_ofe_mixin.
(* iris/algebra/agree.v *)
(* agree_validN is carefully written such that, when applied to a singleton, it
is convertible to True. This makes working with agreement much more pleasant. *)
Instance agree_validN_instance : ValidN (agree A)
:= λ n x,
  match agree_car x with
  | [a] => True
  | _ => ∀ a b, a ∈ agree_car x → b ∈ agree_car x → a ≡{n}≡ b
  end.
(* iris/algebra/agree.v *)
Instance agree_valid_instance : Valid (agree A)
:= λ x, ∀ n, ✓{n} x.
(* iris/algebra/agree.v *)
Instance agree_op_instance : Op (agree A) := λ x y,
  {| agree_car := agree_car x ++ agree_car y |}.
Next Obligation. by intros [[|??]] y. Qed.
(* iris/algebra/agree.v *)
Instance agree_pcore_instance : PCore (agree A)
:= Some.
(* iris/algebra/agree.v *)
Lemma agree_validN_def n x :
  ✓{n} x ↔ ∀ a b, a ∈ agree_car x → b ∈ agree_car x → a ≡{n}≡ b.
Proof.
  rewrite /validN /agree_validN_instance. destruct (agree_car _) as [|? [|??]]; auto.
  setoid_rewrite list_elem_of_singleton; naive_solver.
Qed.
(* iris/algebra/agree.v *)
Instance agree_comm : Comm (≡) (@op (agree A) _).
Proof. intros x y n; split=> a /=; setoid_rewrite elem_of_app; naive_solver. Qed.
(* iris/algebra/agree.v *)
Instance agree_assoc : Assoc (≡) (@op (agree A) _).
Proof.
  intros x y z n; split=> a /=; repeat setoid_rewrite elem_of_app; naive_solver.
Qed.
(* iris/algebra/agree.v *)
Lemma agree_idemp x : x ⋅ x ≡ x.
Proof. intros n; split=> a /=; setoid_rewrite elem_of_app; naive_solver. Qed.
(* iris/algebra/agree.v *)
Instance agree_validN_ne n :
  Proper (dist n ==> impl) (@validN SI (agree A) _ n).
Proof.
  intros x y [H H']; rewrite /impl !agree_validN_def; intros Hv a b Ha Hb.
  destruct (H' a) as (a'&?&<-); auto. destruct (H' b) as (b'&?&<-); auto.
Qed.
(* iris/algebra/agree.v *)
Instance agree_validN_proper n :
  Proper (equiv ==> iff) (@validN SI (agree A) _ n).
Proof. move=> x y /equiv_dist H. by split; rewrite (H n). Qed.
(* iris/algebra/agree.v *)
Instance agree_op_ne' x : NonExpansive (op x).
Proof.
  intros n y1 y2 [H H']; split=> a /=; setoid_rewrite elem_of_app; naive_solver.
Qed.
(* iris/algebra/agree.v *)
Instance agree_op_ne : NonExpansive2 (@op (agree A) _).
Proof. by intros n x1 x2 Hx y1 y2 Hy; rewrite Hy !(comm _ _ y2) Hx. Qed.
(* iris/algebra/agree.v *)
Instance agree_op_proper : Proper ((≡) ==> (≡) ==> (≡)) (op (A := agree A))
:=
  ne_proper_2 _.
(* iris/algebra/agree.v *)
Lemma agree_included x y : x ≼ y ↔ y ≡ x ⋅ y.
Proof.
  split; [|by intros ?; exists y].
  by intros [z Hz]; rewrite Hz assoc agree_idemp.
Qed.
(* iris/algebra/agree.v *)
Lemma agree_includedN n x y : x ≼{n} y ↔ y ≡{n}≡ x ⋅ y.
Proof.
  split; [|by intros ?; exists y].
  by intros [z Hz]; rewrite Hz assoc agree_idemp.
Qed.
(* iris/algebra/agree.v *)
Lemma agree_op_invN n x1 x2 : ✓{n} (x1 ⋅ x2) → x1 ≡{n}≡ x2.
Proof.
  rewrite agree_validN_def /=. setoid_rewrite elem_of_app=> Hv; split=> a Ha.
  - destruct (elem_of_agree x2); naive_solver.
  - destruct (elem_of_agree x1); naive_solver.
Qed.
(* iris/algebra/agree.v *)
Definition agree_cmra_mixin : CmraMixin (agree A).
Proof.
  apply cmra_total_mixin; try apply _ || by eauto.
  - intros n m x; rewrite !agree_validN_def; eauto using dist_le.
  - intros x. apply agree_idemp.
  - intros n x y; rewrite !agree_validN_def /=.
    setoid_rewrite elem_of_app; naive_solver.
  - intros n x y1 y2 Hval Hx; exists x, x; simpl; split.
    + by rewrite agree_idemp.
    + by move: Hval; rewrite Hx; move=> /agree_op_invN->; rewrite agree_idemp.
Qed.
(* iris/algebra/agree.v *)
Canonical agreeR : cmra
:= Cmra (agree A) agree_cmra_mixin.
(* iris/algebra/agree.v *)
Instance agree_cmra_total : CmraTotal agreeR.
Proof. rewrite /CmraTotal; eauto. Qed.
(* iris/algebra/agree.v *)
Instance agree_core_id x : CoreId x.
Proof. by constructor. Qed.
(* iris/algebra/agree.v *)
Lemma agree_pcore x : pcore x = Some x.
Proof. done. Qed.
(* iris/algebra/agree.v *)
Instance agree_cmra_discrete : OfeDiscrete A → CmraDiscrete agreeR.
Proof.
  intros HD. split.
  - intros x y [H H'] n; split=> a; setoid_rewrite <-(discrete_iff_0 _ _ _); auto.
  - intros x; rewrite agree_validN_def=> Hv n. apply agree_validN_def=> a b ??.
    apply (discrete_iff_0 _ _ _); auto.
Qed.
(* iris/algebra/agree.v *)
Instance to_agree_ne : NonExpansive to_agree.
Proof.
  intros n a1 a2 Hx; split=> b /=;
    setoid_rewrite list_elem_of_singleton; naive_solver.
Qed.
(* iris/algebra/agree.v *)
Instance to_agree_proper : Proper ((≡) ==> (≡)) to_agree
:= ne_proper _.
(* iris/algebra/agree.v *)
Instance to_agree_discrete a : Discrete a → Discrete (to_agree a).
Proof.
  intros ? y [H H'] n; split.
  - intros a' ->%list_elem_of_singleton. destruct (H a) as [b ?]; first by left.
    exists b. by rewrite -discrete_iff_0.
  - intros b Hb. destruct (H' b) as (b'&->%list_elem_of_singleton&?); auto.
    exists a. by rewrite list_elem_of_singleton -discrete_iff_0.
Qed.
(* iris/algebra/agree.v *)
Lemma agree_op_inv x y : ✓ (x ⋅ y) → x ≡ y.
Proof.
  intros ?. apply equiv_dist=> n. by apply agree_op_invN, cmra_valid_validN.
Qed.
(* iris/algebra/agree.v *)
Instance to_agree_injN n : Inj (dist n) (dist n) (to_agree).
Proof.
  move=> a b [_] /=. setoid_rewrite list_elem_of_singleton. naive_solver.
Qed.
(* iris/algebra/agree.v *)
Instance to_agree_inj : Inj (≡) (≡) (to_agree).
Proof. intros a b ?. apply equiv_dist=>n. by apply (inj to_agree), equiv_dist. Qed.
(* iris/algebra/agree.v *)
Lemma to_agree_uninjN n x : ✓{n} x → ∃ a, to_agree a ≡{n}≡ x.
Proof.
  rewrite agree_validN_def=> Hv.
  destruct (elem_of_agree x) as [a ?].
  exists a; split=> b /=; setoid_rewrite list_elem_of_singleton; naive_solver.
Qed.
(* iris/algebra/agree.v *)
Lemma to_agree_uninj x : ✓ x → ∃ a, to_agree a ≡ x.
Proof.
  rewrite /valid /agree_valid_instance; setoid_rewrite agree_validN_def.
  destruct (elem_of_agree x) as [a ?].
  exists a; split=> b /=; setoid_rewrite list_elem_of_singleton; naive_solver.
Qed.
(* iris/algebra/agree.v *)
Lemma agree_valid_includedN n x y : ✓{n} y → x ≼{n} y → x ≡{n}≡ y.
Proof.
  move=> Hval [z Hy]; move: Hval; rewrite Hy.
  by move=> /agree_op_invN->; rewrite agree_idemp.
Qed.
(* iris/algebra/agree.v *)
Lemma agree_valid_included x y : ✓ y → x ≼ y → x ≡ y.
Proof.
  move=> Hval [z Hy]; move: Hval; rewrite Hy.
  by move=> /agree_op_inv->; rewrite agree_idemp.
Qed.
(* iris/algebra/agree.v *)
Lemma to_agree_includedN n a b : to_agree a ≼{n} to_agree b ↔ a ≡{n}≡ b.
Proof.
  split; last by intros ->.
  intros. by apply (inj to_agree), agree_valid_includedN.
Qed.
(* iris/algebra/agree.v *)
Lemma to_agree_included a b : to_agree a ≼ to_agree b ↔ a ≡ b.
Proof.
  split; last by intros ->.
  intros. by apply (inj to_agree), agree_valid_included.
Qed.
(* iris/algebra/agree.v *)
Lemma to_agree_included_L `{!LeibnizEquiv A}  a b : to_agree a ≼ to_agree b ↔ a = b.
Proof. unfold_leibniz. apply to_agree_included. Qed.
(* iris/algebra/agree.v *)
Instance agree_cancelable x : Cancelable x.
Proof.
  intros n y z Hv Heq.
  destruct (to_agree_uninjN n x) as [x' EQx]; first by eapply cmra_validN_op_l.
  destruct (to_agree_uninjN n y) as [y' EQy]; first by eapply cmra_validN_op_r.
  destruct (to_agree_uninjN n z) as [z' EQz].
  { eapply (cmra_validN_op_r n x z). by rewrite -Heq. }
  assert (Hx'y' : x' ≡{n}≡ y').
  { apply (inj to_agree), agree_op_invN. by rewrite EQx EQy. }
  assert (Hx'z' : x' ≡{n}≡ z').
  { apply (inj to_agree), agree_op_invN. by rewrite EQx EQz -Heq. }
  by rewrite -EQy -EQz -Hx'y' -Hx'z'.
Qed.
(* iris/algebra/agree.v *)
Lemma to_agree_op_invN a b n : ✓{n} (to_agree a ⋅ to_agree b) → a ≡{n}≡ b.
Proof. by intros ?%agree_op_invN%(inj to_agree). Qed.
(* iris/algebra/agree.v *)
Lemma to_agree_op_inv a b : ✓ (to_agree a ⋅ to_agree b) → a ≡ b.
Proof. by intros ?%agree_op_inv%(inj to_agree). Qed.
(* iris/algebra/agree.v *)
Lemma to_agree_op_inv_L `{!LeibnizEquiv A} a b : ✓ (to_agree a ⋅ to_agree b) → a = b.
Proof. by intros ?%to_agree_op_inv%leibniz_equiv. Qed.
(* iris/algebra/agree.v *)
Lemma to_agree_op_validN a b n : ✓{n} (to_agree a ⋅ to_agree b) ↔ a ≡{n}≡ b.
Proof.
  split; first by apply to_agree_op_invN.
  intros ->. rewrite agree_idemp //.
Qed.
(* iris/algebra/agree.v *)
Lemma to_agree_op_valid a b : ✓ (to_agree a ⋅ to_agree b) ↔ a ≡ b.
Proof.
  split; first by apply to_agree_op_inv.
  intros ->. rewrite agree_idemp //.
Qed.
(* iris/algebra/agree.v *)
Lemma to_agree_op_valid_L `{!LeibnizEquiv A} a b : ✓ (to_agree a ⋅ to_agree b) ↔ a = b.
Proof. rewrite to_agree_op_valid. by fold_leibniz. Qed.
(* iris/algebra/agree.v *)
Instance : Params (@to_agree) 1
:= {}.
(* iris/algebra/agree.v *)
Definition agree_map {A B} (f : A → B) (x : agree A) : agree B :=
  {| agree_car := f <$> agree_car x |}.
Next Obligation. by intros A B f [[|??] ?]. Qed.
(* iris/algebra/agree.v *)
Lemma agree_map_id {A} (x : agree A) : agree_map id x = x.
Proof. apply agree_eq. by rewrite /= list_fmap_id. Qed.
(* iris/algebra/agree.v *)
Lemma agree_map_compose {A B C} (f : A → B) (g : B → C) (x : agree A) :
  agree_map (g ∘ f) x = agree_map g (agree_map f x).
Proof. apply agree_eq. by rewrite /= list_fmap_compose. Qed.
(* iris/algebra/agree.v *)
Lemma agree_map_to_agree {A B} (f : A → B) (x : A) :
  agree_map f (to_agree x) = to_agree (f x).
Proof. by apply agree_eq. Qed.
(* iris/algebra/agree.v *)
Instance agree_map_ne : NonExpansive (agree_map f).
Proof using Type*.
    intros n x y [H H']; split=> b /=; setoid_rewrite list_elem_of_fmap.
    - intros (a&->&?). destruct (H a) as (a'&?&?); auto. naive_solver.
    - intros (a&->&?). destruct (H' a) as (a'&?&?); auto. naive_solver.
  Qed.
(* iris/algebra/agree.v *)
Instance agree_map_proper : Proper ((≡) ==> (≡)) (agree_map f)
:= ne_proper _.
(* iris/algebra/agree.v *)
Lemma agree_map_ext (g : A → B) x :
    (∀ a, f a ≡ g a) → agree_map f x ≡ agree_map g x.
Proof using Hf.
    intros Hfg n; split=> b /=; setoid_rewrite list_elem_of_fmap.
    - intros (a&->&?). exists (g a). rewrite Hfg; eauto.
    - intros (a&->&?). exists (f a). rewrite -Hfg; eauto.
  Qed.
(* iris/algebra/agree.v *)
Instance agree_map_morphism : CmraMorphism (agree_map f).
Proof using Hf.
    split; first apply _.
    - intros n x. rewrite !agree_validN_def=> Hv b b' /=.
      intros (a&->&?)%list_elem_of_fmap (a'&->&?)%list_elem_of_fmap.
      apply Hf; eauto.
    - done.
    - intros x y n; split=> b /=;
        rewrite !fmap_app; setoid_rewrite elem_of_app; eauto.
  Qed.
(* iris/algebra/agree.v *)
Definition agreeO_map {SI : sidx} {A B : ofe}
    (f : A -n> B) : agreeO A -n> agreeO B
:=
  OfeMor (agree_map f : agreeO A → agreeO B).
(* iris/algebra/agree.v *)
Instance agreeO_map_ne {SI : sidx} A B : NonExpansive (@agreeO_map SI A B).
Proof.
  intros n f g Hfg x; split=> b /=;
    setoid_rewrite list_elem_of_fmap; naive_solver.
Qed.
(* iris/algebra/agree.v *)
Definition agreeRF {SI : sidx} (F : oFunctor) : rFunctor := {|
  rFunctor_car A _ B _ := agreeR (oFunctor_car F A B);
  rFunctor_map A1 _ A2 _ B1 _ B2 _ fg := agreeO_map (oFunctor_map F fg)
|}.
Next Obligation.
  intros ? ? A1 ? A2 ? B1 ? B2 ? n ???; simpl.
  by apply agreeO_map_ne, oFunctor_map_ne.
Qed.
(* iris/algebra/agree.v *)
Instance agreeRF_contractive {SI : sidx} F :
  oFunctorContractive F → rFunctorContractive (agreeRF F).
Proof.
  intros ? A1 ? A2 ? B1 ? B2 ? n ???; simpl.
  by apply agreeO_map_ne, oFunctor_map_contractive.
Qed.
(* iris/algebra/auth.v *)
(* The authoritative camera is obtained by instantiating the view camera. *)
Definition auth_view_rel_raw {SI : sidx} {A : ucmra} (n : SI) (a b : A) : Prop
:=
  b ≼{n} a ∧ ✓{n} a.
(* iris/algebra/auth.v *)
Lemma auth_view_rel_raw_mono {SI : sidx} (A : ucmra) n1 n2 (a1 a2 b1 b2 : A) :
  auth_view_rel_raw n1 a1 b1 →
  a1 ≡{n2}≡ a2 →
  b2 ≼{n2} b1 →
  (n2 ≤ n1)%sidx →
  auth_view_rel_raw n2 a2 b2.
Proof.
  intros [??] Ha12 ??. split.
  - trans b1; [done|]. rewrite -Ha12. by apply cmra_includedN_le with n1.
  - rewrite -Ha12. by apply cmra_validN_le with n1.
Qed.
(* iris/algebra/auth.v *)
Lemma auth_view_rel_raw_valid {SI : sidx} (A : ucmra) n (a b : A) :
  auth_view_rel_raw n a b → ✓{n} b.
Proof. intros [??]; eauto using cmra_validN_includedN. Qed.
(* iris/algebra/auth.v *)
Lemma auth_view_rel_raw_unit {SI : sidx} (A : ucmra) n :
  ∃ a : A, auth_view_rel_raw n a ε.
Proof. exists ε. split; [done|]. apply ucmra_unit_validN. Qed.
(* iris/algebra/auth.v *)
Canonical auth_view_rel {SI : sidx} {A : ucmra} : view_rel A A
:=
  ViewRel auth_view_rel_raw (auth_view_rel_raw_mono A)
          (auth_view_rel_raw_valid A) (auth_view_rel_raw_unit A).
(* iris/algebra/auth.v *)
Lemma auth_view_rel_unit {SI : sidx} {A : ucmra} n (a : A) :
  auth_view_rel n a ε ↔ ✓{n} a.
Proof. split; [by intros [??]|]. split; auto using ucmra_unit_leastN. Qed.
(* iris/algebra/auth.v *)
Lemma auth_view_rel_exists {SI : sidx} {A : ucmra} n (b : A) :
  (∃ a, auth_view_rel n a b) ↔ ✓{n} b.
Proof.
  split; [|intros; exists b; by split].
  intros [a Hrel]. eapply auth_view_rel_raw_valid, Hrel.
Qed.
(* iris/algebra/auth.v *)
Instance auth_view_rel_discrete {SI : sidx} {A : ucmra} :
  CmraDiscrete A → ViewRelDiscrete (auth_view_rel (A:=A)).
Proof.
  intros ? n a b [??]; split.
  - by apply cmra_discrete_included_iff_0.
  - by apply cmra_discrete_valid_iff_0.
Qed.
(* iris/algebra/auth.v *)
(* The type [auth] is not defined as a [Definition], but as a [Notation].
This way, one can use [auth A] with [A : Type] instead of [A : ucmra], and let
canonical structure search determine the corresponding camera instance. *)
Notation auth A
:= (view (A:=A) (B:=A) auth_view_rel_raw).
(* iris/algebra/auth.v *)
Definition authO {SI : sidx} (A : ucmra) : ofe
:=
  viewO (A:=A) (B:=A) auth_view_rel.
(* iris/algebra/auth.v *)
Definition authR {SI : sidx} (A : ucmra) : cmra
:=
  viewR (A:=A) (B:=A) auth_view_rel.
(* iris/algebra/auth.v *)
Definition authUR {SI : sidx} (A : ucmra) : ucmra
:=
  viewUR (A:=A) (B:=A) auth_view_rel.
(* iris/algebra/auth.v *)
Definition auth_auth {SI : sidx} {A: ucmra} : dfrac → A → auth A
:= view_auth.
(* iris/algebra/auth.v *)
Definition auth_frag {SI : sidx} {A: ucmra} : A → auth A
:= view_frag.
(* iris/algebra/auth.v *)
Instance : Params (@auth_auth) 3
:= {}.
(* iris/algebra/auth.v *)
Instance : Params (@auth_frag) 2
:= {}.
(* iris/algebra/auth.v *)
Notation "● dq a"
:= (auth_auth dq a)
  (at level 20, dq custom dfrac at level 1, format "● dq  a").
(* iris/algebra/auth.v *)
Notation "◯ a"
:= (auth_frag a) (at level 20).
(* iris/algebra/auth.v *)
Instance auth_auth_ne dq : NonExpansive (@auth_auth SI A dq).
Proof. rewrite /auth_auth. apply _. Qed.
(* iris/algebra/auth.v *)
Instance auth_auth_proper dq : Proper ((≡) ==> (≡)) (@auth_auth SI A dq).
Proof. rewrite /auth_auth. apply _. Qed.
(* iris/algebra/auth.v *)
Instance auth_frag_ne : NonExpansive (@auth_frag SI A).
Proof. rewrite /auth_frag. apply _. Qed.
(* iris/algebra/auth.v *)
Instance auth_frag_proper : Proper ((≡) ==> (≡)) (@auth_frag SI A).
Proof. rewrite /auth_frag. apply _. Qed.
(* iris/algebra/auth.v *)
Instance auth_auth_dist_inj n :
    Inj2 (=) (dist n) (dist n) (@auth_auth SI A).
Proof. rewrite /auth_auth. apply _. Qed.
(* iris/algebra/auth.v *)
Instance auth_auth_inj : Inj2 (=) (≡) (≡) (@auth_auth SI A).
Proof. rewrite /auth_auth. apply _. Qed.
(* iris/algebra/auth.v *)
Instance auth_frag_dist_inj n : Inj (dist n) (dist n) (@auth_frag SI A).
Proof. rewrite /auth_frag. apply _. Qed.
(* iris/algebra/auth.v *)
Instance auth_frag_inj : Inj (≡) (≡) (@auth_frag SI A).
Proof. rewrite /auth_frag. apply _. Qed.
(* iris/algebra/auth.v *)
Instance auth_ofe_discrete : OfeDiscrete A → OfeDiscrete (authO A).
Proof. apply _. Qed.
(* iris/algebra/auth.v *)
Instance auth_auth_discrete dq a :
    Discrete a → Discrete (ε : A) → Discrete (●{dq} a).
Proof. rewrite /auth_auth. apply _. Qed.
(* iris/algebra/auth.v *)
Instance auth_frag_discrete a : Discrete a → Discrete (◯ a).
Proof. rewrite /auth_frag. apply _. Qed.
(* iris/algebra/auth.v *)
Instance auth_cmra_discrete : CmraDiscrete A → CmraDiscrete (authR A).
Proof. apply _. Qed.
(* iris/algebra/auth.v *)
(* Operation *)
Lemma auth_auth_dfrac_op dq1 dq2 a : ●{dq1 ⋅ dq2} a ≡ ●{dq1} a ⋅ ●{dq2} a.
Proof. apply view_auth_dfrac_op. Qed.
(* iris/algebra/auth.v *)
Instance auth_auth_dfrac_is_op dq dq1 dq2 a :
    IsOp dq dq1 dq2 → IsOp' (●{dq} a) (●{dq1} a) (●{dq2} a).
Proof. rewrite /auth_auth. apply _. Qed.
(* iris/algebra/auth.v *)
Lemma auth_frag_op a b : ◯ (a ⋅ b) = ◯ a ⋅ ◯ b.
Proof. apply view_frag_op. Qed.
(* iris/algebra/auth.v *)
Lemma auth_frag_mono a b : a ≼ b → ◯ a ≼ ◯ b.
Proof. apply view_frag_mono. Qed.
(* iris/algebra/auth.v *)
Lemma auth_frag_core a : core (◯ a) = ◯ (core a).
Proof. apply view_frag_core. Qed.
(* iris/algebra/auth.v *)
Lemma auth_both_core_discarded a b :
    core (●□ a ⋅ ◯ b) ≡ ●□ a ⋅ ◯ (core b).
Proof. apply view_both_core_discarded. Qed.
(* iris/algebra/auth.v *)
Lemma auth_both_core_frac q a b :
    core (●{#q} a ⋅ ◯ b) ≡ ◯ (core b).
Proof. apply view_both_core_frac. Qed.
(* iris/algebra/auth.v *)
Instance auth_auth_core_id a : CoreId (●□ a).
Proof. rewrite /auth_auth. apply _. Qed.
(* iris/algebra/auth.v *)
Instance auth_frag_core_id a : CoreId a → CoreId (◯ a).
Proof. rewrite /auth_frag. apply _. Qed.
(* iris/algebra/auth.v *)
Instance auth_both_core_id a1 a2 : CoreId a2 → CoreId (●□ a1 ⋅ ◯ a2).
Proof. rewrite /auth_auth /auth_frag. apply _. Qed.
(* iris/algebra/auth.v *)
Instance auth_frag_is_op a b1 b2 :
    IsOp a b1 b2 → IsOp' (◯ a) (◯ b1) (◯ b2).
Proof. rewrite /auth_frag. apply _. Qed.
(* iris/algebra/auth.v *)
Instance auth_frag_sep_homomorphism :
    MonoidHomomorphism op op (≡) (@auth_frag SI A).
Proof. rewrite /auth_frag. apply _. Qed.
(* iris/algebra/auth.v *)
Lemma big_opL_auth_frag {B} (g : nat → B → A) (l : list B) :
    (◯ [^op list] k↦x ∈ l, g k x) ≡ [^op list] k↦x ∈ l, ◯ (g k x).
Proof. apply (big_opL_commute _). Qed.
(* iris/algebra/auth.v *)
Lemma big_opM_auth_frag `{Countable K} {B} (g : K → B → A) (m : gmap K B) :
    (◯ [^op map] k↦x ∈ m, g k x) ≡ [^op map] k↦x ∈ m, ◯ (g k x).
Proof. apply (big_opM_commute _). Qed.
(* iris/algebra/auth.v *)
Lemma big_opS_auth_frag `{Countable B} (g : B → A) (X : gset B) :
    (◯ [^op set] x ∈ X, g x) ≡ [^op set] x ∈ X, ◯ (g x).
Proof. apply (big_opS_commute _). Qed.
(* iris/algebra/auth.v *)
Lemma big_opMS_auth_frag `{Countable B} (g : B → A) (X : gmultiset B) :
    (◯ [^op mset] x ∈ X, g x) ≡ [^op mset] x ∈ X, ◯ (g x).
Proof. apply (big_opMS_commute _). Qed.
(* iris/algebra/auth.v *)
(* Validity *)
Lemma auth_auth_dfrac_op_invN n dq1 a dq2 b : ✓{n} (●{dq1} a ⋅ ●{dq2} b) → a ≡{n}≡ b.
Proof. apply view_auth_dfrac_op_invN. Qed.
(* iris/algebra/auth.v *)
Lemma auth_auth_dfrac_op_inv dq1 a dq2 b : ✓ (●{dq1} a ⋅ ●{dq2} b) → a ≡ b.
Proof. apply view_auth_dfrac_op_inv. Qed.
(* iris/algebra/auth.v *)
Lemma auth_auth_dfrac_op_inv_L `{!LeibnizEquiv A} dq1 a dq2 b :
    ✓ (●{dq1} a ⋅ ●{dq2} b) → a = b.
Proof. by apply view_auth_dfrac_op_inv_L. Qed.
(* iris/algebra/auth.v *)
Lemma auth_auth_dfrac_validN n dq a : ✓{n} (●{dq} a) ↔ ✓ dq ∧ ✓{n} a.
Proof. by rewrite view_auth_dfrac_validN auth_view_rel_unit. Qed.
(* iris/algebra/auth.v *)
Lemma auth_auth_validN n a : ✓{n} (● a) ↔ ✓{n} a.
Proof. by rewrite view_auth_validN auth_view_rel_unit. Qed.
(* iris/algebra/auth.v *)
Lemma auth_auth_dfrac_op_validN n dq1 dq2 a1 a2 :
    ✓{n} (●{dq1} a1 ⋅ ●{dq2} a2) ↔  ✓ (dq1 ⋅ dq2) ∧ a1 ≡{n}≡ a2 ∧ ✓{n} a1.
Proof. by rewrite view_auth_dfrac_op_validN auth_view_rel_unit. Qed.
(* iris/algebra/auth.v *)
Lemma auth_auth_op_validN n a1 a2 : ✓{n} (● a1 ⋅ ● a2) ↔ False.
Proof. apply view_auth_op_validN. Qed.
(* iris/algebra/auth.v *)
(* The following lemmas are also stated as implications, which can be used
  to force [apply] to use the lemma in the right direction. *)
Lemma auth_frag_validN n b : ✓{n} (◯ b) ↔ ✓{n} b.
Proof. by rewrite view_frag_validN auth_view_rel_exists. Qed.
(* iris/algebra/auth.v *)
Lemma auth_frag_validN_1 n b : ✓{n} (◯ b) → ✓{n} b.
Proof. apply auth_frag_validN. Qed.
(* iris/algebra/auth.v *)
Lemma auth_frag_validN_2 n b : ✓{n} b → ✓{n} (◯ b).
Proof. apply auth_frag_validN. Qed.
(* iris/algebra/auth.v *)
Lemma auth_frag_op_validN n b1 b2 : ✓{n} (◯ b1 ⋅ ◯ b2) ↔ ✓{n} (b1 ⋅ b2).
Proof. apply auth_frag_validN. Qed.
(* iris/algebra/auth.v *)
Lemma auth_frag_op_validN_1 n b1 b2 : ✓{n} (◯ b1 ⋅ ◯ b2) → ✓{n} (b1 ⋅ b2).
Proof. apply auth_frag_op_validN. Qed.
(* iris/algebra/auth.v *)
Lemma auth_frag_op_validN_2 n b1 b2 : ✓{n} (b1 ⋅ b2) → ✓{n} (◯ b1 ⋅ ◯ b2).
Proof. apply auth_frag_op_validN. Qed.
(* iris/algebra/auth.v *)
Lemma auth_both_dfrac_validN n dq a b :
    ✓{n} (●{dq} a ⋅ ◯ b) ↔ ✓ dq ∧ b ≼{n} a ∧ ✓{n} a.
Proof. apply view_both_dfrac_validN. Qed.
(* iris/algebra/auth.v *)
Lemma auth_both_validN n a b : ✓{n} (● a ⋅ ◯ b) ↔ b ≼{n} a ∧ ✓{n} a.
Proof. apply view_both_validN. Qed.
(* iris/algebra/auth.v *)
Lemma auth_auth_dfrac_valid dq a : ✓ (●{dq} a) ↔ ✓ dq ∧ ✓ a.
Proof.
    rewrite view_auth_dfrac_valid !cmra_valid_validN.
    by setoid_rewrite auth_view_rel_unit.
  Qed.
(* iris/algebra/auth.v *)
Lemma auth_auth_valid a : ✓ (● a) ↔ ✓ a.
Proof.
    rewrite view_auth_valid !cmra_valid_validN.
    by setoid_rewrite auth_view_rel_unit.
  Qed.
(* iris/algebra/auth.v *)
Lemma auth_auth_dfrac_op_valid dq1 dq2 a1 a2 :
    ✓ (●{dq1} a1 ⋅ ●{dq2} a2) ↔ ✓ (dq1 ⋅ dq2) ∧ a1 ≡ a2 ∧ ✓ a1.
Proof.
    rewrite view_auth_dfrac_op_valid !cmra_valid_validN.
    setoid_rewrite auth_view_rel_unit. done.
  Qed.
(* iris/algebra/auth.v *)
Lemma auth_auth_op_valid a1 a2 : ✓ (● a1 ⋅ ● a2) ↔ False.
Proof. apply view_auth_op_valid. Qed.
(* iris/algebra/auth.v *)
(* The following lemmas are also stated as implications, which can be used
  to force [apply] to use the lemma in the right direction. *)
Lemma auth_frag_valid b : ✓ (◯ b) ↔ ✓ b.
Proof.
    rewrite view_frag_valid cmra_valid_validN.
    by setoid_rewrite auth_view_rel_exists.
  Qed.
(* iris/algebra/auth.v *)
Lemma auth_frag_valid_1 b : ✓ (◯ b) → ✓ b.
Proof. apply auth_frag_valid. Qed.
(* iris/algebra/auth.v *)
Lemma auth_frag_valid_2 b : ✓ b → ✓ (◯ b).
Proof. apply auth_frag_valid. Qed.
(* iris/algebra/auth.v *)
Lemma auth_frag_op_valid b1 b2 : ✓ (◯ b1 ⋅ ◯ b2) ↔ ✓ (b1 ⋅ b2).
Proof. apply auth_frag_valid. Qed.
(* iris/algebra/auth.v *)
Lemma auth_frag_op_valid_1 b1 b2 : ✓ (◯ b1 ⋅ ◯ b2) → ✓ (b1 ⋅ b2).
Proof. apply auth_frag_op_valid. Qed.
(* iris/algebra/auth.v *)
Lemma auth_frag_op_valid_2 b1 b2 : ✓ (b1 ⋅ b2) → ✓ (◯ b1 ⋅ ◯ b2).
Proof. apply auth_frag_op_valid. Qed.