Library stdpp.list

This file collects general purpose definitions and theorems on lists that are not in the Coq standard library.
From Coq Require Export Permutation.
From stdpp Require Export numbers base option.
From stdpp Require Import options.

Set Default Proof Using "Type*".

Arguments length {_} _ : assert.
Arguments cons {_} _ _ : assert.
Arguments app {_} _ _ : assert.

Instance: Params (@length) 1 := {}.
Instance: Params (@cons) 1 := {}.
Instance: Params (@app) 1 := {}.

Notation tail := tl.
Notation take := firstn.
Notation drop := skipn.

Arguments head {_} _ : assert.
Arguments tail {_} _ : assert.
Arguments take {_} !_ !_ / : assert.
Arguments drop {_} !_ !_ / : assert.

Instance: Params (@head) 1 := {}.
Instance: Params (@tail) 1 := {}.
Instance: Params (@take) 1 := {}.
Instance: Params (@drop) 1 := {}.

Arguments Permutation {_} _ _ : assert.
Arguments Forall_cons {_} _ _ _ _ _ : assert.
Remove Hints Permutation_cons : typeclass_instances.

Notation "(::)" := cons (only parsing) : list_scope.
Notation "( x ::.)" := (cons x) (only parsing) : list_scope.
Notation "(.:: l )" := (λ x, cons x l) (only parsing) : list_scope.
Notation "(++)" := app (only parsing) : list_scope.
Notation "( l ++.)" := (app l) (only parsing) : list_scope.
Notation "(.++ k )" := (λ l, app l k) (only parsing) : list_scope.

Infix "≡ₚ" := Permutation (at level 70, no associativity) : stdpp_scope.
Notation "(≡ₚ)" := Permutation (only parsing) : stdpp_scope.
Notation "( x ≡ₚ.)" := (Permutation x) (only parsing) : stdpp_scope.
Notation "(.≡ₚ x )" := (λ y, y ≡ₚ x) (only parsing) : stdpp_scope.
Notation "(≢ₚ)" := (λ x y, ¬x ≡ₚ y) (only parsing) : stdpp_scope.
Notation "x ≢ₚ y":= (¬x ≡ₚ y) (at level 70, no associativity) : stdpp_scope.
Notation "( x ≢ₚ.)" := (λ y, x ≢ₚ y) (only parsing) : stdpp_scope.
Notation "(.≢ₚ x )" := (λ y, y ≢ₚ x) (only parsing) : stdpp_scope.

Infix "≡ₚ@{ A }" :=
  (@Permutation A) (at level 70, no associativity, only parsing) : stdpp_scope.
Notation "(≡ₚ@{ A } )" := (@Permutation A) (only parsing) : stdpp_scope.

Instance maybe_cons {A} : Maybe2 (@cons A) := λ l,
  match l with x :: lSome (x,l) | _None end.

Definitions

Setoid equality lifted to lists
Inductive list_equiv `{Equiv A} : Equiv (list A) :=
  | nil_equiv : [] []
  | cons_equiv x y l k : x y l k x :: l y :: k.
Existing Instance list_equiv.

The operation l !! i gives the ith element of the list l, or None in case i is out of bounds.
Instance list_lookup {A} : Lookup nat A (list A) :=
  fix go i l {struct l} : option A := let _ : Lookup _ _ _ := @go in
  match l with
  | []None | x :: lmatch i with 0 ⇒ Some x | S il !! i end
  end.

The operation l !!! i is a total version of the lookup operation l !! i.
Instance list_lookup_total `{!Inhabited A} : LookupTotal nat A (list A) :=
  fix go i l {struct l} : A := let _ : LookupTotal _ _ _ := @go in
  match l with
  | []inhabitant
  | x :: lmatch i with 0 ⇒ x | S il !!! i end
  end.

The operation alter f i l applies the function f to the ith element of l. In case i is out of bounds, the list is returned unchanged.
Instance list_alter {A} : Alter nat A (list A) := λ f,
  fix go i l {struct l} :=
  match l with
  | [][]
  | x :: lmatch i with 0 ⇒ f x :: l | S ix :: go i l end
  end.

The operation <[i:=x]> l overwrites the element at position i with the value x. In case i is out of bounds, the list is returned unchanged.
Instance list_insert {A} : Insert nat A (list A) :=
  fix go i y l {struct l} := let _ : Insert _ _ _ := @go in
  match l with
  | [][]
  | x :: lmatch i with 0 ⇒ y :: l | S ix :: <[i:=y]>l end
  end.
Fixpoint list_inserts {A} (i : nat) (k l : list A) : list A :=
  match k with
  | []l
  | y :: k<[i:=y]>(list_inserts (S i) k l)
  end.
Instance: Params (@list_inserts) 1 := {}.

The operation delete i l removes the ith element of l and moves all consecutive elements one position ahead. In case i is out of bounds, the list is returned unchanged.
Instance list_delete {A} : Delete nat (list A) :=
  fix go (i : nat) (l : list A) {struct l} : list A :=
  match l with
  | [][]
  | x :: lmatch i with 0 ⇒ l | S ix :: @delete _ _ go i l end
  end.

The function option_list o converts an element Some x into the singleton list [x], and None into the empty list [].
Definition option_list {A} : option A list A := option_rect _ (λ x, [x]) [].
Instance: Params (@option_list) 1 := {}.
Instance maybe_list_singleton {A} : Maybe (λ x : A, [x]) := λ l,
  match l with [x]Some x | _None end.

The function filter P l returns the list of elements of l that satisfies P. The order remains unchanged.
Instance list_filter {A} : Filter A (list A) :=
  fix go P _ l := let _ : Filter _ _ := @go in
  match l with
  | [][]
  | x :: lif decide (P x) then x :: filter P l else filter P l
  end.

The function list_find P l returns the first index i whose element satisfies the predicate P.
Definition list_find {A} P `{ x, Decision (P x)} : list A option (nat × A) :=
  fix go l :=
  match l with
  | []None
  | x :: lif decide (P x) then Some (0,x) else prod_map S id <$> go l
  end.
Instance: Params (@list_find) 3 := {}.

The function replicate n x generates a list with length n of elements with value x.
Fixpoint replicate {A} (n : nat) (x : A) : list A :=
  match n with 0 ⇒ [] | S nx :: replicate n x end.
Instance: Params (@replicate) 2 := {}.

The function rotate n l rotates the list l by n, e.g., rotate 1 [x0; x1; ...; xm] becomes x1; ...; xm; x0. Rotating by a multiple of length l is the identity function.
Definition rotate {A} (n : nat) (l : list A) : list A :=
  drop (Z.to_nat (n `mod` length l)%Z) l ++ take (Z.to_nat (n `mod` length l)%Z) l.
Instance: Params (@rotate) 2 := {}.

The function rotate_take s e l returns the range between the indices s (inclusive) and e (exclusive) of l. If e s, all elements after s and before e are returned.
Definition rotate_take {A} (s e : nat) (l : list A) : list A :=
  take (rotate_nat_sub s e (length l)) (rotate s l).
Instance: Params (@rotate_take) 3 := {}.

The function reverse l returns the elements of l in reverse order.
Definition reverse {A} (l : list A) : list A := rev_append l [].
Instance: Params (@reverse) 1 := {}.

The function last l returns the last element of the list l, or None if the list l is empty.
Fixpoint last {A} (l : list A) : option A :=
  match l with []None | [x]Some x | _ :: llast l end.
Instance: Params (@last) 1 := {}.

The function resize n y l takes the first n elements of l in case length l n, and otherwise appends elements with value x to l to obtain a list of length n.
Fixpoint resize {A} (n : nat) (y : A) (l : list A) : list A :=
  match l with
  | []replicate n y
  | x :: lmatch n with 0 ⇒ [] | S nx :: resize n y l end
  end.
Arguments resize {_} !_ _ !_ : assert.
Instance: Params (@resize) 2 := {}.

The function reshape k l transforms l into a list of lists whose sizes are specified by k. In case l is too short, the resulting list will be padded with empty lists. In case l is too long, it will be truncated.
Fixpoint reshape {A} (szs : list nat) (l : list A) : list (list A) :=
  match szs with
  | [][] | sz :: szstake sz l :: reshape szs (drop sz l)
  end.
Instance: Params (@reshape) 2 := {}.

Definition sublist_lookup {A} (i n : nat) (l : list A) : option (list A) :=
  guard (i + n length l); Some (take n (drop i l)).
Definition sublist_alter {A} (f : list A list A)
    (i n : nat) (l : list A) : list A :=
  take i l ++ f (take n (drop i l)) ++ drop (i + n) l.

Functions to fold over a list. We redefine foldl with the arguments in the same order as in Haskell.
Notation foldr := fold_right.
Definition foldl {A B} (f : A B A) : A list B A :=
  fix go a l := match l with []a | x :: lgo (f a x) l end.

The monadic operations.
Instance list_ret: MRet list := λ A x, x :: @nil A.
Instance list_fmap : FMap list := λ A B f,
  fix go (l : list A) := match l with [][] | x :: lf x :: go l end.
Instance list_omap : OMap list := λ A B f,
  fix go (l : list A) :=
  match l with
  | [][]
  | x :: lmatch f x with Some yy :: go l | Nonego l end
  end.
Instance list_bind : MBind list := λ A B f,
  fix go (l : list A) := match l with [][] | x :: lf x ++ go l end.
Instance list_join: MJoin list :=
  fix go A (ls : list (list A)) : list A :=
  match ls with [][] | l :: lsl ++ @mjoin _ go _ ls end.
Definition mapM `{MBind M, MRet M} {A B} (f : A M B) : list A M (list B) :=
  fix go l :=
  match l with []mret [] | x :: ly f x; k go l; mret (y :: k) end.

We define stronger variants of map and fold that allow the mapped function to use the index of the elements.
Fixpoint imap {A B} (f : nat A B) (l : list A) : list B :=
  match l with
  | [][]
  | x :: lf 0 x :: imap (f S) l
  end.

Definition zipped_map {A B} (f : list A list A A B) :
    list A list A list B := fix go l k :=
  match k with
  | [][]
  | x :: kf l k x :: go (x :: l) k
  end.

