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.
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 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.
seqZ m n generates the sequence m, m + 1, ..., m + n - 1 over integers, provided n 0. If n < 0, then the range is empty.
Definition seqZ (m len: Z) : list Z :=
  (λ i: nat, Z.add i m) <$> (seq 0 (Z.to_nat len)).
Arguments seqZ : simpl never.

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_nil i : @nil A !! i = None.
Proof. by destruct i. Qed.
Lemma lookup_tail 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 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_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_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 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_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. done. intros [|i]. done. apply (IHl i). 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_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_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_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 : l !! i = Some x <[i:=x]>l = l.
Proof. revert i. induction l; intros [|i] [=]; f_equal/=; auto. 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_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_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_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 l1 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 l1 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.
  - split; [by right|]. intros [Hx|]; [|done]. by destruct (elem_of_nil x).
  - simpl. rewrite !elem_of_cons, IHl1. tauto.
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_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 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_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|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. rewrite elem_of_list_difference; intuition. done.
  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. rewrite elem_of_list_intersection; intuition. done.
    - 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.
Lemma sum_list_with_app (f : A nat) l k :
  sum_list_with f (l ++ k) = sum_list_with f l + sum_list_with f k.
Proof. induction l; simpl; lia. Qed.
Lemma sum_list_with_reverse (f : A nat) l :
  sum_list_with f (reverse l) = sum_list_with f l.
Proof.
  induction l; simpl; rewrite ?reverse_cons, ?sum_list_with_app; simpl; lia.
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_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 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 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 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_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 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.

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

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.
Lemma join_reshape szs l :
  sum_list szs = length l mjoin (reshape szs l) = l.
Proof.
  revert l. induction szs as [|sz szs IH]; simpl; intros l Hl; [by destruct l|].
  by rewrite IH, take_drop by (rewrite drop_length; lia).
Qed.
Lemma sum_list_replicate n m : sum_list (replicate m n) = m × n.
Proof. induction m; simpl; auto. 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 < n length l = m × n
  reshape (replicate m n) l !! i = sublist_lookup (i × n) n l.
Proof.
  intros Hn Hl. unfold sublist_lookup. apply option_eq; intros x; split.
  - intros Hx. case_option_guard as Hi.
    { f_equal. clear Hi. revert i l Hl Hx.
      induction m as [|m IH]; intros [|i] l ??; simplify_eq/=; auto.
      rewrite <-drop_drop. apply IH; rewrite ?drop_length; auto with lia. }
    destruct Hi. rewrite Hl, <-Nat.mul_succ_l.
    apply Nat.mul_le_mono_r, Nat.le_succ_l. apply lookup_lt_Some in Hx.
    by rewrite reshape_length, replicate_length in Hx.
  - intros Hx. case_option_guard as Hi; simplify_eq/=.
    revert i l Hl Hi. induction m as [|m IH]; [auto with lia|].
    intros [|i] l ??; simpl; [done|]. rewrite <-drop_drop.
    rewrite IH; rewrite ?drop_length; auto with lia.
Qed.
Lemma sublist_lookup_compose l1 l2 l3 i n j m :
  sublist_lookup i n l1 = Some l2 sublist_lookup j m l2 = Some l3
  sublist_lookup (i + j) m l1 = Some l3.
Proof.
  unfold sublist_lookup; intros; simplify_option_eq;
    repeat match goal with
    | H : _ length _ |- _rewrite take_length, drop_length in H
    end; rewrite ?take_drop_commute, ?drop_drop, ?take_take,
      ?Min.min_l, Nat.add_assoc by lia; auto with lia.
Qed.
Lemma sublist_alter_length f l i n k :
  sublist_lookup i n l = Some k length (f k) = n
  length (sublist_alter f i n l) = length l.
Proof.
  unfold sublist_alter, sublist_lookup. intros Hk ?; simplify_option_eq.
  rewrite !app_length, Hk, !take_length, !drop_length; lia.
Qed.
Lemma sublist_lookup_alter f l i n k :
  sublist_lookup i n l = Some k length (f k) = n
  sublist_lookup i n (sublist_alter f i n l) = f <$> sublist_lookup i n l.
