phanerozoic/Coq-Iris huggingface dataset:
(* iris/algebra/lib/gmap_view.v *)
(* We do not use [local_update] ([~l~>]) in the premise because we also want
  to expose the role of the fractions. *)
Lemma gmap_view_update m 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.
    { (* prove that other keys are unaffected *)
      simplify_map_eq. rewrite lookup_singleton_ne //.
      (* FIXME simplify_map_eq should have done this *)
      rewrite left_id. intros Hbf.
      edestruct (Hrel j) as (mva & mdf & Hlookup & Hval & Hincl).
      { rewrite lookup_op lookup_singleton_ne // left_id //. }
      naive_solver. }
    simplify_map_eq. rewrite lookup_singleton_eq.
    (* FIXME simplify_map_eq should have done this *)
    intros Hbf.
    edestruct (Hrel k) as (mv & mdf & Hlookup & Hval & Hincl).
    { 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'. (* the complete frame *)
    change (bf !! k ⋅ f') with f in Hincl.
    specialize (Hup n mv f). destruct Hup as (Hval' & Hincl').
    { done. }
    { rewrite -Hincl. done. }
    { destruct Hincl as [_ Hincl]. simpl in Hincl. rewrite Hincl.
      by destruct f. }
    eexists mv', (dq' ⋅? (fst <$> f)). split; first done.
    rewrite -Hbf. clear Hbf. split.
    - rewrite Hincl'. destruct Hval'. by destruct f.
    - rewrite Some_op_opM. rewrite Some_includedN_opM.
      exists f'. rewrite Hincl'. 
      rewrite cmra_opM_opM_assoc. change (bf !! k ⋅ f') with f.
      by destruct f.
  Qed.
(* iris/algebra/lib/gmap_view.v *)
(* This derived version cannot exploit [dq = DfracOwn 1]. *)
Lemma gmap_view_update_local m 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.
(* iris/algebra/lib/gmap_view.v *)
Lemma gmap_view_replace m 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.
    (* There would be a simple proof via delete-then-insert... but we use this as a
       sanity check to make sure the update lemma is strong enough. *)
    intros Hval'. apply gmap_view_update.
    intros n mv f Hlookup Hval Hincl.
    destruct f; simpl.
    { apply exclusiveN_l in Hval; first done. apply _. }
    split; last done.
    split; first done. simpl. apply cmra_valid_validN. done.
  Qed.
(* iris/algebra/lib/gmap_view.v *)
Lemma gmap_view_replace_big m 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.
(* iris/algebra/lib/gmap_view.v *)
Lemma gmap_view_auth_persist dq m :
    gmap_view_auth dq m ~~> gmap_view_auth DfracDiscarded m.
Proof. apply view_update_auth_persist. Qed.
(* iris/algebra/lib/gmap_view.v *)
Lemma gmap_view_auth_unpersist m :
    gmap_view_auth DfracDiscarded m ~~>: λ a, ∃ q, a = gmap_view_auth (DfracOwn q) m.
Proof. apply view_updateP_auth_unpersist. Qed.
(* iris/algebra/lib/gmap_view.v *)
Lemma gmap_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'. (* the complete frame *)
    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.
(* iris/algebra/lib/gmap_view.v *)
Lemma gmap_view_frag_persist k 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.
(* iris/algebra/lib/gmap_view.v *)
Lemma gmap_view_frag_unpersist k 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.
(* iris/algebra/lib/gmap_view.v *)
(* Typeclass instances *)
Instance gmap_view_frag_core_id k dq v :
    CoreId dq → CoreId v → CoreId (gmap_view_frag k dq v).
Proof. apply _. Qed.
(* iris/algebra/lib/gmap_view.v *)
Instance gmap_view_cmra_discrete :
    CmraDiscrete V → CmraDiscrete (gmap_viewR K V).
Proof. apply _. Qed.
(* iris/algebra/lib/gmap_view.v *)
Instance gmap_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.
(* iris/algebra/lib/gmap_view.v *)
(* Functor *)
Definition gmap_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.
(* iris/algebra/lib/gmap_view.v *)
Instance gmap_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.
(* iris/algebra/lib/gmap_view.v *)
Definition gmap_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)))
|}.
(* iris/algebra/lib/gmap_view.v *)
Instance gmap_viewRF_contractive {SI : sidx} `{Countable K} F :
  rFunctorContractive F → rFunctorContractive (gmap_viewRF K F).
Proof. apply gmap_viewURF_contractive. Qed.
(* iris/algebra/lib/gset_bij.v *)
(* [gset_bijective] states that for a graph [L] of [(a, b)] pairs, [L] maps
  from [A] to [B] and back deterministically. The key property characterizing
  [gset_bijective] is [gset_bijective_eq_iff]. *)
Definition gset_bijective (L : gset (A * B))
:=
    ∀ a b, (a, b) ∈ L →
    (∀ b', (a, b') ∈ L → b' = b) ∧ (∀ a', (a', b) ∈ L → a' = a).
(* iris/algebra/lib/gset_bij.v *)
(* Properties of [gset_bijective]. *)
Lemma gset_bijective_empty : gset_bijective (∅ : gset (A * B)).
Proof. by intros ?? []%not_elem_of_empty. Qed.
(* iris/algebra/lib/gset_bij.v *)
(* a bijective graph [L] can be extended with a new mapping [(a,b)] as long as
  neither [a] nor [b] is currently mapped to anything. *)
Lemma gset_bijective_extend L a b :
    gset_bijective L →
    (∀ b', (a, b') ∉ L) →
    (∀ a', (a', b) ∉ L) →
    gset_bijective ({[(a, b)]} ∪ L).
Proof. rewrite /gset_bijective. set_solver. Qed.
(* iris/algebra/lib/gset_bij.v *)
Lemma gset_bijective_eq_iff L (a1 a2 : A) (b1 b2 : B) :
    gset_bijective L →
    (a1, b1) ∈ L →
    (a2, b2) ∈ L →
    a1 = a2 ↔ b1 = b2.
Proof. rewrite /gset_bijective. set_solver. Qed.
(* iris/algebra/lib/gset_bij.v *)
Lemma gset_bijective_pair a1 b1 a2 b2 :
    gset_bijective {[(a1, b1); (a2, b2)]} →
    (a1 = a2 ↔ b1 = b2).
Proof. rewrite /gset_bijective. set_solver. Qed.
(* iris/algebra/lib/gset_bij.v *)
Lemma subseteq_gset_bijective L L' :
    gset_bijective L →
    L' ⊆ L →
    gset_bijective L'.
Proof. rewrite /gset_bijective. set_solver. Qed.
(* iris/algebra/lib/gset_bij.v *)
Definition gset_bij_view_rel_raw (n : SI) bijL L: Prop
:=
    L ⊆ bijL ∧ gset_bijective bijL.
(* iris/algebra/lib/gset_bij.v *)
Lemma gset_bij_view_rel_raw_mono n1 n2 bijL1 bijL2 L1 L2 :
    gset_bij_view_rel_raw n1 bijL1 L1 →
    bijL1 ≡{n2}≡ bijL2 →
    L2 ≼{n2} L1 →
    (n2 ≤ n1)%sidx →
    gset_bij_view_rel_raw n2 bijL2 L2.
Proof.
    intros [??] <-%(discrete_iff _ _ _)%leibniz_equiv ?%gset_included _.
    split; [|done]. by trans L1.
  Qed.
(* iris/algebra/lib/gset_bij.v *)
Lemma gset_bij_view_rel_raw_valid n bijL L :
    gset_bij_view_rel_raw n bijL L → ✓{n}L.
Proof. by intros _. Qed.
(* iris/algebra/lib/gset_bij.v *)
Lemma gset_bij_view_rel_raw_unit n :
    ∃ bijL, gset_bij_view_rel_raw n bijL ε.
Proof. exists ∅. split; eauto using gset_bijective_empty. Qed.
(* iris/algebra/lib/gset_bij.v *)
Canonical gset_bij_view_rel : view_rel (gsetO (A * B)) (gsetUR (A * B))
:=
    ViewRel gset_bij_view_rel_raw gset_bij_view_rel_raw_mono
            gset_bij_view_rel_raw_valid gset_bij_view_rel_raw_unit.
(* iris/algebra/lib/gset_bij.v *)
Instance gset_bij_view_rel_discrete : ViewRelDiscrete gset_bij_view_rel.
Proof. intros n bijL L [??]. split; auto. Qed.
(* iris/algebra/lib/gset_bij.v *)
Lemma gset_bij_view_rel_iff n bijL L :
    gset_bij_view_rel n bijL L ↔ L ⊆ bijL ∧ gset_bijective bijL.
Proof. done. Qed.
(* iris/algebra/lib/gset_bij.v *)
Definition gset_bij {SI : sidx} A B `{Countable A, Countable B}
:=
  view (gset_bij_view_rel_raw (A:=A) (B:=B)).
