# Library Coq.Lists.List

Require Setoid.
Require Import PeanoNat Le Gt Minus Bool Lt.

Set Implicit Arguments.

# Basics: definition of polymorphic lists and some operations

The definition of list is now in Init/Datatypes, as well as the definitions of length and app

Open Scope list_scope.

Standard notations for lists. In a special module to avoid conflicts.
Module ListNotations.
Notation "[ ]" := nil (format "[ ]") : list_scope.
Notation "[ x ]" := (cons x nil) : list_scope.
Notation "[ x ; y ; .. ; z ]" := (cons x (cons y .. (cons z nil) ..)) : list_scope.
End ListNotations.

Import ListNotations.

Section Lists.

Variable A : Type.

Definition hd (default:A) (l:list A) :=
match l with
| [] => default
| x :: _ => x
end.

Definition hd_error (l:list A) :=
match l with
| [] => None
| x :: _ => Some x
end.

Definition tl (l:list A) :=
match l with
| [] => nil
| a :: m => m
end.

The In predicate
Fixpoint In (a:A) (l:list A) : Prop :=
match l with
| [] => False
| b :: m => b = a \/ In a m
end.

End Lists.

Section Facts.

Variable A : Type.

### Generic facts

Discrimination
Theorem nil_cons : forall (x:A) (l:list A), [] <> x :: l.

Destruction

Theorem destruct_list : forall l : list A, {x:A & {tl:list A | l = x::tl}}+{l = []}.

Lemma hd_error_tl_repr : forall l (a:A) r,
hd_error l = Some a /\ tl l = r <-> l = a :: r.

Lemma hd_error_some_nil : forall l (a:A), hd_error l = Some a -> l <> nil.

Theorem length_zero_iff_nil (l : list A):
length l = 0 <-> l=[].

Theorem hd_error_nil : hd_error (@nil A) = None.

Theorem hd_error_cons : forall (l : list A) (x : A), hd_error (x::l) = Some x.

Characterization of In

Theorem in_eq : forall (a:A) (l:list A), In a (a :: l).

Theorem in_cons : forall (a b:A) (l:list A), In b l -> In b (a :: l).

Theorem not_in_cons (x a : A) (l : list A):
~ In x (a::l) <-> x<>a /\ ~ In x l.

Theorem in_nil : forall a:A, ~ In a [].

Theorem in_split : forall x (l:list A), In x l -> exists l1 l2, l = l1++x::l2.

Inversion
Lemma in_inv : forall (a b:A) (l:list A), In b (a :: l) -> a = b \/ In b l.

Decidability of In
Theorem in_dec :
(forall x y:A, {x = y} + {x <> y}) ->
forall (a:A) (l:list A), {In a l} + {~ In a l}.

Discrimination
Theorem app_cons_not_nil : forall (x y:list A) (a:A), [] <> x ++ a :: y.

Concat with nil
Theorem app_nil_l : forall l:list A, [] ++ l = l.

Theorem app_nil_r : forall l:list A, l ++ [] = l.

app is associative
Theorem app_assoc : forall l m n:list A, l ++ m ++ n = (l ++ m) ++ n.

app commutes with cons
Theorem app_comm_cons : forall (x y:list A) (a:A), a :: (x ++ y) = (a :: x) ++ y.

Facts deduced from the result of a concatenation

Theorem app_eq_nil : forall l l':list A, l ++ l' = [] -> l = [] /\ l' = [].

Theorem app_eq_unit :
forall (x y:list A) (a:A),
x ++ y = [a] -> x = [] /\ y = [a] \/ x = [a] /\ y = [].

Lemma app_inj_tail :
forall (x y:list A) (a b:A), x ++ [a] = y ++ [b] -> x = y /\ a = b.

Compatibility with other operations

Lemma app_length : forall l l' : list A, length (l++l') = length l + length l'.

Lemma in_app_or : forall (l m:list A) (a:A), In a (l ++ m) -> In a l \/ In a m.

Lemma in_or_app : forall (l m:list A) (a:A), In a l \/ In a m -> In a (l ++ m).

Lemma in_app_iff : forall l l' (a:A), In a (l++l') <-> In a l \/ In a l'.

forall l l1 l2 : list A, l ++ l1 = l ++ l2 -> l1 = l2.

