phanerozoic/Coq-Iris huggingface dataset:
(* iris/algebra/vector.v *)
Instance vec_to_list_proper m : Proper ((≡) ==> (≡)) (@vec_to_list A m).
Proof. by intros v v'. Qed.
(* iris/algebra/vector.v *)
(* Functor *)
Definition vec_map {SI : sidx} {A B : ofe} m (f : A → B) : vecO A m → vecO B m
:=
  @vmap A B f m.
(* iris/algebra/vector.v *)
Lemma vec_map_ext_ne {SI : sidx} {A B : ofe} m (f g : A → B) (v : vec A m) n :
  (∀ x, f x ≡{n}≡ g x) → vec_map m f v ≡{n}≡ vec_map m g v.
Proof.
  intros Hf. eapply (list_fmap_ext_ne f g v) in Hf.
  by rewrite -!vec_to_list_map in Hf.
Qed.
(* iris/algebra/vector.v *)
Instance vec_map_ne {SI : sidx} {A B : ofe} m f n :
  Proper (dist n ==> dist n) f →
  Proper (dist n ==> dist n) (@vec_map SI A B m f).
Proof.
  intros ? v v' H. eapply list_fmap_ne in H; last done.
  by rewrite -!vec_to_list_map in H.
Qed.
(* iris/algebra/vector.v *)
Definition vecO_map {SI : sidx} {A B : ofe} m (f : A -n> B) : vecO A m -n> vecO B m
:=
  OfeMor (vec_map m f).
(* iris/algebra/vector.v *)
Instance vecO_map_ne {SI : sidx} {A A'} m :
  NonExpansive (@vecO_map SI A A' m).
Proof. intros n f g ? v. by apply vec_map_ext_ne. Qed.
(* iris/algebra/vector.v *)
Definition vecOF {SI : sidx} (F : oFunctor) m : oFunctor := {|
  oFunctor_car A _ B _ := vecO (oFunctor_car F A B) m;
  oFunctor_map A1 _ A2 _ B1 _ B2 _ fg := vecO_map m (oFunctor_map F fg)
|}.
Next Obligation.
  intros ? F A1 ? A2 ? B1 ? B2 ? n m f g Hfg. by apply vecO_map_ne, oFunctor_map_ne.
Qed.
(* iris/algebra/vector.v *)
Instance vecOF_contractive {SI : sidx} F m :
  oFunctorContractive F → oFunctorContractive (vecOF F m).
Proof.
  by intros ?? A1 ? A2 ? B1 ? B2 ? n ???; apply vecO_map_ne;
    apply oFunctor_map_contractive.
Qed.
(* iris/algebra/view.v *)
(* To relate the authoritative element [a] to its possible fragments [b], the
view camera is parametrized by a (step-indexed) relation [view_rel n a b]. This
relation should be a.) closed under smaller step-indexes [n], b.) non-expansive
w.r.t. the argument [a], c.) closed under smaller [b] (which implies
non-expansiveness w.r.t. [b]), and d.) ensure validity of the argument [b].

Note 1: Instead of requiring both a step-indexed and a non-step-indexed version
of the relation (like cameras do for validity), we use [∀ n, view_rel n] as the
non-step-indexed version. This is anyway necessary when using [≼{n}] as the
relation (like the authoritative camera does) as its non-step-indexed version
is not equivalent to [∀ n, x ≼{n} y].

Note 2: The view relation is defined as a canonical structure so that given a
relation [nat → A → B → Prop], the instance with the laws can be inferred. We do
not use type classes for this purpose because cameras themselves are represented
using canonical structures. It has proven fragile for a canonical structure
instance to take a type class as a parameter (in this case, [viewR] would need
to take a class with the view relation laws). *)
Structure view_rel {SI : sidx} (A : ofe) (B : ucmra)
:= ViewRel {
  view_rel_holds :> SI → A → B → Prop;
  view_rel_mono n1 n2 a1 a2 b1 b2 :
    view_rel_holds n1 a1 b1 →
    a1 ≡{n2}≡ a2 →
    b2 ≼{n2} b1 →
    (n2 ≤ n1)%sidx →
    view_rel_holds n2 a2 b2;
  view_rel_validN n a b :
    view_rel_holds n a b → ✓{n} b;
  view_rel_unit n :
    ∃ a, view_rel_holds n a ε
}.
(* iris/algebra/view.v *)
Instance : Params (@view_rel_holds) 5
:= {}.
(* iris/algebra/view.v *)
Instance view_rel_ne {SI : sidx} {A B} (rel : view_rel A B) n :
  Proper (dist n ==> dist n ==> iff) (rel n).