Proof.
  unfold sublist_lookup. intros Hk ?. erewrite sublist_alter_length by eauto.
  unfold sublist_alter; simplify_option_eq.
  by rewrite Hk, drop_app_alt, take_app_alt by (rewrite ?take_length; lia).
Qed.
Lemma sublist_lookup_alter_ne f l i j n k :
  sublist_lookup j n l = Some k length (f k) = n i + n j j + n i
  sublist_lookup i n (sublist_alter f j n l) = sublist_lookup i n l.
Proof.
  unfold sublist_lookup. intros Hk Hi ?. erewrite sublist_alter_length by eauto.
  unfold sublist_alter; simplify_option_eq; f_equal; rewrite Hk.
  apply list_eq; intros ii.
  destruct (decide (ii < length (f k))); [|by rewrite !lookup_take_ge by lia].
  rewrite !lookup_take, !lookup_drop by done. destruct (decide (i + ii < j)).
  { by rewrite lookup_app_l, lookup_take by (rewrite ?take_length; lia). }
  rewrite lookup_app_r by (rewrite take_length; lia).
  rewrite take_length_le, lookup_app_r, lookup_drop by lia. f_equal; lia.
Qed.
Lemma sublist_alter_all f l n : length l = n sublist_alter f 0 n l = f l.
Proof.
  intros <-. unfold sublist_alter; simpl.
  by rewrite drop_all, (right_id_L [] (++)), take_ge.
Qed.
Lemma sublist_alter_compose f g l i n k :
  sublist_lookup i n l = Some k length (f k) = n length (g k) = n
  sublist_alter (f g) i n l = sublist_alter f i n (sublist_alter g i n l).
Proof.
  unfold sublist_alter, sublist_lookup. intros Hk ??; simplify_option_eq.
  by rewrite !take_app_alt, drop_app_alt, !(assoc_L (++)), drop_app_alt,
    take_app_alt by (rewrite ?app_length, ?take_length, ?Hk; lia).
Qed.

Properties of the mask function

Lemma mask_nil f βs : mask f βs [] =@{list A} [].
Proof. by destruct βs. Qed.
Lemma mask_length f βs l : length (mask f βs l) = length l.
Proof. revert βs. induction l; intros [|??]; f_equal/=; auto. Qed.
Lemma mask_true f l n : length l n mask f (replicate n true) l = f <$> l.
Proof. revert n. induction l; intros [|?] ?; f_equal/=; auto with lia. Qed.
Lemma mask_false f l n : mask f (replicate n false) l = l.
Proof. revert l. induction n; intros [|??]; f_equal/=; auto. Qed.
Lemma mask_app f βs1 βs2 l :
  mask f (βs1 ++ βs2) l
  = mask f βs1 (take (length βs1) l) ++ mask f βs2 (drop (length βs1) l).
Proof. revert l. induction βs1;intros [|??]; f_equal/=; auto using mask_nil. Qed.
Lemma mask_app_2 f βs l1 l2 :
  mask f βs (l1 ++ l2)
  = mask f (take (length l1) βs) l1 ++ mask f (drop (length l1) βs) l2.
Proof. revert βs. induction l1; intros [|??]; f_equal/=; auto. Qed.
Lemma take_mask f βs l n : take n (mask f βs l) = mask f (take n βs) (take n l).
Proof. revert n βs. induction l; intros [|?] [|[] ?]; f_equal/=; auto. Qed.
Lemma drop_mask f βs l n : drop n (mask f βs l) = mask f (drop n βs) (drop n l).
Proof.
  revert n βs. induction l; intros [|?] [|[] ?]; f_equal/=; auto using mask_nil.
Qed.
Lemma sublist_lookup_mask f βs l i n :
  sublist_lookup i n (mask f βs l)
  = mask f (take n (drop i βs)) <$> sublist_lookup i n l.
Proof.
  unfold sublist_lookup; rewrite mask_length; simplify_option_eq; auto.
  by rewrite drop_mask, take_mask.
