(* iris/algebra/view.v *)
From iris.algebra Require Export updates local_updates frac dfrac agree
From iris.algebra Require Import proofmode_classes big_op
From iris.prelude Require Import options

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 ε
}.

Global ArgumentsViewRel {_ _ _} _ _.

Global Argumentsview_rel_holds {_ _ _} _ _ _ _.

Global Instance: Params (@view_rel_holds) 5 := {}.

Global Instanceview_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.

Global Instanceview_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.

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.

Record view{SI : sidx} {A B} (rel : SI → A → B → Prop) :=
  View { view_auth_proj : option (dfrac * agree A) ; view_frag_proj : B }.
Add Printing Constructor view.

Global ArgumentsView {_ _ _ _} _ _.

Global Argumentsview_auth_proj {_ _ _ _} _.

Global Argumentsview_frag_proj {_ _ _ _} _.

Global Instance: Params (@View) 4 := {}.

Global Instance: Params (@view_auth_proj) 4 := {}.

Global Instance: Params (@view_frag_proj) 4 := {}.

Definition view_auth{SI : sidx} {A B} {rel : view_rel A B}
    (dq : dfrac) (a : A) : view rel :=
  View (Some (dq, to_agree a)) ε.

Definition view_frag{SI : sidx} {A B} {rel : view_rel A B} (b : B) : view rel :=
  View None b.

Global TypeclassesOpaque view_auth view_frag.

Global Instance: Params (@view_auth) 4 := {}.

Global Instance: Params (@view_frag) 4 := {}.

Local Instanceview_equiv : Equiv (view rel) := λ x y,
    view_auth_proj x ≡ view_auth_proj y ∧ view_frag_proj x ≡ view_frag_proj y.

Local Instanceview_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.

Global InstanceView_ne : NonExpansive2 (@View SI A B rel).
  Proof. by split. Qed.

Global InstanceView_proper : Proper ((≡) ==> (≡) ==> (≡)) (@View SI A B rel).
  Proof. by split. Qed.

Global Instanceview_auth_proj_ne : NonExpansive (@view_auth_proj SI A B rel).
  Proof. by destruct 1. Qed.

Global Instanceview_auth_proj_proper :
    Proper ((≡) ==> (≡)) (@view_auth_proj SI A B rel).
  Proof. by destruct 1. Qed.

Global Instanceview_frag_proj_ne : NonExpansive (@view_frag_proj SI A B rel).
  Proof. by destruct 1. Qed.

Global Instanceview_frag_proj_proper :
    Proper ((≡) ==> (≡)) (@view_frag_proj SI A B rel).
  Proof. by destruct 1. Qed.

Definition view_ofe_mixin: OfeMixin (view rel).
  Proof. by apply (iso_ofe_mixin (λ x, (view_auth_proj x, view_frag_proj x))). Qed.
  Canonical Structure viewO := Ofe (view rel) view_ofe_mixin.

Global InstanceView_discrete ag b :
    Discrete ag → Discrete b → Discrete (View ag b).
  Proof. by intros ?? [??] [??]; split; apply: discrete. Qed.

Global Instanceview_ofe_discrete :
    OfeDiscrete A → OfeDiscrete B → OfeDiscrete viewO.
  Proof. intros ?? [??]; apply _. Qed.

Global Instanceview_auth_ne dq : NonExpansive (@view_auth SI A B rel dq).
  Proof. solve_proper. Qed.

Global Instanceview_auth_proper dq :
    Proper ((≡) ==> (≡)) (@view_auth SI A B rel dq).
  Proof. solve_proper. Qed.

Global Instanceview_frag_ne : NonExpansive (@view_frag SI A B rel).
  Proof. done. Qed.

Global Instanceview_frag_proper : Proper ((≡) ==> (≡)) (@view_frag SI A B rel).
  Proof. done. Qed.

Global Instanceview_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.

Global Instanceview_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.

Global Instanceview_frag_dist_inj n :
    Inj (dist n) (dist n) (@view_frag SI A B rel).
  Proof. by intros ?? [??]. Qed.

Global Instanceview_frag_inj : Inj (≡) (≡) (@view_frag SI A B rel).
  Proof. by intros ?? [??]. Qed.

Local Instanceview_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.

Local Instanceview_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.

Local Instanceview_pcore_instance : PCore (view rel) := λ x,
    Some (View (core (view_auth_proj x)) (core (view_frag_proj x))).

Local Instanceview_op_instance : Op (view rel) := λ x y,
    View (view_auth_proj x ⋅ view_auth_proj y) (view_frag_proj x ⋅ view_frag_proj y).

Local Definitionview_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 _.

Local Definitionview_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 _.

Local Definitionview_pcore_eq :
      pcore = λ x, Some (View (core (view_auth_proj x)) (core (view_frag_proj x))) :=
    eq_refl _.

Local Definitionview_core_eq :
      core = λ x, View (core (view_auth_proj x)) (core (view_frag_proj x)) :=
    eq_refl _.

Local Definitionview_op_eq :
      op = λ x y, View (view_auth_proj x ⋅ view_auth_proj y)
                       (view_frag_proj x ⋅ view_frag_proj y) :=
    eq_refl _.

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);
...

Global Instanceview_auth_discrete dq a :
    Discrete a → Discrete (ε : B) → Discrete (●V{dq} a : view rel).
  Proof. intros. apply View_discrete; apply _. Qed.

Global Instanceview_frag_discrete b :
    Discrete b → Discrete (◯V b : view rel).
  Proof. intros. apply View_discrete; apply _. Qed.

Global Instanceview_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.

Local Instanceview_empty_instance : Unit (view rel) := View ε ε.

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.
  Canonical Structure viewUR := Ucmra (view rel) view_ucmra_mixin.