Proof.
  intros a1 a2 Ha b1 b2 Hb.
  split=> ?; (eapply view_rel_mono; [done|done|by rewrite Hb|done]).
Qed.
(* iris/algebra/view.v *)
Instance view_rel_proper {SI : sidx} {A B} (rel : view_rel A B) n :
  Proper ((≡) ==> (≡) ==> iff) (rel n).
Proof. intros a1 a2 Ha b1 b2 Hb. apply view_rel_ne; by apply equiv_dist. Qed.
(* iris/algebra/view.v *)
Class ViewRelDiscrete {SI : sidx} {A B} (rel : view_rel A B)
:=
  view_rel_discrete n a b : rel 0ᵢ a b → rel n a b.
(* iris/algebra/view.v *)
(* To make use of the lemmas provided in this file, elements of [view] should
always be constructed using [●V] and [◯V], and never using the constructor
[View]. *)
Record view {SI : sidx} {A B} (rel : SI → A → B → Prop)
:=
  View { view_auth_proj : option (dfrac * agree A) ; view_frag_proj : B }.
(* iris/algebra/view.v *)
Instance : Params (@View) 4
:= {}.
(* iris/algebra/view.v *)
Instance : Params (@view_auth_proj) 4
:= {}.
(* iris/algebra/view.v *)
Instance : Params (@view_frag_proj) 4
:= {}.
(* iris/algebra/view.v *)
Definition view_auth {SI : sidx} {A B} {rel : view_rel A B}
    (dq : dfrac) (a : A) : view rel
:=
  View (Some (dq, to_agree a)) ε.
(* iris/algebra/view.v *)
Definition view_frag {SI : sidx} {A B} {rel : view_rel A B} (b : B) : view rel
:=
  View None b.
(* iris/algebra/view.v *)
Instance : Params (@view_auth) 4
:= {}.
(* iris/algebra/view.v *)
Instance : Params (@view_frag) 4
:= {}.
(* iris/algebra/view.v *)
Notation "●V dq a"
:= (view_auth dq a)
  (at level 20, dq custom dfrac at level 1, format "●V dq  a").
(* iris/algebra/view.v *)
Notation "◯V a"
:= (view_frag a) (at level 20).
(* iris/algebra/view.v *)
Instance view_equiv : Equiv (view rel)
:= λ x y,
    view_auth_proj x ≡ view_auth_proj y ∧ view_frag_proj x ≡ view_frag_proj y.
(* iris/algebra/view.v *)
Instance view_dist : Dist (view rel)
:= λ n x y,
    view_auth_proj x ≡{n}≡ view_auth_proj y ∧
    view_frag_proj x ≡{n}≡ view_frag_proj y.
(* iris/algebra/view.v *)
Instance View_ne : NonExpansive2 (@View SI A B rel).
Proof. by split. Qed.
(* iris/algebra/view.v *)
Instance View_proper : Proper ((≡) ==> (≡) ==> (≡)) (@View SI A B rel).
Proof. by split. Qed.
(* iris/algebra/view.v *)
Instance view_auth_proj_ne : NonExpansive (@view_auth_proj SI A B rel).
Proof. by destruct 1. Qed.
(* iris/algebra/view.v *)
Instance view_auth_proj_proper :
    Proper ((≡) ==> (≡)) (@view_auth_proj SI A B rel).
Proof. by destruct 1. Qed.
(* iris/algebra/view.v *)
Instance view_frag_proj_ne : NonExpansive (@view_frag_proj SI A B rel).
Proof. by destruct 1. Qed.
(* iris/algebra/view.v *)
Instance view_frag_proj_proper :
    Proper ((≡) ==> (≡)) (@view_frag_proj SI A B rel).
Proof. by destruct 1. Qed.
(* iris/algebra/view.v *)
Definition view_ofe_mixin : OfeMixin (view rel).
Proof. by apply (iso_ofe_mixin (λ x, (view_auth_proj x, view_frag_proj x))). Qed.
(* iris/algebra/view.v *)
Canonical viewO
:= Ofe (view rel) view_ofe_mixin.
(* iris/algebra/view.v *)
Instance View_discrete ag b :
    Discrete ag → Discrete b → Discrete (View ag b).