Qed.
Lemma mask_mask f g βs1 βs2 l :
  ( x, f (g x) = f x) βs1 =.>* βs2
  mask f βs2 (mask g βs1 l) = mask f βs2 l.
Proof.
  intros ? Hβs. revert l. by induction Hβs as [|[] []]; intros [|??]; f_equal/=.
Qed.
Lemma lookup_mask f βs l i :
  βs !! i = Some true mask f βs l !! i = f <$> l !! i.
Proof.
  revert i βs. induction l; intros [] [] ?; simplify_eq/=; f_equal; auto.
Qed.
Lemma lookup_mask_notin f βs l i :
  βs !! i Some true mask f βs l !! i = l !! i.
Proof.
  revert i βs. induction l; intros [] [|[]] ?; simplify_eq/=; auto.
Qed.

Properties of the Permutation predicate

Lemma Permutation_nil l : l ≡ₚ [] l = [].
Proof. split. by intro; apply Permutation_nil. by intros →. Qed.
Lemma Permutation_singleton l x : l ≡ₚ [x] l = [x].
Proof. split. by intro; apply Permutation_length_1_inv. by intros →. Qed.
Definition Permutation_skip := @perm_skip A.
Definition Permutation_swap := @perm_swap A.
Definition Permutation_singleton_inj := @Permutation_length_1 A.

Global Instance Permutation_cons : Proper ((≡ₚ) ==> (≡ₚ)) (@cons A x).
Proof. by constructor. Qed.
Global Existing Instance Permutation_app'.

Global Instance: Proper ((≡ₚ) ==> (=)) (@length A).
Proof. induction 1; simpl; auto with lia. Qed.
Global Instance: Comm (≡ₚ) (@app A).
Proof.
  intros l1. induction l1 as [|x l1 IH]; intros l2; simpl.
  - by rewrite (right_id_L [] (++)).
  - rewrite Permutation_middle, IH. simpl. by rewrite Permutation_middle.
Qed.
Global Instance: x : A, Inj (≡ₚ) (≡ₚ) (x ::.).
Proof. red. eauto using Permutation_cons_inv. Qed.
Global Instance: k : list A, Inj (≡ₚ) (≡ₚ) (k ++.).
Proof.
  red. induction k as [|x k IH]; intros l1 l2; simpl; auto.
  intros. by apply IH, (inj (x ::.)).
Qed.
Global Instance: k : list A, Inj (≡ₚ) (≡ₚ) (.++ k).
Proof. intros k l1 l2. rewrite !(comm (++) _ k). by apply (inj (k ++.)). Qed.
Lemma replicate_Permutation n x l : replicate n x ≡ₚ l replicate n x = l.
Proof.
  intros Hl. apply replicate_as_elem_of. split.
  - by rewrite <-Hl, replicate_length.
  - intros y. rewrite <-Hl. by apply elem_of_replicate_inv.
Qed.
Lemma reverse_Permutation l : reverse l ≡ₚ l.
Proof.
  induction l as [|x l IH]; [done|].
  by rewrite reverse_cons, (comm (++)), IH.
Qed.
Lemma delete_Permutation l i x : l !! i = Some x l ≡ₚ x :: delete i l.
Proof.
  revert i; induction l as [|y l IH]; intros [|i] ?; simplify_eq/=; auto.
  by rewrite Permutation_swap, <-(IH i).
Qed.
Lemma elem_of_Permutation l x : x l k, l ≡ₚ x :: k.
Proof. intros [i ?]%elem_of_list_lookup. eauto using delete_Permutation. Qed.

Lemma Permutation_cons_inv l k x :
  k ≡ₚ x :: l k1 k2, k = k1 ++ x :: k2 l ≡ₚ k1 ++ k2.
Proof.
  intros Hk. assert ( i, k !! i = Some x) as [i Hi].
  { apply elem_of_list_lookup. rewrite Hk, elem_of_cons; auto. }
   (take i k), (drop (S i) k). split.
  - by rewrite take_drop_middle.
  - rewrite <-delete_take_drop. apply (inj (x ::.)).
    by rewrite <-Hk, <-(delete_Permutation k) by done.
