list.v

(* Copyright (c) 2012-2013, Robbert Krebbers. *)
(* This file is distributed under the terms of the BSD license. *)
(** This file collects general purpose definitions and theorems on lists that
are not in the Coq standard library. *)

Require Import Permutation.
Require Export numbers base decidable option.

Arguments length {_} _.
Arguments cons {_} _ _.
Arguments app {_} _ _.
Arguments Permutation {_} _ _.
Arguments Forall_cons {_} _ _ _ _ _.

Notation Forall_nil_2 := Forall_nil.
Notation Forall_cons_2 := Forall_cons.

Notation tail := tl.
Notation take := firstn.
Notation drop := skipn.
Notation take_drop := firstn_skipn.
Arguments take {_} !_ !_ /.
Arguments drop {_} !_ !_ /.

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

(** * Definitions *)
(** The operation [l !! i] gives the [i]th 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 : nat) (l : list A) {struct l} : option A :=
  match l with
  | [] => None
  | x :: l =>
    match i with
    | 0 => Some x
    | S i => @lookup _ _ _ go i l
    end
  end.

(** The operation [alter f i l] applies the function [f] to the [i]th element
of [l]. In case [i] is out of bounds, the list is returned unchanged. *)
Instance list_alter {A} (f : A → A) : AlterD nat A (list A) f :=
  fix go (i : nat) (l : list A) {struct l} :=
  match l with
  | [] => []
  | x :: l =>
    match i with
    | 0 => f x :: l
    | S i => x :: @alter _ _ _ f go i l
    end
  end.

(** The operation [delete i l] removes the [i]th 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 :: l =>
    match i with
    | 0 => l
    | S i => x :: @delete _ _ 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) := λ i x,
  alter (λ _, x) i.

(** 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]) [].