Fixpoint imap2 {A B C} (f : nat A B C) (l : list A) (k : list B) : list C :=
  match l, k with
  | [], _ | _, [][]
  | x :: l, y :: kf 0 x y :: imap2 (f S) l k
  end.

Inductive zipped_Forall {A} (P : list A list A A Prop) :
    list A list A Prop :=
  | zipped_Forall_nil l : zipped_Forall P l []
  | zipped_Forall_cons l k x :
     P l k x zipped_Forall P (x :: l) k zipped_Forall P l (x :: k).
Arguments zipped_Forall_nil {_ _} _ : assert.
Arguments zipped_Forall_cons {_ _} _ _ _ _ _ : assert.

The function mask f βs l applies the function f to elements in l at positions that are true in βs.
Fixpoint mask {A} (f : A A) (βs : list bool) (l : list A) : list A :=
  match βs, l with
  | β :: βs, x :: l(if β then f x else x) :: mask f βs l
  | _, _l
  end.

The function permutations l yields all permutations of l.
Fixpoint interleave {A} (x : A) (l : list A) : list (list A) :=
  match l with
  | [][[x]]| y :: l(x :: y :: l) :: ((y ::.) <$> interleave x l)
  end.
Fixpoint permutations {A} (l : list A) : list (list A) :=
  match l with [][[]] | x :: lpermutations l ≫= interleave x end.

The predicate suffix holds if the first list is a suffix of the second. The predicate prefix holds if the first list is a prefix of the second.
Definition suffix {A} : relation (list A) := λ l1 l2, k, l2 = k ++ l1.
Definition prefix {A} : relation (list A) := λ l1 l2, k, l2 = l1 ++ k.
Infix "`suffix_of`" := suffix (at level 70) : stdpp_scope.
Infix "`prefix_of`" := prefix (at level 70) : stdpp_scope.
Hint Extern 0 (_ `prefix_of` _) ⇒ reflexivity : core.
Hint Extern 0 (_ `suffix_of` _) ⇒ reflexivity : core.

Section prefix_suffix_ops.
  Context `{EqDecision A}.

  Definition max_prefix : list A list A list A × list A × list A :=
    fix go l1 l2 :=
    match l1, l2 with
    | [], l2([], l2, [])
    | l1, [](l1, [], [])
    | x1 :: l1, x2 :: l2
      if decide_rel (=) x1 x2
      then prod_map id (x1 ::.) (go l1 l2) else (x1 :: l1, x2 :: l2, [])
    end.
  Definition max_suffix (l1 l2 : list A) : list A × list A × list A :=
    match max_prefix (reverse l1) (reverse l2) with
    | (k1, k2, k3)(reverse k1, reverse k2, reverse k3)
    end.
  Definition strip_prefix (l1 l2 : list A) := (max_prefix l1 l2).1.2.
  Definition strip_suffix (l1 l2 : list A) := (max_suffix l1 l2).1.2.
End prefix_suffix_ops.

A list l1 is a sublist of l2 if l2 is obtained by removing elements from l1 without changing the order.
Inductive sublist {A} : relation (list A) :=
  | sublist_nil : sublist [] []
  | sublist_skip x l1 l2 : sublist l1 l2 sublist (x :: l1) (x :: l2)
  | sublist_cons x l1 l2 : sublist l1 l2 sublist l1 (x :: l2).
Infix "`sublist_of`" := sublist (at level 70) : stdpp_scope.
Hint Extern 0 (_ `sublist_of` _) ⇒ reflexivity : core.

A list l2 submseteq a list l1 if l2 is obtained by removing elements from l1 while possiblity changing the order.
Inductive submseteq {A} : relation (list A) :=
  | submseteq_nil : submseteq [] []
  | submseteq_skip x l1 l2 : submseteq l1 l2 submseteq (x :: l1) (x :: l2)
  | submseteq_swap x y l : submseteq (y :: x :: l) (x :: y :: l)
  | submseteq_cons x l1 l2 : submseteq l1 l2 submseteq l1 (x :: l2)
  | submseteq_trans l1 l2 l3 : submseteq l1 l2 submseteq l2 l3 submseteq l1 l3.
Infix "⊆+" := submseteq (at level 70) : stdpp_scope.
Hint Extern 0 (_ ⊆+ _) ⇒ reflexivity : core.

Removes x from the list l. The function returns a Some when the +removal succeeds and None when x is not in l.
Fixpoint list_remove `{EqDecision A} (x : A) (l : list A) : option (list A) :=
  match l with
  | []None
  | y :: lif decide (x = y) then Some l else (y ::.) <$> list_remove x l
  end.

Removes all elements in the list k from the list l. The function returns a Some when the removal succeeds and None some element of k is not in l.
Fixpoint list_remove_list `{EqDecision A} (k : list A) (l : list A) : option (list A) :=
  match k with
  | []Some l | x :: klist_remove x l ≫= list_remove_list k
  end.

Inductive Forall3 {A B C} (P : A B C Prop) :
     list A list B list C Prop :=
  | Forall3_nil : Forall3 P [] [] []
  | Forall3_cons x y z l k k' :
     P x y z Forall3 P l k k' Forall3 P (x :: l) (y :: k) (z :: k').

Set operations on lists
Instance list_subseteq {A} : SubsetEq (list A) := λ l1 l2, x, x l1 x l2.

Section list_set.
  Context `{dec : EqDecision A}.
  Global Instance elem_of_list_dec : RelDecision (∈@{list A}).
  Proof.
   refine (
    fix go x l :=
    match l return Decision (x l) with
    | []right _
    | y :: lcast_if_or (decide (x = y)) (go x l)
    end); clear go dec; subst; try (by constructor); abstract by inversion 1.
  Defined.
  Fixpoint remove_dups (l : list A) : list A :=
    match l with
    | [][]
    | x :: l
      if decide_rel (∈) x l then remove_dups l else x :: remove_dups l
    end.
  Fixpoint list_difference (l k : list A) : list A :=
    match l with
    | [][]
    | x :: l
      if decide_rel (∈) x k
      then list_difference l k else x :: list_difference l k
    end.
  Definition list_union (l k : list A) : list A := list_difference l k ++ k.
  Fixpoint list_intersection (l k : list A) : list A :=
    match l with
    | [][]
    | x :: l
      if decide_rel (∈) x k
      then x :: list_intersection l k else list_intersection l k
    end.
  Definition list_intersection_with (f : A A option A) :
    list A list A list A := fix go l k :=
    match l with
    | [][]
    | x :: lfoldr (λ y,
        match f x y with Noneid | Some z(z ::.) end) (go l k) k
    end.
End list_set.

These next functions allow to efficiently encode lists of positives (bit strings) into a single positive and go in the other direction as well. This is for example used for the countable instance of lists and in namespaces. The main functions are positives_flatten and positives_unflatten.
Fixpoint positives_flatten_go (xs : list positive) (acc : positive) : positive :=
  match xs with
  | []acc
  | x :: xspositives_flatten_go xs (acc~1~0 ++ Preverse (Pdup x))
  end.

Flatten a list of positives into a single positive by duplicating the bits of each element, so that:
  • 0 00
  • 1 11
and then separating each element with 10.
Definition positives_flatten (xs : list positive) : positive :=
  positives_flatten_go xs 1.

Fixpoint positives_unflatten_go
        (p : positive)
        (acc_xs : list positive)
        (acc_elm : positive)
  : option (list positive) :=
  match p with
  | 1 ⇒ Some acc_xs
  | p'~0~0positives_unflatten_go p' acc_xs (acc_elm~0)
  | p'~1~1positives_unflatten_go p' acc_xs (acc_elm~1)
  | p'~1~0positives_unflatten_go p' (acc_elm :: acc_xs) 1
  | _None
  end%positive.

Unflatten a positive into a list of positives, assuming the encoding used by positives_flatten.

Basic tactics on lists

The tactic discriminate_list discharges a goal if it submseteq a list equality involving (::) and (++) of two lists that have a different length as one of its hypotheses.
Tactic Notation "discriminate_list" hyp(H) :=
  apply (f_equal length) in H;
  repeat (csimpl in H || rewrite app_length in H); exfalso; lia.
Tactic Notation "discriminate_list" :=
  match goal with H : _ =@{list _} _ |- _discriminate_list H end.

The tactic simplify_list_eq simplifies hypotheses involving equalities on lists using injectivity of (::) and (++). Also, it simplifies lookups in singleton lists.
Lemma app_inj_1 {A} (l1 k1 l2 k2 : list A) :
  length l1 = length k1 l1 ++ l2 = k1 ++ k2 l1 = k1 l2 = k2.
Proof. revert k1. induction l1; intros [|??]; naive_solver. Qed.
Lemma app_inj_2 {A} (l1 k1 l2 k2 : list A) :
  length l2 = length k2 l1 ++ l2 = k1 ++ k2 l1 = k1 l2 = k2.
Proof.
  intros ? Hl. apply app_inj_1; auto.
  apply (f_equal length) in Hl. rewrite !app_length in Hl. lia.
Qed.
Ltac simplify_list_eq :=
  repeat match goal with
  | _progress simplify_eq/=
  | H : _ ++ _ = _ ++ _ |- _first
    [ apply app_inv_head in H | apply app_inv_tail in H
    | apply app_inj_1 in H; [destruct H|done]
    | apply app_inj_2 in H; [destruct H|done] ]
  | H : [?x] !! ?i = Some ?y |- _
    destruct i; [change (Some x = Some y) in H | discriminate]
  end.

General theorems

Section general_properties.
Context {A : Type}.
Implicit Types x y z : A.
Implicit Types l k : list A.

Global Instance: Inj2 (=) (=) (=) (@cons A).
Proof. by injection 1. Qed.
Global Instance: k, Inj (=) (=) (k ++.).
Proof. intros ???. apply app_inv_head. Qed.
Global Instance: k, Inj (=) (=) (.++ k).
Proof. intros ???. apply app_inv_tail. Qed.
Global Instance: Assoc (=) (@app A).
Proof. intros ???. apply app_assoc. Qed.
Global Instance: LeftId (=) [] (@app A).
Proof. done. Qed.
Global Instance: RightId (=) [] (@app A).
Proof. intro. apply app_nil_r. Qed.

