Library Coq.Lists.List



Require Import Le Gt Minus Min Bool.


Basics: definition of polymorphic lists and some operations


Definitions


Section Lists.

  Variable A : Type.

  Inductive list : Type :=
    | nil : list
    | cons : A -> list -> list.

  Infix "::" := cons (at level 60, right associativity) : list_scope.

  Open Scope list_scope.

Head and tail
  Definition head (l:list) :=
    match l with
      | nil => error
      | x :: _ => value x
    end.

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

  Definition tail (l:list) : list :=
    match l with
      | nil => nil
      | a :: m => m
    end.

Length of lists
  Fixpoint length (l:list) : nat :=
    match l with
      | nil => 0
      | _ :: m => S (length m)
    end.

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

Concatenation of two lists
  Fixpoint app (l m:list) {struct l} : list :=
    match l with
      | nil => m
      | a :: l1 => a :: app l1 m
    end.

  Infix "++" := app (right associativity, at level 60) : list_scope.

End Lists.

Exporting list notations and tactics

Implicit Arguments nil [A].
Infix "::" := cons (at level 60, right associativity) : list_scope.
Infix "++" := app (right associativity, at level 60) : list_scope.

Open Scope list_scope.

Delimit Scope list_scope with list.



Facts about lists


Section Facts.

  Variable A : Type.

Genereric facts


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

Destruction

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

Head and tail


  Theorem head_nil : head (@nil A) = None.

  Theorem head_cons : forall (l : list A) (x : A), head (x::l) = Some x.

Facts about In


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 in_nil : forall a:A, ~ In a nil.

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

Inversion
  Theorem 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}.

Facts about app


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

Concat with nil

  Theorem app_nil_end : forall l:list A, l = l ++ nil.

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

  Theorem ass_app : 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' = nil -> l = nil /\ l' = nil.

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

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

Compatibility wtih 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 app_inv_head:
   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_nil_end ass_app app_ass: datatypes v62.
Hint Resolve app_comm_cons app_cons_not_nil: datatypes v62.
Hint Immediate app_eq_nil: datatypes v62.
Hint Resolve app_eq_unit app_inj_tail: datatypes v62.
Hint Resolve in_eq in_cons in_inv in_nil in_app_or in_or_app: datatypes v62.

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, nil => 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, nil => 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} : Exc A :=
    match n, l with
      | O, x :: _ => value x
      | S n, _ :: l => nth_error l n
      | _, _ => error
    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_In :
    forall (n:nat) (l:list A) (d:A), n < length l -> In (nth n l d) l.

  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.

Remove


  Section Remove.

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

    Fixpoint remove (x : A) (l : list A){struct l} : list A :=
      match l with
        | nil => nil
        | 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).

  End Remove.

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) {struct l} : A :=
  match l with
    | nil => d
    | a :: nil => a
    | a :: l => last l d
  end.

removelast l remove the last element of l

  Fixpoint removelast (l:list A) {struct l} : list A :=
    match l with
      | nil => nil
      | a :: nil => nil
      | a :: l => a :: removelast l
    end.

  Lemma app_removelast_last :
    forall l d, l<>nil -> l = removelast l ++ (last l d :: nil).

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

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


Counting occurences of a element


  Hypotheses eqA_dec : forall x y : A, {x = y}+{x <> y}.

  Fixpoint count_occ (l : list A) (x : A){struct l} : nat :=
    match l with
      | nil => 0
      | y :: tl =>
        let n := count_occ tl x in
          if eqA_dec y x then S n else n
    end.

