(* iris/algebra/lib/gmap_view.v *)
From Stdlib.QArith Require Import Qcanon
From iris.algebra Require Export view gmap frac dfrac
From iris.algebra Require Import local_updates proofmode_classes big_op
From iris.prelude Require Import options

Local Definitiongmap_view_fragUR {SI : sidx}
     (K : Type) `{Countable K} (V : cmra) : ucmra :=
  gmapUR K (prodR dfracR V).

Local Definitiongmap_view_rel_raw n m f :=
    map_Forall (λ k fv,
      ∃ v dq, m !! k = Some v ∧ ✓{n} (dq, v) ∧ (Some fv ≼{n} Some (dq, v))) f.

Local Lemmagmap_view_rel_raw_mono n1 n2 m1 m2 f1 f2 :
    gmap_view_rel_raw n1 m1 f1 →
    m1 ≡{n2}≡ m2 →
    f2 ≼{n2} f1 →
    (n2 ≤ n1)%sidx →
    gmap_view_rel_raw n2 m2 f2.
  Proof.
    intros Hrel Hm Hf Hn k [dqa va] Hk.

Local Lemmagmap_view_rel_raw_valid n m f :
    gmap_view_rel_raw n m f → ✓{n} f.
  Proof.
    intros Hrel k. destruct (f !! k) as [[dqa va]|] eqn:Hf; rewrite Hf; last done.
    specialize (Hrel _ _ Hf) as (v & dq & Hmval & Hvval & Hvincl). simpl in *.
    eapply cmra_validN_includedN. 2:done. done.
  Qed.

Local Lemmagmap_view_rel_raw_unit n :
    ∃ m, gmap_view_rel_raw n m ε.
  Proof. exists ∅. apply: map_Forall_empty. Qed.

Local CanonicalStructure gmap_view_rel :
      view_rel (gmapO K V) (gmap_view_fragUR K V) :=
    ViewRel gmap_view_rel_raw gmap_view_rel_raw_mono
            gmap_view_rel_raw_valid gmap_view_rel_raw_unit.

Local Lemmagmap_view_rel_exists n f :
    (∃ m, gmap_view_rel n m f) ↔ ✓{n} f.
  Proof.
    split.
    { intros [m Hrel]. eapply gmap_view_rel_raw_valid, Hrel. }
    intros Hf.
    cut (∃ m, gmap_view_rel n m f ∧ ∀ k, f !! k = None → m !! k = None).
    { naive_solver. }
    induction f as [|k [dq v] f Hk' IH] using map_ind.
    { exists ∅. split; [|done]. apply: map_Forall_empty. }
    move: (Hf k). rewrite lookup_insert_eq=> -[/= ??].
    destruct IH as (m & Hm & Hdom).
    { intros k'. destruct (decide (k = k')) as [->|?]; [by rewrite Hk'|].
      move: (Hf k'). by rewrite lookup_insert_ne. }
    exists (<[k:=v]> m).
    rewrite /gmap_view_rel /= /gmap_view_rel_raw map_Forall_insert //=. split_and!.
    - exists v, dq. split; first by rewrite lookup_insert_eq.
      split; first by split. done.
    - eapply map_Forall_impl; [apply Hm|]; simpl.
      intros k' [dq' ag'] (v'&?&?&?). exists v'.
      rewrite lookup_insert_ne; naive_solver.
    - intros k'. rewrite !lookup_insert_None. naive_solver.
  Qed.

Local Lemmagmap_view_rel_unit n m : gmap_view_rel n m ε.
  Proof. apply: map_Forall_empty. Qed.

Local Lemmagmap_view_rel_discrete :
    CmraDiscrete V → ViewRelDiscrete gmap_view_rel.
  Proof.
    intros ? n m f Hrel k [df va] Hk.
    destruct (Hrel _ _ Hk) as (v & dq & Hm & Hvval & Hvincl).
    exists v, dq. split; first done.
    split; first by apply cmra_discrete_valid_iff_0.
    rewrite -cmra_discrete_included_iff_0. done.
  Qed.

Local ExistingInstance gmap_view_rel_discrete.

Notation gmap_viewK V := (view (gmap_view_rel_raw K V)).

Definition gmap_viewO{SI : sidx} (K : Type) `{Countable K} (V : cmra) : ofe :=
  viewO (gmap_view_rel K V).