Lemma app_nil l1 l2 : l1 ++ l2 = [] l1 = [] l2 = [].
Proof. split; [apply app_eq_nil|]. by intros [-> ->]. Qed.
Lemma app_singleton l1 l2 x :
  l1 ++ l2 = [x] l1 = [] l2 = [x] l1 = [x] l2 = [].
Proof. split; [apply app_eq_unit|]. by intros [[-> ->]|[-> ->]]. Qed.
Lemma cons_middle x l1 l2 : l1 ++ x :: l2 = l1 ++ [x] ++ l2.
Proof. done. Qed.
Lemma list_eq l1 l2 : ( i, l1 !! i = l2 !! i) l1 = l2.
Proof.
  revert l2. induction l1 as [|x l1 IH]; intros [|y l2] H.
  - done.
  - discriminate (H 0).
  - discriminate (H 0).
  - f_equal; [by injection (H 0)|]. apply (IH _ $ λ i, H (S i)).
Qed.
Global Instance list_eq_dec {dec : EqDecision A} : EqDecision (list A) :=
  list_eq_dec dec.
Global Instance list_eq_nil_dec l : Decision (l = []).
Proof. by refine match l with []left _ | _right _ end. Defined.
Lemma list_singleton_reflect l :
  option_reflect (λ x, l = [x]) (length l 1) (maybe (λ x, [x]) l).
Proof. by destruct l as [|? []]; constructor. Defined.

Definition nil_length : length (@nil A) = 0 := eq_refl.
Definition cons_length x l : length (x :: l) = S (length l) := eq_refl.
Lemma nil_or_length_pos l : l = [] length l 0.
Proof. destruct l; simpl; auto with lia. Qed.
Lemma nil_length_inv l : length l = 0 l = [].
Proof. by destruct l. Qed.
Lemma lookup_cons_ne_0 l x i : i 0 (x :: l) !! i = l !! pred i.
Proof. by destruct i. Qed.
Lemma lookup_total_cons_ne_0 `{!Inhabited A} l x i :
  i 0 (x :: l) !!! i = l !!! pred i.
Proof. by destruct i. Qed.
Lemma lookup_nil i : @nil A !! i = None.
Proof. by destruct i. Qed.
Lemma lookup_total_nil `{!Inhabited A} i : @nil A !!! i = inhabitant.
Proof. by destruct i. Qed.
Lemma lookup_tail l i : tail l !! i = l !! S i.
Proof. by destruct l. Qed.
Lemma lookup_total_tail `{!Inhabited A} l i : tail l !!! i = l !!! S i.
Proof. by destruct l. Qed.
Lemma lookup_lt_Some l i x : l !! i = Some x i < length l.
Proof. revert i. induction l; intros [|?] ?; naive_solver auto with arith. Qed.
Lemma lookup_lt_is_Some_1 l i : is_Some (l !! i) i < length l.
Proof. intros [??]; eauto using lookup_lt_Some. Qed.
Lemma lookup_lt_is_Some_2 l i : i < length l is_Some (l !! i).
Proof. revert i. induction l; intros [|?] ?; naive_solver eauto with lia. Qed.
Lemma lookup_lt_is_Some l i : is_Some (l !! i) i < length l.
Proof. split; auto using lookup_lt_is_Some_1, lookup_lt_is_Some_2. Qed.
Lemma lookup_ge_None l i : l !! i = None length l i.
Proof. rewrite eq_None_not_Some, lookup_lt_is_Some. lia. Qed.
Lemma lookup_ge_None_1 l i : l !! i = None length l i.
Proof. by rewrite lookup_ge_None. Qed.
Lemma lookup_ge_None_2 l i : length l i l !! i = None.
Proof. by rewrite lookup_ge_None. Qed.

Lemma list_eq_same_length l1 l2 n :
  length l2 = n length l1 = n
  ( i x y, i < n l1 !! i = Some x l2 !! i = Some y x = y) l1 = l2.
Proof.
  intros <- Hlen Hl; apply list_eq; intros i. destruct (l2 !! i) as [x|] eqn:Hx.
  - destruct (lookup_lt_is_Some_2 l1 i) as [y Hy].
    { rewrite Hlen; eauto using lookup_lt_Some. }
    rewrite Hy; f_equal; apply (Hl i); eauto using lookup_lt_Some.
  - by rewrite lookup_ge_None, Hlen, <-lookup_ge_None.
Qed.

Lemma nth_lookup l i d : nth i l d = default d (l !! i).
Proof. revert i. induction l as [|x l IH]; intros [|i]; simpl; auto. Qed.
Lemma nth_lookup_Some l i d x : l !! i = Some x nth i l d = x.
Proof. rewrite nth_lookup. by intros →. Qed.
Lemma nth_lookup_or_length l i d : {l !! i = Some (nth i l d)} + {length l i}.
Proof.
  rewrite nth_lookup. destruct (l !! i) eqn:?; eauto using lookup_ge_None_1.
Qed.

Lemma list_lookup_total_alt `{!Inhabited A} l i :
  l !!! i = default inhabitant (l !! i).
Proof. revert i. induction l; intros []; naive_solver. Qed.
Lemma list_lookup_total_correct `{!Inhabited A} l i x :
  l !! i = Some x l !!! i = x.
Proof. rewrite list_lookup_total_alt. by intros →. Qed.
Lemma list_lookup_lookup_total `{!Inhabited A} l i :
  is_Some (l !! i) l !! i = Some (l !!! i).
Proof. rewrite list_lookup_total_alt; by intros [x ->]. Qed.
Lemma list_lookup_lookup_total_lt `{!Inhabited A} l i :
  i < length l l !! i = Some (l !!! i).
Proof. intros ?. by apply list_lookup_lookup_total, lookup_lt_is_Some_2. Qed.
Lemma list_lookup_alt `{!Inhabited A} l i x :
  l !! i = Some x i < length l l !!! i = x.
Proof.
  naive_solver eauto using list_lookup_lookup_total_lt,
    list_lookup_total_correct, lookup_lt_Some.
Qed.

Lemma lookup_app_l l1 l2 i : i < length l1 (l1 ++ l2) !! i = l1 !! i.
Proof. revert i. induction l1; intros [|?]; naive_solver auto with lia. Qed.
Lemma lookup_total_app_l `{!Inhabited A} l1 l2 i :
  i < length l1 (l1 ++ l2) !!! i = l1 !!! i.
Proof. intros. by rewrite !list_lookup_total_alt, lookup_app_l. Qed.
Lemma lookup_app_l_Some l1 l2 i x : l1 !! i = Some x (l1 ++ l2) !! i = Some x.
Proof. intros. rewrite lookup_app_l; eauto using lookup_lt_Some. Qed.
Lemma lookup_app_r l1 l2 i :
  length l1 i (l1 ++ l2) !! i = l2 !! (i - length l1).
Proof. revert i. induction l1; intros [|?]; simpl; auto with lia. Qed.
Lemma lookup_total_app_r `{!Inhabited A} l1 l2 i :
  length l1 i (l1 ++ l2) !!! i = l2 !!! (i - length l1).
Proof. intros. by rewrite !list_lookup_total_alt, lookup_app_r. Qed.
Lemma lookup_app_Some l1 l2 i x :
  (l1 ++ l2) !! i = Some x
    l1 !! i = Some x length l1 i l2 !! (i - length l1) = Some x.
Proof.
  split.
  - revert i. induction l1 as [|y l1 IH]; intros [|i] ?;
      simplify_eq/=; auto with lia.
    destruct (IH i) as [?|[??]]; auto with lia.
  - intros [?|[??]]; auto using lookup_app_l_Some. by rewrite lookup_app_r.
Qed.
Lemma list_lookup_middle l1 l2 x n :
  n = length l1 (l1 ++ x :: l2) !! n = Some x.
Proof. intros →. by induction l1. Qed.
Lemma list_lookup_total_middle `{!Inhabited A} l1 l2 x n :
  n = length l1 (l1 ++ x :: l2) !!! n = x.
Proof. intros. by rewrite !list_lookup_total_alt, list_lookup_middle. Qed.

Lemma list_insert_alter l i x : <[i:=x]>l = alter (λ _, x) i l.
Proof. by revert i; induction l; intros []; intros; f_equal/=. Qed.
Lemma alter_length f l i : length (alter f i l) = length l.
Proof. revert i. by induction l; intros [|?]; f_equal/=. Qed.
Lemma insert_length l i x : length (<[i:=x]>l) = length l.
Proof. revert i. by induction l; intros [|?]; f_equal/=. Qed.
Lemma list_lookup_alter f l i : alter f i l !! i = f <$> l !! i.
Proof.
  revert i.
  induction l as [|?? IHl]; [done|].
  intros [|i]; [done|]. apply (IHl i).
Qed.
Lemma list_lookup_total_alter `{!Inhabited A} f l i :
  i < length l alter f i l !!! i = f (l !!! i).
Proof.
  intros [x Hx]%lookup_lt_is_Some_2.
  by rewrite !list_lookup_total_alt, list_lookup_alter, Hx.
Qed.
Lemma list_lookup_alter_ne f l i j : i j alter f i l !! j = l !! j.
Proof. revert i j. induction l; [done|]. intros [] []; naive_solver. Qed.
Lemma list_lookup_total_alter_ne `{!Inhabited A} f l i j :
  i j alter f i l !!! j = l !!! j.
Proof. intros. by rewrite !list_lookup_total_alt, list_lookup_alter_ne. Qed.

Lemma list_lookup_insert l i x : i < length l <[i:=x]>l !! i = Some x.
Proof. revert i. induction l; intros [|?] ?; f_equal/=; auto with lia. Qed.
Lemma list_lookup_total_insert `{!Inhabited A} l i x :
  i < length l <[i:=x]>l !!! i = x.