Lemma app_inv_tail:
forall l l1 l2 : list A, l1 ++ l = l2 ++ l -> l1 = l2.

End Facts.

Hint Resolve app_assoc app_assoc_reverse: datatypes.
Hint Resolve app_comm_cons app_cons_not_nil: datatypes.
Hint Immediate app_eq_nil: datatypes.
Hint Resolve app_eq_unit app_inj_tail: datatypes.
Hint Resolve in_eq in_cons in_inv in_nil in_app_or in_or_app: datatypes.

# Operations on the elements of a list

Section Elts.

Variable A : Type.

## Nth element of a list

Fixpoint nth (n:nat) (l:list A) (default:A) {struct l} : A :=
match n, l with
| O, x :: l' => x
| O, other => default
| S m, [] => default
| S m, x :: t => nth m t default
end.

Fixpoint nth_ok (n:nat) (l:list A) (default:A) {struct l} : bool :=
match n, l with
| O, x :: l' => true
| O, other => false
| S m, [] => false
| S m, x :: t => nth_ok m t default
end.

Lemma nth_in_or_default :
forall (n:nat) (l:list A) (d:A), {In (nth n l d) l} + {nth n l d = d}.

Lemma nth_S_cons :
forall (n:nat) (l:list A) (d a:A),
In (nth n l d) l -> In (nth (S n) (a :: l) d) (a :: l).

Fixpoint nth_error (l:list A) (n:nat) {struct n} : option A :=
match n, l with
| O, x :: _ => Some x
| S n, _ :: l => nth_error l n
| _, _ => None
end.

Definition nth_default (default:A) (l:list A) (n:nat) : A :=
match nth_error l n with
| Some x => x
| None => default
end.

Lemma nth_default_eq :
forall n l (d:A), nth_default d l n = nth n l d.

Lemma nth_In :
forall (n:nat) (l:list A) (d:A), n < length l -> In (nth n l d) l.

Lemma In_nth l x d : In x l ->
exists n, n < length l /\ nth n l d = x.

Lemma nth_overflow : forall l n d, length l <= n -> nth n l d = d.

Lemma nth_indep :
forall l n d d', n < length l -> nth n l d = nth n l d'.

Lemma app_nth1 :
forall l l' d n, n < length l -> nth n (l++l') d = nth n l d.

Lemma app_nth2 :
forall l l' d n, n >= length l -> nth n (l++l') d = nth (n-length l) l' d.

Lemma nth_split n l d : n < length l ->
exists l1, exists l2, l = l1 ++ nth n l d :: l2 /\ length l1 = n.

## Remove

Hypothesis eq_dec : forall x y : A, {x = y}+{x <> y}.

Fixpoint remove (x : A) (l : list A) : list A :=
match l with
| [] => []
| y::tl => if (eq_dec x y) then remove x tl else y::(remove x tl)
end.

Theorem remove_In : forall (l : list A) (x : A), ~ In x (remove x l).

## Last element of a list

last l d returns the last element of the list l, or the default value d if l is empty.

Fixpoint last (l:list A) (d:A) : A :=
match l with
| [] => d
| [a] => a
| a :: l => last l d
end.

removelast l remove the last element of l

Fixpoint removelast (l:list A) : list A :=
match l with
| [] => []
| [a] => []
| a :: l => a :: removelast l
end.

Lemma app_removelast_last :
forall l d, l <> [] -> l = removelast l ++ [last l d].

Lemma exists_last :
forall l, l <> [] -> { l' : (list A) & { a : A | l = l' ++ [a]}}.