Definition gmap_viewR{SI : sidx} (K : Type) `{Countable K} (V : cmra) : cmra :=
  viewR (gmap_view_rel K V).

Definition gmap_viewUR{SI : sidx} (K : Type) `{Countable K} (V : cmra) : ucmra :=
  viewUR (gmap_view_rel K V).

Definition gmap_view_auth(dq : dfrac) (m : gmap K V) : gmap_viewR K V :=
    ●V{dq} m.

Definition gmap_view_frag(k : K) (dq : dfrac) (v : V) : gmap_viewR K V :=
    ◯V {[k := (dq, v)]}.

Global Instance: Params (@gmap_view_auth) 6 := {}.

Global Instancegmap_view_auth_ne dq :
    NonExpansive (gmap_view_auth (K:=K) (V:=V) dq).
  Proof. solve_proper. Qed.

Global Instancegmap_view_auth_proper dq :
    Proper ((≡) ==> (≡)) (gmap_view_auth (K:=K) (V:=V) dq).
  Proof. apply ne_proper, _. Qed.

Global Instance: Params (@gmap_view_frag) 7 := {}.

Global Instancegmap_view_frag_ne k oq : NonExpansive (gmap_view_frag (V:=V) k oq).
  Proof. solve_proper. Qed.

Global Instancegmap_view_frag_proper k oq :
    Proper ((≡) ==> (≡)) (gmap_view_frag (V:=V) k oq).
  Proof. apply ne_proper, _. Qed.

Local Lemmagmap_view_rel_lookup n m k dq v :
    gmap_view_rel K V n m {[k := (dq, v)]} ↔
    ∃ v' dq', m !! k = Some v' ∧ ✓{n} (dq', v') ∧ Some (dq, v) ≼{n} Some (dq', v').
  Proof.
    split.
    - intros Hrel.
      edestruct (Hrel k) as (v' & dq' & Hlookup & Hval & Hinc).
      { rewrite lookup_singleton_eq. done. }
      simpl in *. eexists _, _. split_and!; done.
    - intros (v' & dq' & Hlookup & Hval & ?) j [df va].
      destruct (decide (k = j)) as [<-|Hne]; last by rewrite lookup_singleton_ne.
      rewrite lookup_singleton_eq. intros [= <- <-]. simpl.
      exists v', dq'. split_and!; by rewrite ?Hv'.
  Qed.

Lemma gmap_view_auth_dfrac_opdp dq m :
    gmap_view_auth (dp ⋅ dq) m ≡
    gmap_view_auth dp m ⋅ gmap_view_auth dq m.
  Proof. by rewrite /gmap_view_auth view_auth_dfrac_op. Qed.

Global Instancegmap_view_auth_dfrac_is_op dq dq1 dq2 m :
    IsOp dq dq1 dq2 →
    IsOp' (gmap_view_auth dq m) (gmap_view_auth dq1 m) (gmap_view_auth dq2 m).
  Proof. rewrite /gmap_view_auth. apply _. Qed.

Lemma gmap_view_auth_dfrac_op_invNn dp m1 dq m2 :
    ✓{n} (gmap_view_auth dp m1 ⋅ gmap_view_auth dq m2) → m1 ≡{n}≡ m2.
  Proof. apply view_auth_dfrac_op_invN. Qed.

Lemma gmap_view_auth_dfrac_op_invdp m1 dq m2 :
    ✓ (gmap_view_auth dp m1 ⋅ gmap_view_auth dq m2) → m1 ≡ m2.
  Proof. apply view_auth_dfrac_op_inv. Qed.

Lemma gmap_view_auth_dfrac_validNm n dq : ✓{n} gmap_view_auth dq m ↔ ✓ dq.
  Proof.
    rewrite view_auth_dfrac_validN. intuition eauto using gmap_view_rel_unit.
  Qed.

Lemma gmap_view_auth_dfrac_validm dq : ✓ gmap_view_auth dq m ↔ ✓ dq.
  Proof.
    rewrite view_auth_dfrac_valid. intuition eauto using gmap_view_rel_unit.
  Qed.