Proof. intros. by rewrite !list_lookup_total_alt, list_lookup_insert. Qed.
Lemma list_lookup_insert_ne l i j x : i j <[i:=x]>l !! j = l !! j.
Proof. revert i j. induction l; [done|]. intros [] []; naive_solver. Qed.
Lemma list_lookup_total_insert_ne `{!Inhabited A} l i j x :
  i j <[i:=x]>l !!! j = l !!! j.
Proof. intros. by rewrite !list_lookup_total_alt, list_lookup_insert_ne. Qed.
Lemma list_lookup_insert_Some l i x j y :
  <[i:=x]>l !! j = Some y
    i = j x = y j < length l i j l !! j = Some y.
Proof.
  destruct (decide (i = j)) as [->|];
    [split|rewrite list_lookup_insert_ne by done; tauto].
  - intros Hy. assert (j < length l).
    { rewrite <-(insert_length l j x); eauto using lookup_lt_Some. }
    rewrite list_lookup_insert in Hy by done; naive_solver.
  - intros [(?&?&?)|[??]]; rewrite ?list_lookup_insert; naive_solver.
Qed.
Lemma list_insert_commute l i j x y :
  i j <[i:=x]>(<[j:=y]>l) = <[j:=y]>(<[i:=x]>l).
Proof. revert i j. by induction l; intros [|?] [|?] ?; f_equal/=; auto. Qed.
Lemma list_insert_id' l i x : (i < length l l !! i = Some x) <[i:=x]>l = l.
Proof. revert i. induction l; intros [|i] ?; f_equal/=; naive_solver lia. Qed.
Lemma list_insert_id l i x : l !! i = Some x <[i:=x]>l = l.
Proof. intros ?. by apply list_insert_id'. Qed.
Lemma list_insert_ge l i x : length l i <[i:=x]>l = l.
Proof. revert i. induction l; intros [|i] ?; f_equal/=; auto with lia. Qed.
Lemma list_insert_insert l i x y : <[i:=x]> (<[i:=y]> l) = <[i:=x]> l.
Proof. revert i. induction l; intros [|i]; f_equal/=; auto. Qed.

Lemma list_lookup_other l i x :
  length l 1 l !! i = Some x j y, j i l !! j = Some y.
Proof.
  intros. destruct i, l as [|x0 [|x1 l]]; simplify_eq/=.
  - by 1, x1.
  - by 0, x0.
Qed.

Lemma alter_app_l f l1 l2 i :
  i < length l1 alter f i (l1 ++ l2) = alter f i l1 ++ l2.
Proof. revert i. induction l1; intros [|?] ?; f_equal/=; auto with lia. Qed.
Lemma alter_app_r f l1 l2 i :
  alter f (length l1 + i) (l1 ++ l2) = l1 ++ alter f i l2.
Proof. revert i. induction l1; intros [|?]; f_equal/=; auto. Qed.
Lemma alter_app_r_alt f l1 l2 i :
  length l1 i alter f i (l1 ++ l2) = l1 ++ alter f (i - length l1) l2.
Proof.
  intros. assert (i = length l1 + (i - length l1)) as Hi by lia.
  rewrite Hi at 1. by apply alter_app_r.
Qed.
Lemma list_alter_id f l i : ( x, f x = x) alter f i l = l.
Proof. intros ?. revert i. induction l; intros [|?]; f_equal/=; auto. Qed.
Lemma list_alter_ext f g l k i :
  ( x, l !! i = Some x f x = g x) l = k alter f i l = alter g i k.
Proof. intros H →. revert i H. induction k; intros [|?] ?; f_equal/=; auto. Qed.
Lemma list_alter_compose f g l i :
  alter (f g) i l = alter f i (alter g i l).
Proof. revert i. induction l; intros [|?]; f_equal/=; auto. Qed.
Lemma list_alter_commute f g l i j :
  i j alter f i (alter g j l) = alter g j (alter f i l).
Proof. revert i j. induction l; intros [|?][|?] ?; f_equal/=; auto with lia. Qed.
Lemma insert_app_l l1 l2 i x :
  i < length l1 <[i:=x]>(l1 ++ l2) = <[i:=x]>l1 ++ l2.
Proof. revert i. induction l1; intros [|?] ?; f_equal/=; auto with lia. Qed.
Lemma insert_app_r l1 l2 i x : <[length l1+i:=x]>(l1 ++ l2) = l1 ++ <[i:=x]>l2.
Proof. revert i. induction l1; intros [|?]; f_equal/=; auto. Qed.
Lemma insert_app_r_alt l1 l2 i x :
  length l1 i <[i:=x]>(l1 ++ l2) = l1 ++ <[i - length l1:=x]>l2.
Proof.
  intros. assert (i = length l1 + (i - length l1)) as Hi by lia.
  rewrite Hi at 1. by apply insert_app_r.
Qed.
Lemma delete_middle l1 l2 x : delete (length l1) (l1 ++ x :: l2) = l1 ++ l2.
Proof. induction l1; f_equal/=; auto. Qed.

Lemma inserts_length l i k : length (list_inserts i k l) = length l.
Proof.
  revert i. induction k; intros ?; csimpl; rewrite ?insert_length; auto.
Qed.
Lemma list_lookup_inserts l i k j :
  i j < i + length k j < length l
  list_inserts i k l !! j = k !! (j - i).
Proof.
  revert i j. induction k as [|y k IH]; csimpl; intros i j ??; [lia|].
  destruct (decide (i = j)) as [->|].
  { by rewrite list_lookup_insert, Nat.sub_diag
      by (rewrite inserts_length; lia). }
  rewrite list_lookup_insert_ne, IH by lia.
  by replace (j - i) with (S (j - S i)) by lia.
Qed.
Lemma list_lookup_total_inserts `{!Inhabited A} l i k j :
  i j < i + length k j < length l
  list_inserts i k l !!! j = k !!! (j - i).
Proof. intros. by rewrite !list_lookup_total_alt, list_lookup_inserts. Qed.
Lemma list_lookup_inserts_lt l i k j :
  j < i list_inserts i k l !! j = l !! j.
Proof.
  revert i j. induction k; intros i j ?; csimpl;
    rewrite ?list_lookup_insert_ne by lia; auto with lia.
Qed.
Lemma list_lookup_total_inserts_lt `{!Inhabited A}l i k j :
  j < i list_inserts i k l !!! j = l !!! j.
Proof. intros. by rewrite !list_lookup_total_alt, list_lookup_inserts_lt. Qed.
Lemma list_lookup_inserts_ge l i k j :
  i + length k j list_inserts i k l !! j = l !! j.
Proof.
  revert i j. induction k; csimpl; intros i j ?;
    rewrite ?list_lookup_insert_ne by lia; auto with lia.
Qed.
Lemma list_lookup_total_inserts_ge `{!Inhabited A} l i k j :
  i + length k j list_inserts i k l !!! j = l !!! j.
Proof. intros. by rewrite !list_lookup_total_alt, list_lookup_inserts_ge. Qed.
Lemma list_lookup_inserts_Some l i k j y :
  list_inserts i k l !! j = Some y
    (j < i i + length k j) l !! j = Some y
    i j < i + length k j < length l k !! (j - i) = Some y.
Proof.
  destruct (decide (j < i)).
  { rewrite list_lookup_inserts_lt by done; intuition lia. }
  destruct (decide (i + length k j)).
  { rewrite list_lookup_inserts_ge by done; intuition lia. }
  split.
  - intros Hy. assert (j < length l).
    { rewrite <-(inserts_length l i k); eauto using lookup_lt_Some. }
    rewrite list_lookup_inserts in Hy by lia. intuition lia.
  - intuition. by rewrite list_lookup_inserts by lia.
Qed.
Lemma list_insert_inserts_lt l i j x k :
  i < j <[i:=x]>(list_inserts j k l) = list_inserts j k (<[i:=x]>l).
Proof.
  revert i j. induction k; intros i j ?; simpl;
    rewrite 1?list_insert_commute by lia; auto with f_equal.
Qed.
Lemma list_inserts_app_l l1 l2 l3 i :
  list_inserts i (l1 ++ l2) l3 = list_inserts (length l1 + i) l2 (list_inserts i l1 l3).
Proof.
  revert i; induction l1 as [|x l1 IH]; [done|].
  intro i. simpl. rewrite IH, Nat.add_succ_r. apply list_insert_inserts_lt. lia.
Qed.
Lemma list_inserts_app_r l1 l2 l3 i :
  list_inserts (length l2 + i) l1 (l2 ++ l3) = l2 ++ list_inserts i l1 l3.
Proof.
  revert i; induction l1 as [|x l1 IH]; [done|].
  intros i. simpl. by rewrite plus_n_Sm, IH, insert_app_r.
Qed.
Lemma list_inserts_nil l1 i : list_inserts i l1 [] = [].
Proof.
  revert i; induction l1 as [|x l1 IH]; [done|].
  intro i. simpl. by rewrite IH.
Qed.
Lemma list_inserts_cons l1 l2 i x :
  list_inserts (S i) l1 (x :: l2) = x :: list_inserts i l1 l2.
Proof.
  revert i; induction l1 as [|y l1 IH]; [done|].
  intro i. simpl. by rewrite IH.
Qed.
Lemma list_inserts_0_r l1 l2 l3 :
  length l1 = length l2 list_inserts 0 l1 (l2 ++ l3) = l1 ++ l3.
Proof.
  revert l2. induction l1 as [|x l1 IH]; intros [|y l2] ?; simplify_eq/=; [done|].
  rewrite list_inserts_cons. simpl. by rewrite IH.
Qed.
Lemma list_inserts_0_l l1 l2 l3 :
  length l1 = length l3 list_inserts 0 (l1 ++ l2) l3 = l1.
Proof.
  revert l3. induction l1 as [|x l1 IH]; intros [|z l3] ?; simplify_eq/=.
  { by rewrite list_inserts_nil. }
  rewrite list_inserts_cons. simpl. by rewrite IH.
Qed.

Properties of the elem_of predicate