Lemma view_auth_dfrac_opdq1 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.

Global Instanceview_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.

Lemma view_frag_opb1 b2 : ◯V (b1 ⋅ b2) = ◯V b1 ⋅ ◯V b2.
  Proof. done. Qed.

Lemma view_frag_monob1 b2 : b1 ≼ b2 → ◯V b1 ≼ ◯V b2.
  Proof. intros [c ->]. by rewrite view_frag_op. Qed.

Lemma view_frag_coreb : core (◯V b) = ◯V (core b).
  Proof. done. Qed.

Lemma view_both_core_discardeda b :
    core (●V□ a ⋅ ◯V b) ≡ ●V□ a ⋅ ◯V (core b).
  Proof. rewrite view_core_eq view_op_eq /= !left_id //. Qed.

Lemma view_both_core_fracq a b :
    core (●V{#q} a ⋅ ◯V b) ≡ ◯V (core b).
  Proof. rewrite view_core_eq view_op_eq /= !left_id //. Qed.

Global Instanceview_auth_core_id a : CoreId (●V□ a).
  Proof. do 2 constructor; simpl; auto. apply: core_id_core. Qed.

Global Instanceview_frag_core_id b : CoreId b → CoreId (◯V b).
  Proof. do 2 constructor; simpl; auto. apply: core_id_core. Qed.

Global Instanceview_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.

Global Instanceview_frag_is_op b b1 b2 :
    IsOp b b1 b2 → IsOp' (◯V b) (◯V b1) (◯V b2).
  Proof. done. Qed.

Global Instanceview_frag_sep_homomorphism :
    MonoidHomomorphism op op (≡) (@view_frag SI A B rel).
  Proof. by split; [split; try apply _|]. Qed.

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.

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.

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.

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.

Lemma view_auth_dfrac_op_invNn 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.

Lemma view_auth_dfrac_op_invdq1 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.

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.

Lemma view_auth_dfrac_validNn 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.

Lemma view_auth_validNn a : ✓{n} (●V a) ↔ rel n a ε.
  Proof. rewrite view_auth_dfrac_validN. split; [naive_solver|done]. Qed.

Lemma view_auth_dfrac_op_validNn 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.

Lemma view_auth_op_validNn a1 a2 : ✓{n} (●V a1 ⋅ ●V a2) ↔ False.
  Proof. rewrite view_auth_dfrac_op_validN. naive_solver. Qed.

Lemma view_frag_validNn b : ✓{n} (◯V b) ↔ ∃ a, rel n a b.
  Proof. done. Qed.

Lemma view_both_dfrac_validNn 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.

Lemma view_both_validNn a b : ✓{n} (●V a ⋅ ◯V b) ↔ rel n a b.
  Proof. rewrite view_both_dfrac_validN. split; [naive_solver|done]. Qed.

Lemma view_auth_dfrac_validdq 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.

Lemma view_auth_valida : ✓ (●V a) ↔ ∀ n, rel n a ε.
  Proof. rewrite view_auth_dfrac_valid. split; [naive_solver|done]. Qed.

Lemma view_auth_dfrac_op_validdq1 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.

Lemma view_auth_op_valida1 a2 : ✓ (●V a1 ⋅ ●V a2) ↔ False.
  Proof. rewrite view_auth_dfrac_op_valid. naive_solver. Qed.

Lemma view_frag_validb : ✓ (◯V b) ↔ ∀ n, ∃ a, rel n a b.
  Proof. done. Qed.

Lemma view_both_dfrac_validdq 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.

Lemma view_both_valida b : ✓ (●V a ⋅ ◯V b) ↔ ∀ n, rel n a b.
  Proof. rewrite view_both_dfrac_valid. split; [naive_solver|done]. Qed.

Lemma view_auth_dfrac_includedNn 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.

Lemma view_auth_dfrac_includeddq1 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.

Lemma view_auth_includedNn a1 a2 b :
    ●V a1 ≼{n} ●V a2 ⋅ ◯V b ↔ a1 ≡{n}≡ a2.
  Proof. rewrite view_auth_dfrac_includedN. naive_solver. Qed.

Lemma view_auth_includeda1 a2 b :
    ●V a1 ≼ ●V a2 ⋅ ◯V b ↔ a1 ≡ a2.
  Proof. rewrite view_auth_dfrac_included. naive_solver. Qed.

Lemma view_frag_includedNn 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.

Lemma view_frag_includedp 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.

Lemma view_both_dfrac_includedNn 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.

Lemma view_both_dfrac_includeddq1 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.

Lemma view_both_includedNn 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.

Lemma view_both_includeda1 a2 b1 b2 :
    ●V a1 ⋅ ◯V b1 ≼ ●V a2 ⋅ ◯V b2 ↔ a1 ≡ a2 ∧ b1 ≼ b2.
  Proof. rewrite view_both_dfrac_included. naive_solver. Qed.

Lemma view_updatePa 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.

Lemma view_updatea 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.

Lemma view_update_alloca 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.

Lemma view_update_dealloca 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.

Lemma view_update_autha 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.

Local Lemmaview_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.

Lemma view_update_auth_persistdq 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.

Lemma view_updateP_auth_unpersista : ●V□ a ~~>: λ k, ∃ q, k = ●V{#q} a.
  Proof.
    eapply cmra_updateP_weaken.
    { eapply view_updateP_auth_dfrac, dfrac_undiscard_update. }
    naive_solver.
  Qed.

Lemma view_updateP_both_unpersista 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.

Lemma view_updateP_fragb 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.

Lemma view_update_fragb 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.

Lemma view_update_dfrac_allocdq 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.

Lemma view_local_updatea 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.

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)).

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.

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.

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.

Global Instanceview_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.

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).

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.

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.