(** 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 :=
  match l with
  | [] => []
  | x :: l =>
     if decide (P x)
     then x :: @filter _ _ (@go) _ _ l
     else @filter _ _ (@go) _ _ l
  end.

(** 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 n => x :: replicate n x
  end.

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

Fixpoint last' {A} (x : A) (l : list A) : A :=
  match l with
  | [] => x
  | x :: l => last' x l
  end.
Definition last {A} (l : list A) : option A :=
  match l with
  | [] => None
  | x :: l => Some (last' x l)
  end.

(** 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 :: l =>
    match n with
    | 0 => []
    | S n => x :: resize n y l
    end
  end.
Arguments resize {_} !_ _ !_.

(** 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 :: l => go (f a x) l
  end.

(** The monadic operations. *)
Instance list_ret: MRet list := λ A x, x :: @nil A.
Instance list_fmap {A B} (f : A → B) : FMapD list f :=
  fix go (l : list A) :=
  match l with
  | [] => []
  | x :: l => f x :: @fmap _ _ _ f go l
  end.
Instance list_bind {A B} (f : A → list B) : MBindD list f :=
  fix go (l : list A) :=
  match l with
  | [] => []
  | x :: l => f x ++ @mbind _ _ _ f go l
  end.
Instance list_join: MJoin list :=
  fix go A (ls : list (list A)) : list A :=
  match ls with
  | [] => []
  | l :: ls => l ++ @mjoin _ go _ ls
  end.

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

Definition ifoldr {A B} (f : nat → B → A → A)
    (a : nat → A) : nat → list B → A :=
  fix go (n : nat) (l : list B) : A :=
  match l with
  | nil => a n
  | b :: l => f n b (go (S n) l)
  end.

(** Zipping lists. *)
Definition zip_with {A B C} (f : A → B → C) : list A → list B → list C :=
  fix go l1 l2 :=
  match l1, l2 with
  | x1 :: l1, x2 :: l2 => f x1 x2 :: go l1 l2
  | _ , _ => []
  end.
Notation zip := (zip_with pair).

(** 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 :: l => permutations l ≫= interleave x
  end.

(** The predicate [suffix_of] holds if the first list is a suffix of the second.
The predicate [prefix_of] holds if the first list is a prefix of the second. *)
Definition suffix_of {A} : relation (list A) := λ l1 l2, ∃ k, l2 = k ++ l1.
Definition prefix_of {A} : relation (list A) := λ l1 l2, ∃ k, l2 = l1 ++ k.

Section prefix_suffix_ops.
  Context `{∀ x y : A, Decision (x = y)}.

  Definition max_prefix_of : 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 snd_map (x1 ::) (go l1 l2)
       else (x1 :: l1, x2 :: l2, [])
    end.
  Definition max_suffix_of (l1 l2 : list A) : list A * list A * list A :=
    match max_prefix_of (reverse l1) (reverse l2) with
    | (k1, k2, k3) => (reverse k1, reverse k2, reverse k3)
    end.

  Definition strip_prefix (l1 l2 : list A) := snd $ fst $ max_prefix_of l1 l2.
  Definition strip_suffix (l1 l2 : list A) := snd $ fst $ max_suffix_of l1 l2.
End prefix_suffix_ops.

(** A list [l1] is a sub list 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_cons x l1 l2 : sublist l1 l2 → sublist (x :: l1) (x :: l2)
  | sublist_cons_skip x l1 l2 : sublist l1 l2 → sublist l1 (x :: l2).

(** The [same_length] view allows convenient induction over two lists with the
same length. *)
Inductive same_length {A B} : list A → list B → Prop :=
  | same_length_nil : same_length [] []
  | same_length_cons x y l k :
     same_length l k → same_length (x :: l) (y :: k).

(** * Basic tactics on lists *)
(** The tactic [discriminate_list_equality] discharges a goal if it contains
a list equality involving [(::)] and [(++)] of two lists that have a different
length as one of its hypotheses. *)
Tactic Notation "discriminate_list_equality" hyp(H) :=
  apply (f_equal length) in H;
  repeat (simpl in H || rewrite app_length in H);
  exfalso; lia.
Tactic Notation "discriminate_list_equality" :=
  solve [repeat_on_hyps (fun H => discriminate_list_equality H)].

(** The tactic [simplify_list_equality] simplifies hypotheses involving
equalities on lists using injectivity of [(::)] and [(++)]. Also, it simplifies
lookups in singleton lists. *)
Lemma cons_inv {A} (l1 l2 : list A) x1 x2 :
  x1 :: l1 = x2 :: l2 → x1 = x2 ∧ l1 = l2.
Proof. by injection 1. Qed.

Ltac simplify_list_equality := repeat
  match goal with
  | H : _ :: _ = _ :: _ |- _ =>
     apply cons_inv in H; destruct H
     (* to circumvent bug #2939 in some situations *)
  | H : _ ++ _ = _ ++ _ |- _ => first
     [ apply app_inj_tail in H; destruct H
     | apply app_inv_head in H
     | apply app_inv_tail in H ]
  | H : [?x] !! ?i = Some ?y |- _ =>
     destruct i; [change (Some x = Some y) in H|discriminate]
  | _ => progress simplify_equality
  | H : _ |- _ => discriminate_list_equality H
  end.

(** * General theorems *)
Section general_properties.
Context {A : Type}.

Global Instance: ∀ x : A, Injective (=) (=) (x ::).
Proof. by injection 1. Qed.
Global Instance: ∀ l : list A, Injective (=) (=) (:: l).
Proof. by injection 1. Qed.
Global Instance: ∀ k : list A, Injective (=) (=) (k ++).
Proof. intros ???. apply app_inv_head. Qed.
Global Instance: ∀ k : list A, Injective (=) (=) (++ k).
Proof. intros ???. apply app_inv_tail. Qed.
Global Instance: Associative (=) (@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_inj (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 list_eq (l1 l2 : list A) : (∀ i, l1 !! i = l2 !! i)%C → l1 = l2.
Proof.
  revert l2. induction l1; intros [|??] H.
  * done.
  * discriminate (H 0).
  * discriminate (H 0).
  * f_equal; [by injection (H 0) |].
    apply IHl1. intro. apply (H (S _)).
Qed.
Lemma list_eq_nil (l : list A) : (∀ i, l !! i = None) → l = nil.
Proof. intros. by apply list_eq. Qed.

Global Instance list_eq_dec {dec : ∀ x y : A, Decision (x = y)} : ∀ l k,
  Decision (l = k) := list_eq_dec dec.
Definition list_singleton_dec (l : list A) :
  { x | l = [x] } + { length l ≠ 1 }.
Proof.
 by refine (
  match l with
  | [x] => inleft (x ↾ _)
  | _ => inright _
  end).
Defined.

Global Instance: Proper (Permutation ==> (=)) (@length A).
Proof. induction 1; simpl; auto with lia. Qed.

Lemma nil_or_length_pos (l : list A) : l = [] ∨ length l ≠ 0.
Proof. destruct l; simpl; auto with lia. Qed.
Lemma nil_length (l : list A) : length l = 0 → l = [].
Proof. by destruct l. Qed.
Lemma lookup_nil i : @nil A !! i = None.
Proof. by destruct i. Qed.
Lemma lookup_tail (l : list A) i : tail l !! i = l !! S i.
Proof. by destruct l. Qed.

Lemma lookup_lt_length (l : list A) i :
  is_Some (l !! i) ↔ i < length l.
Proof.
  revert i. induction l.
  * split; by inversion 1.
  * intros [|?]; simpl.
    + split; eauto with arith.
    + by rewrite <-NPeano.Nat.succ_lt_mono.
Qed.
Lemma lookup_lt_length_1 (l : list A) i :
  is_Some (l !! i) → i < length l.
Proof. apply lookup_lt_length. Qed.
Lemma lookup_lt_length_alt (l : list A) i x :
  l !! i = Some x → i < length l.
Proof. intros Hl. by rewrite <-lookup_lt_length, Hl. Qed.
Lemma lookup_lt_length_2 (l : list A) i :
  i < length l → is_Some (l !! i).
Proof. apply lookup_lt_length. Qed.

Lemma lookup_ge_length (l : list A) i :
  l !! i = None ↔ length l ≤ i.
Proof. rewrite eq_None_not_Some, lookup_lt_length. lia. Qed.
Lemma lookup_ge_length_1 (l : list A) i :
  l !! i = None → length l ≤ i.
Proof. by rewrite lookup_ge_length. Qed.
Lemma lookup_ge_length_2 (l : list A) i :
  length l ≤ i → l !! i = None.
Proof. by rewrite lookup_ge_length. Qed.

Lemma list_eq_length_eq (l1 l2 : list A) :
  length l2 = length l1 →
  (∀ i x y, l1 !! i = Some x → l2 !! i = Some y → x = y) →
  l1 = l2.
Proof.
  intros Hlength Hlookup. apply list_eq. intros i.
  destruct (l2 !! i) as [x|] eqn:E.
  * feed inversion (lookup_lt_length_2 l1 i) as [y].
    { pose proof (lookup_lt_length_alt l2 i x E). lia. }
    f_equal. eauto.
  * rewrite lookup_ge_length in E |- *. lia.
Qed.

Lemma lookup_app_l (l1 l2 : list A) i :
  i < length l1 →
  (l1 ++ l2) !! i = l1 !! i.
Proof. revert i. induction l1; intros [|?]; simpl; auto with lia. Qed.
Lemma lookup_app_l_Some (l1 l2 : list A) i x :
  l1 !! i = Some x →
  (l1 ++ l2) !! i = Some x.
Proof. intros. rewrite lookup_app_l; eauto using lookup_lt_length_alt. Qed.

Lemma lookup_app_r (l1 l2 : list A) i :
  (l1 ++ l2) !! (length l1 + i) = l2 !! i.
Proof.
  revert i.
  induction l1; intros [|i]; simpl in *; simplify_equality; auto.
Qed.
Lemma lookup_app_r_alt (l1 l2 : list A) i :
  length l1 ≤ i →
  (l1 ++ l2) !! i = l2 !! (i - length l1).
Proof.
  intros. assert (i = length l1 + (i - length l1)) as Hi by lia.
  rewrite Hi at 1. by apply lookup_app_r.
Qed.
Lemma lookup_app_r_Some (l1 l2 : list A) i x :
  l2 !! i = Some x →
  (l1 ++ l2) !! (length l1 + i) = Some x.
Proof. by rewrite lookup_app_r. Qed.
Lemma lookup_app_r_Some_alt (l1 l2 : list A) i x :
  length l1 ≤ i →
  l2 !! (i - length l1) = Some x →
  (l1 ++ l2) !! i = Some x.
Proof. intro. by rewrite lookup_app_r_alt. Qed.

Lemma lookup_app_inv (l1 l2 : list A) i x :
  (l1 ++ l2) !! i = Some x →
  l1 !! i = Some x ∨ l2 !! (i - length l1) = Some x.
Proof.
  revert i.
  induction l1; intros [|i] ?; simpl in *; simplify_equality; auto.
Qed.

Lemma list_lookup_middle (l1 l2 : list A) (x : A) :
  (l1 ++ x :: l2) !! length l1 = Some x.
Proof. by induction l1; simpl. Qed.

Lemma alter_length (f : A → A) l i :
  length (alter f i l) = length l.
Proof. revert i. induction l; intros [|?]; simpl; auto with lia. Qed.
Lemma insert_length (l : list A) i x :
  length (<[i:=x]>l) = length l.
Proof. apply alter_length. Qed.

Lemma list_lookup_alter (f : A → A) 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 : A → A) l i j :
  i ≠ j → alter f i l !! j = l !! j.
Proof.
  revert i j. induction l; [done|].
  intros [|i] [|j] ?; try done. apply (IHl i). congruence.
Qed.
Lemma list_lookup_insert (l : list A) i x :
  i < length l →
  <[i:=x]>l !! i = Some x.
Proof.
  intros Hi. unfold insert, list_insert.
  rewrite list_lookup_alter.
  by feed inversion (lookup_lt_length_2 l i).
Qed.
Lemma list_lookup_insert_ne (l : list A) i j x :
  i ≠ j → <[i:=x]>l !! j = l !! j.
Proof. apply list_lookup_alter_ne. Qed.

Lemma list_lookup_other (l : list A) i x :
  length l ≠ 1 →
  l !! i = Some x →
  ∃ j y, j ≠ i ∧ l !! j = Some y.
Proof.
  intros Hl Hi.
  destruct i; destruct l as [|x0 [|x1 l]]; simpl in *; simplify_equality.
  * by exists 1 x1.
  * by exists 0 x0.
Qed.

Lemma alter_app_l (f : A → A) (l1 l2 : list A) i :
  i < length l1 →
  alter f i (l1 ++ l2) = alter f i l1 ++ l2.
Proof.
  revert i.
  induction l1; intros [|?] ?; simpl in *; f_equal; auto with lia.
Qed.
Lemma alter_app_r (f : A → A) (l1 l2 : list A) i :
  alter f (length l1 + i) (l1 ++ l2) = l1 ++ alter f i l2.
Proof.
  revert i.
  induction l1; intros [|?]; simpl in *; f_equal; auto.
Qed.
Lemma alter_app_r_alt (f : A → A) (l1 l2 : list A) 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 insert_app_l (l1 l2 : list A) i x :
  i < length l1 →
  <[i:=x]>(l1 ++ l2) = <[i:=x]>l1 ++ l2.
Proof. apply alter_app_l. Qed.
Lemma insert_app_r (l1 l2 : list A) i x :
  <[length l1 + i:=x]>(l1 ++ l2) = l1 ++ <[i:=x]>l2.
Proof. apply alter_app_r. Qed.
Lemma insert_app_r_alt (l1 l2 : list A) i x :
  length l1 ≤ i →
  <[i:=x]>(l1 ++ l2) = l1 ++ <[i - length l1:=x]>l2.
Proof. apply alter_app_r_alt. Qed.

Lemma insert_consecutive_length (l : list A) i k :
  length (insert_consecutive i k l) = length l.
Proof. revert i. by induction k; intros; simpl; rewrite ?insert_length. Qed.

Lemma delete_middle (l1 l2 : list A) x :
  delete (length l1) (l1 ++ x :: l2) = l1 ++ l2.
Proof. induction l1; simpl; f_equal; auto. Qed.

(** ** Properties of the [elem_of] predicate *)
Lemma not_elem_of_nil (x : A) : x ∉ [].
Proof. by inversion 1. Qed.
Lemma elem_of_nil (x : A) : x ∈ [] ↔ False.
Proof. intuition. by destruct (not_elem_of_nil x). Qed.
Lemma elem_of_nil_inv (l : list A) : (∀ x, x ∉ l) → l = [].
Proof. destruct l. done. by edestruct 1; constructor. Qed.
Lemma elem_of_cons (l : list A) x y :
  x ∈ y :: l ↔ x = y ∨ x ∈ l.
Proof.
  split.
  * inversion 1; subst. by left. by right.
  * intros [?|?]; subst. by left. by right.
Qed.
Lemma not_elem_of_cons (l : list A) x y :
  x ∉ y :: l ↔ x ≠ y ∧ x ∉ l.
Proof. rewrite elem_of_cons. tauto. Qed.
Lemma elem_of_app (l1 l2 : list A) 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 : list A) x :
  x ∉ l1 ++ l2 ↔ x ∉ l1 ∧ x ∉ l2.
Proof. rewrite elem_of_app. tauto. Qed.

Lemma elem_of_list_singleton (x y : A) : x ∈ [y] ↔ x = y.
Proof. rewrite elem_of_cons, elem_of_nil. tauto. Qed.

Global Instance elem_of_list_permutation_proper (x : A) :
  Proper (Permutation ==> iff) (x ∈).
Proof. induction 1; rewrite ?elem_of_nil, ?elem_of_cons; intuition. Qed.

Lemma elem_of_list_split (l : list A) x :
  x ∈ l → ∃ l1 l2, l = l1 ++ x :: l2.
Proof.
  induction 1 as [x l|x y l ? [l1 [l2 ?]]].
  * by eexists [], l.
  * subst. by exists (y :: l1) l2.
Qed.

Global Instance elem_of_list_dec {dec : ∀ x y : A, Decision (x = y)} :
  ∀ (x : A) l, Decision (x ∈ l).
Proof.
 intros x. refine (
  fix go l :=
  match l return Decision (x ∈ l) with
  | [] => right (not_elem_of_nil _)
  | y :: l => cast_if_or (decide_rel (=) x y) (go l)
  end); clear go dec; subst; try (by constructor); by inversion 1.
Defined.

Lemma elem_of_list_lookup_1 (l : list A) x :
  x ∈ l → ∃ i, l !! i = Some x.
Proof.
  induction 1 as [|???? IH].
  * by exists 0.
  * destruct IH as [i ?]; auto. by exists (S i).
Qed.
Lemma elem_of_list_lookup_2 (l : list A) i x :
  l !! i = Some x → x ∈ l.
Proof.
  revert i. induction l; intros [|i] ?;
    simpl; simplify_equality; constructor; eauto.
Qed.
Lemma elem_of_list_lookup (l : list A) x :
  x ∈ l ↔ ∃ i, l !! i = Some x.
Proof.
  firstorder eauto using
    elem_of_list_lookup_1, elem_of_list_lookup_2.
Qed.

(** ** Properties of the [NoDup] predicate *)
Lemma NoDup_nil : NoDup (@nil A) ↔ True.
Proof. split; constructor. Qed.
Lemma NoDup_cons (x : A) l : NoDup (x :: l) ↔ x ∉ l ∧ NoDup l.
Proof. split. by inversion 1. intros [??]. by constructor. Qed.
Lemma NoDup_cons_11 (x : A) l : NoDup (x :: l) → x ∉ l.
Proof. rewrite NoDup_cons. by intros [??]. Qed.
Lemma NoDup_cons_12 (x : A) l : NoDup (x :: l) → NoDup l.
Proof. rewrite NoDup_cons. by intros [??]. Qed.
Lemma NoDup_singleton (x : A) : NoDup [x].
Proof. constructor. apply not_elem_of_nil. constructor. Qed.

Lemma NoDup_app (l k : list A) :
  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 (Permutation ==> 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_Permutation (l k : list A) :
  NoDup l → NoDup k → (∀ x, x ∈ l ↔ x ∈ k) → Permutation l k.
Proof.
  intros Hl. revert k. induction Hl as [|x l Hin ? IH].
  * intros k _ Hk.
    rewrite (elem_of_nil_inv k); [done |].
    intros x. rewrite <-Hk, elem_of_nil. intros [].
  * intros k Hk Hlk.
    destruct (elem_of_list_split k x) as [l1 [l2 ?]]; subst.
    { rewrite <-Hlk. by constructor. }
    rewrite <-Permutation_middle, NoDup_cons in Hk.
    destruct Hk as [??].
    apply Permutation_cons_app, IH; [done |].
    intros y. specialize (Hlk y).
    rewrite <-Permutation_middle, !elem_of_cons in Hlk.
    naive_solver.
Qed.

Global Instance NoDup_dec {dec : ∀ x y : A, Decision (x = y)} :
    ∀ (l : list A), 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 Hin => right (λ H, NoDup_cons_11 _ _ H Hin)
    | right Hin =>
      match NoDup_dec l with
      | left H => left (NoDup_cons_2 _ _ Hin H)
      | right H => right (H ∘ NoDup_cons_12 _ _)
      end
    end
  end.

Section remove_dups.
  Context `{!∀ x y : A, Decision (x = y)}.

  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.

  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_equality; auto).
  Qed.

  Lemma remove_dups_nodup l : NoDup (remove_dups l).
  Proof.
    induction l; simpl; repeat case_decide; try constructor; auto.
    by rewrite elem_of_remove_dups.
  Qed.
End remove_dups.

(** ** Properties of the [filter] function *)
Lemma elem_of_list_filter `{∀ x : A, Decision (P x)} l x :
  x ∈ filter P l ↔ P x ∧ x ∈ l.
Proof.
  unfold filter. induction l; simpl; repeat case_decide;
     rewrite ?elem_of_nil, ?elem_of_cons; naive_solver.
Qed.
Lemma filter_nodup P `{∀ x : A, Decision (P x)} l :
  NoDup l → NoDup (filter P l).
Proof.
  unfold filter. induction 1; simpl; repeat case_decide;
    rewrite ?NoDup_nil, ?NoDup_cons, ?elem_of_list_filter; tauto.
Qed.

(** ** Properties of the [reverse] function *)
Lemma reverse_nil : reverse [] = @nil A.
Proof. done. Qed.
Lemma reverse_singleton (x : A) : reverse [x] = [x].
Proof. done. Qed.
Lemma reverse_cons (l : list A) x : reverse (x :: l) = reverse l ++ [x].
Proof. unfold reverse. by rewrite <-!rev_alt. Qed.
Lemma reverse_snoc (l : list A) x : reverse (l ++ [x]) = x :: reverse l.
Proof. unfold reverse. by rewrite <-!rev_alt, rev_unit. Qed.
Lemma reverse_app (l1 l2 : list A) :
  reverse (l1 ++ l2) = reverse l2 ++ reverse l1.
Proof. unfold reverse. rewrite <-!rev_alt. apply rev_app_distr. Qed.
Lemma reverse_length (l : list A) : length (reverse l) = length l.
Proof. unfold reverse. rewrite <-!rev_alt. apply rev_length. Qed.
Lemma reverse_involutive (l : list A) : reverse (reverse l) = l.
Proof. unfold reverse. rewrite <-!rev_alt. apply rev_involutive. Qed.

(** ** Properties of the [take] function *)
Lemma take_nil n :
  take n (@nil A) = [].
Proof. by destruct n. Qed.
Lemma take_app (l k : list A) :
  take (length l) (l ++ k) = l.
Proof. induction l; simpl; f_equal; auto. Qed.
Lemma take_app_alt (l k : list A) n :
  n = length l →
  take n (l ++ k) = l.
Proof. intros Hn. by rewrite Hn, take_app. Qed.
Lemma take_app_le (l k : list A) n :
  n ≤ length l →
  take n (l ++ k) = take n l.
Proof.
  revert n;
  induction l; intros [|?] ?; simpl in *; f_equal; auto with lia.
Qed.
Lemma take_app_ge (l k : list A) n :
  length l ≤ n →
  take n (l ++ k) = l ++ take (n - length l) k.
Proof.
  revert n;
  induction l; intros [|?] ?; simpl in *; f_equal; auto with lia.
Qed.
Lemma take_ge (l : list A) n :
  length l ≤ n →
  take n l = l.
Proof.
  revert n.
  induction l; intros [|?] ?; simpl in *; f_equal; auto with lia.
Qed.

Lemma take_take (l : list A) n m :
  take n (take m l) = take (min n m) l.
Proof. revert n m. induction l; intros [|?] [|?]; simpl; f_equal; auto. Qed.
Lemma take_idempotent (l : list A) n :
  take n (take n l) = take n l.
Proof. by rewrite take_take, Min.min_idempotent. Qed.

Lemma take_length (l : list A) n :
  length (take n l) = min n (length l).
Proof. revert n. induction l; intros [|?]; simpl; f_equal; done. Qed.
Lemma take_length_alt (l : list A) n :
  n ≤ length l →
  length (take n l) = n.
Proof. rewrite take_length. apply Min.min_l. Qed.

Lemma lookup_take (l : list A) n i :
  i < n → take n l !! i = l !! i.
Proof.
  revert n i. induction l; intros [|n] i ?; trivial.
  * auto with lia.
  * destruct i; simpl; auto with arith.
Qed.
Lemma lookup_take_ge (l : list A) 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 : A → A) 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 : list A) n i x :
  n ≤ i → take n (<[i:=x]>l) = take n l.
Proof take_alter _ _ _ _.

(** ** Properties of the [drop] function *)
Lemma drop_nil n :
  drop n (@nil A) = [].
Proof. by destruct n. Qed.
Lemma drop_app (l k : list A) :
  drop (length l) (l ++ k) = k.
Proof. induction l; simpl; f_equal; auto. Qed.
Lemma drop_app_alt (l k : list A) n :
  n = length l →
  drop n (l ++ k) = k.
Proof. intros Hn. by rewrite Hn, drop_app. Qed.
Lemma drop_length (l : list A) n :
  length (drop n l) = length l - n.
Proof.
  revert n. by induction l; intros [|i]; simpl; f_equal.
Qed.
Lemma drop_all (l : list A) :
  drop (length l) l = [].
Proof. induction l; simpl; auto. Qed.
Lemma drop_all_alt (l : list A) n :
  n = length l →
  drop n l = [].
Proof. intros. subst. by rewrite drop_all. Qed.

Lemma lookup_drop (l : list A) n i :
  drop n l !! i = l !! (n + i).
Proof. revert n i. induction l; intros [|i] ?; simpl; auto. Qed.
Lemma drop_alter (f : A → A) 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 : list A) n i x :
  i < n → drop n (<[i:=x]>l) = drop n l.
Proof drop_alter _ _ _ _.

Lemma delete_take_drop (l : list A) i :
  delete i l = take i l ++ drop (S i) l.
Proof. revert i. induction l; intros [|?]; simpl; auto using f_equal. Qed.

(** ** Properties of the [replicate] function *)
Lemma replicate_length n (x : A) : length (replicate n x) = n.
Proof. induction n; simpl; auto. Qed.
Lemma lookup_replicate n (x : A) i :
  i < n →
  replicate n x !! i = Some x.
Proof.
  revert i.
  induction n; intros [|?]; naive_solver auto with lia.
Qed.
Lemma lookup_replicate_inv n (x y : A) i :
  replicate n x !! i = Some y → y = x ∧ i < n.
Proof.
  revert i.
  induction n; intros [|?]; naive_solver auto with lia.
Qed.
Lemma replicate_S n (x : A) :
  replicate (S n) x = x :: replicate  n x.
Proof. done. Qed.
Lemma replicate_plus n m (x : A) :
  replicate (n + m) x = replicate n x ++ replicate m x.
Proof. induction n; simpl; f_equal; auto. Qed.

Lemma take_replicate n m (x : A) :
  take n (replicate m x) = replicate (min n m) x.
Proof. revert m. by induction n; intros [|?]; simpl; f_equal. Qed.
Lemma take_replicate_plus n m (x : A) :
  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 : A) :
  drop n (replicate m x) = replicate (m - n) x.
Proof. revert m. by induction n; intros [|?]; simpl; f_equal. Qed.
Lemma drop_replicate_plus n m (x : A) :
  drop n (replicate (n + m) x) = replicate m x.
Proof. rewrite drop_replicate. f_equal. lia. Qed.

Lemma reverse_replicate n (x : A) :
  reverse (replicate n x) = replicate n x.
Proof.
  induction n as [|n IH]; [done|].
  simpl. rewrite reverse_cons, IH. change [x] with (replicate 1 x).
  by rewrite <-replicate_plus, plus_comm.
Qed.

(** ** Properties of the [resize] function *)
Lemma resize_spec (l : list A) n x :
  resize n x l = take n l ++ replicate (n - length l) x.
Proof.
  revert n.
  induction l; intros [|?]; simpl; f_equal; auto.
Qed.
Lemma resize_0 (l : list A) x :
  resize 0 x l = [].
Proof. by destruct l. Qed.
Lemma resize_nil n (x : A) :
  resize n x [] = replicate n x.
Proof. rewrite resize_spec. rewrite take_nil. simpl. f_equal. lia. Qed.
Lemma resize_ge (l : list A) 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 : list A) n x :
  n ≤ length l →
  resize n x l = take n l.