(* iris/algebra/lib/gset_bij.v *)
Definition gset_bijO {SI : sidx} A B `{Countable A, Countable B} : ofe
:=
  viewO (gset_bij_view_rel (A:=A) (B:=B)).
(* iris/algebra/lib/gset_bij.v *)
Definition gset_bijR {SI : sidx} A B `{Countable A, Countable B} : cmra
:=
  viewR (gset_bij_view_rel (A:=A) (B:=B)).
(* iris/algebra/lib/gset_bij.v *)
Definition gset_bijUR {SI : sidx} A B `{Countable A, Countable B} : ucmra
:=
  viewUR (gset_bij_view_rel (A:=A) (B:=B)).
(* iris/algebra/lib/gset_bij.v *)
Definition gset_bij_auth {SI : sidx} `{Countable A, Countable B}
  (dq : dfrac) (L : gset (A * B)) : gset_bij A B
:= ●V{dq} L ⋅ ◯V L.
(* iris/algebra/lib/gset_bij.v *)
Definition gset_bij_elem {SI : sidx} `{Countable A, Countable B}
  (a : A) (b : B) : gset_bij A B
:= ◯V {[ (a, b) ]}.
(* iris/algebra/lib/gset_bij.v *)
Instance gset_bij_elem_core_id a b : CoreId (gset_bij_elem a b).
Proof. apply _. Qed.
(* iris/algebra/lib/gset_bij.v *)
Lemma gset_bij_auth_dfrac_op dq1 dq2 L :
    gset_bij_auth dq1 L ⋅ gset_bij_auth dq2 L ≡ gset_bij_auth (dq1 ⋅ dq2) L.
Proof.
    rewrite /gset_bij_auth view_auth_dfrac_op.
    rewrite (comm _ (●V{dq2} _)) -!assoc (assoc _ (◯V _)).
    by rewrite -core_id_dup (comm _ (◯V _)).
  Qed.
(* iris/algebra/lib/gset_bij.v *)
Lemma gset_bij_auth_dfrac_valid dq L : ✓ gset_bij_auth dq L ↔ ✓ dq ∧ gset_bijective L.
Proof.
    rewrite /gset_bij_auth view_both_dfrac_valid.
    setoid_rewrite gset_bij_view_rel_iff. pose 0ᵢ. naive_solver.
  Qed.
(* iris/algebra/lib/gset_bij.v *)
Lemma gset_bij_auth_valid L : ✓ gset_bij_auth (DfracOwn 1) L ↔ gset_bijective L.
Proof. rewrite gset_bij_auth_dfrac_valid. naive_solver by done. Qed.
(* iris/algebra/lib/gset_bij.v *)
Lemma gset_bij_auth_empty_dfrac_valid dq : ✓ gset_bij_auth (A:=A) (B:=B) dq ∅ ↔ ✓ dq.
Proof.
    rewrite gset_bij_auth_dfrac_valid. naive_solver eauto using gset_bijective_empty.
  Qed.
(* iris/algebra/lib/gset_bij.v *)
Lemma gset_bij_auth_empty_valid : ✓ gset_bij_auth (A:=A) (B:=B) (DfracOwn 1) ∅.
Proof. by apply gset_bij_auth_empty_dfrac_valid. Qed.
(* iris/algebra/lib/gset_bij.v *)
Lemma gset_bij_auth_dfrac_op_valid dq1 dq2 L1 L2 :
    ✓ (gset_bij_auth dq1 L1 ⋅ gset_bij_auth dq2 L2)
    ↔ ✓ (dq1 ⋅ dq2) ∧ L1 = L2 ∧ gset_bijective L1.
Proof.
    rewrite /gset_bij_auth (comm _ (●V{dq2} _)) -!assoc (assoc _ (◯V _)).
    rewrite -view_frag_op (comm _ (◯V _)) assoc. split.
    - move=> /cmra_valid_op_l /view_auth_dfrac_op_valid.
      setoid_rewrite gset_bij_view_rel_iff. pose 0ᵢ. naive_solver.
    - intros (?&->&?). rewrite -core_id_dup -view_auth_dfrac_op.
      apply view_both_dfrac_valid. setoid_rewrite gset_bij_view_rel_iff. naive_solver.
  Qed.
(* iris/algebra/lib/gset_bij.v *)
Lemma gset_bij_auth_op_valid L1 L2 :
    ✓ (gset_bij_auth (DfracOwn 1) L1 ⋅ gset_bij_auth (DfracOwn 1) L2) ↔ False.
Proof. rewrite gset_bij_auth_dfrac_op_valid. naive_solver. Qed.
(* iris/algebra/lib/gset_bij.v *)
Lemma bij_both_dfrac_valid dq L a b :
    ✓ (gset_bij_auth dq L ⋅ gset_bij_elem a b) ↔ ✓ dq ∧ gset_bijective L ∧ (a, b) ∈ L.
Proof.
    rewrite /gset_bij_auth /gset_bij_elem -assoc -view_frag_op view_both_dfrac_valid.
    setoid_rewrite gset_bij_view_rel_iff. pose 0ᵢ. set_solver.
  Qed.
(* iris/algebra/lib/gset_bij.v *)
Lemma bij_both_valid L a b :
    ✓ (gset_bij_auth (DfracOwn 1) L ⋅ gset_bij_elem a b) ↔ gset_bijective L ∧ (a, b) ∈ L.
Proof. rewrite bij_both_dfrac_valid. naive_solver by done. Qed.
(* iris/algebra/lib/gset_bij.v *)
Lemma gset_bij_elem_agree a1 b1 a2 b2 :
    ✓ (gset_bij_elem a1 b1 ⋅ gset_bij_elem a2 b2) → (a1 = a2 ↔ b1 = b2).
Proof.
    rewrite /gset_bij_elem -view_frag_op gset_op view_frag_valid.
    setoid_rewrite gset_bij_view_rel_iff. intros. apply gset_bijective_pair.
    pose 0ᵢ. naive_solver eauto using subseteq_gset_bijective.
  Qed.
(* iris/algebra/lib/gset_bij.v *)
Lemma bij_view_included dq L a b :
    (a,b) ∈ L → gset_bij_elem a b ≼ gset_bij_auth dq L.
Proof.
    intros. etrans; [|apply cmra_included_r].
    apply view_frag_mono, gset_included. set_solver.
  Qed.
(* iris/algebra/lib/gset_bij.v *)
Lemma gset_bij_auth_extend {L} a b :
    (∀ b', (a, b') ∉ L) → (∀ a', (a', b) ∉ L) →
    gset_bij_auth (DfracOwn 1) L ~~> gset_bij_auth (DfracOwn 1) ({[(a, b)]} ∪ L).
Proof.
    intros. apply view_update=> n bijL.
    rewrite !gset_bij_view_rel_iff gset_op.
    set_solver by eauto using gset_bijective_extend.
  Qed.
(* iris/algebra/lib/mono_list.v *)
Definition mono_listR {SI : sidx} (A : ofe) : cmra
:= authR (max_prefix_listUR A).
(* iris/algebra/lib/mono_list.v *)
Definition mono_listUR {SI : sidx} (A : ofe) : ucmra
:= authUR (max_prefix_listUR A).
(* iris/algebra/lib/mono_list.v *)
Definition mono_list_auth {SI : sidx}
    {A : ofe} (q : dfrac) (l : list A) : mono_listR A
:=
  ●{q} (to_max_prefix_list l) ⋅ ◯ (to_max_prefix_list l).
(* iris/algebra/lib/mono_list.v *)
Definition mono_list_lb {SI : sidx} {A : ofe} (l : list A) : mono_listR A
:=
  ◯ (to_max_prefix_list l).
(* iris/algebra/lib/mono_list.v *)
Instance : Params (@mono_list_auth) 3
:= {}.
(* iris/algebra/lib/mono_list.v *)
Instance : Params (@mono_list_lb) 2
:= {}.
(* iris/algebra/lib/mono_list.v *)
Notation "●ML dq l"
:= (mono_list_auth dq l)
  (at level 20, dq custom dfrac at level 1, format "●ML dq  l").
(* iris/algebra/lib/mono_list.v *)
Notation "◯ML l"
:= (mono_list_lb l) (at level 20).
(* iris/algebra/lib/mono_list.v *)
(* Setoid properties *)
Instance mono_list_auth_ne dq : NonExpansive (@mono_list_auth SI A dq).
Proof. solve_proper. Qed.
(* iris/algebra/lib/mono_list.v *)
Instance mono_list_auth_proper dq :
    Proper ((≡) ==> (≡)) (@mono_list_auth SI A dq).
Proof. solve_proper. Qed.
(* iris/algebra/lib/mono_list.v *)
Instance mono_list_lb_ne : NonExpansive (@mono_list_lb SI A).
Proof. solve_proper. Qed.
(* iris/algebra/lib/mono_list.v *)
Instance mono_list_lb_proper : Proper ((≡) ==> (≡)) (@mono_list_lb SI A).
Proof. solve_proper. Qed.
(* iris/algebra/lib/mono_list.v *)
Instance mono_list_lb_dist_inj n :
    Inj (dist n) (dist n) (@mono_list_lb SI A).
Proof. rewrite /mono_list_lb. by intros ?? ?%(inj _)%(inj _). Qed.
(* iris/algebra/lib/mono_list.v *)
Instance mono_list_lb_inj : Inj (≡) (≡) (@mono_list_lb SI A).
Proof. rewrite /mono_list_lb. by intros ?? ?%(inj _)%(inj _). Qed.
(* iris/algebra/lib/mono_list.v *)
(* * Operation *)
Instance mono_list_lb_core_id l : CoreId (◯ML l).
Proof. rewrite /mono_list_lb. apply _. Qed.
(* iris/algebra/lib/mono_list.v *)
Instance mono_list_auth_core_id l : CoreId (●ML□ l).
Proof. rewrite /mono_list_auth. apply _. Qed.
(* iris/algebra/lib/mono_list.v *)
Lemma mono_list_auth_dfrac_op dq1 dq2 l :
    ●ML{dq1 ⋅ dq2} l ≡ ●ML{dq1} l ⋅ ●ML{dq2} l.
Proof.
    rewrite /mono_list_auth auth_auth_dfrac_op.
    rewrite (comm _ (●{dq2} _)) -!assoc (assoc _ (◯ _)).
    by rewrite -core_id_dup (comm _ (◯ _)).
  Qed.
(* iris/algebra/lib/mono_list.v *)
Lemma mono_list_lb_op_l l1 l2 : l1 `prefix_of` l2 → ◯ML l1 ⋅ ◯ML l2 ≡ ◯ML l2.
Proof. intros ?. by rewrite /mono_list_lb -auth_frag_op to_max_prefix_list_op_l. Qed.
(* iris/algebra/lib/mono_list.v *)
Lemma mono_list_lb_op_r l1 l2 : l1 `prefix_of` l2 → ◯ML l2 ⋅ ◯ML l1 ≡ ◯ML l2.
Proof. intros ?. by rewrite /mono_list_lb -auth_frag_op to_max_prefix_list_op_r. Qed.
(* iris/algebra/lib/mono_list.v *)
Lemma mono_list_auth_lb_op dq l : ●ML{dq} l ≡ ●ML{dq} l ⋅ ◯ML l.
Proof.
    by rewrite /mono_list_auth /mono_list_lb -!assoc -auth_frag_op -core_id_dup.
  Qed.
(* iris/algebra/lib/mono_list.v *)
Instance mono_list_auth_dfrac_is_op dq dq1 dq2 l :
    IsOp dq dq1 dq2 → IsOp' (●ML{dq} l) (●ML{dq1} l) (●ML{dq2} l).
Proof. rewrite /IsOp' /IsOp=> ->. rewrite mono_list_auth_dfrac_op //. Qed.
(* iris/algebra/lib/mono_list.v *)
(* * Validity *)
Lemma mono_list_auth_dfrac_validN n dq l : ✓{n} (●ML{dq} l) ↔ ✓ dq.
Proof.
    rewrite /mono_list_auth auth_both_dfrac_validN.
    naive_solver apply to_max_prefix_list_validN.
  Qed.
(* iris/algebra/lib/mono_list.v *)
Lemma mono_list_auth_validN n l : ✓{n} (●ML l).
Proof. by apply mono_list_auth_dfrac_validN. Qed.
(* iris/algebra/lib/mono_list.v *)
Lemma mono_list_auth_dfrac_valid dq l : ✓ (●ML{dq} l) ↔ ✓ dq.
Proof.
    rewrite /mono_list_auth auth_both_dfrac_valid.
    naive_solver apply to_max_prefix_list_valid.
  Qed.
(* iris/algebra/lib/mono_list.v *)
Lemma mono_list_auth_valid l : ✓ (●ML l).
Proof. by apply mono_list_auth_dfrac_valid. Qed.
(* iris/algebra/lib/mono_list.v *)
Lemma mono_list_auth_dfrac_op_validN n dq1 dq2 l1 l2 :
    ✓{n} (●ML{dq1} l1 ⋅ ●ML{dq2} l2) ↔ ✓ (dq1 ⋅ dq2) ∧ l1 ≡{n}≡ l2.
Proof.
    rewrite /mono_list_auth (comm _ (●{dq2} _)) -!assoc (assoc _ (◯ _)).
    rewrite -auth_frag_op (comm _ (◯ _)) assoc. split.
    - move=> /cmra_validN_op_l /auth_auth_dfrac_op_validN.
      rewrite (inj_iff to_max_prefix_list). naive_solver.
    - intros [? ->]. rewrite -core_id_dup -auth_auth_dfrac_op auth_both_dfrac_validN.
      naive_solver apply to_max_prefix_list_validN.
  Qed.
(* iris/algebra/lib/mono_list.v *)
Lemma mono_list_auth_op_validN n l1 l2 : ✓{n} (●ML l1 ⋅ ●ML l2) ↔ False.
Proof. rewrite mono_list_auth_dfrac_op_validN. naive_solver. Qed.
(* iris/algebra/lib/mono_list.v *)
Lemma mono_list_auth_dfrac_op_valid dq1 dq2 l1 l2 :
    ✓ (●ML{dq1} l1 ⋅ ●ML{dq2} l2) ↔ ✓ (dq1 ⋅ dq2) ∧ l1 ≡ l2.
Proof.
    rewrite cmra_valid_validN equiv_dist.
    setoid_rewrite mono_list_auth_dfrac_op_validN. pose 0ᵢ. naive_solver.
  Qed.
(* iris/algebra/lib/mono_list.v *)
Lemma mono_list_auth_op_valid l1 l2 : ✓ (●ML l1 ⋅ ●ML l2) ↔ False.
Proof. rewrite mono_list_auth_dfrac_op_valid. naive_solver. Qed.
(* iris/algebra/lib/mono_list.v *)
Lemma mono_list_auth_dfrac_op_valid_L `{!LeibnizEquiv A} dq1 dq2 l1 l2 :
    ✓ (●ML{dq1} l1 ⋅ ●ML{dq2} l2) ↔ ✓ (dq1 ⋅ dq2) ∧ l1 = l2.