Lemma gmap_view_auth_validm : ✓ gmap_view_auth (DfracOwn 1) m.
  Proof. rewrite gmap_view_auth_dfrac_valid. done. Qed.

Lemma gmap_view_auth_dfrac_op_validNn dq1 dq2 m1 m2 :
    ✓{n} (gmap_view_auth dq1 m1 ⋅ gmap_view_auth dq2 m2) ↔ ✓ (dq1 ⋅ dq2) ∧ m1 ≡{n}≡ m2.
  Proof.
    rewrite view_auth_dfrac_op_validN. intuition eauto using gmap_view_rel_unit.
  Qed.

Lemma gmap_view_auth_dfrac_op_validdq1 dq2 m1 m2 :
    ✓ (gmap_view_auth dq1 m1 ⋅ gmap_view_auth dq2 m2) ↔ ✓ (dq1 ⋅ dq2) ∧ m1 ≡ m2.
  Proof.
    rewrite view_auth_dfrac_op_valid. intuition eauto using gmap_view_rel_unit.
  Qed.

Lemma gmap_view_auth_op_validNn m1 m2 :
    ✓{n} (gmap_view_auth (DfracOwn 1) m1 ⋅ gmap_view_auth (DfracOwn 1) m2) ↔ False.
  Proof. apply view_auth_op_validN. Qed.

Lemma gmap_view_auth_op_validm1 m2 :
    ✓ (gmap_view_auth (DfracOwn 1) m1 ⋅ gmap_view_auth (DfracOwn 1) m2) ↔ False.
  Proof. apply view_auth_op_valid. Qed.

Lemma gmap_view_frag_validNn k dq v : ✓{n} gmap_view_frag k dq v ↔ ✓ dq ∧ ✓{n} v.
  Proof.
    rewrite view_frag_validN gmap_view_rel_exists singleton_validN pair_validN.
    naive_solver.
  Qed.

Lemma gmap_view_frag_validk dq v : ✓ gmap_view_frag k dq v ↔ ✓ dq ∧ ✓ v.
  Proof.
    rewrite cmra_valid_validN. setoid_rewrite gmap_view_frag_validN.
    rewrite [_ v]cmra_valid_validN. pose 0ᵢ. naive_solver.
  Qed.

Lemma gmap_view_frag_opk dq1 dq2 v1 v2 :
    gmap_view_frag k (dq1 ⋅ dq2) (v1 ⋅ v2) ≡
      gmap_view_frag k dq1 v1 ⋅ gmap_view_frag k dq2 v2.
  Proof. rewrite -view_frag_op singleton_op -pair_op //. Qed.

Lemma gmap_view_frag_addk q1 q2 v1 v2 :
    gmap_view_frag k (DfracOwn (q1 + q2)) (v1 ⋅ v2) ≡
      gmap_view_frag k (DfracOwn q1) v1 ⋅ gmap_view_frag k (DfracOwn q2) v2.
  Proof. rewrite -gmap_view_frag_op. done. Qed.

Lemma gmap_view_frag_op_validNn k dq1 dq2 v1 v2 :
    ✓{n} (gmap_view_frag k dq1 v1 ⋅ gmap_view_frag k dq2 v2) ↔
      ✓ (dq1 ⋅ dq2) ∧ ✓{n} (v1 ⋅ v2).
  Proof.
    rewrite view_frag_validN gmap_view_rel_exists singleton_op singleton_validN.
    by rewrite -pair_op pair_validN.
  Qed.

Lemma gmap_view_frag_op_validk dq1 dq2 v1 v2 :
    ✓ (gmap_view_frag k dq1 v1 ⋅ gmap_view_frag k dq2 v2) ↔
      ✓ (dq1 ⋅ dq2) ∧ ✓ (v1 ⋅ v2).
  Proof.
    rewrite view_frag_valid. setoid_rewrite gmap_view_rel_exists.
    rewrite -cmra_valid_validN singleton_op singleton_valid.
    by rewrite -pair_op pair_valid.
  Qed.