Qed.

Lemma length_delete l i :
  is_Some (l !! i) length (delete i l) = length l - 1.
Proof.
  rewrite lookup_lt_is_Some. revert i.
  induction l as [|x l IH]; intros [|i] ?; simpl in *; [lia..|].
  rewrite IH by lia. lia.
Qed.
Lemma lookup_delete_lt l i j : j < i delete i l !! j = l !! j.
Proof. revert i j; induction l; intros [] []; naive_solver eauto with lia. Qed.
Lemma lookup_delete_ge l i j : i j delete i l !! j = l !! S j.
Proof. revert i j; induction l; intros [] []; naive_solver eauto with lia. Qed.

Lemma Permutation_inj l1 l2 :
  Permutation l1 l2
    length l1 = length l2
     f : nat nat, Inj (=) (=) f i, l1 !! i = l2 !! f i.
Proof.
  split.
  - intros Hl; split; [by apply Permutation_length|].
    induction Hl as [|x l1 l2 _ [f [??]]|x y l|l1 l2 l3 _ [f [? Hf]] _ [g [? Hg]]].
    + id; split; [apply _|done].
    + (λ i, match i with 0 ⇒ 0 | S iS (f i) end); split.
      × by intros [|i] [|j] ?; simplify_eq/=.
      × intros [|i]; simpl; auto.
    + (λ i, match i with 0 ⇒ 1 | 1 ⇒ 0 | _i end); split.
      × intros [|[|i]] [|[|j]]; congruence.
      × by intros [|[|i]].
    + (g f); split; [apply _|]. intros i; simpl. by rewrite <-Hg, <-Hf.
  - intros (Hlen & f & Hf & Hl). revert l2 f Hlen Hf Hl.
    induction l1 as [|x l1 IH]; intros l2 f Hlen Hf Hl; [by destruct l2|].
    rewrite (delete_Permutation l2 (f 0) x) by (by rewrite <-Hl).
    pose (g n := let m := f (S n) in if lt_eq_lt_dec m (f 0) then m else m - 1).
    eapply Permutation_cons, (IH _ g).
    + rewrite length_delete by (rewrite <-Hl; eauto); simpl in *; lia.
    + unfold g. intros i j Hg.
      repeat destruct (lt_eq_lt_dec _ _) as [[?|?]|?]; simplify_eq/=; try lia.
      apply (inj S), (inj f); lia.
    + intros i. unfold g. destruct (lt_eq_lt_dec _ _) as [[?|?]|?].
      × by rewrite lookup_delete_lt, <-Hl.
      × simplify_eq.
      × rewrite lookup_delete_ge, <-Nat.sub_succ_l by lia; simpl.
        by rewrite Nat.sub_0_r, <-Hl.
Qed.

Properties of the filter function