Proof. unfold_leibniz. apply mono_list_auth_dfrac_op_valid. Qed.
(* iris/algebra/lib/mono_list.v *)
Lemma mono_list_both_dfrac_validN n dq l1 l2 :
    ✓{n} (●ML{dq} l1 ⋅ ◯ML l2) ↔ ✓ dq ∧ ∃ l, l1 ≡{n}≡ l2 ++ l.
Proof.
    rewrite /mono_list_auth /mono_list_lb -assoc
      -auth_frag_op auth_both_dfrac_validN -to_max_prefix_list_includedN.
    f_equiv; split.
    - intros [Hincl _]. etrans; [apply: cmra_includedN_r|done].
    - intros. split; [|by apply to_max_prefix_list_validN].
      rewrite {2}(core_id_dup (to_max_prefix_list l1)). by f_equiv.
  Qed.
(* iris/algebra/lib/mono_list.v *)
Lemma mono_list_both_validN n l1 l2 :
    ✓{n} (●ML l1 ⋅ ◯ML l2) ↔ ∃ l, l1 ≡{n}≡ l2 ++ l.
Proof. rewrite mono_list_both_dfrac_validN. split; [naive_solver|done]. Qed.
(* iris/algebra/lib/mono_list.v *)
Lemma mono_list_both_dfrac_valid dq l1 l2 :
    ✓ (●ML{dq} l1 ⋅ ◯ML l2) ↔ ✓ dq ∧ ∃ l, l1 ≡ l2 ++ l.
