Library listlemmasnoproofs
These are some lemmas about lists that are used in words.v
Developed for Coq 8.3Written 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.
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.
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.
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.
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).
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.
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.
This page has been generated by coqdoc