Proof. by intros ?? [??] [??]; split; apply: discrete. Qed.
(* iris/algebra/view.v *)
Instance view_ofe_discrete :
    OfeDiscrete A → OfeDiscrete B → OfeDiscrete viewO.
Proof. intros ?? [??]; apply _. Qed.
(* iris/algebra/view.v *)
Instance view_auth_ne dq : NonExpansive (@view_auth SI A B rel dq).
Proof. solve_proper. Qed.
(* iris/algebra/view.v *)
Instance view_auth_proper dq :
    Proper ((≡) ==> (≡)) (@view_auth SI A B rel dq).
Proof. solve_proper. Qed.
(* iris/algebra/view.v *)
Instance view_frag_ne : NonExpansive (@view_frag SI A B rel).
Proof. done. Qed.
(* iris/algebra/view.v *)
Instance view_frag_proper : Proper ((≡) ==> (≡)) (@view_frag SI A B rel).
Proof. done. Qed.
(* iris/algebra/view.v *)
Instance view_auth_dist_inj n :
    Inj2 (=) (dist n) (dist n) (@view_auth SI A B rel).
Proof.
    intros dq1 a1 dq2 a2 [Hag ?]; inversion Hag as [?? [??]|]; simplify_eq/=.
    split; [done|]. by apply (inj to_agree).
  Qed.
(* iris/algebra/view.v *)
Instance view_auth_inj : Inj2 (=) (≡) (≡) (@view_auth SI A B rel).
Proof.
    intros dq1 a1 dq2 a2 [Hag ?]; inversion Hag as [?? [??]|]; simplify_eq/=.
    split; [done|]. by apply (inj to_agree).
  Qed.
(* iris/algebra/view.v *)
Instance view_frag_dist_inj n :
    Inj (dist n) (dist n) (@view_frag SI A B rel).
Proof. by intros ?? [??]. Qed.
(* iris/algebra/view.v *)
Instance view_frag_inj : Inj (≡) (≡) (@view_frag SI A B rel).
Proof. by intros ?? [??]. Qed.
(* iris/algebra/view.v *)
Instance view_valid_instance : Valid (view rel)
:= λ x,
    match view_auth_proj x with
    | Some (dq, ag) =>
       ✓ dq ∧ (∀ n, ∃ a, ag ≡{n}≡ to_agree a ∧ rel n a (view_frag_proj x))
    | None => ∀ n, ∃ a, rel n a (view_frag_proj x)
    end.
(* iris/algebra/view.v *)
Instance view_validN_instance : ValidN (view rel)
:= λ n x,
    match view_auth_proj x with
    | Some (dq, ag) =>
       ✓{n} dq ∧ ∃ a, ag ≡{n}≡ to_agree a ∧ rel n a (view_frag_proj x)
    | None => ∃ a, rel n a (view_frag_proj x)
    end.
(* iris/algebra/view.v *)
Instance view_pcore_instance : PCore (view rel)
:= λ x,
    Some (View (core (view_auth_proj x)) (core (view_frag_proj x))).
(* iris/algebra/view.v *)
Instance view_op_instance : Op (view rel)
:= λ x y,
    View (view_auth_proj x ⋅ view_auth_proj y) (view_frag_proj x ⋅ view_frag_proj y).
(* iris/algebra/view.v *)
Definition view_valid_eq :
    valid = λ x,
      match view_auth_proj x with
      | Some (dq, ag) =>
         ✓ dq ∧ (∀ n, ∃ a, ag ≡{n}≡ to_agree a ∧ rel n a (view_frag_proj x))
      | None => ∀ n, ∃ a, rel n a (view_frag_proj x)
      end
:= eq_refl _.
(* iris/algebra/view.v *)
Definition view_validN_eq :
    validN = λ n x,
      match view_auth_proj x with
      | Some (dq, ag) => ✓{n} dq ∧ ∃ a, ag ≡{n}≡ to_agree a ∧ rel n a (view_frag_proj x)
      | None => ∃ a, rel n a (view_frag_proj x)
      end
:= eq_refl _.
(* iris/algebra/view.v *)
Definition view_pcore_eq :
      pcore = λ x, Some (View (core (view_auth_proj x)) (core (view_frag_proj x)))
:=
    eq_refl _.
(* iris/algebra/view.v *)
Definition view_core_eq :
      core = λ x, View (core (view_auth_proj x)) (core (view_frag_proj x))
:=
    eq_refl _.