Lemma not_elem_of_nil x : x [].
Proof. by inversion 1. Qed.
Lemma elem_of_nil x : x [] False.
Proof. intuition. by destruct (not_elem_of_nil x). Qed.
Lemma elem_of_nil_inv l : ( x, x l) l = [].
Proof. destruct l; [done|]. by edestruct 1; constructor. Qed.
Lemma elem_of_not_nil x l : x l l [].
Proof. intros ? →. by apply (elem_of_nil x). Qed.
Lemma elem_of_cons l x y : x y :: l x = y x l.
Proof. by split; [inversion 1; subst|intros [->|?]]; constructor. Qed.
Lemma not_elem_of_cons l x y : x y :: l x y x l.
Proof. rewrite elem_of_cons. tauto. Qed.
Lemma elem_of_app l1 l2 x : x l1 ++ l2 x l1 x l2.
Proof.
  induction l1 as [|y l1 IH]; simpl.
  - rewrite elem_of_nil. naive_solver.
  - rewrite !elem_of_cons, IH. naive_solver.
Qed.
Lemma not_elem_of_app l1 l2 x : x l1 ++ l2 x l1 x l2.
Proof. rewrite elem_of_app. tauto. Qed.
Lemma elem_of_list_singleton x y : x [y] x = y.
Proof. rewrite elem_of_cons, elem_of_nil. tauto. Qed.
Global Instance elem_of_list_permutation_proper x : Proper ((≡ₚ) ==> iff) (x ∈.).
Proof. induction 1; rewrite ?elem_of_nil, ?elem_of_cons; intuition. Qed.
Lemma elem_of_list_lookup_1 l x : x l i, l !! i = Some x.
Proof.
  induction 1 as [|???? IH]; [by 0 |].
  destruct IH as [i ?]; auto. by (S i).
Qed.
Lemma elem_of_list_lookup_total_1 `{!Inhabited A} l x :
  x l i, i < length l l !!! i = x.
Proof.
  intros [i Hi]%elem_of_list_lookup_1.
  eauto using lookup_lt_Some, list_lookup_total_correct.
Qed.
Lemma elem_of_list_lookup_2 l i x : l !! i = Some x x l.
Proof.
  revert i. induction l; intros [|i] ?; simplify_eq/=; constructor; eauto.
Qed.
Lemma elem_of_list_lookup_total_2 `{!Inhabited A} l i :
  i < length l l !!! i l.
Proof. intros. by eapply elem_of_list_lookup_2, list_lookup_lookup_total_lt. Qed.
Lemma elem_of_list_lookup l x : x l i, l !! i = Some x.
Proof. firstorder eauto using elem_of_list_lookup_1, elem_of_list_lookup_2. Qed.
Lemma elem_of_list_lookup_total `{!Inhabited A} l x :
  x l i, i < length l l !!! i = x.
Proof.
  naive_solver eauto using elem_of_list_lookup_total_1, elem_of_list_lookup_total_2.
Qed.
Lemma elem_of_list_split_length l i x :
  l !! i = Some x l1 l2, l = l1 ++ x :: l2 i = length l1.
Proof.
  revert i; induction l as [|y l IH]; intros [|i] Hl; simplify_eq/=.
  - []; eauto.
  - destruct (IH _ Hl) as (?&?&?&?); simplify_eq/=.
    eexists (y :: _); eauto.
Qed.
Lemma elem_of_list_split l x : x l l1 l2, l = l1 ++ x :: l2.
Proof.
  intros [? (?&?&?&_)%elem_of_list_split_length]%elem_of_list_lookup_1; eauto.
Qed.
Lemma elem_of_list_split_l `{EqDecision A} l x :
  x l l1 l2, l = l1 ++ x :: l2 x l1.
Proof.
  induction 1 as [x l|x y l ? IH].
  { [], l. rewrite elem_of_nil. naive_solver. }
  destruct (decide (x = y)) as [->|?].
  - [], l. rewrite elem_of_nil. naive_solver.
  - destruct IH as (l1 & l2 & → & ?).
     (y :: l1), l2. rewrite elem_of_cons. naive_solver.
Qed.
Lemma elem_of_list_split_r `{EqDecision A} l x :
  x l l1 l2, l = l1 ++ x :: l2 x l2.
Proof.
  induction l as [|y l IH] using rev_ind.
  { by rewrite elem_of_nil. }
  destruct (decide (x = y)) as [->|].
  - l, []. rewrite elem_of_nil. naive_solver.
  - rewrite elem_of_app, elem_of_list_singleton. intros [?| ->]; try done.
    destruct IH as (l1 & l2 & → & ?); auto.
     l1, (l2 ++ [y]).
    rewrite elem_of_app, elem_of_list_singleton, <-(assoc_L (++)). naive_solver.
Qed.
Lemma list_elem_of_insert l i x : i < length l x <[i:=x]>l.
Proof. intros. by eapply elem_of_list_lookup_2, list_lookup_insert. Qed.
Lemma nth_elem_of l i d : i < length l nth i l d l.
Proof.
  intros; eapply elem_of_list_lookup_2.
  destruct (nth_lookup_or_length l i d); [done | by lia].
Qed.

Properties of the NoDup predicate

Lemma NoDup_nil : NoDup (@nil A) True.
Proof. split; constructor. Qed.
Lemma NoDup_cons x l : NoDup (x :: l) x l NoDup l.
Proof. split; [by inversion 1|]. intros [??]. by constructor. Qed.
Lemma NoDup_cons_11 x l : NoDup (x :: l) x l.
Proof. rewrite NoDup_cons. by intros [??]. Qed.
Lemma NoDup_cons_12 x l : NoDup (x :: l) NoDup l.
Proof. rewrite NoDup_cons. by intros [??]. Qed.
Lemma NoDup_singleton x : NoDup [x].
Proof. constructor; [apply not_elem_of_nil | constructor]. Qed.
Lemma NoDup_app l k : NoDup (l ++ k) NoDup l ( x, x l x k) NoDup k.
Proof.
  induction l; simpl.
  - rewrite NoDup_nil. setoid_rewrite elem_of_nil. naive_solver.
  - rewrite !NoDup_cons.
    setoid_rewrite elem_of_cons. setoid_rewrite elem_of_app. naive_solver.
Qed.
Global Instance NoDup_proper: Proper ((≡ₚ) ==> iff) (@NoDup A).
Proof.
  induction 1 as [|x l k Hlk IH | |].
  - by rewrite !NoDup_nil.
  - by rewrite !NoDup_cons, IH, Hlk.
  - rewrite !NoDup_cons, !elem_of_cons. intuition.
  - intuition.
Qed.
Lemma NoDup_lookup l i j x :
  NoDup l l !! i = Some x l !! j = Some x i = j.
Proof.
  intros Hl. revert i j. induction Hl as [|x' l Hx Hl IH].
  { intros; simplify_eq. }
  intros [|i] [|j] ??; simplify_eq/=; eauto with f_equal;
    exfalso; eauto using elem_of_list_lookup_2.
Qed.
Lemma NoDup_alt l :
  NoDup l i j x, l !! i = Some x l !! j = Some x i = j.
Proof.
  split; eauto using NoDup_lookup.
  induction l as [|x l IH]; intros Hl; constructor.
  - rewrite elem_of_list_lookup. intros [i ?].
    by feed pose proof (Hl (S i) 0 x); auto.
  - apply IH. intros i j x' ??. by apply (inj S), (Hl (S i) (S j) x').
Qed.

Section no_dup_dec.
  Context `{!EqDecision A}.
  Global Instance NoDup_dec: l, Decision (NoDup l) :=
    fix NoDup_dec l :=
    match l return Decision (NoDup l) with
    | []left NoDup_nil_2
    | x :: l
      match decide_rel (∈) x l with
      | left Hinright (λ H, NoDup_cons_11 _ _ H Hin)
      | right Hin
        match NoDup_dec l with
        | left Hleft (NoDup_cons_2 _ _ Hin H)
        | right Hright (H NoDup_cons_12 _ _)
        end
      end
    end.
  Lemma elem_of_remove_dups l x : x remove_dups l x l.
  Proof.
    split; induction l; simpl; repeat case_decide;
      rewrite ?elem_of_cons; intuition (simplify_eq; auto).
  Qed.
  Lemma NoDup_remove_dups l : NoDup (remove_dups l).
  Proof.
    induction l; simpl; repeat case_decide; try constructor; auto.
    by rewrite elem_of_remove_dups.
  Qed.
End no_dup_dec.

Set operations on lists