Section filter.
  Context (P : A Prop) `{ x, Decision (P x)}.
  Local Arguments filter {_ _ _} _ {_} !_ /.

  Lemma filter_nil : filter P [] = [].
  Proof. done. Qed.
  Lemma filter_cons x l :
    filter P (x :: l) = if decide (P x) then x :: filter P l else filter P l.
  Proof. done. Qed.
  Lemma filter_cons_True x l : P x filter P (x :: l) = x :: filter P l.
  Proof. intros. by rewrite filter_cons, decide_True. Qed.
  Lemma filter_cons_False x l : ¬P x filter P (x :: l) = filter P l.
  Proof. intros. by rewrite filter_cons, decide_False. Qed.

  Lemma elem_of_list_filter l x : x filter P l P x x l.
  Proof.
    induction l; simpl; repeat case_decide;
      rewrite ?elem_of_nil, ?elem_of_cons; naive_solver.
  Qed.
  Lemma NoDup_filter l : NoDup l NoDup (filter P l).
  Proof.
    induction 1; simpl; repeat case_decide;
      rewrite ?NoDup_nil, ?NoDup_cons, ?elem_of_list_filter; tauto.
  Qed.

  Global Instance filter_Permutation : Proper ((≡ₚ) ==> (≡ₚ)) (filter P).
  Proof. induction 1; repeat (simpl; repeat case_decide); by econstructor. Qed.

  Lemma filter_length l : length (filter P l) length l.
  Proof. induction l; simpl; repeat case_decide; simpl; lia. Qed.
  Lemma filter_length_lt l x : x l ¬P x length (filter P l) < length l.
  Proof.
    intros [k ->]%elem_of_Permutation ?; simpl.
    rewrite decide_False, Nat.lt_succ_r by done. apply filter_length.
  Qed.
End filter.

Properties of the prefix and suffix predicates

Global Instance: PreOrder (@prefix A).
Proof.
  split.
  - intros ?. eexists []. by rewrite (right_id_L [] (++)).
  - intros ???[k1->] [k2->]. (k1 ++ k2). by rewrite (assoc_L (++)).
Qed.
Lemma prefix_nil l : [] `prefix_of` l.
Proof. by l. Qed.
Lemma prefix_nil_not x l : ¬x :: l `prefix_of` [].
Proof. by intros [k ?]. Qed.
Lemma prefix_cons x l1 l2 : l1 `prefix_of` l2 x :: l1 `prefix_of` x :: l2.
Proof. intros [k ->]. by k. Qed.
Lemma prefix_cons_alt x y l1 l2 :
  x = y l1 `prefix_of` l2 x :: l1 `prefix_of` y :: l2.
Proof. intros →. apply prefix_cons. Qed.
Lemma prefix_cons_inv_1 x y l1 l2 : x :: l1 `prefix_of` y :: l2 x = y.
Proof. by intros [k ?]; simplify_eq/=. Qed.
Lemma prefix_cons_inv_2 x y l1 l2 :
  x :: l1 `prefix_of` y :: l2 l1 `prefix_of` l2.
Proof. intros [k ?]; simplify_eq/=. by k. Qed.
Lemma prefix_app k l1 l2 : l1 `prefix_of` l2 k ++ l1 `prefix_of` k ++ l2.
Proof. intros [k' ->]. k'. by rewrite (assoc_L (++)). Qed.
Lemma prefix_app_alt k1 k2 l1 l2 :
  k1 = k2 l1 `prefix_of` l2 k1 ++ l1 `prefix_of` k2 ++ l2.
Proof. intros →. apply prefix_app. Qed.
Lemma prefix_app_l l1 l2 l3 : l1 ++ l3 `prefix_of` l2 l1 `prefix_of` l2.
Proof. intros [k ->]. (l3 ++ k). by rewrite (assoc_L (++)). Qed.
Lemma prefix_app_r l1 l2 l3 : l1 `prefix_of` l2 l1 `prefix_of` l2 ++ l3.
Proof. intros [k ->]. (k ++ l3). by rewrite (assoc_L (++)). Qed.
Lemma prefix_lookup l1 l2 i x :
  l1 !! i = Some x l1 `prefix_of` l2 l2 !! i = Some x.
Proof. intros ? [k ->]. rewrite lookup_app_l; eauto using lookup_lt_Some. Qed.
Lemma prefix_length l1 l2 : l1 `prefix_of` l2 length l1 length l2.
Proof. intros [? ->]. rewrite app_length. lia. Qed.
Lemma prefix_snoc_not l x : ¬l ++ [x] `prefix_of` l.
Proof. intros [??]. discriminate_list. Qed.
Global Instance: PreOrder (@suffix A).
Proof.
  split.
  - intros ?. by eexists [].
  - intros ???[k1->] [k2->]. (k2 ++ k1). by rewrite (assoc_L (++)).
Qed.
Global Instance prefix_dec `{!EqDecision A} : RelDecision prefix :=
  fix go l1 l2 :=
  match l1, l2 with
  | [], _left (prefix_nil _)
  | _, []right (prefix_nil_not _ _)
  | x :: l1, y :: l2
    match decide_rel (=) x y with
    | left Hxy
      match go l1 l2 with
      |