(* iris/algebra/view.v *)
Definition view_op_eq :
      op = λ x y, View (view_auth_proj x ⋅ view_auth_proj y)
                       (view_frag_proj x ⋅ view_frag_proj y)
:=
    eq_refl _.
(* iris/algebra/view.v *)
Lemma view_cmra_mixin : CmraMixin (view rel).
Proof.
    apply (iso_cmra_mixin_restrict_validity
      (λ x : option (dfrac * agree A) * B, View x.1 x.2)
      (λ x, (view_auth_proj x, view_frag_proj x))); try done.
    - intros [x b]. by rewrite /= pair_pcore !cmra_pcore_core.
    - intros n [[[dq ag]|] b]; rewrite /= view_validN_eq /=.
      + intros (?&a&->&?). repeat split; simpl; [done|]. by eapply view_rel_validN.
      + intros [a ?]. repeat split; simpl. by eapply view_rel_validN.
    - rewrite view_validN_eq.
      intros n [x1 b1] [x2 b2] [Hx ?]; simpl in *;
        destruct Hx as [[q1 ag1] [q2 ag2] [??]|]; intros ?; by ofe_subst.
    - rewrite view_valid_eq view_validN_eq.
      intros [[[dq aa]|] b]; rewrite /= ?cmra_valid_validN; naive_solver.
    - rewrite view_validN_eq=> n m [[[dq ag]|] b] /=.
      + intros [? (a&?&?)]; split; [done|].
        exists a; split; [by eauto using dist_le|].
        apply view_rel_mono with n a b; auto.
      + intros [a ?]. exists a. apply view_rel_mono with n a b; auto.
    - rewrite view_validN_eq=> n [[[q1 ag1]|] b1] [[[q2 ag2]|] b2] /=.
      + intros [?%cmra_validN_op_l (a & Haga & ?)]. split; [done|].
        assert (ag1 ≡{n}≡ ag2) as Ha12 by (apply agree_op_invN; by rewrite Haga).
        exists a. split; [by rewrite -Haga -Ha12 agree_idemp|].
        apply view_rel_mono with n a (b1 ⋅ b2); eauto using cmra_includedN_l.
      + intros [? (a & Haga & ?)]. split; [done|]. exists a; split; [done|].
        apply view_rel_mono with n a (b1 ⋅ b2); eauto using cmra_includedN_l.
      + intros [? (a & Haga & ?)]. exists a.
        apply view_rel_mono with n a (b1 ⋅ b2); eauto using cmra_includedN_l.
      + intros [a ?]. exists a.
        apply view_rel_mono with n a (b1 ⋅ b2); eauto using cmra_includedN_l.
  Qed.
(* iris/algebra/view.v *)
Canonical viewR
:= Cmra (view rel) view_cmra_mixin.
(* iris/algebra/view.v *)
Instance view_auth_discrete dq a :
    Discrete a → Discrete (ε : B) → Discrete (●V{dq} a : view rel).
Proof. intros. apply View_discrete; apply _. Qed.
(* iris/algebra/view.v *)
Instance view_frag_discrete b :
    Discrete b → Discrete (◯V b : view rel).
Proof. intros. apply View_discrete; apply _. Qed.
(* iris/algebra/view.v *)
Instance view_cmra_discrete :
    OfeDiscrete A → CmraDiscrete B → ViewRelDiscrete rel →
    CmraDiscrete viewR.
Proof.
    split; [apply _|]=> -[[[dq ag]|] b]; rewrite view_valid_eq view_validN_eq /=.
    - rewrite -cmra_discrete_valid_iff.
      setoid_rewrite <-(discrete_iff _ ag _). naive_solver.
    - naive_solver.
  Qed.
(* iris/algebra/view.v *)
Instance view_empty_instance : Unit (view rel)
:= View ε ε.
(* iris/algebra/view.v *)
Lemma view_ucmra_mixin : UcmraMixin (view rel).
Proof.
    split; simpl.
    - rewrite view_valid_eq /=. apply view_rel_unit.
    - by intros x; constructor; rewrite /= left_id.
    - do 2 constructor; [done| apply (core_id_core _)].
  Qed.
(* iris/algebra/view.v *)
Canonical viewUR
:= Ucmra (view rel) view_ucmra_mixin.
(* iris/algebra/view.v *)
(* Operation *)
Lemma view_auth_dfrac_op dq1 dq2 a : ●V{dq1 ⋅ dq2} a ≡ ●V{dq1} a ⋅ ●V{dq2} a.
Proof.
    intros; split; simpl; last by rewrite left_id.
    by rewrite -Some_op -pair_op agree_idemp.
  Qed.
