phanerozoic/Coq-Iris huggingface dataset:
(* iris/algebra/gmultiset.v *)
Lemma gmultiset_op X Y : X ⋅ Y = X ⊎ Y.
Proof. done. Qed.
(* iris/algebra/gmultiset.v *)
Lemma gmultiset_core X : core X = ∅.
Proof. done. Qed.
(* iris/algebra/gmultiset.v *)
Lemma gmultiset_included X Y : X ≼ Y ↔ X ⊆ Y.
Proof.
    split.
    - intros [Z ->%leibniz_equiv].
      rewrite gmultiset_op. apply gmultiset_disj_union_subseteq_l.
    - intros ->%gmultiset_disj_union_difference. by exists (Y ∖ X).
  Qed.
(* iris/algebra/gmultiset.v *)
Lemma gmultiset_ra_mixin : RAMixin (gmultiset K).
Proof.
    apply ra_total_mixin; eauto.
    - by intros X Y Z ->%leibniz_equiv.
    - by intros X Y ->%leibniz_equiv.
    - solve_proper.
    - intros X1 X2 X3. by rewrite !gmultiset_op assoc_L.
    - intros X1 X2. by rewrite !gmultiset_op comm_L.
    - intros X. by rewrite gmultiset_core left_id.
    - intros X1 X2 HX. rewrite !gmultiset_core. exists ∅.
      by rewrite left_id.
  Qed.
(* iris/algebra/gmultiset.v *)
Canonical gmultisetR
:= discreteR (gmultiset K) gmultiset_ra_mixin.
(* iris/algebra/gmultiset.v *)
Instance gmultiset_cmra_discrete : CmraDiscrete gmultisetR.
Proof. apply discrete_cmra_discrete. Qed.
(* iris/algebra/gmultiset.v *)
Lemma gmultiset_ucmra_mixin : UcmraMixin (gmultiset K).
Proof.
    split; [done | | done]. intros X.
    by rewrite gmultiset_op left_id_L.
  Qed.
(* iris/algebra/gmultiset.v *)
Canonical gmultisetUR
:= Ucmra (gmultiset K) gmultiset_ucmra_mixin.
(* iris/algebra/gmultiset.v *)
Instance gmultiset_cancelable X : Cancelable X.
Proof.
    apply: discrete_cancelable=> Y Z _ ?. fold_leibniz. by apply (inj (X ⊎.)).
  Qed.