Section list_set.
  Lemma elem_of_list_intersection_with f l k x :
    x list_intersection_with f l k x1 x2,
        x1 l x2 k f x1 x2 = Some x.
  Proof.
    split.
    - induction l as [|x1 l IH]; simpl; [by rewrite elem_of_nil|].
      intros Hx. setoid_rewrite elem_of_cons.
      cut (( x2, x2 k f x1 x2 = Some x)
            x list_intersection_with f l k); [naive_solver|].
      clear IH. revert Hx. generalize (list_intersection_with f l k).
      induction k; simpl; [by auto|].
      case_match; setoid_rewrite elem_of_cons; naive_solver.
    - intros (x1&x2&Hx1&Hx2&Hx). induction Hx1 as [x1 l|x1 ? l ? IH]; simpl.
      + generalize (list_intersection_with f l k).
        induction Hx2; simpl; [by rewrite Hx; left |].
        case_match; simpl; try setoid_rewrite elem_of_cons; auto.
      + generalize (IH Hx). clear Hx IH Hx2.
        generalize (list_intersection_with f l k).
        induction k; simpl; intros; [done|].
        case_match; simpl; rewrite ?elem_of_cons; auto.
  Qed.

  Context `{!EqDecision A}.
  Lemma elem_of_list_difference l k x : x list_difference l k x l x k.
  Proof.
    split; induction l; simpl; try case_decide;
      rewrite ?elem_of_nil, ?elem_of_cons; intuition congruence.
  Qed.
  Lemma NoDup_list_difference l k : NoDup l NoDup (list_difference l k).
  Proof.
    induction 1; simpl; try case_decide.
    - constructor.
    - done.
    - constructor; [|done]. rewrite elem_of_list_difference; intuition.
  Qed.
  Lemma elem_of_list_union l k x : x list_union l k x l x k.
  Proof.
    unfold list_union. rewrite elem_of_app, elem_of_list_difference.
    intuition. case (decide (x k)); intuition.
  Qed.
  Lemma NoDup_list_union l k : NoDup l NoDup k NoDup (list_union l k).
  Proof.
    intros. apply NoDup_app. repeat split.
    - by apply NoDup_list_difference.
    - intro. rewrite elem_of_list_difference. intuition.
    - done.
  Qed.
  Lemma elem_of_list_intersection l k x :
    x list_intersection l k x l x k.
  Proof.
    split; induction l; simpl; repeat case_decide;
      rewrite ?elem_of_nil, ?elem_of_cons; intuition congruence.
  Qed.
  Lemma NoDup_list_intersection l k : NoDup l NoDup (list_intersection l k).
  Proof.
    induction 1; simpl; try case_decide.
    - constructor.
    - constructor; [|done]. rewrite elem_of_list_intersection; intuition.
    - done.
  Qed.
End list_set.

Properties of the reverse function

Lemma reverse_nil : reverse [] =@{list A} [].
Proof. done. Qed.
Lemma reverse_singleton x : reverse [x] = [x].
Proof. done. Qed.
Lemma reverse_cons l x : reverse (x :: l) = reverse l ++ [x].
Proof. unfold reverse. by rewrite <-!rev_alt. Qed.
Lemma reverse_snoc l x : reverse (l ++ [x]) = x :: reverse l.
Proof. unfold reverse. by rewrite <-!rev_alt, rev_unit. Qed.
Lemma reverse_app l1 l2 : reverse (l1 ++ l2) = reverse l2 ++ reverse l1.
Proof. unfold reverse. rewrite <-!rev_alt. apply rev_app_distr. Qed.
Lemma reverse_length l : length (reverse l) = length l.
Proof. unfold reverse. rewrite <-!rev_alt. apply rev_length. Qed.
Lemma reverse_involutive l : reverse (reverse l) = l.
Proof. unfold reverse. rewrite <-!rev_alt. apply rev_involutive. Qed.
Lemma elem_of_reverse_2 x l : x l x reverse l.
Proof.
  induction 1; rewrite reverse_cons, elem_of_app,
    ?elem_of_list_singleton; intuition.
Qed.
Lemma elem_of_reverse x l : x reverse l x l.
Proof.
  split; auto using elem_of_reverse_2.
  intros. rewrite <-(reverse_involutive l). by apply elem_of_reverse_2.
Qed.
Global Instance: Inj (=) (=) (@reverse A).
Proof.
  intros l1 l2 Hl.
  by rewrite <-(reverse_involutive l1), <-(reverse_involutive l2), Hl.
Qed.

Properties of the last function

Lemma last_snoc x l : last (l ++ [x]) = Some x.
Proof. induction l as [|? []]; simpl; auto. Qed.
Lemma last_reverse l : last (reverse l) = head l.
Proof. by destruct l as [|x l]; rewrite ?reverse_cons, ?last_snoc. Qed.
Lemma head_reverse l : head (reverse l) = last l.
Proof. by rewrite <-last_reverse, reverse_involutive. Qed.

Properties of the take function

Definition take_drop i l : take i l ++ drop i l = l := firstn_skipn i l.
Lemma take_drop_middle l i x :
  l !! i = Some x take i l ++ x :: drop (S i) l = l.
Proof.
  revert i x. induction l; intros [|?] ??; simplify_eq/=; f_equal; auto.
Qed.
Lemma take_nil n : take n [] =@{list A} [].
Proof. by destruct n. Qed.
Lemma take_S_r l n x : l !! n = Some x take (S n) l = take n l ++ [x].
Proof. revert n. induction l; intros []; naive_solver eauto with f_equal. Qed.
Lemma take_app l k : take (length l) (l ++ k) = l.
Proof. induction l; f_equal/=; auto. Qed.
Lemma take_app_alt l k n : n = length l take n (l ++ k) = l.
Proof. intros →. by apply take_app. Qed.
Lemma take_app3_alt l1 l2 l3 n : n = length l1 take n ((l1 ++ l2) ++ l3) = l1.
Proof. intros →. by rewrite <-(assoc_L (++)), take_app. Qed.
Lemma take_app_le l k n : n length l take n (l ++ k) = take n l.
Proof. revert n. induction l; intros [|?] ?; f_equal/=; auto with lia. Qed.
Lemma take_plus_app l k n m :
  length l = n take (n + m) (l ++ k) = l ++ take m k.
Proof. intros <-. induction l; f_equal/=; auto. Qed.
Lemma take_app_ge l k n :
  length l n take n (l ++ k) = l ++ take (n - length l) k.
Proof. revert n. induction l; intros [|?] ?; f_equal/=; auto with lia. Qed.
Lemma take_ge l n : length l n take n l = l.
Proof. revert n. induction l; intros [|?] ?; f_equal/=; auto with lia. Qed.
Lemma take_take l n m : take n (take m l) = take (min n m) l.
Proof. revert n m. induction l; intros [|?] [|?]; f_equal/=; auto. Qed.
Lemma take_idemp l n : take n (take n l) = take n l.
Proof. by rewrite take_take, Min.min_idempotent. Qed.
Lemma take_length l n : length (take n l) = min n (length l).
Proof. revert n. induction l; intros [|?]; f_equal/=; done. Qed.
Lemma take_length_le l n : n length l length (take n l) = n.
Proof. rewrite take_length. apply Min.min_l. Qed.
Lemma take_length_ge l n : length l n length (take n l) = length l.
Proof. rewrite take_length. apply Min.min_r. Qed.
Lemma take_drop_commute l n m : take n (drop m l) = drop m (take (m + n) l).
Proof.
  revert n m. induction l; intros [|?][|?]; simpl; auto using take_nil with lia.
Qed.
Lemma lookup_take l n i : i < n take n l !! i = l !! i.
Proof. revert n i. induction l; intros [|n] [|i] ?; simpl; auto with lia. Qed.
Lemma lookup_total_take `{!Inhabited A} l n i : i < n take n l !!! i = l !!! i.
Proof. intros. by rewrite !list_lookup_total_alt, lookup_take. Qed.
Lemma lookup_take_ge l n i : n i take n l !! i = None.
Proof. revert n i. induction l; intros [|?] [|?] ?; simpl; auto with lia. Qed.
Lemma lookup_total_take_ge `{!Inhabited A} l n i : n i take n l !!! i = inhabitant.
Proof. intros. by rewrite list_lookup_total_alt, lookup_take_ge. Qed.
Lemma take_alter f l n i : n i take n (alter f i l) = take n l.
Proof.
  intros. apply list_eq. intros j. destruct (le_lt_dec n j).
  - by rewrite !lookup_take_ge.
  - by rewrite !lookup_take, !list_lookup_alter_ne by lia.
Qed.
Lemma take_insert l n i x : n i take n (<[i:=x]>l) = take n l.
Proof.
  intros. apply list_eq. intros j. destruct (le_lt_dec n j).
  - by rewrite !lookup_take_ge.
  - by rewrite !lookup_take, !list_lookup_insert_ne by lia.
Qed.
Lemma take_insert_lt l n i x : i < n take n (<[i:=x]>l) = <[i:=x]>(take n l).
Proof.
  revert l i. induction n as [|? IHn]; auto; simpl.
  intros [|] [|] ?; auto; simpl. by rewrite IHn by lia.
Qed.

Properties of the drop function

Lemma drop_0 l : drop 0 l = l.
Proof. done. Qed.
Lemma drop_nil n : drop n [] =@{list A} [].
Proof. by destruct n. Qed.
Lemma drop_S l x n :
  l !! n = Some x drop n l = x :: drop (S n) l.
Proof. revert n. induction l; intros []; naive_solver. Qed.
Lemma drop_length l n : length (drop n l) = length l - n.
Proof. revert n. by induction l; intros [|i]; f_equal/=. Qed.
Lemma drop_ge l n : length l n drop n l = [].
Proof. revert n. induction l; intros [|?]; simpl in *; auto with lia. Qed.
Lemma drop_all l : drop (length l) l = [].
Proof. by apply drop_ge. Qed.
Lemma drop_drop l n1 n2 : drop n1 (drop n2 l) = drop (n2 + n1) l.
Proof. revert n2. induction l; intros [|?]; simpl; rewrite ?drop_nil; auto. Qed.
Lemma drop_app_le l k n :
  n length l drop n (l ++ k) = drop n l ++ k.
Proof. revert n. induction l; intros [|?]; simpl; auto with lia. Qed.
Lemma drop_app l k : drop (length l) (l ++ k) = k.
Proof. by rewrite drop_app_le, drop_all. Qed.
Lemma drop_app_alt l k n : n = length l drop n (l ++ k) = k.
Proof. intros →. by apply drop_app. Qed.
Lemma drop_app3_alt l1 l2 l3 n :
  n = length l1 drop n ((l1 ++ l2) ++ l3) = l2 ++ l3.
Proof. intros →. by rewrite <-(assoc_L (++)), drop_app. Qed.
Lemma drop_app_ge l k n :
  length l n drop n (l ++ k) = drop (n - length l) k.
Proof.
  intros. rewrite <-(Nat.sub_add (length l) n) at 1 by done.
  by rewrite Nat.add_comm, <-drop_drop, drop_app.
Qed.
Lemma drop_plus_app l k n m :
  length l = n drop (n + m) (l ++ k) = drop m k.
Proof. intros <-. by rewrite <-drop_drop, drop_app. Qed.
Lemma lookup_drop l n i : drop n l !! i = l !! (n + i).
Proof. revert n i. induction l; intros [|i] ?; simpl; auto. Qed.
Lemma lookup_total_drop `{!Inhabited A} l n i : drop n l !!! i = l !!! (n + i).
Proof. by rewrite !list_lookup_total_alt, lookup_drop. Qed.
Lemma drop_alter f l n i : i < n drop n (alter f i l) = drop n l.
Proof.
  intros. apply list_eq. intros j.
  by rewrite !lookup_drop, !list_lookup_alter_ne by lia.