(* iris/algebra/view.v *)
Instance view_auth_dfrac_is_op dq dq1 dq2 a :
    IsOp dq dq1 dq2 → IsOp' (●V{dq} a) (●V{dq1} a) (●V{dq2} a).
Proof. rewrite /IsOp' /IsOp => ->. by rewrite -view_auth_dfrac_op. Qed.
(* iris/algebra/view.v *)
Lemma view_frag_op b1 b2 : ◯V (b1 ⋅ b2) = ◯V b1 ⋅ ◯V b2.
Proof. done. Qed.
(* iris/algebra/view.v *)
Lemma view_frag_mono b1 b2 : b1 ≼ b2 → ◯V b1 ≼ ◯V b2.
Proof. intros [c ->]. by rewrite view_frag_op. Qed.
(* iris/algebra/view.v *)
Lemma view_frag_core b : core (◯V b) = ◯V (core b).
Proof. done. Qed.
(* iris/algebra/view.v *)
Lemma view_both_core_discarded a b :
    core (●V□ a ⋅ ◯V b) ≡ ●V□ a ⋅ ◯V (core b).
Proof. rewrite view_core_eq view_op_eq /= !left_id //. Qed.
(* iris/algebra/view.v *)
Lemma view_both_core_frac q a b :
    core (●V{#q} a ⋅ ◯V b) ≡ ◯V (core b).
Proof. rewrite view_core_eq view_op_eq /= !left_id //. Qed.
(* iris/algebra/view.v *)
Instance view_auth_core_id a : CoreId (●V□ a).
Proof. do 2 constructor; simpl; auto. apply: core_id_core. Qed.
(* iris/algebra/view.v *)
Instance view_frag_core_id b : CoreId b → CoreId (◯V b).
Proof. do 2 constructor; simpl; auto. apply: core_id_core. Qed.
(* iris/algebra/view.v *)
Instance view_both_core_id a b : CoreId b → CoreId (●V□ a ⋅ ◯V b).
Proof. do 2 constructor; simpl; auto. rewrite !left_id. apply: core_id_core. Qed.
(* iris/algebra/view.v *)
Instance view_frag_is_op b b1 b2 :
    IsOp b b1 b2 → IsOp' (◯V b) (◯V b1) (◯V b2).
Proof. done. Qed.
(* iris/algebra/view.v *)
Instance view_frag_sep_homomorphism :
    MonoidHomomorphism op op (≡) (@view_frag SI A B rel).
Proof. by split; [split; try apply _|]. Qed.
(* iris/algebra/view.v *)
Lemma big_opL_view_frag {C} (g : nat → C → B) (l : list C) :
    (◯V [^op list] k↦x ∈ l, g k x) ≡ [^op list] k↦x ∈ l, ◯V (g k x).
Proof. apply (big_opL_commute _). Qed.
(* iris/algebra/view.v *)
Lemma big_opM_view_frag `{Countable K} {C} (g : K → C → B) (m : gmap K C) :
    (◯V [^op map] k↦x ∈ m, g k x) ≡ [^op map] k↦x ∈ m, ◯V (g k x).
Proof. apply (big_opM_commute _). Qed.
(* iris/algebra/view.v *)
Lemma big_opS_view_frag `{Countable C} (g : C → B) (X : gset C) :
    (◯V [^op set] x ∈ X, g x) ≡ [^op set] x ∈ X, ◯V (g x).
Proof. apply (big_opS_commute _). Qed.
(* iris/algebra/view.v *)
Lemma big_opMS_view_frag `{Countable C} (g : C → B) (X : gmultiset C) :
    (◯V [^op mset] x ∈ X, g x) ≡ [^op mset] x ∈ X, ◯V (g x).
Proof. apply (big_opMS_commute _). Qed.
(* iris/algebra/view.v *)
(* Validity *)
Lemma view_auth_dfrac_op_invN n dq1 a1 dq2 a2 :
    ✓{n} (●V{dq1} a1 ⋅ ●V{dq2} a2) → a1 ≡{n}≡ a2.
Proof.
    rewrite /op /view_op_instance /= left_id -Some_op -pair_op view_validN_eq /=.
    intros (?&?& Eq &?). apply (inj to_agree), agree_op_invN. by rewrite Eq.
  Qed.
(* iris/algebra/view.v *)
Lemma view_auth_dfrac_op_inv dq1 a1 dq2 a2 : ✓ (●V{dq1} a1 ⋅ ●V{dq2} a2) → a1 ≡ a2.
Proof.
    intros ?. apply equiv_dist. intros n.
    by eapply view_auth_dfrac_op_invN, cmra_valid_validN.
  Qed.
(* iris/algebra/view.v *)
Lemma view_auth_dfrac_op_inv_L `{!LeibnizEquiv A} dq1 a1 dq2 a2 :
    ✓ (●V{dq1} a1 ⋅ ●V{dq2} a2) → a1 = a2.
Proof. by intros ?%view_auth_dfrac_op_inv%leibniz_equiv. Qed.
(* iris/algebra/view.v *)
Lemma view_auth_dfrac_validN n dq a : ✓{n} (●V{dq} a) ↔ ✓{n}dq ∧ rel n a ε.
Proof.
    rewrite view_validN_eq /=. apply and_iff_compat_l. split; [|by eauto].
    by intros [? [->%(inj to_agree) ?]].
  Qed.
(* iris/algebra/view.v *)
Lemma view_auth_validN n a : ✓{n} (●V a) ↔ rel n a ε.
Proof. rewrite view_auth_dfrac_validN. split; [naive_solver|done]. Qed.
(* iris/algebra/view.v *)
Lemma view_auth_dfrac_op_validN n dq1 dq2 a1 a2 :
    ✓{n} (●V{dq1} a1 ⋅ ●V{dq2} a2) ↔ ✓(dq1 ⋅ dq2) ∧ a1 ≡{n}≡ a2 ∧ rel n a1 ε.
Proof.
    split.
    - intros Hval. assert (a1 ≡{n}≡ a2) as Ha by eauto using view_auth_dfrac_op_invN.
      revert Hval. rewrite Ha -view_auth_dfrac_op view_auth_dfrac_validN. naive_solver.
    - intros (?&->&?). by rewrite -view_auth_dfrac_op view_auth_dfrac_validN.
  Qed.
(* iris/algebra/view.v *)
Lemma view_auth_op_validN n a1 a2 : ✓{n} (●V a1 ⋅ ●V a2) ↔ False.
Proof. rewrite view_auth_dfrac_op_validN. naive_solver. Qed.
(* iris/algebra/view.v *)
Lemma view_frag_validN n b : ✓{n} (◯V b) ↔ ∃ a, rel n a b.
Proof. done. Qed.
(* iris/algebra/view.v *)
Lemma view_both_dfrac_validN n dq a b :
    ✓{n} (●V{dq} a ⋅ ◯V b) ↔ ✓dq ∧ rel n a b.
Proof.
    rewrite view_validN_eq /=. apply and_iff_compat_l.
    setoid_rewrite (left_id _ _ b). split; [|by eauto].
    by intros [?[->%(inj to_agree)]].
  Qed.
(* iris/algebra/view.v *)
Lemma view_both_validN n a b : ✓{n} (●V a ⋅ ◯V b) ↔ rel n a b.
Proof. rewrite view_both_dfrac_validN. split; [naive_solver|done]. Qed.
(* iris/algebra/view.v *)
Lemma view_auth_dfrac_valid dq a : ✓ (●V{dq} a) ↔ ✓dq ∧ ∀ n, rel n a ε.
Proof.
    rewrite view_valid_eq /=. apply and_iff_compat_l. split; [|by eauto].
    intros H n. by destruct (H n) as [? [->%(inj to_agree) ?]].
  Qed.
(* iris/algebra/view.v *)
Lemma view_auth_valid a : ✓ (●V a) ↔ ∀ n, rel n a ε.
Proof. rewrite view_auth_dfrac_valid. split; [naive_solver|done]. Qed.
(* iris/algebra/view.v *)
Lemma view_auth_dfrac_op_valid dq1 dq2 a1 a2 :
    ✓ (●V{dq1} a1 ⋅ ●V{dq2} a2) ↔ ✓(dq1 ⋅ dq2) ∧ a1 ≡ a2 ∧ ∀ n, rel n a1 ε.
Proof.
    rewrite 1!cmra_valid_validN equiv_dist. setoid_rewrite view_auth_dfrac_op_validN.
    split; last naive_solver. intros Hv.
    split; last naive_solver. apply (Hv 0ᵢ).
  Qed.
(* iris/algebra/view.v *)
Lemma view_auth_op_valid a1 a2 : ✓ (●V a1 ⋅ ●V a2) ↔ False.
Proof. rewrite view_auth_dfrac_op_valid. naive_solver. Qed.
(* iris/algebra/view.v *)
Lemma view_frag_valid b : ✓ (◯V b) ↔ ∀ n, ∃ a, rel n a b.
Proof. done. Qed.
(* iris/algebra/view.v *)
Lemma view_both_dfrac_valid dq a b : ✓ (●V{dq} a ⋅ ◯V b) ↔ ✓dq ∧ ∀ n, rel n a b.
Proof.
    rewrite view_valid_eq /=. apply and_iff_compat_l.
    setoid_rewrite (left_id _ _ b). split; [|by eauto].
    intros H n. by destruct (H n) as [?[->%(inj to_agree)]].
  Qed.
(* iris/algebra/view.v *)
Lemma view_both_valid a b : ✓ (●V a ⋅ ◯V b) ↔ ∀ n, rel n a b.
Proof. rewrite view_both_dfrac_valid. split; [naive_solver|done]. Qed.
(* iris/algebra/view.v *)
(* Inclusion *)
Lemma view_auth_dfrac_includedN n dq1 dq2 a1 a2 b :
    ●V{dq1} a1 ≼{n} ●V{dq2} a2 ⋅ ◯V b ↔ (dq1 ≼ dq2 ∨ dq1 = dq2) ∧ a1 ≡{n}≡ a2.
Proof.
    split.
    - intros [[[[dqf agf]|] bf]
        [[?%(discrete_iff _ _ _) ?]%(inj Some) _]]; simplify_eq/=.
      + split; [eauto|]. apply to_agree_includedN. by exists agf.
      + split; [right; done|]. by apply (inj to_agree).
    - intros [[[? ->]| ->] ->].
      + rewrite view_auth_dfrac_op -assoc. apply cmra_includedN_l.
      + apply cmra_includedN_l.
  Qed.
(* iris/algebra/view.v *)
Lemma view_auth_dfrac_included dq1 dq2 a1 a2 b :
    ●V{dq1} a1 ≼ ●V{dq2} a2 ⋅ ◯V b ↔ (dq1 ≼ dq2 ∨ dq1 = dq2) ∧ a1 ≡ a2.
Proof.
    intros. split.
    - split.
      + by eapply (view_auth_dfrac_includedN 0ᵢ), cmra_included_includedN.
      + apply equiv_dist=> n.
        by eapply view_auth_dfrac_includedN, cmra_included_includedN.
    - intros [[[dq ->]| ->] ->].
      + by rewrite view_auth_dfrac_op -assoc.
      + done.
  Qed.
(* iris/algebra/view.v *)
Lemma view_auth_includedN n a1 a2 b :
    ●V a1 ≼{n} ●V a2 ⋅ ◯V b ↔ a1 ≡{n}≡ a2.
Proof. rewrite view_auth_dfrac_includedN. naive_solver. Qed.
(* iris/algebra/view.v *)
Lemma view_auth_included a1 a2 b :
    ●V a1 ≼ ●V a2 ⋅ ◯V b ↔ a1 ≡ a2.
Proof. rewrite view_auth_dfrac_included. naive_solver. Qed.
(* iris/algebra/view.v *)
Lemma view_frag_includedN n p a b1 b2 :
    ◯V b1 ≼{n} ●V{p} a ⋅ ◯V b2 ↔ b1 ≼{n} b2.
Proof.
    split.
    - intros [xf [_ Hb]]; simpl in *.
      revert Hb; rewrite left_id. by exists (view_frag_proj xf).
    - intros [bf ->]. rewrite comm view_frag_op -assoc. apply cmra_includedN_l.
  Qed.
(* iris/algebra/view.v *)
Lemma view_frag_included p a b1 b2 :
    ◯V b1 ≼ ●V{p} a ⋅ ◯V b2 ↔ b1 ≼ b2.
Proof.
    split.
    - intros [xf [_ Hb]]; simpl in *.
      revert Hb; rewrite left_id. by exists (view_frag_proj xf).
    - intros [bf ->]. by rewrite comm view_frag_op -assoc.
  Qed.
(* iris/algebra/view.v *)
(* The weaker [view_both_included] lemmas below are a consequence of the
  [view_auth_included] and [view_frag_included] lemmas above. *)
Lemma view_both_dfrac_includedN n dq1 dq2 a1 a2 b1 b2 :
    ●V{dq1} a1 ⋅ ◯V b1 ≼{n} ●V{dq2} a2 ⋅ ◯V b2 ↔
      (dq1 ≼ dq2 ∨ dq1 = dq2) ∧ a1 ≡{n}≡ a2 ∧ b1 ≼{n} b2.
Proof.
    split.
    - intros. rewrite assoc. split.
      + rewrite -view_auth_dfrac_includedN. by etrans; [apply cmra_includedN_l|].
      + rewrite -view_frag_includedN. by etrans; [apply cmra_includedN_r|].
    - intros (?&->&?bf&->). rewrite (comm _ b1) view_frag_op assoc.
      by apply cmra_monoN_r, view_auth_dfrac_includedN.
  Qed.
(* iris/algebra/view.v *)
Lemma view_both_dfrac_included dq1 dq2 a1 a2 b1 b2 :
    ●V{dq1} a1 ⋅ ◯V b1 ≼ ●V{dq2} a2 ⋅ ◯V b2 ↔
      (dq1 ≼ dq2 ∨ dq1 = dq2) ∧ a1 ≡ a2 ∧ b1 ≼ b2.
Proof.
    split.
    - intros. rewrite assoc. split.
      + rewrite -view_auth_dfrac_included. by etrans; [apply cmra_included_l|].
      + rewrite -view_frag_included. by etrans; [apply cmra_included_r|].
    - intros (?&->&?bf&->). rewrite (comm _ b1) view_frag_op assoc.
      by apply cmra_mono_r, view_auth_dfrac_included.
  Qed.
(* iris/algebra/view.v *)
Lemma view_both_includedN n a1 a2 b1 b2 :
    ●V a1 ⋅ ◯V b1 ≼{n} ●V a2 ⋅ ◯V b2 ↔ a1 ≡{n}≡ a2 ∧ b1 ≼{n} b2.
Proof. rewrite view_both_dfrac_includedN. naive_solver. Qed.
(* iris/algebra/view.v *)
Lemma view_both_included a1 a2 b1 b2 :
    ●V a1 ⋅ ◯V b1 ≼ ●V a2 ⋅ ◯V b2 ↔ a1 ≡ a2 ∧ b1 ≼ b2.
Proof. rewrite view_both_dfrac_included. naive_solver. Qed.
(* iris/algebra/view.v *)
(* Note that we quantify over a frame [bf], and since conceptually [rel n a b]
      means "[b] is a valid fragment to be part of [a]", there is another implicit
      frame quantification inside [rel] (usually because [rel] is defined via [≼]
      which contains an existential quantifier). The difference between the two
      frames is that the frame quantified inside [rel] may change but [bf] has
      to be preserved. It is not clear if it is possible to avoid this. *)
Lemma view_updateP a b Pab :
    (∀ n bf, rel n a (b ⋅ bf) → ∃ a' b', Pab a' b' ∧ rel n a' (b' ⋅ bf)) →
    ●V a ⋅ ◯V b ~~>: λ k, ∃ a' b', k = ●V a' ⋅ ◯V b' ∧ Pab a' b'.
Proof.
    intros Hup; apply cmra_total_updateP=> n [[[dq ag]|] bf] [/=].
    { by intros []%(exclusiveN_l _ _). }
    intros _ (a0 & <-%(inj to_agree) & Hrel).
    rewrite !left_id in Hrel. apply Hup in Hrel as (a' & b' & Hab' & Hrel).
    eexists; split.
    - naive_solver.
    - split; simpl; [done|].
      exists a'; split; [done|]. by rewrite left_id.
  Qed.
(* iris/algebra/view.v *)
Lemma view_update a b a' b' :
    (∀ n bf, rel n a (b ⋅ bf) → rel n a' (b' ⋅ bf)) →
    ●V a ⋅ ◯V b ~~> ●V a' ⋅ ◯V b'.
Proof.
    intros Hup.
    eapply cmra_update_updateP, cmra_updateP_weaken.
    { eapply view_updateP with (Pab := λ a b, a = a' ∧ b = b').
      naive_solver. }
    { naive_solver. }
  Qed.
(* iris/algebra/view.v *)
Lemma view_update_alloc a a' b' :
    (∀ n bf, rel n a bf → rel n a' (b' ⋅ bf)) →
    ●V a ~~> ●V a' ⋅ ◯V b'.
Proof.
    intros Hup. rewrite -(right_id _ _ (●V a)).
    apply view_update=> n bf. rewrite left_id. apply Hup.
  Qed.