(* iris/algebra/gmultiset.v *)
Lemma gmultiset_opM X mY : X ⋅? mY = X ⊎ default ∅ mY.
Proof. destruct mY; by rewrite /= ?right_id_L. Qed.
(* iris/algebra/gmultiset.v *)
Lemma gmultiset_update X Y : X ~~> Y.
Proof. done. Qed.
(* iris/algebra/gmultiset.v *)
Lemma gmultiset_local_update X Y X' Y' : X ⊎ Y' = X' ⊎ Y → (X,Y) ~l~> (X', Y').
Proof.
    intros HXY. rewrite local_update_unital_discrete=> Z' _. intros ->%leibniz_equiv.
    split; first done. apply leibniz_equiv_iff, (inj (.⊎ Y)).
    rewrite -HXY !gmultiset_op.
    by rewrite -(comm_L _ Y) (comm_L _ Y') assoc_L.
  Qed.
(* iris/algebra/gmultiset.v *)
Lemma gmultiset_local_update_alloc X Y X' : (X,Y) ~l~> (X ⊎ X', Y ⊎ X').
Proof. apply gmultiset_local_update. by rewrite (comm_L _ Y) assoc_L. Qed.
(* iris/algebra/gmultiset.v *)
Lemma gmultiset_local_update_dealloc X Y X' :
    X' ⊆ Y → (X,Y) ~l~> (X ∖ X', Y ∖ X').
Proof.
    intros ->%gmultiset_disj_union_difference. apply local_update_total_valid.
    intros _ _ ->%gmultiset_included%gmultiset_disj_union_difference.
    apply gmultiset_local_update. apply gmultiset_eq=> x.
    repeat (rewrite multiplicity_difference || rewrite multiplicity_disj_union).
    lia.
  Qed.
(* iris/algebra/gmultiset.v *)
Lemma big_opMS_singletons X :
    ([^op mset] x ∈ X, {[+ x +]}) = X.
Proof.
    induction X as [|x X IH] using gmultiset_ind.
    - rewrite big_opMS_empty. done.
    - unfold_leibniz. rewrite big_opMS_disj_union // big_opMS_singleton IH //.
  Qed.
(* iris/algebra/gset.v *)
Canonical gsetO
:= discreteO (gset K).
(* iris/algebra/gset.v *)
Instance gset_valid_instance : Valid (gset K)
:= λ _, True.
(* iris/algebra/gset.v *)
Instance gset_unit_instance : Unit (gset K)
:= (∅ : gset K).
(* iris/algebra/gset.v *)
Instance gset_op_instance : Op (gset K)
:= union.
(* iris/algebra/gset.v *)
Instance gset_pcore_instance : PCore (gset K)
:= λ X, Some X.
(* iris/algebra/gset.v *)
Lemma gset_op X Y : X ⋅ Y = X ∪ Y.
Proof. done. Qed.
(* iris/algebra/gset.v *)
Lemma gset_core X : core X = X.
Proof. done. Qed.
(* iris/algebra/gset.v *)
Lemma gset_included X Y : X ≼ Y ↔ X ⊆ Y.
Proof.
    split.
    - intros [Z ->]. rewrite gset_op. set_solver.
    - intros (Z&->&?)%subseteq_disjoint_union_L. by exists Z.
  Qed.
(* iris/algebra/gset.v *)
Lemma gset_ra_mixin : RAMixin (gset K).
Proof.
    apply ra_total_mixin; apply _ || eauto; [].
    intros X. by rewrite gset_core idemp_L.
  Qed.
(* iris/algebra/gset.v *)
Canonical gsetR
:= discreteR (gset K) gset_ra_mixin.
(* iris/algebra/gset.v *)
Instance gset_cmra_discrete : CmraDiscrete gsetR.
Proof. apply discrete_cmra_discrete. Qed.
(* iris/algebra/gset.v *)
Lemma gset_ucmra_mixin : UcmraMixin (gset K).
Proof. split; [ done | | done ]. intros X. by rewrite gset_op left_id_L. Qed.
(* iris/algebra/gset.v *)
Canonical gsetUR
:= Ucmra (gset K) gset_ucmra_mixin.
(* iris/algebra/gset.v *)
Lemma gset_opM X mY : X ⋅? mY = X ∪ default ∅ mY.
Proof using SI. destruct mY; by rewrite /= ?right_id_L. Qed.
(* iris/algebra/gset.v *)
Lemma gset_update X Y : X ~~> Y.
Proof. done. Qed.
(* iris/algebra/gset.v *)
Lemma gset_local_update X Y X' : X ⊆ X' → (X,Y) ~l~> (X',X').
Proof.
    intros (Z&->&?)%subseteq_disjoint_union_L.
    rewrite local_update_unital_discrete=> Z' _ /leibniz_equiv_iff->.
    split; [done|]. rewrite gset_op. set_solver.
  Qed.
(* iris/algebra/gset.v *)
Instance gset_core_id X : CoreId X.
Proof. by apply core_id_total; rewrite gset_core. Qed.
(* iris/algebra/gset.v *)
Lemma big_opS_singletons X :
    ([^op set] x ∈ X, {[ x ]}) = X.
Proof.
    induction X as [|x X Hx IH] using set_ind_L.
    - rewrite big_opS_empty. done.
    - unfold_leibniz. rewrite big_opS_insert // IH //.
  Qed.
(* iris/algebra/gset.v *)
(* Add support [X ≼ Y] to [set_solver]. (We get support for [⋅] for free
  because it is definitionally equal to [∪]). *)
Instance set_unfold_gset_included X Y Q :
    SetUnfold (X ⊆ Y) Q → SetUnfold (X ≼ Y) Q.
Proof. intros [?]; constructor. by rewrite gset_included. Qed.
(* iris/algebra/gset.v *)
(* The disjoint union CMRA *)
Inductive gset_disj K `{Countable K}
:=
  | GSet : gset K → gset_disj K
  | GSetInvalid : gset_disj K.
(* iris/algebra/gset.v *)
Instance GSet_inj : Inj (=@{gset K}) (=) GSet.
Proof. intros ???. naive_solver. Qed.
(* iris/algebra/gset.v *)
Canonical gset_disjO
:= leibnizO (gset_disj K).
(* iris/algebra/gset.v *)
Instance gset_disj_valid_instance : Valid (gset_disj K)
:= λ X,
    match X with GSet _ => True | GSetInvalid => False end.
(* iris/algebra/gset.v *)
Instance gset_disj_unit_instance : Unit (gset_disj K)
:= GSet ∅.
(* iris/algebra/gset.v *)
Instance gset_disj_op_instance : Op (gset_disj K)
:= λ X Y,
    match X, Y with
    | GSet X, GSet Y => if decide (X ## Y) then GSet (X ∪ Y) else GSetInvalid
    | _, _ => GSetInvalid
    end.
(* iris/algebra/gset.v *)
Instance gset_disj_pcore_instance : PCore (gset_disj K)
:= λ _, Some ε.
(* iris/algebra/gset.v *)
Ltac gset_disj_solve
:=
    repeat (simpl || case_decide);
    first [apply (f_equal GSet)|done|exfalso]; set_solver by eauto.
(* iris/algebra/gset.v *)
Lemma gset_disj_included X Y : GSet X ≼ GSet Y ↔ X ⊆ Y.
Proof.
    split.
    - move=> [[Z|]]; simpl; try case_decide; set_solver.
    - intros (Z&->&?)%subseteq_disjoint_union_L.
      exists (GSet Z). gset_disj_solve.
  Qed.
(* iris/algebra/gset.v *)
Lemma gset_disj_valid_inv_l X Y : ✓ (GSet X ⋅ Y) → ∃ Y', Y = GSet Y' ∧ X ## Y'.
Proof. destruct Y; repeat (simpl || case_decide); by eauto. Qed.
(* iris/algebra/gset.v *)
Lemma gset_disj_union X Y : X ## Y → GSet X ⋅ GSet Y = GSet (X ∪ Y).
Proof. intros. by rewrite /= decide_True. Qed.
(* iris/algebra/gset.v *)
Lemma gset_disj_valid_op X Y : ✓ (GSet X ⋅ GSet Y) ↔ X ## Y.
Proof. simpl. case_decide; by split. Qed.
(* iris/algebra/gset.v *)
Lemma gset_disj_ra_mixin : RAMixin (gset_disj K).
Proof.
    apply ra_total_mixin; eauto.
    - intros [?|]; destruct 1; gset_disj_solve.
    - by constructor.
    - by destruct 1.
    - intros [X1|] [X2|] [X3|]; gset_disj_solve.
    - intros [X1|] [X2|]; gset_disj_solve.
    - intros [X|]; gset_disj_solve.
    - exists (GSet ∅); gset_disj_solve.
    - intros [X1|] [X2|]; gset_disj_solve.
  Qed.
(* iris/algebra/gset.v *)
Canonical gset_disjR
:= discreteR (gset_disj K) gset_disj_ra_mixin.
(* iris/algebra/gset.v *)
Instance gset_disj_cmra_discrete : CmraDiscrete gset_disjR.
Proof. apply discrete_cmra_discrete. Qed.
(* iris/algebra/gset.v *)
Lemma gset_disj_ucmra_mixin : UcmraMixin (gset_disj K).
Proof. split; try apply _ || done. intros [X|]; gset_disj_solve. Qed.
(* iris/algebra/gset.v *)
Canonical gset_disjUR
:= Ucmra (gset_disj K) gset_disj_ucmra_mixin.
(* iris/algebra/gset.v *)
Lemma gset_disj_alloc_updateP_strong P (Q : gset_disj K → Prop) X :
    (∀ Y, X ⊆ Y → ∃ j, j ∉ Y ∧ P j) →
    (∀ i, i ∉ X → P i → Q (GSet ({[i]} ∪ X))) →
    GSet X ~~>: Q.
Proof.
    intros Hfresh HQ.
    apply cmra_discrete_total_updateP=> ? /gset_disj_valid_inv_l [Y [->?]].
    destruct (Hfresh (X ∪ Y)) as (i&?&?); first set_solver.
    exists (GSet ({[ i ]} ∪ X)); split.
    - apply HQ; set_solver by eauto.
    - apply gset_disj_valid_op. set_solver by eauto.
  Qed.
(* iris/algebra/gset.v *)
Lemma gset_disj_alloc_updateP_strong' P X :
    (∀ Y, X ⊆ Y → ∃ j, j ∉ Y ∧ P j) →
    GSet X ~~>: λ Y, ∃ i, Y = GSet ({[ i ]} ∪ X) ∧ i ∉ X ∧ P i.
Proof. eauto using gset_disj_alloc_updateP_strong. Qed.
(* iris/algebra/gset.v *)
Lemma gset_disj_alloc_empty_updateP_strong P (Q : gset_disj K → Prop) :
    (∀ Y : gset K, ∃ j, j ∉ Y ∧ P j) →
    (∀ i, P i → Q (GSet {[i]})) → GSet ∅ ~~>: Q.
Proof.
    intros. apply (gset_disj_alloc_updateP_strong P); eauto.
    intros i; rewrite right_id_L; auto.
  Qed.
(* iris/algebra/gset.v *)
Lemma gset_disj_alloc_empty_updateP_strong' P :
    (∀ Y : gset K, ∃ j, j ∉ Y ∧ P j) →
    GSet ∅ ~~>: λ Y, ∃ i, Y = GSet {[ i ]} ∧ P i.
Proof. eauto using gset_disj_alloc_empty_updateP_strong. Qed.
(* iris/algebra/gset.v *)
Lemma gset_disj_alloc_updateP (Q : gset_disj K → Prop) X :
      (∀ i, i ∉ X → Q (GSet ({[i]} ∪ X))) → GSet X ~~>: Q.
Proof.
      intro; eapply gset_disj_alloc_updateP_strong with (λ _, True); eauto.
      intros Y ?; exists (fresh Y). split; [|done]. apply is_fresh.
    Qed.
(* iris/algebra/gset.v *)
Lemma gset_disj_alloc_updateP' X :
      GSet X ~~>: λ Y, ∃ i, Y = GSet ({[ i ]} ∪ X) ∧ i ∉ X.
Proof. eauto using gset_disj_alloc_updateP. Qed.
(* iris/algebra/gset.v *)
Lemma gset_disj_alloc_empty_updateP (Q : gset_disj K → Prop) :
      (∀ i, Q (GSet {[i]})) → GSet ∅ ~~>: Q.
Proof.
      intro. apply gset_disj_alloc_updateP. intros i; rewrite right_id_L; auto.
    Qed.
(* iris/algebra/gset.v *)
Lemma gset_disj_alloc_empty_updateP' : GSet ∅ ~~>: λ Y, ∃ i, Y = GSet {[ i ]}.
Proof. eauto using gset_disj_alloc_empty_updateP. Qed.
(* iris/algebra/gset.v *)
Lemma gset_disj_dealloc_local_update X Y :
    (GSet X, GSet Y) ~l~> (GSet (X ∖ Y), GSet ∅).
Proof.
    apply local_update_total_valid=> _ _ /gset_disj_included HYX.
    rewrite local_update_unital_discrete=> -[Xf|] _ /leibniz_equiv_iff //=.
    rewrite {1}/op /=. destruct (decide _) as [HXf|]; [intros[= ->]|done].
    by rewrite difference_union_distr_l_L
      difference_diag_L !left_id_L difference_disjoint_L.
  Qed.
(* iris/algebra/gset.v *)
Lemma gset_disj_dealloc_empty_local_update X Z :
    (GSet Z ⋅ GSet X, GSet Z) ~l~> (GSet X, GSet ∅).
Proof.
    apply local_update_total_valid=> /gset_disj_valid_op HZX _ _.
    assert (X = (Z ∪ X) ∖ Z) as HX by set_solver.
    rewrite gset_disj_union // {2}HX. apply gset_disj_dealloc_local_update.
  Qed.
(* iris/algebra/gset.v *)
Lemma gset_disj_dealloc_op_local_update X Y Z :
    (GSet Z ⋅ GSet X, GSet Z ⋅ GSet Y) ~l~> (GSet X,GSet Y).
Proof.
    rewrite -{2}(left_id ε _ (GSet Y)).
    apply op_local_update_frame, gset_disj_dealloc_empty_local_update.
  Qed.
(* iris/algebra/gset.v *)
Lemma gset_disj_alloc_op_local_update X Y Z :
    Z ## X → (GSet X,GSet Y) ~l~> (GSet Z ⋅ GSet X, GSet Z ⋅ GSet Y).
Proof.
    intros. apply op_local_update_discrete. by rewrite gset_disj_valid_op.
  Qed.
(* iris/algebra/gset.v *)
Lemma gset_disj_alloc_local_update X Y Z :
    Z ## X → (GSet X,GSet Y) ~l~> (GSet (Z ∪ X), GSet (Z ∪ Y)).
Proof.
    intros. apply local_update_total_valid=> _ _ /gset_disj_included ?.
    rewrite -!gset_disj_union //; last set_solver.
    auto using gset_disj_alloc_op_local_update.
  Qed.
(* iris/algebra/gset.v *)
Lemma gset_disj_alloc_empty_local_update X Z :
    Z ## X → (GSet X, GSet ∅) ~l~> (GSet (Z ∪ X), GSet Z).
Proof.
    intros. rewrite -{2}(right_id_L _ union Z).
    apply gset_disj_alloc_local_update; set_solver.
  Qed.
(* iris/algebra/gset.v *)
(* Add some basic support for [GSet X = GSet Y], [GSet X ≼ GSet Y], and
  [✓ (GSet X ⋅ GSet Y)] to [set_solver]. There are probably more cases we could
  cover (e.g., involving [GSetInvalid], or nesting of [⋅]), but it is not clear
  these are useful in practice, nor how to handle them effectively. *)
Instance set_unfold_gset_eq (X Y : gset K) Q :
    SetUnfold (X = Y) Q → SetUnfold (GSet X = GSet Y) Q.
Proof. intros [?]; constructor. by rewrite (inj_iff _). Qed.
(* iris/algebra/gset.v *)
Instance set_unfold_gset_disj_included (X Y : gset K) Q :
    SetUnfold (X ⊆ Y) Q → SetUnfold (GSet X ≼ GSet Y) Q.
Proof. intros [?]; constructor. by rewrite gset_disj_included. Qed.
(* iris/algebra/gset.v *)
Instance set_unfold_gset_disj_valid_op (X Y : gset K) Q :
    SetUnfold (X ## Y) Q → SetUnfold (✓ (GSet X ⋅ GSet Y)) Q.
Proof. intros [?]; constructor. by rewrite gset_disj_valid_op. Qed.
(* iris/algebra/list.v *)
Instance list_dist : Dist (list A)
:= λ n, Forall2 (dist n).
(* iris/algebra/list.v *)
Lemma list_dist_Forall2 n l k : l ≡{n}≡ k ↔ Forall2 (dist n) l k.
Proof. done. Qed.
(* iris/algebra/list.v *)
Lemma list_dist_lookup n l1 l2 : l1 ≡{n}≡ l2 ↔ ∀ i, l1 !! i ≡{n}≡ l2 !! i.
Proof. setoid_rewrite option_dist_Forall2. apply Forall2_lookup. Qed.
(* iris/algebra/list.v *)
Instance cons_ne : NonExpansive2 (@cons A)
:= _.
(* iris/algebra/list.v *)
Instance app_ne : NonExpansive2 (@app A)
:= _.
(* iris/algebra/list.v *)
Instance length_ne n : Proper (dist n ==> (=)) (@length A)
:= _.
(* iris/algebra/list.v *)
Instance tail_ne : NonExpansive (@tail A)
:= _.
(* iris/algebra/list.v *)
Instance take_ne n : NonExpansive (@take A n)
:= _.
(* iris/algebra/list.v *)
Instance drop_ne n : NonExpansive (@drop A n)
:= _.
(* iris/algebra/list.v *)
Instance head_ne : NonExpansive (head (A:=A)).
Proof. destruct 1; by constructor. Qed.
(* iris/algebra/list.v *)
Instance list_lookup_ne i : NonExpansive (lookup (M:=list A) i).
Proof. intros ????. by apply option_dist_Forall2, Forall2_lookup. Qed.
(* iris/algebra/list.v *)
Instance list_lookup_total_ne `{!Inhabited A} i :
  NonExpansive (lookup_total (M:=list A) i).
Proof. intros ???. rewrite !list_lookup_total_alt. by intros ->. Qed.
(* iris/algebra/list.v *)
Instance list_alter_ne n :
  Proper ((dist n ==> dist n) ==> (=) ==> dist n ==> dist n) (alter (M:=list A))
:= _.
(* iris/algebra/list.v *)
Instance list_insert_ne i : NonExpansive2 (insert (M:=list A) i)
:= _.
(* iris/algebra/list.v *)
Instance list_inserts_ne i : NonExpansive2 (@list_inserts A i)
:= _.
(* iris/algebra/list.v *)
Instance list_delete_ne i : NonExpansive (delete (M:=list A) i)
:= _.
(* iris/algebra/list.v *)
Instance option_list_ne : NonExpansive (@option_list A).
Proof. intros ????; by apply Forall2_option_list, option_dist_Forall2. Qed.
(* iris/algebra/list.v *)
Instance list_filter_ne n P `{∀ x, Decision (P x)} :
  Proper (dist n ==> iff) P →
  Proper (dist n ==> dist n) (filter (B:=list A) P)
:= _.
(* iris/algebra/list.v *)
Instance replicate_ne n : NonExpansive (@replicate A n)
:= _.
(* iris/algebra/list.v *)
Instance reverse_ne : NonExpansive (@reverse A)
:= _.
(* iris/algebra/list.v *)
Instance last_ne : NonExpansive (@last A).
Proof. intros ????; by apply option_dist_Forall2, Forall2_last. Qed.
(* iris/algebra/list.v *)
Instance resize_ne n : NonExpansive2 (@resize A n)
:= _.
(* iris/algebra/list.v *)
Instance cons_dist_inj n :
  Inj2 (dist n) (dist n) (dist n) (@cons A).
Proof. by inversion_clear 1. Qed.
(* iris/algebra/list.v *)
Lemma nil_dist_eq n l : l ≡{n}≡ [] ↔ l = [].
Proof. split; by inversion 1. Qed.
(* iris/algebra/list.v *)
Lemma cons_dist_eq n l k y :
  l ≡{n}≡ y :: k → ∃ x l', x ≡{n}≡ y ∧ l' ≡{n}≡ k ∧ l = x :: l'.
Proof. apply Forall2_cons_inv_r. Qed.
(* iris/algebra/list.v *)
Lemma app_dist_eq n l k1 k2 :
  l ≡{n}≡ k1 ++ k2 ↔ ∃ k1' k2', l = k1' ++ k2' ∧ k1' ≡{n}≡ k1 ∧ k2' ≡{n}≡ k2.
Proof. rewrite list_dist_Forall2 Forall2_app_inv_r. naive_solver. Qed.
(* iris/algebra/list.v *)
Lemma list_singleton_dist_eq n l x :
  l ≡{n}≡ [x] ↔ ∃ x', l = [x'] ∧ x' ≡{n}≡ x.
Proof.
  split; [|by intros (?&->&->)].
  intros (?&?&?&->%Forall2_nil_inv_r&->)%list_dist_Forall2%Forall2_cons_inv_r.
  eauto.
Qed.
(* iris/algebra/list.v *)
Definition list_ofe_mixin : OfeMixin (list A).
Proof.
  split.
  - intros l k. rewrite list_equiv_Forall2 -Forall2_forall.
    split; induction 1; constructor; intros; try apply equiv_dist; auto.
  - apply _.
  - rewrite /dist /list_dist. eauto using Forall2_impl, dist_le.
Qed.
(* iris/algebra/list.v *)
Canonical listO
:= Ofe (list A) list_ofe_mixin.
(* iris/algebra/list.v *)
(* To define [compl : chain (list A) → list A] we make use of the fact that
given a given chain [c0, c1, c2, ...] of lists, the list [c0] completely
determines the shape (i.e., the length) of all lists in the chain. So, the
[compl] operation is defined by structural recursion on [c0], and takes the
completion of the elements of all lists in the chain point-wise. We use [head]
and [tail] as the inverse of [cons]. *)
Fixpoint list_compl_go `{!Cofe A} (c0 : list A) (c : chain listO) : listO
:=
  match c0 with
  | [] => []
  | x :: c0 => compl (chain_map (default x ∘ head) c) ::
               list_compl_go c0 (chain_map tail c)
  end.
(* iris/algebra/list.v *)
Fixpoint list_lbcompl_go `{!Cofe A} (c0 : list A) {n} Hn (c : bchain listO n) : listO
:=
  match c0 with
  | [] => []
  | x :: c0 => lbcompl Hn (bchain_map (default x ∘ head) c) ::
               list_lbcompl_go c0 Hn (bchain_map tail c)
  end.
(* iris/algebra/list.v *)
Instance list_cofe `{!Cofe A} : Cofe listO := {
  compl c := list_compl_go (c 0ᵢ) c;
  lbcompl n Hn c := list_lbcompl_go (c _ (SIdx.limit_lt_0 _ Hn)) Hn c
}.
Next Obligation.
  intros ? n c; simpl.
  assert (c 0ᵢ ≡{0ᵢ}≡ c n) as Hc0 by (symmetry; apply chain_cauchy, SIdx.le_0_l).
  revert Hc0. generalize (c 0ᵢ)=> c0. revert c.
  induction c0 as [|x c0 IH]=> c Hc0 /=.
  { by inversion Hc0. }
  apply symmetry, cons_dist_eq in Hc0 as (x' & xs' & Hx & Hc0 & Hcn).
  rewrite Hcn. f_equiv.
  - rewrite conv_compl.
    by rewrite /chain_map //= Hcn.
  - rewrite IH /chain_map /= ?Hcn //.
Qed.
(* iris/algebra/list.v *)
Instance list_ofe_discrete : OfeDiscrete A → OfeDiscrete listO.
Proof. induction 2; constructor; try apply (discrete_0 _); auto. Qed.
(* iris/algebra/list.v *)
Instance nil_discrete : Discrete (@nil A).
Proof. inversion_clear 1; constructor. Qed.
(* iris/algebra/list.v *)
Instance cons_discrete x l : Discrete x → Discrete l → Discrete (x :: l).
Proof. intros ??; inversion_clear 1; constructor; by apply discrete_0. Qed.
(* iris/algebra/list.v *)
Lemma dist_Permutation n l1 l2 l3 :
  l1 ≡{n}≡ l2 → l2 ≡ₚ l3 → ∃ l2', l1 ≡ₚ l2' ∧ l2' ≡{n}≡ l3.
Proof.
  intros Hequiv Hperm. revert l1 Hequiv.
  induction Hperm as [|x l2 l3 _ IH|x y l2|l2 l3 l4 _ IH1 _ IH2]; intros l1.
  - intros ?. by exists l1.
  - intros (x'&l2'&?&(l2''&?&?)%IH&->)%cons_dist_eq.
    exists (x' :: l2''). by repeat constructor.
  - intros (y'&?&?&(x'&l2'&?&?&->)%cons_dist_eq&->)%cons_dist_eq.
    exists (x' :: y' :: l2'). by repeat constructor.
  - intros (l2'&?&(l3'&?&?)%IH2)%IH1. exists l3'. split; [by etrans|done].
Qed.
(* iris/algebra/list.v *)
(* Non-expansiveness of higher-order list functions and big-ops *)
Instance list_fmap_ne {SI : sidx} {A B : ofe} n :
  Proper ((dist n ==> dist n) ==> (≡{n}@{list A}≡) ==> (≡{n}@{list B}≡)) fmap.
Proof. intros f1 f2 Hf l1 l2 Hl; by eapply Forall2_fmap, Forall2_impl; eauto. Qed.
(* iris/algebra/list.v *)
Instance list_omap_ne {SI : sidx} {A B : ofe} n :
  Proper ((dist n ==> dist n) ==> (≡{n}@{list A}≡) ==> (≡{n}@{list B}≡)) omap.
Proof.
  intros f1 f2 Hf. induction 1 as [|x1 x2 l1 l2 Hx Hl]; csimpl; [constructor|].
  destruct (Hf _ _ Hx); [f_equiv|]; auto.
Qed.
(* iris/algebra/list.v *)
Instance imap_ne {SI : sidx} {A B : ofe} n :
  Proper (pointwise_relation _ ((dist n ==> dist n)) ==> dist n ==> dist n)
         (imap (A:=A) (B:=B)).
Proof.
  intros f1 f2 Hf l1 l2 Hl. revert f1 f2 Hf.
  induction Hl as [|x1 x2 l1 l2 ?? IH]; intros f1 f2 Hf; simpl; [constructor|].
  f_equiv; [by apply Hf|]. apply IH. intros i y1 y2 Hy. by apply Hf.
Qed.
(* iris/algebra/list.v *)
Instance list_bind_ne {SI : sidx} {A B : ofe} n :
  Proper ((dist n ==> dist n) ==> (≡{n}@{list B}≡) ==> (≡{n}@{list A}≡)) mbind.
Proof. intros f1 f2 Hf. induction 1; csimpl; [constructor|f_equiv; auto]. Qed.
(* iris/algebra/list.v *)
Instance list_join_ne {SI : sidx} {A : ofe} n :
  Proper (dist n ==> (≡{n}@{list A}≡)) mjoin.
Proof. induction 1; simpl; [constructor|solve_proper]. Qed.
(* iris/algebra/list.v *)
Instance zip_with_ne {SI : sidx} {A B C : ofe} n :
  Proper ((dist n ==> dist n ==> dist n) ==> dist n ==> dist n ==> dist n)
         (zip_with (A:=A) (B:=B) (C:=C)).
Proof.
  intros f1 f2 Hf.
  induction 1; destruct 1; simpl; [constructor..|f_equiv; try apply Hf; auto].
Qed.
(* iris/algebra/list.v *)
Instance list_fmap_dist_inj {SI : sidx} {A B : ofe} (f : A → B) n :
  Inj (≡{n}≡) (≡{n}≡) f → Inj (≡{n}@{list A}≡) (≡{n}@{list B}≡) (fmap f).
Proof. apply list_fmap_inj. Qed.
(* iris/algebra/list.v *)
Lemma big_opL_ne_2 {SI : sidx} {M : ofe}
    {o : M → M → M} `{!Monoid o u} {A : ofe} (f g : nat → A → M) l1 l2 n :
  l1 ≡{n}≡ l2 →
  (∀ k y1 y2,
    l1 !! k = Some y1 → l2 !! k = Some y2 → y1 ≡{n}≡ y2 → f k y1 ≡{n}≡ g k y2) →
  ([^o list] k ↦ y ∈ l1, f k y) ≡{n}≡ ([^o list] k ↦ y ∈ l2, g k y).
Proof.
  intros Hl Hf. apply big_opL_gen_proper_2; try (apply _ || done).
  { apply monoid_ne. }
  intros k. assert (l1 !! k ≡{n}≡ l2 !! k) as Hlk by (by f_equiv).
  destruct (l1 !! k) eqn:?, (l2 !! k) eqn:?; inversion Hlk; naive_solver.
Qed.
(* iris/algebra/list.v *)
(* Functor *)
Lemma list_fmap_ext_ne {SI : sidx} {A} {B : ofe} (f g : A → B) (l : list A) n :
  (∀ x, f x ≡{n}≡ g x) → f <$> l ≡{n}≡ g <$> l.
Proof. intros Hf. by apply Forall2_fmap, Forall_Forall2_diag, Forall_true. Qed.
(* iris/algebra/list.v *)
Definition listO_map {SI : sidx} {A B} (f : A -n> B) : listO A -n> listO B
:=
  OfeMor (fmap f : listO A → listO B).
(* iris/algebra/list.v *)
Instance listO_map_ne {SI : sidx} A B : NonExpansive (@listO_map SI A B).
Proof. intros n f g ? l. by apply list_fmap_ext_ne. Qed.
(* iris/algebra/list.v *)
Definition listOF {SI : sidx} (F : oFunctor) : oFunctor := {|
  oFunctor_car A _ B _ := listO (oFunctor_car F A B);
  oFunctor_map A1 _ A2 _ B1 _ B2 _ fg := listO_map (oFunctor_map F fg)
|}.
Next Obligation.
  by intros ? F A1 ? A2 ? B1 ? B2 ? n f g Hfg; apply listO_map_ne, oFunctor_map_ne.
Qed.
(* iris/algebra/list.v *)
Instance listOF_contractive {SI : sidx} F :
  oFunctorContractive F → oFunctorContractive (listOF F).
Proof.
  intros ? A1 ? A2 ? B1 ? B2 ? n f g Hfg;
    by apply listO_map_ne, oFunctor_map_contractive.
Qed.
(* iris/algebra/local_updates.v *)
(* * Local updates *)
Definition local_update {SI : sidx} {A : cmra} (x y : A * A)
:= ∀ n mz,
  ✓{n} x.1 → x.1 ≡{n}≡ x.2 ⋅? mz → ✓{n} y.1 ∧ y.1 ≡{n}≡ y.2 ⋅? mz.
(* iris/algebra/local_updates.v *)
Instance : Params (@local_update) 2
:= {}.
(* iris/algebra/local_updates.v *)
Instance local_update_proper :
    Proper ((≡) ==> (≡) ==> iff) (@local_update SI A).
Proof. unfold local_update. by repeat intro; setoid_subst. Qed.
(* iris/algebra/local_updates.v *)
Instance local_update_preorder : PreOrder (@local_update SI A).
Proof. split; unfold local_update; red; naive_solver. Qed.
(* iris/algebra/local_updates.v *)
Lemma exclusive_local_update `{!Exclusive y} x x' : ✓ x' → (x,y) ~l~> (x',x').
Proof.
    intros ? n mz Hxv Hx; simpl in *.
    move: Hxv; rewrite Hx; move=> /exclusiveN_opM=> ->; split; auto.
    by apply cmra_valid_validN.
  Qed.
(* iris/algebra/local_updates.v *)
Lemma op_local_update x y z :
    (∀ n, ✓{n} x → ✓{n} (z ⋅ x)) → (x,y) ~l~> (z ⋅ x, z ⋅ y).
Proof.
    intros Hv n mz Hxv Hx; simpl in *; split; [by auto|].
    by rewrite Hx -cmra_op_opM_assoc.
  Qed.
(* iris/algebra/local_updates.v *)
Lemma op_local_update_discrete `{!CmraDiscrete A} x y z :
    (✓ x → ✓ (z ⋅ x)) → (x,y) ~l~> (z ⋅ x, z ⋅ y).
Proof.
    intros; apply op_local_update=> n. by rewrite -!(cmra_discrete_valid_iff n).
  Qed.