Library listlemmasnoproofs



These are some lemmas about lists that are used in words.v

Developed for Coq 8.3

Written by P. Christopher Staecker, updated November 2010.

See also the version with proofs.

Require Import List.

Require Import Omega.


Lemma length_nil: forall A:Type, forall l:list A,
  l = nil <-> length l = 0.


Lemma nat_strong_ind: forall (P:nat -> Prop),
P 0 -> (forall n:nat, (forall (m:nat), m <= n -> P m) -> P (S n)) -> forall n, P n.


strong induction by length for lists
Lemma length_strong_ind: forall (A:Type) (P:list A -> Prop),
P nil -> (forall (n:nat) (k:list A), (forall (l:list A), length l <= n -> P l) -> length k = S n -> P k) -> forall l, P l.

General list facts

Lemma app_nil_head : forall A:Type, forall x:list A, x = nil ++ x.

Lemma length_not_nil: forall A:Type, forall l:list A,
  l <> nil <-> length l <> 0.

Lemma hd_nth: forall A:Type, forall l:list A, forall v:A,
  hd v l = nth 0 l v.

Lemma last_nth: forall A:Type, forall l:list A, forall v:A,
  last l v = nth (length l - 1) l v.


Lemma hd_last_rev: forall A:Type, forall l:list A, forall v:A,
  hd v l = last (rev l) v.


Lemma hd_rev_last: forall A:Type, forall l:list A, forall v:A,
  hd v (rev l) = last l v.

Lemma hd_app: forall A:Type, forall l k: list A, forall d:A,
  l <> nil -> hd d (l++k) = hd d l.

Lemma last_app: forall A:Type, forall l k: list A, forall d:A,
  k <> nil -> last (l++k) d = last k d.

Lemma hd_indep: forall A:Type, forall l:list A, forall a b:A,
  l <> nil -> hd a l = hd b l.

Lemma last_indep: forall A:Type, forall l:list A, forall a b:A,
  l <> nil -> last l a = last l b.


Lemma nth_0: forall A:Type, forall l:list A, forall d:A,
  nth 0 l d = hd d l.

Lemma nth_last: forall A:Type, forall l:list A, forall d:A,
  nth (length l-1) l d = last l d.

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

Lemma firstn_app: forall A:Type, forall l k:list A, forall n:nat,
  length l = n -> firstn n (l++k) = l.




Lemma skipn_app: forall A:Type, forall l k:list A, forall n:nat,
  length l = n -> skipn n (l++k) = k.





Lemma initial_app_eq: forall A:Type, forall l l' k k':list A,
  length l = length l' -> l++k = l'++k' -> l = l'.

Lemma terminal_app_eq: forall A:Type, forall l l' k k':list A,
  length k = length k' -> l++k = l'++k' -> k = k'.

Lemma skipn_length: forall A:Type, forall l:list A, forall n:nat,
  n <= length l -> length (skipn n l) = length l - n.




Lemma skipn_nth: forall A:Type, forall l:list A, forall n m:nat, forall d:A,
  nth m (skipn n l) d = nth (n+m) l d.

Lemma firstn_nth: forall A:Type, forall l:list A, forall n m:nat, forall d:A,
  m < n -> nth m (firstn n l) d = nth m l d.

Lemma skipn_overflow: forall A:Type, forall l:list A, forall n:nat,
  n >= length l -> skipn n l = nil.

Pairwise propositions.

About a prop which holds for all consecutive pairs in the list

Definition list_prop_pairwise (A:Type) (l:list A) (P:A->A->Prop):Prop :=
  forall pos:nat, pos + 2 <= length l -> forall a:A,
    P (nth pos l a) (nth (pos + 1) l a).

Lemma list_pp_rev: forall A:Type, forall l:list A, forall P:A->A->Prop,
  (forall a b:A, P a b -> P b a) -> (list_prop_pairwise l P <-> list_prop_pairwise (rev l) P).

Sublists

This gives the sublist from position n to m including the lower, never including the upper. (So sublist n n l is empty)
Definition sublist (A:Type) (n m:nat) (l:list A) :=
  skipn n (firstn m l).

Lemma sublist_firstn: forall A:Type, forall l:list A, forall n:nat,
  firstn n l = sublist 0 n l.

Lemma sublist_skipn: forall A:Type, forall l:list A, forall n:nat,
  skipn n l = sublist n (length l) l.

Lemma sublist_app: forall A:Type, forall l:list A, forall m n k:nat,
  m<=n<=k -> sublist m n l ++ sublist n k l = sublist m k l.



Lemma sublist_length: forall A:Type, forall l:list A, forall m n:nat,
  m <= n <= length l -> length (sublist m n l) = n - m.

Lemma sublist_degenerate: forall A:Type, forall l:list A, forall m n:nat,
  n <= m \/ m >= length l -> sublist m n l = nil.

Lemma sublist_singleton: forall A:Type, forall l:list A, forall n k:nat, forall d:A,
  k = n+1 -> n < length l -> sublist n k l = (nth n l d)::nil.

Lemma app_sublist1: forall A:Type, forall n m:nat, forall l k: list A,
  n <= length l -> sublist m n (l++k) = sublist m n l.

Lemma app_sublist2: forall A:Type, forall l k: list A, forall m n:nat,
  m >= length l -> sublist m n (l++k) = sublist (m-length l) (n-length l) k.

Lemma sublist_cons: forall A:Type, forall l:list A, forall m n:nat, forall d:A,
  m < n -> m < length l -> sublist m n l = nth m l d :: sublist (m+1) n l.

Lemma sublist_nth: forall A:Type, forall l:list A, forall n m k:nat, forall d:A,
  m+k < n -> nth k (sublist m n l) d = nth (m+k) l d.

Lemma sublist_full: forall A:Type, forall l:list A, forall n:nat,
  n >= length l -> sublist 0 n l = l.

Lemma sublist_sublist_front: forall A:Type, forall l k:list A, forall n:nat,
  length l = n -> sublist 0 n (l ++ k) = l.

Lemma sublist_sublist_back: forall A:Type, forall l k:list A, forall m n:nat,
  length l = m -> length k + m <= n-> sublist m n (l++k) = k.

Lemma sublist_full_app: forall A:Type, forall l:list A, forall n k:nat,
  k >= length l -> sublist 0 n l ++ sublist n k l = l.

Written by P. Christopher Staecker

Creative Commons License

This page has been generated by coqdoc