Qed.
Lemma drop_insert_le l n i x : n i drop n (<[i:=x]>l) = <[i-n:=x]>(drop n l).
Proof. revert i n. induction l; intros [] []; naive_solver lia. Qed.
Lemma drop_insert_gt l n i x : i < n drop n (<[i:=x]>l) = drop n l.
Proof.
  intros. apply list_eq. intros j.
  by rewrite !lookup_drop, !list_lookup_insert_ne by lia.
Qed.
Lemma delete_take_drop l i : delete i l = take i l ++ drop (S i) l.
Proof. revert i. induction l; intros [|?]; f_equal/=; auto. Qed.
Lemma take_take_drop l n m : take n l ++ take m (drop n l) = take (n + m) l.
Proof. revert n m. induction l; intros [|?] [|?]; f_equal/=; auto. Qed.
Lemma drop_take_drop l n m : n m drop n (take m l) ++ drop m l = drop n l.
Proof.
  revert n m. induction l; intros [|?] [|?] ?;
    f_equal/=; auto using take_drop with lia.
Qed.

Lemma app_eq_inv l1 l2 k1 k2 :
  l1 ++ l2 = k1 ++ k2
  ( k, l1 = k1 ++ k k2 = k ++ l2) ( k, k1 = l1 ++ k l2 = k ++ k2).
Proof.
  intros Hlk. destruct (decide (length l1 < length k1)).
  - right. rewrite <-(take_drop (length l1) k1), <-(assoc_L _) in Hlk.
    apply app_inj_1 in Hlk as [Hl1 Hl2]; [|rewrite take_length; lia].
     (drop (length l1) k1). by rewrite Hl1 at 1; rewrite take_drop.
  - left. rewrite <-(take_drop (length k1) l1), <-(assoc_L _) in Hlk.
    apply app_inj_1 in Hlk as [Hk1 Hk2]; [|rewrite take_length; lia].
     (drop (length k1) l1). by rewrite <-Hk1 at 1; rewrite take_drop.
Qed.

Properties of the replicate function

Lemma replicate_length n x : length (replicate n x) = n.
Proof. induction n; simpl; auto. Qed.
Lemma lookup_replicate n x y i :
  replicate n x !! i = Some y y = x i < n.
Proof.
  split.
  - revert i. induction n; intros [|?]; naive_solver auto with lia.
  - intros [-> Hi]. revert i Hi.
    induction n; intros [|?]; naive_solver auto with lia.
Qed.
Lemma elem_of_replicate n x y : y replicate n x y = x n 0.
Proof.
  rewrite elem_of_list_lookup, Nat.neq_0_lt_0.
  setoid_rewrite lookup_replicate; naive_solver eauto with lia.
Qed.
Lemma lookup_replicate_1 n x y i :
  replicate n x !! i = Some y y = x i < n.
Proof. by rewrite lookup_replicate. Qed.
Lemma lookup_replicate_2 n x i : i < n replicate n x !! i = Some x.
Proof. by rewrite lookup_replicate. Qed.
Lemma lookup_total_replicate_2 `{!Inhabited A} n x i :
  i < n replicate n x !!! i = x.
Proof. intros. by rewrite list_lookup_total_alt, lookup_replicate_2. Qed.
Lemma lookup_replicate_None n x i : n i replicate n x !! i = None.
Proof.
  rewrite eq_None_not_Some, Nat.le_ngt. split.
  - intros Hin [x' Hx']; destruct Hin. rewrite lookup_replicate in Hx'; tauto.
  - intros Hx ?. destruct Hx. x; auto using lookup_replicate_2.
Qed.
Lemma insert_replicate x n i : <[i:=x]>(replicate n x) = replicate n x.
Proof. revert i. induction n; intros [|?]; f_equal/=; auto. Qed.
Lemma insert_replicate_lt x y n i :
  i < n
  <[i:=y]>(replicate n x) = replicate i x ++ y :: replicate (n - S i) x.
Proof.
  revert i. induction n as [|n IH]; intros [|i] Hi; simpl; [lia..| |].
  - by rewrite Nat.sub_0_r.
  - by rewrite IH by lia.
Qed.
Lemma elem_of_replicate_inv x n y : x replicate n y x = y.
Proof. induction n; simpl; rewrite ?elem_of_nil, ?elem_of_cons; intuition. Qed.
Lemma replicate_S n x : replicate (S n) x = x :: replicate n x.
Proof. done. Qed.
Lemma replicate_S_end n x : replicate (S n) x = replicate n x ++ [x].
Proof. induction n; f_equal/=; auto. Qed.
Lemma replicate_plus n m x :
  replicate (n + m) x = replicate n x ++ replicate m x.
Proof. induction n; f_equal/=; auto. Qed.
Lemma replicate_cons_app n x :
  x :: replicate n x = replicate n x ++ [x].
Proof. induction n; f_equal/=; eauto. Qed.
Lemma take_replicate n m x : take n (replicate m x) = replicate (min n m) x.
Proof. revert m. by induction n; intros [|?]; f_equal/=. Qed.
Lemma take_replicate_plus n m x : take n (replicate (n + m) x) = replicate n x.
Proof. by rewrite take_replicate, min_l by lia. Qed.
Lemma drop_replicate n m x : drop n (replicate m x) = replicate (m - n) x.
Proof. revert m. by induction n; intros [|?]; f_equal/=. Qed.
Lemma drop_replicate_plus n m x : drop n (replicate (n + m) x) = replicate m x.
Proof. rewrite drop_replicate. f_equal. lia. Qed.
Lemma replicate_as_elem_of x n l :
  replicate n x = l length l = n y, y l y = x.
Proof.
  split; [intros <-; eauto using elem_of_replicate_inv, replicate_length|].
  intros [<- Hl]. symmetry. induction l as [|y l IH]; f_equal/=.
  - apply Hl. by left.
  - apply IH. intros ??. apply Hl. by right.
Qed.
Lemma reverse_replicate n x : reverse (replicate n x) = replicate n x.
Proof.
  symmetry. apply replicate_as_elem_of.
  rewrite reverse_length, replicate_length. split; auto.
  intros y. rewrite elem_of_reverse. by apply elem_of_replicate_inv.
Qed.
Lemma replicate_false βs n : length βs = n replicate n false =.>* βs.
Proof. intros <-. by induction βs; simpl; constructor. Qed.
Lemma tail_replicate x n : tail (replicate n x) = replicate (pred n) x.
Proof. by destruct n. Qed.

Properties of the resize function

Lemma resize_spec l n x : resize n x l = take n l ++ replicate (n - length l) x.
Proof. revert n. induction l; intros [|?]; f_equal/=; auto. Qed.
Lemma resize_0 l x : resize 0 x l = [].
Proof. by destruct l. Qed.
Lemma resize_nil n x : resize n x [] = replicate n x.
Proof. rewrite resize_spec. rewrite take_nil. f_equal/=. lia. Qed.
Lemma resize_ge l n x :
  length l n resize n x l = l ++ replicate (n - length l) x.
Proof. intros. by rewrite resize_spec, take_ge. Qed.
Lemma resize_le l n x : n length l resize n x l = take n l.
Proof.
  intros. rewrite resize_spec, (proj2 (Nat.sub_0_le _ _)) by done.
  simpl. by rewrite (right_id_L [] (++)).
Qed.
Lemma resize_all l x : resize (length l) x l = l.
Proof. intros. by rewrite resize_le, take_ge. Qed.
Lemma resize_all_alt l n x : n = length l resize n x l = l.
Proof. intros →. by rewrite resize_all. Qed.
Lemma resize_plus l n m x :
  resize (n + m) x l = resize n x l ++ resize m x (drop n l).
Proof.
  revert n m. induction l; intros [|?] [|?]; f_equal/=; auto.
  - by rewrite Nat.add_0_r, (right_id_L [] (++)).
  - by rewrite replicate_plus.
Qed.
Lemma resize_plus_eq l n m x :
  length l = n resize (n + m) x l = l ++ replicate m x.
Proof. intros <-. by rewrite resize_plus, resize_all, drop_all, resize_nil. Qed.
Lemma resize_app_le l1 l2 n x :
  n length l1 resize n x (l1 ++ l2) = resize n x l1.
Proof.
  intros. by rewrite !resize_le, take_app_le by (rewrite ?app_length; lia).
Qed.
Lemma resize_app l1 l2 n x : n = length l1 resize n x (l1 ++ l2) = l1.
Proof. intros →. by rewrite resize_app_le, resize_all. Qed.
Lemma resize_app_ge l1 l2 n x :
  length l1 n resize n x (l1 ++ l2) = l1 ++ resize (n - length l1) x l2.
Proof.
  intros. rewrite !resize_spec, take_app_ge, (assoc_L (++)) by done.
  do 2 f_equal. rewrite app_length. lia.
Qed.
Lemma resize_length l n x : length (resize n x l) = n.
Proof. rewrite resize_spec, app_length, replicate_length, take_length. lia. Qed.
Lemma resize_replicate x n m : resize n x (replicate m x) = replicate n x.
Proof. revert m. induction n; intros [|?]; f_equal/=; auto. Qed.
Lemma resize_resize l n m x : n m resize n x (resize m x l) = resize n x l.
Proof.
  revert n m. induction l; simpl.
  - intros. by rewrite !resize_nil, resize_replicate.
  - intros [|?] [|?] ?; f_equal/=; auto with lia.
Qed.
Lemma resize_idemp l n x : resize n x (resize n x l) = resize n x l.
Proof. by rewrite resize_resize. Qed.
Lemma resize_take_le l n m x : n m resize n x (take m l) = resize n x l.
Proof. revert n m. induction l; intros [|?][|?] ?; f_equal/=; auto with lia. Qed.
Lemma resize_take_eq l n x : resize n x (take n l) = resize n x l.
Proof. by rewrite resize_take_le. Qed.
Lemma take_resize l n m x : take n (resize m x l) = resize (min n m) x l.
Proof.
  revert n m. induction l; intros [|?][|?]; f_equal/=; auto using take_replicate.
Qed.
Lemma take_resize_le l n m x : n m take n (resize m x l) = resize n x l.
Proof. intros. by rewrite take_resize, Min.min_l. Qed.
Lemma take_resize_eq l n x : take n (resize n x l) = resize n x l.
Proof. intros. by rewrite take_resize, Min.min_l. Qed.
Lemma take_resize_plus l n m x : take n (resize (n + m) x l) = resize n x l.
Proof. by rewrite take_resize, min_l by lia. Qed.
Lemma drop_resize_le l n m x :
  n m drop n (resize m x l) = resize (m - n) x (drop n l).
Proof.
  revert n m. induction l; simpl.
  - intros. by rewrite drop_nil, !resize_nil, drop_replicate.
  - intros [|?] [|?] ?; simpl; try case_match; auto with lia.
Qed.
Lemma drop_resize_plus l n m x :
  drop n (resize (n + m) x l) = resize m x (drop n l).
Proof. rewrite drop_resize_le by lia. f_equal. lia. Qed.
Lemma lookup_resize l n x i : i < n i < length l resize n x l !! i = l !! i.
Proof.
  intros ??. destruct (decide (n < length l)).
  - by rewrite resize_le, lookup_take by lia.
  - by rewrite resize_ge, lookup_app_l by lia.
Qed.
Lemma lookup_total_resize `{!Inhabited A} l n x i :
  i < n i < length l resize n x l !!! i = l !!! i.