Lemma gmap_view_both_dfrac_validNn dp m k dq v :
    ✓{n} (gmap_view_auth dp m ⋅ gmap_view_frag k dq v) ↔
      ∃ v' dq', ✓ dp ∧ m !! k = Some v' ∧ ✓{n} (dq', v') ∧
                Some (dq, v) ≼{n} Some (dq', v').
  Proof.
    rewrite /gmap_view_auth /gmap_view_frag.
    rewrite view_both_dfrac_validN gmap_view_rel_lookup. naive_solver.
  Qed.

Lemma gmap_view_both_validNn dp m k v :
    ✓{n} (gmap_view_auth dp m ⋅ gmap_view_frag k (DfracOwn 1) v) ↔
      ✓ dp ∧ ✓{n} v ∧ m !! k ≡{n}≡ Some v.
  Proof.
    rewrite gmap_view_both_dfrac_validN. split.
    - intros [Hdp (v' & dq' & Hlookup & Hvalid & Hincl)].
      split; first done. rewrite Hlookup.
      destruct (Some_includedN_exclusive _ _ _ Hincl Hvalid) as [_ Heq].
      simpl in Heq. split.
      + rewrite pair_validN in Hvalid. rewrite Heq. naive_solver.
      + by rewrite Heq.
    - intros (Hdp & Hval & Hlookup).
      apply dist_Some_inv_r' in Hlookup as [v' [Hlookup Heq]].
      exists v', (DfracOwn 1). do 2 (split; [done|]). split.
      + rewrite pair_validN. by rewrite -Heq.
      + by apply: Some_includedN_refl.
  Qed.

Lemma gmap_view_both_dfrac_validN_total`{!CmraTotal V} n dp m k dq v :
    ✓{n} (gmap_view_auth dp m ⋅ gmap_view_frag k dq v) →
    ∃ v', ✓ dp ∧ ✓ dq ∧ m !! k = Some v' ∧ ✓{n} v' ∧ v ≼{n} v'.
  Proof.
    rewrite gmap_view_both_dfrac_validN.
    intros (v' & dq' & Hdp & Hlookup & Hvalid & Hincl).
    exists v'. split; first done. split.
    - eapply (cmra_valid_Some_included dq'); first by apply Hvalid.
      eapply cmra_discrete_included_iff.
      eapply Some_pair_includedN_l. done.
    - split; first done. split; first apply Hvalid.
      move:Hincl=> /Some_pair_includedN_r /Some_includedN_total. done.
  Qed.

Lemma gmap_view_both_dfrac_valid_discrete`{!CmraDiscrete V} dp m k dq v :
    ✓ (gmap_view_auth dp m ⋅ gmap_view_frag k dq v) ↔
      ∃ v' dq', ✓ dp ∧ m !! k = Some v' ∧
                ✓ (dq', v') ∧
                Some (dq, v) ≼ Some (dq', v').
  Proof.
    rewrite cmra_valid_validN. setoid_rewrite gmap_view_both_dfrac_validN. split.
    - intros Hvalid. specialize (Hvalid 0ᵢ).
      destruct Hvalid as (v' & dq' & Hdp & Hlookup & Hvalid & Hincl).
      exists v', dq'. do 2 (split; first done).
      split; first by apply cmra_discrete_valid.
      by apply: cmra_discrete_included_r.
    - intros (v' & dq' & Hdp & Hlookup & Hvalid & Hincl) n.
      exists v', dq'. do 2 (split; first done).
      split; first by apply cmra_valid_validN.
      by apply: cmra_included_includedN.
  Qed.