Proof.
  intros. rewrite resize_spec, (proj2 (NPeano.Nat.sub_0_le _ _)) by done.
  simpl. by rewrite (right_id [] (++)).
Qed.

Lemma resize_all (l : list A) x :
  resize (length l) x l = l.
Proof. intros. by rewrite resize_le, take_ge. Qed.
Lemma resize_all_alt (l : list A) n x :
  n = length l →
  resize n x l = l.
Proof. intros. subst. by rewrite resize_all. Qed.

Lemma resize_plus (l : list A) 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 [|?] [|?]; simpl; f_equal; auto.
  * by rewrite plus_0_r, (right_id [] (++)).
  * by rewrite replicate_plus.
Qed.
Lemma resize_plus_eq (l : list A) n m x :
  length l = n →
  resize (n + m) x l = l ++ replicate m x.
Proof.
  intros. subst.
  by rewrite resize_plus, resize_all, drop_all, resize_nil.
Qed.

Lemma resize_app_le (l1 l2 : list A) 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_ge (l1 l2 : list A) 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, (associative (++)) by done.
  do 2 f_equal. rewrite app_length. lia.
Qed.

Lemma resize_length (l : list A) n x : length (resize n x l) = n.
Proof.
  rewrite resize_spec, app_length, replicate_length, take_length. lia.