Lemma removelast_app :
forall l l', l' <> [] -> removelast (l++l') = l ++ removelast l'.

## Counting occurrences of an element

Fixpoint count_occ (l : list A) (x : A) : nat :=
match l with
| [] => 0
| y :: tl =>
let n := count_occ tl x in
if eq_dec y x then S n else n
end.

Compatibility of count_occ with operations on list
Theorem count_occ_In l x : In x l <-> count_occ l x > 0.

Theorem count_occ_not_In l x : ~ In x l <-> count_occ l x = 0.

Lemma count_occ_nil x : count_occ [] x = 0.

Theorem count_occ_inv_nil l :
(forall x:A, count_occ l x = 0) <-> l = [].

Lemma count_occ_cons_eq l x y :
x = y -> count_occ (x::l) y = S (count_occ l y).

Lemma count_occ_cons_neq l x y :
x <> y -> count_occ (x::l) y = count_occ l y.

End Elts.

# Manipulating whole lists

Section ListOps.

Variable A : Type.

## Reverse

Fixpoint rev (l:list A) : list A :=
match l with
| [] => []
| x :: l' => rev l' ++ [x]
end.

Lemma rev_app_distr : forall x y:list A, rev (x ++ y) = rev y ++ rev x.

Remark rev_unit : forall (l:list A) (a:A), rev (l ++ [a]) = a :: rev l.

Lemma rev_involutive : forall l:list A, rev (rev l) = l.

Compatibility with other operations

Lemma in_rev : forall l x, In x l <-> In x (rev l).

Lemma rev_length : forall l, length (rev l) = length l.

Lemma rev_nth : forall l d n, n < length l ->
nth n (rev l) d = nth (length l - S n) l d.

An alternative tail-recursive definition for reverse

Fixpoint rev_append (l l': list A) : list A :=
match l with
| [] => l'
| a::l => rev_append l (a::l')
end.

Definition rev' l : list A := rev_append l [].

Lemma rev_append_rev : forall l l', rev_append l l' = rev l ++ l'.

Lemma rev_alt : forall l, rev l = rev_append l [].

Reverse Induction Principle on Lists

Section Reverse_Induction.

Lemma rev_list_ind :
forall P:list A-> Prop,
P [] ->
(forall (a:A) (l:list A), P (rev l) -> P (rev (a :: l))) ->
forall l:list A, P (rev l).

Theorem rev_ind :
forall P:list A -> Prop,
P [] ->
(forall (x:A) (l:list A), P l -> P (l ++ [x])) -> forall l:list A, P l.

End Reverse_Induction.

## Concatenation

Fixpoint concat (l : list (list A)) : list A :=
match l with
| nil => nil
| cons x l => x ++ concat l
end.

Lemma concat_nil : concat nil = nil.

Lemma concat_cons : forall x l, concat (cons x l) = x ++ concat l.

Lemma concat_app : forall l1 l2, concat (l1 ++ l2) = concat l1 ++ concat l2.

## Decidable equality on lists

Hypothesis eq_dec : forall (x y : A), {x = y}+{x <> y}.

Lemma list_eq_dec : forall l l':list A, {l = l'} + {l <> l'}.

End ListOps.

# Applying functions to the elements of a list

## Map

Section Map.
Variables (A : Type) (B : Type).
Variable f : A -> B.

Fixpoint map (l:list A) : list B :=
match l with
| [] => []
| a :: t => (f a) :: (map t)
end.

Lemma map_cons (x:A)(l:list A) : map (x::l) = (f x) :: (map l).

Lemma in_map :
forall (l:list A) (x:A), In x l -> In (f x) (map l).

Lemma in_map_iff : forall l y, In y (map l) <-> exists x, f x = y /\ In x l.

Lemma map_length : forall l, length (map l) = length l.

Lemma map_nth : forall l d n,
nth n (map l) (f d) = f (nth n l d).

Lemma map_nth_error : forall n l d,
nth_error l n = Some d -> nth_error (map l) n = Some (f d).

Lemma map_app : forall l l',
map (l++l') = (map l)++(map l').

Lemma map_rev : forall l, map (rev l) = rev (map l).

Lemma map_eq_nil : forall l, map l = [] -> l = [].

map and count of occurrences

Hypothesis decA: forall x1 x2 : A, {x1 = x2} + {x1 <> x2}.
Hypothesis decB: forall y1 y2 : B, {y1 = y2} + {y1 <> y2}.
Hypothesis Hfinjective: forall x1 x2: A, (f x1) = (f x2) -> x1 = x2.

Theorem count_occ_map x l:
count_occ decA l x = count_occ decB (map l) (f x).

flat_map

Definition flat_map (f:A -> list B) :=
fix flat_map (l:list A) : list B :=
match l with
| nil => nil
| cons x t => (f x)++(flat_map t)
end.

Lemma in_flat_map : forall (f:A->list B)(l:list A)(y:B),
In y (flat_map f l) <-> exists x, In x l /\ In y (f x).

End Map.

Lemma flat_map_concat_map : forall A B (f : A -> list B) l,
flat_map f l = concat (map f l).

Lemma concat_map : forall A B (f : A -> B) l, map f (concat l) = concat (map (map f) l).

Lemma map_id : forall (A :Type) (l : list A),
map (fun x => x) l = l.

Lemma map_map : forall (A B C:Type)(f:A->B)(g:B->C) l,
map g (map f l) = map (fun x => g (f x)) l.

Lemma map_ext_in :
forall (A B : Type)(f g:A->B) l, (forall a, In a l -> f a = g a) -> map f l = map g l.

Lemma map_ext :
forall (A B : Type)(f g:A->B), (forall a, f a = g a) -> forall l, map f l = map g l.

Left-to-right iterator on lists

Section Fold_Left_Recursor.
Variables (A : Type) (B : Type).
Variable f : A -> B -> A.

Fixpoint fold_left (l:list B) (a0:A) : A :=
match l with
| nil => a0
| cons b t => fold_left t (f a0 b)
end.

Lemma fold_left_app : forall (l l':list B)(i:A),
fold_left (l++l') i = fold_left l' (fold_left l i).

End Fold_Left_Recursor.

Lemma fold_left_length :
forall (A:Type)(l:list A), fold_left (fun x _ => S x) l 0 = length l.

Right-to-left iterator on lists

Section Fold_Right_Recursor.
Variables (A : Type) (B : Type).
Variable f : B -> A -> A.
Variable a0 : A.

Fixpoint fold_right (l:list B) : A :=
match l with
| nil => a0
| cons b t => f b (fold_right t)
end.

End Fold_Right_Recursor.

Lemma fold_right_app : forall (A B:Type)(f:A->B->B) l l' i,
fold_right f i (l++l') = fold_right f (fold_right f i l') l.

Lemma fold_left_rev_right : forall (A B:Type)(f:A->B->B) l i,
fold_right f i (rev l) = fold_left (fun x y => f y x) l i.

Theorem fold_symmetric :
forall (A : Type) (f : A -> A -> A),
(forall x y z : A, f x (f y z) = f (f x y) z) ->
forall (a0 : A), (forall y : A, f a0 y = f y a0) ->
forall (l : list A), fold_left f l a0 = fold_right f a0 l.

(list_power x y) is y^x, or the set of sequences of elts of y indexed by elts of x, sorted in lexicographic order.

Fixpoint list_power (A B:Type)(l:list A) (l':list B) :
list (list (A * B)) :=
match l with
| nil => cons nil nil
| cons x t =>
flat_map (fun f:list (A * B) => map (fun y:B => cons (x, y) f) l')
(list_power t l')
end.

## Boolean operations over lists

Section Bool.
Variable A : Type.
Variable f : A -> bool.

find whether a boolean function can be satisfied by an elements of the list.

Fixpoint existsb (l:list A) : bool :=
match l with
| nil => false
| a::l => f a || existsb l
end.

Lemma existsb_exists :
forall l, existsb l = true <-> exists x, In x l /\ f x = true.

Lemma existsb_nth : forall l n d, n < length l ->
existsb l = false -> f (nth n l d) = false.

Lemma existsb_app : forall l1 l2,
existsb (l1++l2) = existsb l1 || existsb l2.

find whether a boolean function is satisfied by all the elements of a list.

Fixpoint forallb (l:list A) : bool :=
match l with
| nil => true
| a::l => f a && forallb l
end.

Lemma forallb_forall :
forall l, forallb l = true <-> (forall x, In x l -> f x = true).

Lemma forallb_app :
forall l1 l2, forallb (l1++l2) = forallb l1 && forallb l2.
filter

Fixpoint filter (l:list A) : list A :=
match l with
| nil => nil
| x :: l => if f x then x::(filter l) else filter l
end.

Lemma filter_In : forall x l, In x (filter l) <-> In x l /\ f x = true.

find

Fixpoint find (l:list A) : option A :=
match l with
| nil => None
| x :: tl => if f x then Some x else find tl
end.

Lemma find_some l x : find l = Some x -> In x l /\ f x = true.

Lemma find_none l : find l = None -> forall x, In x l -> f x = false.

partition

Fixpoint partition (l:list A) : list A * list A :=
match l with
| nil => (nil, nil)
| x :: tl => let (g,d) := partition tl in
if f x then (x::g,d) else (g,x::d)
end.

Theorem partition_cons1 a l l1 l2:
partition l = (l1, l2) ->
f a = true ->
partition (a::l) = (a::l1, l2).

Theorem partition_cons2 a l l1 l2:
partition l = (l1, l2) ->
f a=false ->
partition (a::l) = (l1, a::l2).

Theorem partition_length l l1 l2:
partition l = (l1, l2) ->
length l = length l1 + length l2.

Theorem partition_inv_nil (l : list A):
partition l = ([], []) <-> l = [].

Theorem elements_in_partition l l1 l2:
partition l = (l1, l2) ->
forall x:A, In x l <-> In x l1 \/ In x l2.

End Bool.

## Operations on lists of pairs or lists of lists

Section ListPairs.
Variables (A : Type) (B : Type).

split derives two lists from a list of pairs

Fixpoint split (l:list (A*B)) : list A * list B :=
match l with
| [] => ([], [])
| (x,y) :: tl => let (left,right) := split tl in (x::left, y::right)
end.

Lemma in_split_l : forall (l:list (A*B))(p:A*B),
In p l -> In (fst p) (fst (split l)).

Lemma in_split_r : forall (l:list (A*B))(p:A*B),
In p l -> In (snd p) (snd (split l)).

Lemma split_nth : forall (l:list (A*B))(n:nat)(d:A*B),
nth n l d = (nth n (fst (split l)) (fst d), nth n (snd (split l)) (snd d)).

Lemma split_length_l : forall (l:list (A*B)),
length (fst (split l)) = length l.

Lemma split_length_r : forall (l:list (A*B)),
length (snd (split l)) = length l.

combine is the opposite of split. Lists given to combine are meant to be of same length. If not, combine stops on the shorter list

Fixpoint combine (l : list A) (l' : list B) : list (A*B) :=
match l,l' with
| x::tl, y::tl' => (x,y)::(combine tl tl')
| _, _ => nil
end.

Lemma split_combine : forall (l: list (A*B)),
let (l1,l2) := split l in combine l1 l2 = l.

Lemma combine_split : forall (l:list A)(l':list B), length l = length l' ->
split (combine l l') = (l,l').

Lemma in_combine_l : forall (l:list A)(l':list B)(x:A)(y:B),
In (x,y) (combine l l') -> In x l.

Lemma in_combine_r : forall (l:list A)(l':list B)(x:A)(y:B),
In (x,y) (combine l l') -> In y l'.

Lemma combine_length : forall (l:list A)(l':list B),
length (combine l l') = min (length l) (length l').

Lemma combine_nth : forall (l:list A)(l':list B)(n:nat)(x:A)(y:B),
length l = length l' ->
nth n (combine l l') (x,y) = (nth n l x, nth n l' y).

list_prod has the same signature as combine, but unlike combine, it adds every possible pairs, not only those at the same position.

Fixpoint list_prod (l:list A) (l':list B) :
list (A * B) :=
match l with
| nil => nil
| cons x t => (map (fun y:B => (x, y)) l')++(list_prod t l')
end.

Lemma in_prod_aux :
forall (x:A) (y:B) (l:list B),
In y l -> In (x, y) (map (fun y0:B => (x, y0)) l).

Lemma in_prod :
forall (l:list A) (l':list B) (x:A) (y:B),
In x l -> In y l' -> In (x, y) (list_prod l l').

Lemma in_prod_iff :
forall (l:list A)(l':list B)(x:A)(y:B),
In (x,y) (list_prod l l') <-> In x l /\ In y l'.

Lemma prod_length : forall (l:list A)(l':list B),
length (list_prod l l') = (length l) * (length l').

End ListPairs.

# Miscellaneous operations on lists

## Length order of lists

Section length_order.
Variable A : Type.

Definition lel (l m:list A) := length l <= length m.

Variables a b : A.
Variables l m n : list A.

Lemma lel_refl : lel l l.

Lemma lel_trans : lel l m -> lel m n -> lel l n.

Lemma lel_cons_cons : lel l m -> lel (a :: l) (b :: m).

Lemma lel_cons : lel l m -> lel l (b :: m).

Lemma lel_tail : lel (a :: l) (b :: m) -> lel l m.

Lemma lel_nil : forall l':list A, lel l' nil -> nil = l'.
End length_order.

Hint Resolve lel_refl lel_cons_cons lel_cons lel_nil lel_nil nil_cons:
datatypes.

## Set inclusion on list

Section SetIncl.

Variable A : Type.

Definition incl (l m:list A) := forall a:A, In a l -> In a m.
Hint Unfold incl.

Lemma incl_refl : forall l:list A, incl l l.
Hint Resolve incl_refl.

Lemma incl_tl : forall (a:A) (l m:list A), incl l m -> incl l (a :: m).
Hint Immediate incl_tl.

Lemma incl_tran : forall l m n:list A, incl l m -> incl m n -> incl l n.

Lemma incl_appl : forall l m n:list A, incl l n -> incl l (n ++ m).
Hint Immediate incl_appl.

Lemma incl_appr : forall l m n:list A, incl l n -> incl l (m ++ n).
Hint Immediate incl_appr.

Lemma incl_cons :
forall (a:A) (l m:list A), In a m -> incl l m -> incl (a :: l) m.
Hint Resolve incl_cons.

Lemma incl_app : forall l m n:list A, incl l n -> incl m n -> incl (l ++ m) n.
Hint Resolve incl_app.

End SetIncl.

Hint Resolve incl_refl incl_tl incl_tran incl_appl incl_appr incl_cons
incl_app: datatypes.

# Cutting a list at some position

Section Cutting.

Variable A : Type.

Fixpoint firstn (n:nat)(l:list A) : list A :=
match n with
| 0 => nil
| S n => match l with
| nil => nil
| a::l => a::(firstn n l)
end
end.

Lemma firstn_nil n: firstn n [] = [].

Lemma firstn_cons n a l: firstn (S n) (a::l) = a :: (firstn n l).

Lemma firstn_all l: firstn (length l) l = l.

Lemma firstn_all2 n: forall (l:list A), (length l) <= n -> firstn n l = l.

Lemma firstn_O l: firstn 0 l = [].

Lemma firstn_le_length n: forall l:list A, length (firstn n l) <= n.

Lemma firstn_length_le: forall l:list A, forall n:nat,
n <= length l -> length (firstn n l) = n.

Lemma firstn_app n:
forall l1 l2,
firstn n (l1 ++ l2) = (firstn n l1) ++ (firstn (n - length l1) l2).

Lemma firstn_app_2 n:
forall l1 l2,
firstn ((length l1) + n) (l1 ++ l2) = l1 ++ firstn n l2.

Lemma firstn_firstn:
forall l:list A,
forall i j : nat,
firstn i (firstn j l) = firstn (min i j) l.

Fixpoint skipn (n:nat)(l:list A) : list A :=
match n with
| 0 => l
| S n => match l with
| nil => nil
| a::l => skipn n l
end
end.

Lemma firstn_skipn : forall n l, firstn n l ++ skipn n l = l.

Lemma firstn_length : forall n l, length (firstn n l) = min n (length l).

Lemma removelast_firstn : forall n l, n < length l ->
removelast (firstn (S n) l) = firstn n l.

Lemma firstn_removelast : forall n l, n < length l ->
firstn n (removelast l) = firstn n l.

End Cutting.

## Predicate for List addition/removal (no need for decidability)

Variable A : Type.

Inductive Add (a:A) : list A -> list A -> Prop :=

Lemma Add_split a l l' :
Add a l l' -> exists l1 l2, l = l1++l2 /\ l' = l1++a::l2.

forall x, In x l' <-> In x (a::l).

Lemma Add_length a l l' : Add a l l' -> length l' = S (length l).

Lemma Add_inv a l : In a l -> exists l', Add a l' l.

Lemma incl_Add_inv a l u v :
~In a l -> incl (a::l) v -> Add a u v -> incl l u.

## Lists without redundancy

Section ReDun.

Variable A : Type.

Inductive NoDup : list A -> Prop :=
| NoDup_nil : NoDup nil
| NoDup_cons : forall x l, ~ In x l -> NoDup l -> NoDup (x::l).

Lemma NoDup_Add a l l' : Add a l l' -> (NoDup l' <-> NoDup l /\ ~In a l).

Lemma NoDup_remove l l' a :
NoDup (l++a::l') -> NoDup (l++l') /\ ~In a (l++l').

Lemma NoDup_remove_1 l l' a : NoDup (l++a::l') -> NoDup (l++l').

Lemma NoDup_remove_2 l l' a : NoDup (l++a::l') -> ~In a (l++l').

Theorem NoDup_cons_iff a l:
NoDup (a::l) <-> ~ In a l /\ NoDup l.

Effective computation of a list without duplicates

Hypothesis decA: forall x y : A, {x = y} + {x <> y}.

Fixpoint nodup (l : list A) : list A :=
match l with
| [] => []
| x::xs => if in_dec decA x xs then nodup xs else x::(nodup xs)
end.

Lemma nodup_In l x : In x (nodup l) <-> In x l.

Lemma NoDup_nodup l: NoDup (nodup l).

Lemma nodup_inv k l a : nodup k = a :: l -> ~ In a l.

Theorem NoDup_count_occ l:
NoDup l <-> (forall x:A, count_occ decA l x <= 1).

Theorem NoDup_count_occ' l:
NoDup l <-> (forall x:A, In x l -> count_occ decA l x = 1).

Alternative characterisations of being without duplicates, thanks to nth_error and nth

Lemma NoDup_nth_error l :
NoDup l <->
(forall i j, i<length l -> nth_error l i = nth_error l j -> i = j).
Lemma NoDup_nth l d :
NoDup l <->
(forall i j, i<length l -> j<length l ->
nth i l d = nth j l d -> i = j).
Having NoDup hypotheses bring more precise facts about incl.
NoDup and map
NB: the reciprocal result holds only for injective functions, see FinFun.v

Lemma NoDup_map_inv A B (f:A->B) l : NoDup (map f l) -> NoDup l.

## Sequence of natural numbers

Section NatSeq.

seq computes the sequence of len contiguous integers that starts at start. For instance, seq 2 3 is 2::3::4::nil.

Fixpoint seq (start len:nat) : list nat :=
match len with
| 0 => nil
| S len => start :: seq (S start) len
end.

Lemma seq_length : forall len start, length (seq start len) = len.

Lemma seq_nth : forall len start n d,
n < len -> nth n (seq start len) d = start+n.

Lemma seq_shift : forall len start,
map S (seq start len) = seq (S start) len.

Lemma in_seq len start n :
In n (seq start len) <-> start <= n < start+len.

Lemma seq_NoDup len start : NoDup (seq start len).

End NatSeq.

Section Exists_Forall.

# Existential and universal predicates over lists

Variable A:Type.

Section One_predicate.

Variable P:A->Prop.

Inductive Exists : list A -> Prop :=
| Exists_cons_hd : forall x l, P x -> Exists (x::l)
| Exists_cons_tl : forall x l, Exists l -> Exists (x::l).

Hint Constructors Exists.

Lemma Exists_exists (l:list A) :
Exists l <-> (exists x, In x l /\ P x).

Lemma Exists_nil : Exists nil <-> False.

Lemma Exists_cons x l:
Exists (x::l) <-> P x \/ Exists l.

Lemma Exists_dec l:
(forall x:A, {P x} + { ~ P x }) ->
{Exists l} + {~ Exists l}.

Inductive Forall : list A -> Prop :=
| Forall_nil : Forall nil
| Forall_cons : forall x l, P x -> Forall l -> Forall (x::l).

Hint Constructors Forall.

Lemma Forall_forall (l:list A):
Forall l <-> (forall x, In x l -> P x).

Lemma Forall_inv : forall (a:A) l, Forall (a :: l) -> P a.

Lemma Forall_rect : forall (Q : list A -> Type),
Q [] -> (forall b l, P b -> Q (b :: l)) -> forall l, Forall l -> Q l.

Lemma Forall_dec :
(forall x:A, {P x} + { ~ P x }) ->
forall l:list A, {Forall l} + {~ Forall l}.

End One_predicate.

Lemma Forall_Exists_neg (P:A->Prop)(l:list A) :
Forall (fun x => ~ P x) l <-> ~(Exists P l).

Lemma Exists_Forall_neg (P:A->Prop)(l:list A) :
(forall x, P x \/ ~P x) ->
Exists (fun x => ~ P x) l <-> ~(Forall P l).

Lemma neg_Forall_Exists_neg (P:A->Prop) (l:list A) :
(forall x:A, {P x} + { ~ P x }) ->
~ Forall P l ->
Exists (fun x => ~ P x) l.

Lemma Forall_Exists_dec (P:A->Prop) :
(forall x:A, {P x} + { ~ P x }) ->
forall l:list A,
{Forall P l} + {Exists (fun x => ~ P x) l}.

Lemma Forall_impl : forall (P Q : A -> Prop), (forall a, P a -> Q a) ->
forall l, Forall P l -> Forall Q l.

End Exists_Forall.

Hint Constructors Exists.
Hint Constructors Forall.

Section Forall2.

Forall2: stating that elements of two lists are pairwise related.

Variables A B : Type.
Variable R : A -> B -> Prop.

Inductive Forall2 : list A -> list B -> Prop :=
| Forall2_nil : Forall2 [] []
| Forall2_cons : forall x y l l',
R x y -> Forall2 l l' -> Forall2 (x::l) (y::l').

Hint Constructors Forall2.

Theorem Forall2_refl : Forall2 [] [].

Theorem Forall2_app_inv_l : forall l1 l2 l',
Forall2 (l1 ++ l2) l' ->
exists l1' l2', Forall2 l1 l1' /\ Forall2 l2 l2' /\ l' = l1' ++ l2'.

Theorem Forall2_app_inv_r : forall l1' l2' l,
Forall2 l (l1' ++ l2') ->
exists l1 l2, Forall2 l1 l1' /\ Forall2 l2 l2' /\ l = l1 ++ l2.

Theorem Forall2_app : forall l1 l2 l1' l2',
Forall2 l1 l1' -> Forall2 l2 l2' -> Forall2 (l1 ++ l2) (l1' ++ l2').
End Forall2.

Hint Constructors Forall2.

Section ForallPairs.

ForallPairs : specifies that a certain relation should always hold when inspecting all possible pairs of elements of a list.

Variable A : Type.
Variable R : A -> A -> Prop.

Definition ForallPairs l :=
forall a b, In a l -> In b l -> R a b.

ForallOrdPairs : we still check a relation over all pairs of elements of a list, but now the order of elements matters.

Inductive ForallOrdPairs : list A -> Prop :=
| FOP_nil : ForallOrdPairs nil
| FOP_cons : forall a l,
Forall (R a) l -> ForallOrdPairs l -> ForallOrdPairs (a::l).

Hint Constructors ForallOrdPairs.

Lemma ForallOrdPairs_In : forall l,
ForallOrdPairs l ->
forall x y, In x l -> In y l -> x=y \/ R x y \/ R y x.

ForallPairs implies ForallOrdPairs. The reverse implication is true only when R is symmetric and reflexive.

Lemma ForallPairs_ForallOrdPairs l: ForallPairs l -> ForallOrdPairs l.

Lemma ForallOrdPairs_ForallPairs :
(forall x, R x x) ->
(forall x y, R x y -> R y x) ->
forall l, ForallOrdPairs l -> ForallPairs l.
End ForallPairs.

# Inversion of predicates over lists based on head symbol

Ltac is_list_constr c :=
match c with
| nil => idtac
| (_::_) => idtac
| _ => fail
end.

Ltac invlist f :=
match goal with
| H:f ?l |- _ => is_list_constr l; inversion_clear H; invlist f
| H:f _ ?l |- _ => is_list_constr l; inversion_clear H; invlist f
| H:f _ _ ?l |- _ => is_list_constr l; inversion_clear H; invlist f
| H:f _ _ _ ?l |- _ => is_list_constr l; inversion_clear H; invlist f
| H:f _ _ _ _ ?l |- _ => is_list_constr l; inversion_clear H; invlist f
| _ => idtac
end.

# Exporting hints and tactics

Hint Rewrite
rev_involutive
rev_unit
map_nth
map_length
seq_length
app_length
rev_length
app_nil_r
: list.

Ltac simpl_list := autorewrite with list.
Ltac ssimpl_list := autorewrite with list using simpl.

Section Repeat.

Variable A : Type.
Fixpoint repeat (x : A) (n: nat ) :=
match n with
| O => []
| S k => x::(repeat x k)
end.

Theorem repeat_length x n:
length (repeat x n) = n.

Theorem repeat_spec n x y:
In y (repeat x n) -> y=x.

End Repeat.