Proof.
    rewrite /mono_list_auth /mono_list_lb -assoc -auth_frag_op
      auth_both_dfrac_valid -max_prefix_list_included_includedN
      -to_max_prefix_list_included.
    f_equiv; split.
    - intros [Hincl _]. etrans; [apply: cmra_included_r|done].
    - intros. split; [|by apply to_max_prefix_list_valid].
      rewrite {2}(core_id_dup (to_max_prefix_list l1)). by f_equiv.
  Qed.
(* iris/algebra/lib/mono_list.v *)
Lemma mono_list_both_valid l1 l2 :
    ✓ (●ML l1 ⋅ ◯ML l2) ↔ ∃ l, l1 ≡ l2 ++ l.
Proof. rewrite mono_list_both_dfrac_valid. split; [naive_solver|done]. Qed.
(* iris/algebra/lib/mono_list.v *)
Lemma mono_list_both_dfrac_valid_L `{!LeibnizEquiv A} dq l1 l2 :
    ✓ (●ML{dq} l1 ⋅ ◯ML l2) ↔ ✓ dq ∧ l2 `prefix_of` l1.
Proof. rewrite /prefix. rewrite mono_list_both_dfrac_valid. naive_solver. Qed.
(* iris/algebra/lib/mono_list.v *)
Lemma mono_list_both_valid_L `{!LeibnizEquiv A} l1 l2 :
    ✓ (●ML l1 ⋅ ◯ML l2) ↔ l2 `prefix_of` l1.
Proof. rewrite /prefix. rewrite mono_list_both_valid. naive_solver. Qed.
(* iris/algebra/lib/mono_list.v *)
Lemma mono_list_lb_op_validN n l1 l2 :
    ✓{n} (◯ML l1 ⋅ ◯ML l2) ↔ (∃ l, l2 ≡{n}≡ l1 ++ l) ∨ (∃ l, l1 ≡{n}≡ l2 ++ l).
Proof. by rewrite auth_frag_op_validN to_max_prefix_list_op_validN. Qed.