Proof. intros. by rewrite !list_lookup_total_alt, lookup_resize. Qed.
Lemma lookup_resize_new l n x i :
  length l i i < n resize n x l !! i = Some x.
Proof.
  intros ??. rewrite resize_ge by lia.
  replace i with (length l + (i - length l)) by lia.
  by rewrite lookup_app_r, lookup_replicate_2 by lia.
Qed.
Lemma lookup_total_resize_new `{!Inhabited A} l n x i :
  length l i i < n resize n x l !!! i = x.
Proof. intros. by rewrite !list_lookup_total_alt, lookup_resize_new. Qed.
Lemma lookup_resize_old l n x i : n i resize n x l !! i = None.
Proof. intros ?. apply lookup_ge_None_2. by rewrite resize_length. Qed.
Lemma lookup_total_resize_old `{!Inhabited A} l n x i :
  n i resize n x l !!! i = inhabitant.
Proof. intros. by rewrite !list_lookup_total_alt, lookup_resize_old. Qed.

Properties of the rotate function

Lemma rotate_replicate n1 n2 x:
  rotate n1 (replicate n2 x) = replicate n2 x.
Proof.
  unfold rotate. rewrite drop_replicate, take_replicate, <-replicate_plus.
  f_equal. lia.
Qed.

Lemma rotate_length l n:
  length (rotate n l) = length l.
Proof. unfold rotate. rewrite app_length, drop_length, take_length. lia. Qed.

Lemma lookup_rotate_r l n i:
  i < length l
  rotate n l !! i = l !! rotate_nat_add n i (length l).
Proof.
  intros Hlen. destruct (Z_mod_lt n (length l)) as [??];[lia|].
  assert (Z.to_nat (n `mod` length l) < length l) as Hr.
  { apply Nat2Z.inj_lt. rewrite Z2Nat.id; lia. }
  unfold rotate. rewrite rotate_nat_add_add_mod, rotate_nat_add_alt by done.
  remember (Z.to_nat (n `mod` length l)) as n'.
  case_decide.
  - by rewrite lookup_app_l, lookup_drop by (rewrite drop_length; lia).
  - rewrite lookup_app_r, lookup_take, drop_length by (rewrite drop_length; lia).
    f_equal. lia.
Qed.

Lemma lookup_rotate_r_Some l n i x:
  rotate n l !! i = Some x
  l !! rotate_nat_add n i (length l) = Some x i < length l.
Proof.
  split.
  - intros Hl. pose proof (lookup_lt_Some _ _ _ Hl) as Hlen.
    rewrite rotate_length in Hlen. by rewrite <-lookup_rotate_r.
  - intros [??]. by rewrite lookup_rotate_r.
Qed.

Lemma lookup_rotate_l l n i:
  i < length l rotate n l !! rotate_nat_sub n i (length l) = l !! i.
Proof.
  intros ?. rewrite lookup_rotate_r, rotate_nat_add_sub;[done..|].
  apply rotate_nat_sub_lt. lia.
Qed.

Lemma elem_of_rotate l n x:
  x rotate n l x l.
Proof.
  unfold rotate. rewrite <-(take_drop (Z.to_nat (n `mod` length l)) l) at 5.
  rewrite !elem_of_app. naive_solver.
Qed.

Lemma rotate_insert_l l n i x:
  i < length l
  rotate n (<[rotate_nat_add n i (length l):=x]> l) = <[i:=x]> (rotate n l).
Proof.
  intros Hlen. destruct (Z_mod_lt n (length l)) as [Hn1 Hn2];[lia|].
  assert (Z.to_nat (n `mod` length l) < length l) as Hr.
  { apply Nat2Z.inj_lt. rewrite Z2Nat.id; lia. } unfold rotate.
  rewrite insert_length, rotate_nat_add_add_mod, rotate_nat_add_alt by done.
  remember (Z.to_nat (n `mod` length l)) as n'.
  case_decide.
  - rewrite take_insert, drop_insert_le, insert_app_l
      by (rewrite ?drop_length; lia). do 2 f_equal. lia.
  - rewrite take_insert_lt, drop_insert_gt, insert_app_r_alt, drop_length
      by (rewrite ?drop_length; lia). do 2 f_equal. lia.
Qed.

Lemma rotate_insert_r l n i x:
  i < length l
  rotate n (<[i:=x]> l) = <[rotate_nat_sub n i (length l):=x]> (rotate n l).
Proof.
  intros ?. rewrite <-rotate_insert_l, rotate_nat_add_sub;[done..|].
  apply rotate_nat_sub_lt. lia.
Qed.

Properties of the rotate_take function

Lemma rotate_take_insert l s e i x:
  i < length l
  rotate_take s e (<[i:=x]>l) =
  if decide (rotate_nat_sub s i (length l) < rotate_nat_sub s e (length l)) then
    <[rotate_nat_sub s i (length l):=x]> (rotate_take s e l) else rotate_take s e l.
Proof.
  intros ?. unfold rotate_take. rewrite rotate_insert_r, insert_length by done.
  case_decide; [rewrite take_insert_lt | rewrite take_insert]; naive_solver lia.
Qed.

Lemma rotate_take_add l b i :
  i < length l
  rotate_take b (rotate_nat_add b i (length l)) l = take i (rotate b l).
Proof. intros ?. unfold rotate_take. by rewrite rotate_nat_sub_add. Qed.

Properties of the reshape function

Lemma reshape_length szs l : length (reshape szs l) = length szs.
Proof. revert l. by induction szs; intros; f_equal/=. Qed.
End general_properties.

Section more_general_properties.
Context {A : Type}.
Implicit Types x y z : A.
Implicit Types l k : list A.

Properties of sublist_lookup and sublist_alter

Lemma sublist_lookup_length l i n k :
  sublist_lookup i n l = Some k length k = n.
Proof.
  unfold sublist_lookup; intros; simplify_option_eq.
  rewrite take_length, drop_length; lia.
Qed.
Lemma sublist_lookup_all l n : length l = n sublist_lookup 0 n l = Some l.
Proof.
  intros. unfold sublist_lookup; case_option_guard; [|lia].
  by rewrite take_ge by (rewrite drop_length; lia).
Qed.
Lemma sublist_lookup_Some l i n :
  i + n length l sublist_lookup i n l = Some (take n (drop i l)).
Proof. by unfold sublist_lookup; intros; simplify_option_eq. Qed.
Lemma sublist_lookup_None l i n :
  length l < i + n sublist_lookup i n l = None.
Proof. by unfold sublist_lookup; intros; simplify_option_eq by lia. Qed.
Lemma sublist_eq l k n :
  (n | length l) (n | length k)
  ( i, sublist_lookup (i × n) n l = sublist_lookup (i × n) n k) l = k.
Proof.
  revert l k. assert ( l i,
    n 0 (n | length l) ¬n × i `div` n + n length l length l i).
  { intros l i ? [j ->] Hjn. apply Nat.nlt_ge; contradict Hjn.
    rewrite <-Nat.mul_succ_r, (Nat.mul_comm n).
    apply Nat.mul_le_mono_r, Nat.le_succ_l, Nat.div_lt_upper_bound; lia. }
  intros l k Hl Hk Hlookup. destruct (decide (n = 0)) as [->|].
  { by rewrite (nil_length_inv l),
      (nil_length_inv k) by eauto using Nat.divide_0_l. }
  apply list_eq; intros i. specialize (Hlookup (i `div` n)).
  rewrite (Nat.mul_comm _ n) in Hlookup.
  unfold sublist_lookup in *; simplify_option_eq;
    [|by rewrite !lookup_ge_None_2 by auto].
  apply (f_equal (.!! i `mod` n)) in Hlookup.
  by rewrite !lookup_take, !lookup_drop, <-!Nat.div_mod in Hlookup
    by (auto using Nat.mod_upper_bound with lia).
Qed.
Lemma sublist_eq_same_length l k j n :
  length l = j × n length k = j × n
  ( i,i < j sublist_lookup (i × n) n l = sublist_lookup (i × n) n k) l = k.
Proof.
  intros Hl Hk ?. destruct (decide (n = 0)) as [->|].
  { by rewrite (nil_length_inv l), (nil_length_inv k) by lia. }
  apply sublist_eq with n; [by j|by j|].
  intros i. destruct (decide (i < j)); [by auto|].
  assert ( m, m = j × n m < i × n + n).
  { intros ? →. replace (i × n + n) with (S i × n) by lia.
    apply Nat.mul_lt_mono_pos_r; lia. }
  by rewrite !sublist_lookup_None by auto.
Qed.
Lemma sublist_lookup_reshape l i n m :
  0 <