Compatibility of count_occ with operations on list
  Theorem count_occ_In : forall (l : list A) (x : A), In x l <-> count_occ l x > 0.

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

  Lemma count_occ_nil : forall (x : A), count_occ nil x = 0.

  Lemma count_occ_cons_eq : forall (l : list A) (x y : A), x = y -> count_occ (x::l) y = S (count_occ l y).

  Lemma count_occ_cons_neq : forall (l : list A) (x y : A), 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
      | nil => nil
      | x :: l' => rev l' ++ x :: nil
    end.

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

  Remark rev_unit : forall (l:list A) (a:A), rev (l ++ a :: nil) = 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) {struct l} : list A :=
    match l with
      | nil => l'
      | a::l => rev_append l (a::l')
    end.

  Definition rev' l : list A := rev_append l nil.

  Notation rev_acc := rev_append (only parsing).

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

  Notation rev_acc_rev := rev_append_rev (only parsing).

  Lemma rev_alt : forall l, rev l = rev_append l nil.

Reverse Induction Principle on Lists

  Section Reverse_Induction.


    Lemma rev_list_ind :
      forall P:list A-> Prop,
        P nil ->
        (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 nil ->
        (forall (x:A) (l:list A), P l -> P (l ++ x :: nil)) -> forall l:list A, P l.

  End Reverse_Induction.

Lists modulo permutation


  Section Permutation.

    Inductive Permutation : list A -> list A -> Prop :=
      | perm_nil: Permutation nil nil
      | perm_skip: forall (x:A) (l l':list A), Permutation l l' -> Permutation (cons x l) (cons x l')
      | perm_swap: forall (x y:A) (l:list A), Permutation (cons y (cons x l)) (cons x (cons y l))
      | perm_trans: forall (l l' l'':list A), Permutation l l' -> Permutation l' l'' -> Permutation l l''.

    Hint Constructors Permutation.

Some facts about Permutation

    Theorem Permutation_nil : forall (l : list A), Permutation nil l -> l = nil.

    Theorem Permutation_nil_cons : forall (l : list A) (x : A), ~ Permutation nil (x::l).

Permutation over lists is a equivalence relation

    Theorem Permutation_refl : forall l : list A, Permutation l l.

    Theorem Permutation_sym : forall l l' : list A, Permutation l l' -> Permutation l' l.

    Theorem Permutation_trans : forall l l' l'' : list A, Permutation l l' -> Permutation l' l'' -> Permutation l l''.

    Hint Resolve Permutation_refl Permutation_sym Permutation_trans.

Compatibility with others operations on lists

    Theorem Permutation_in : forall (l l' : list A) (x : A), Permutation l l' -> In x l -> In x l'.

    Lemma Permutation_app_tail : forall (l l' tl : list A), Permutation l l' -> Permutation (l++tl) (l'++tl).

    Lemma Permutation_app_head : forall (l tl tl' : list A), Permutation tl tl' -> Permutation (l++tl) (l++tl').

    Theorem Permutation_app : forall (l m l' m' : list A), Permutation l l' -> Permutation m m' -> Permutation (l++m) (l'++m').

    Theorem Permutation_app_swap : forall (l l' : list A), Permutation (l++l') (l'++l).

    Theorem Permutation_cons_app : forall (l l1 l2:list A) a,
      Permutation l (l1 ++ l2) -> Permutation (a :: l) (l1 ++ a :: l2).
    Hint Resolve Permutation_cons_app.

    Theorem Permutation_length : forall (l l' : list A), Permutation l l' -> length l = length l'.

    Theorem Permutation_rev : forall (l : list A), Permutation l (rev l).

    Theorem Permutation_ind_bis :
     forall P : list A -> list A -> Prop,
       P (@nil A) (@nil A) ->
       (forall x l l', Permutation l l' -> P l l' -> P (x :: l) (x :: l')) ->
       (forall x y l l', Permutation l l' -> P l l' -> P (y :: x :: l) (x :: y :: l')) ->
       (forall l l' l'', Permutation l l' -> P l l' -> Permutation l' l'' -> P l' l'' -> P l l'') ->
       forall l l', Permutation l l' -> P l l'.

    Ltac break_list l x l' H :=
     destruct l as [|x l']; simpl in *;
     injection H; intros; subst; clear H.

    Theorem Permutation_app_inv : forall (l1 l2 l3 l4:list A) a,
      Permutation (l1++a::l2) (l3++a::l4) -> Permutation (l1++l2) (l3 ++ l4).

    Theorem Permutation_cons_inv :
       forall l l' a, Permutation (a::l) (a::l') -> Permutation l l'.

    Theorem Permutation_cons_app_inv :
       forall l l1 l2 a, Permutation (a :: l) (l1 ++ a :: l2) -> Permutation l (l1 ++ l2).

    Theorem Permutation_app_inv_l :
        forall l l1 l2, Permutation (l ++ l1) (l ++ l2) -> Permutation l1 l2.

    Theorem Permutation_app_inv_r :
       forall l l1 l2, Permutation (l1 ++ l) (l2 ++ l) -> Permutation l1 l2.

  End Permutation.

Decidable equality on lists


  Hypotheses eqA_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 B : Type.
  Variable f : A -> B.

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

  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_app : forall l l',
    map (l++l') = (map l)++(map l').

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

  Hint Constructors Permutation.

  Lemma Permutation_map :
    forall l l', Permutation l l' -> Permutation (map l) (map l').

flat_map

  Definition flat_map (f:A -> list B) :=
    fix flat_map (l:list A) {struct l} : 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 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 :
  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 B : Type.
  Variable f : A -> B -> A.

  Fixpoint fold_left (l:list B) (a0:A) {struct l} : 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 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 x y:A, f x y = f y x) ->
      forall (a0:A) (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) {struct l} :
    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) {struct l}: 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.

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

    Fixpoint forallb (l:list A) {struct l} : 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).

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.

partition

    Fixpoint partition (l:list A) {struct l} : 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.

  End Bool.

Operations on lists of pairs or lists of lists


  Section ListPairs.
    Variables A B : Type.

split derives two lists from a list of pairs

    Fixpoint split (l:list (A*B)) { struct l }: list A * list B :=
      match l with
        | nil => (nil, nil)
        | (x,y) :: tl => let (g,d) := split tl in (x::g, y::d)
      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){struct l} : 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) {struct l} :
      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.

Miscelenous 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 v62.

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

Cutting a list at some position


Section Cutting.

  Variable A : Type.

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

  Fixpoint skipn (n:nat)(l:list A) { struct n } : 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.

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_remove_1 : forall l l' a, NoDup (l++a::l') -> NoDup (l++l').

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

  Lemma NoDup_Permutation : forall l l',
    NoDup l -> NoDup l' -> (forall x, In x l <-> In x l') -> Permutation l l'.

End ReDun.

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) {struct len} : 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.

End NatSeq.

Exporting hints and tactics


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

Hint Rewrite <-
  app_nil_end
  : list.

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