Lemma gmap_view_both_dfrac_valid_discrete_total`{!CmraDiscrete V, !CmraTotal V} dp m k dq v :
    ✓ (gmap_view_auth dp m ⋅ gmap_view_frag k dq v) →
    ∃ v', ✓ dp ∧ ✓ dq ∧ m !! k = Some v' ∧ ✓ v' ∧ v ≼ v'.
  Proof.
    rewrite gmap_view_both_dfrac_valid_discrete.
    intros (v' & dq' & Hdp & Hlookup & Hvalid & Hincl).
    exists v'. split; first done. split.
    - eapply (cmra_valid_Some_included dq'); first by apply Hvalid.
      eapply Some_pair_included_l. done.
    - split; first done. split; first apply Hvalid.
      move:Hincl=> /Some_pair_included_r /Some_included_total. done.
  Qed.

Lemma gmap_view_both_validm dp k v :
    ✓ (gmap_view_auth dp m ⋅ gmap_view_frag k (DfracOwn 1) v) ↔
    ✓ dp ∧ ✓ v ∧ m !! k ≡ Some v.
  Proof.
    rewrite cmra_valid_validN. setoid_rewrite gmap_view_both_validN. split.
    - intros Hvalid. split; last split.
      + eapply (Hvalid 0ᵢ).
      + apply cmra_valid_validN. intros n. eapply Hvalid.
      + apply equiv_dist. intros n. eapply Hvalid.
    - intros (Hdp & Hval & Hlookup). intros n.
      split; first done. split.
      + apply cmra_valid_validN. done.
      + rewrite Hlookup. done.
  Qed.

Lemma gmap_view_allocm k dq v :
    m !! k = None →
    ✓ dq →
    ✓ v →
    gmap_view_auth (DfracOwn 1) m ~~>
      gmap_view_auth (DfracOwn 1) (<[k := v]> m) ⋅ gmap_view_frag k dq v.
  Proof.
    intros Hfresh Hdq Hval. apply view_update_alloc=>n bf Hrel j [df va] /=.
    rewrite lookup_op. destruct (decide (j = k)) as [->|Hne].
    - assert (bf !! k = None) as Hbf.
      { destruct (bf !! k) as [[df' va']|] eqn:Hbf; last done.
        specialize (Hrel _ _ Hbf). destruct Hrel as (v' & dq' & Hm & _).
        exfalso. rewrite Hm in Hfresh. done. }
      rewrite lookup_singleton_eq Hbf right_id.
      intros [= <- <-]. eexists _, _.
      rewrite lookup_insert_eq. split; first done.
      split; last by apply: Some_includedN_refl.
      split; first done. by eapply cmra_valid_validN.
    - rewrite lookup_singleton_ne; last done.
      rewrite left_id=>Hbf.
      specialize (Hrel _ _ Hbf). destruct Hrel as (v' & ? & Hm & ?).
      eexists _, _. split; last done.
      rewrite lookup_insert_ne //.
  Qed.

Lemma gmap_view_alloc_bigm m' dq :
    m' ##ₘ m →
    ✓ dq →
    map_Forall (λ k v, ✓ v) m' →
    gmap_view_auth (DfracOwn 1) m ~~>
      gmap_view_auth (DfracOwn 1) (m' ∪ m) ⋅
      ([^op map] k↦v ∈ m', gmap_view_frag k dq v).
  Proof.
    intros ?? Hm'.
    induction m' as [|k v m' ? IH] using map_ind; decompose_map_disjoint.
    { rewrite big_opM_empty left_id_L right_id. done. }
    apply map_Forall_insert in Hm' as [??]; last done.
    rewrite IH //. rewrite big_opM_insert // assoc.
    apply cmra_update_op; last done.
    rewrite -insert_union_l. apply (gmap_view_alloc _ k dq); [|done..].
    by apply lookup_union_None.
  Qed.

Lemma gmap_view_deletem k v :
    gmap_view_auth (DfracOwn 1) m ⋅ gmap_view_frag k (DfracOwn 1) v ~~>
    gmap_view_auth (DfracOwn 1) (delete k m).
  Proof.
    apply view_update_dealloc=>n bf Hrel j [df va] Hbf /=.
    destruct (decide (j = k)) as [->|Hne].
    - edestruct (Hrel k) as (v' & dq' & ? & Hval & Hincl).
      { rewrite lookup_op Hbf lookup_singleton_eq -Some_op. done. }
      eapply (cmra_validN_Some_includedN _ _ _ Hval) in Hincl as Hval'.
      exfalso. clear Hval Hincl.
      rewrite pair_validN /= in Hval'.
      apply: dfrac_full_exclusive. apply Hval'.
    - edestruct (Hrel j) as (v' & ? & ? & ?).
      { rewrite lookup_op lookup_singleton_ne // Hbf. done. }
      eexists v', _. split; last done.
      rewrite lookup_delete_ne //.
  Qed.

Lemma gmap_view_delete_bigm m' :
    gmap_view_auth (DfracOwn 1) m ⋅
    ([^op map] k↦v ∈ m', gmap_view_frag k (DfracOwn 1) v) ~~>
      gmap_view_auth (DfracOwn 1) (m ∖ m').
  Proof.
    induction m' as [|k v m' ? IH] using map_ind.
    { rewrite right_id_L big_opM_empty right_id //. }
    rewrite big_opM_insert //.
    rewrite [gmap_view_frag _ _ _ ⋅ _]comm assoc IH gmap_view_delete.
    rewrite -delete_difference. done.
  Qed.

Lemma gmap_view_updatem k dq v mv' v' dq' :
    (∀ n mv f,
      m !! k = Some mv →
      ✓{n} ((dq, v) ⋅? f) →
      mv ≡{n}≡ v ⋅? (snd <$> f) →
      ✓{n} ((dq', v') ⋅? f) ∧ mv' ≡{n}≡ v' ⋅? (snd <$> f)) →
    gmap_view_auth (DfracOwn 1) m ⋅ gmap_view_frag k dq v ~~>
      gmap_view_auth (DfracOwn 1) (<[k := mv']> m) ⋅ gmap_view_frag k dq' v'.
  Proof.
    intros Hup. apply view_update=> n bf Hrel j [df va].
    rewrite lookup_op.
    destruct (decide (j = k)) as [->|Hne]; last first.
    {
      simplify_map_eq. rewrite lookup_singleton_ne //.

Lemma gmap_view_update_localm k dq mv v mv' v' :
    m !! k = Some mv →
    (mv, v) ~l~> (mv', v') →
    gmap_view_auth (DfracOwn 1) m ⋅ gmap_view_frag k dq v ~~>
    gmap_view_auth (DfracOwn 1) (<[k := mv']> m) ⋅ gmap_view_frag k dq v'.
  Proof.
    intros Hlookup Hup. apply gmap_view_update.
    intros n mv0 f Hmv0 Hval Hincl.
    rewrite Hlookup in Hmv0. injection Hmv0 as [= <-].
    specialize (Hup n (snd <$> f)). destruct Hup as (Hval' & Hincl').
    { rewrite Hincl. destruct Hval. by destruct f. }
    { simpl. done. }
    split; last done. split.
    - destruct Hval. by destruct f.
    - simpl in *. replace (((dq, v') ⋅? f).2) with (v' ⋅? (snd <$> f)).
      2:{ by destruct f. }
      rewrite -Hincl'. done.
  Qed.

Lemma gmap_view_replacem k v v' :
    ✓ v' →
    gmap_view_auth (DfracOwn 1) m ⋅ gmap_view_frag k (DfracOwn 1) v ~~>
      gmap_view_auth (DfracOwn 1) (<[k := v']> m) ⋅ gmap_view_frag k (DfracOwn 1) v'.
  Proof.

Lemma gmap_view_replace_bigm m0 m1 :
    dom m0 = dom m1 →
    map_Forall (λ k v, ✓ v) m1 →
    gmap_view_auth (DfracOwn 1) m ⋅
    ([^op map] k↦v ∈ m0, gmap_view_frag k (DfracOwn 1) v) ~~>
      gmap_view_auth (DfracOwn 1) (m1 ∪ m) ⋅
      ([^op map] k↦v ∈ m1, gmap_view_frag k (DfracOwn 1) v).
  Proof.
    intros Hdom%eq_sym. revert m1 Hdom.
    induction m0 as [|k v m0 Hnotdom IH] using map_ind; intros m1 Hdom Hval.
    { rewrite dom_empty_L in Hdom.
      apply dom_empty_iff_L in Hdom as ->.
      rewrite left_id_L big_opM_empty. done. }
    rewrite dom_insert_L in Hdom.
    assert (k ∈ dom m1) as Hindom by set_solver.
    apply elem_of_dom in Hindom as [v' Hlookup].
    rewrite big_opM_insert //.
    rewrite [gmap_view_frag _ _ _ ⋅ _]comm assoc.
    rewrite (IH (delete k m1)); last first.
    { by apply map_Forall_delete. }
    { rewrite dom_delete_L Hdom.
      apply not_elem_of_dom in Hnotdom. set_solver -Hdom. }
    rewrite -assoc [_ ⋅ gmap_view_frag _ _ _]comm assoc.
    rewrite (gmap_view_replace _ _ _ v').
    2:{ eapply Hval. done. }
    rewrite (big_opM_delete _ m1 k v') // -assoc.
    rewrite insert_union_r; last by rewrite lookup_delete_eq.
    rewrite union_delete_insert //.
  Qed.

Lemma gmap_view_auth_persistdq m :
    gmap_view_auth dq m ~~> gmap_view_auth DfracDiscarded m.
  Proof. apply view_update_auth_persist. Qed.

Lemma gmap_view_auth_unpersistm :
    gmap_view_auth DfracDiscarded m ~~>: λ a, ∃ q, a = gmap_view_auth (DfracOwn q) m.
  Proof. apply view_updateP_auth_unpersist. Qed.

Local Lemmagmap_view_frag_dfrac k dq P v :
    dq ~~>: P →
    gmap_view_frag k dq v ~~>: λ a, ∃ dq', a = gmap_view_frag k dq' v ∧ P dq'.
  Proof.
    intros Hdq.
    eapply cmra_updateP_weaken;
      [apply view_updateP_frag
         with (P := λ b', ∃ dq', ◯V b' = gmap_view_frag k dq' v ∧ P dq')
      |naive_solver].
    intros m n bf Hrel.
    destruct (Hrel k ((dq, v) ⋅? bf !! k)) as (v' & dq' & Hlookup & Hval & Hincl).
    { by rewrite lookup_op lookup_singleton_eq Some_op_opM. }
    rewrite Some_includedN_opM in Hincl.
    destruct Hincl as [f' Hincl]. rewrite cmra_opM_opM_assoc in Hincl.
    set f := bf !! k ⋅ f'.
    change (bf !! k ⋅ f') with f in Hincl.
    destruct (Hdq n (option_map fst f)) as (dq'' & HPdq'' & Hvdq'').
    { destruct Hincl as [Heq _]. simpl in Heq. rewrite Heq in Hval.
      destruct Hval as [Hval _]. by destruct f. }
    eexists. split; first by exists dq''.
    intros j [df va] Heq.
    destruct (decide (k = j)) as [->|Hne].
    - rewrite lookup_op lookup_singleton_eq in Heq.
      eexists v', (dq'' ⋅? (fst <$> f)).
      split; first done. split.
      + split; last by apply Hval. simpl. done.
      + rewrite -Heq. exists f'.
        rewrite -assoc. change (bf !! j ⋅ f') with f.
        destruct Hincl as [_ Hincl]. simpl in Hincl. rewrite Hincl.
        by destruct f.
    - rewrite lookup_op lookup_singleton_ne // left_id in Heq.
      eapply Hrel. rewrite lookup_op lookup_singleton_ne // left_id Heq //.
  Qed.

Lemma gmap_view_frag_persistk dq v :
    gmap_view_frag k dq v ~~> gmap_view_frag k DfracDiscarded v.
  Proof.
    eapply (cmra_update_lift_updateP (λ dq, gmap_view_frag k dq v)).
    - intros. by apply gmap_view_frag_dfrac.
    - apply dfrac_discard_update.
  Qed.

Lemma gmap_view_frag_unpersistk v :
    gmap_view_frag k DfracDiscarded v ~~>:
      λ a, ∃ q, a = gmap_view_frag k (DfracOwn q) v.
  Proof.
    eapply cmra_updateP_weaken.
    { apply gmap_view_frag_dfrac, dfrac_undiscard_update. }
    naive_solver.
  Qed.

Global Instancegmap_view_frag_core_id k dq v :
    CoreId dq → CoreId v → CoreId (gmap_view_frag k dq v).
  Proof. apply _. Qed.

Global Instancegmap_view_cmra_discrete :
    CmraDiscrete V → CmraDiscrete (gmap_viewR K V).
  Proof. apply _. Qed.

Global Instancegmap_view_frag_mut_is_op dq dq1 dq2 k v v1 v2 :
    IsOp dq dq1 dq2 →
    IsOp v v1 v2 →
    IsOp' (gmap_view_frag k dq v) (gmap_view_frag k dq1 v1) (gmap_view_frag k dq2 v2).
  Proof. rewrite /IsOp' /IsOp => -> ->. apply gmap_view_frag_op. Qed.

Program Definitiongmap_viewURF {SI : sidx} (K : Type) `{Countable K}
    (F : rFunctor) : urFunctor := {|
  urFunctor_car A _ B _ := gmap_viewUR K (rFunctor_car F A B);
  urFunctor_map A1 _ A2 _ B1 _ B2 _ fg :=
    viewO_map (rel:=gmap_view_rel K (rFunctor_car F A1 B1))
              (rel':=gmap_view_rel K (rFunctor_car F A2 B2))
              (gmapO_map (K:=K) (rFunctor_map F fg))
              (gmapO_map (K:=K) (prodO_map cid (rFunctor_map F fg)))
|}.
Next Obligation.
  intros ? K ?? F A1 ? A2 ? B1 ? B2 ? n f g Hfg.
  apply viewO_map_ne.
  - apply gmapO_map_ne, rFunctor_map_ne. done.
  - apply gmapO_map_ne. apply prodO_map_ne; first done.
    apply rFunctor_map_ne. done.
Qed.
Next Obligation.
  intros ? K ? ? F A ? B ? m; simpl in *. rewrite -{2}(view_map_id m).
  apply (view_map_ext _ _ _ _)=> y.
  - rewrite /= -{2}(map_fmap_id y).
    apply: map_fmap_equiv_ext=>k ??.
    apply rFunctor_map_id.
  - rewrite /= -{2}(map_fmap_id y).
    apply: map_fmap_equiv_ext=>k [df va] ?.
    split; first done. simpl.
    apply rFunctor_map_id.
Qed.
Next Obligation.
  intros ? K ?? F A1 ? A2 ? A3 ? B1 ? B2 ? B3 ? f g f' g' m; simpl in *.
  rewrite -view_map_compose.
  apply (view_map_ext _ _ _ _)=> y.
  - rewrite /= -map_fmap_compose.
    apply: map_fmap_equiv_ext=>k ??.
    apply rFunctor_map_compose.
  - rewrite /= -map_fmap_compose.
    apply: map_fmap_equiv_ext=>k [df va] ?.
    split; first done. simpl.
    apply rFunctor_map_compose.
Qed.
Next Obligation.

Global Instancegmap_viewURF_contractive {SI : sidx} `{Countable K} F :
  rFunctorContractive F → urFunctorContractive (gmap_viewURF K F).
Proof.
  intros ? A1 ? A2 ? B1 ? B2 ? n f g Hfg.
  apply viewO_map_ne.
  - apply gmapO_map_ne. apply rFunctor_map_contractive. done.
  - apply gmapO_map_ne. apply prodO_map_ne; first done.
    apply rFunctor_map_contractive. done.
Qed.

Program Definitiongmap_viewRF {SI : sidx} (K : Type) `{Countable K}
     (F : rFunctor) : rFunctor := {|
  rFunctor_car A _ B _ := gmap_viewR K (rFunctor_car F A B);
  rFunctor_map A1 _ A2 _ B1 _ B2 _ fg :=
    viewO_map (rel:=gmap_view_rel K (rFunctor_car F A1 B1))
              (rel':=gmap_view_rel K (rFunctor_car F A2 B2))
              (gmapO_map (K:=K) (rFunctor_map F fg))
              (gmapO_map (K:=K) (prodO_map cid (rFunctor_map F fg)))
|}.
Solve Obligations with apply @gmap_viewURF.

Global Instancegmap_viewRF_contractive {SI : sidx} `{Countable K} F :
  rFunctorContractive F → rFunctorContractive (gmap_viewRF K F).
Proof. apply gmap_viewURF_contractive. Qed.

Global TypeclassesOpaque gmap_view_auth gmap_view_frag.