Qed.
Lemma resize_replicate (x : A) n m :
  resize n x (replicate m x) = replicate n x.
Proof. revert m. induction n; intros [|?]; simpl; f_equal; auto. Qed.

Lemma resize_resize (l : list A) 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 [|?] [|?] ?; simpl; f_equal; auto with lia.
Qed.
Lemma resize_idempotent (l : list A) n x :
  resize n x (resize n x l) = resize n x l.
Proof. by rewrite resize_resize. Qed.

Lemma resize_take_le (l : list A) n m x :
  n ≤ m →
  resize n x (take m l) = resize n x l.
Proof.
  revert n m.
  induction l; intros [|?] [|?] ?; simpl; f_equal; auto with lia.
Qed.
Lemma resize_take_eq (l : list A) n x :
  resize n x (take n l) = resize n x l.
Proof. by rewrite resize_take_le. Qed.

Lemma take_resize (l : list A) n m x :
  take n (resize m x l) = resize (min n m) x l.
Proof.
  revert n m.
  induction l; intros [|?] [|?]; simpl; f_equal; auto using take_replicate.
Qed.
Lemma take_resize_le (l : list A) 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 : list A) n x :
  take n (resize n x l) = resize n x l.
Proof. intros. by rewrite take_resize, Min.min_l. Qed.
Lemma take_length_resize (l : list A) n x :
  length l ≤ n →
  take (length l) (resize n x l) = l.
Proof. intros. by rewrite take_resize_le, resize_all. Qed.
Lemma take_length_resize_alt (l : list A) n m x :
  m = length l →
  m ≤ n →
  take m (resize n x l) = l.
Proof. intros. subst. by apply take_length_resize. Qed.
Lemma take_resize_plus (l : list A) 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 : list A) 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 : list A) 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.

(** ** Properties of the [sublist] predicate *)
Lemma sublist_nil_l (l : list A) :
  sublist [] l.
Proof. induction l; try constructor; auto. Qed.
Lemma sublist_nil_r (l : list A) :
  sublist l [] ↔ l = [].
Proof. split. by inversion 1. intros. subst. constructor. Qed.

Lemma sublist_app_skip_l (k : list A) l1 l2 :
  sublist l1 l2 →
  sublist l1 (k ++ l2).
Proof. induction k; try constructor; auto. Qed.
Lemma sublist_app_skip_r (k : list A) l1 l2 :