Library listlemmasproofs
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 without proofs.
Require Import List.
Require Import Omega.
Set Implicit Arguments.
Unset Strict Implicit.
Lemma length_nil: forall A:Type, forall l:list A,
l = nil <-> length l = 0.
Proof.
split; intros H.
rewrite H; simpl; auto.
destruct l. auto.
contradict H; simpl.
apply sym_not_eq; apply O_S.
Qed.
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.
Proof.
intros P B IHs n.
destruct n.
exact B.
apply IHs.
induction n.
intros m H; replace m with 0; try omega; exact B.
intros m H.
assert (m <= n \/ m = S n) as J; try omega.
destruct J as [J|J].
apply IHn; omega.
rewrite J.
apply IHs.
apply IHn.
Qed.
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.
Proof.
intros A P B IH.
assert (forall (n:nat) (l:list A), length l <= n -> P l) as G.
intro n.
induction n as [| n IHS] using nat_strong_ind.
intros l H.
assert (length l = 0) as G; try omega.
apply length_nil in G.
rewrite G; exact B.
intro l.
intro H.
assert (length l <= n \/ length l = S n) as G; try omega.
destruct G as [G|G].
apply IHS with (m:=n); auto.
apply IH with (n:=n); try exact G.
intro k.
apply IHS with (m:=n) (l:=k).
auto.
intro l.
apply G with (n:=length l); auto.
Qed.
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.
Proof.
intros A P B IH.
assert (forall (n:nat) (l:list A), length l <= n -> P l) as G.
intro n.
induction n as [| n IHS] using nat_strong_ind.
intros l H.
assert (length l = 0) as G; try omega.
apply length_nil in G.
rewrite G; exact B.
intro l.
intro H.
assert (length l <= n \/ length l = S n) as G; try omega.
destruct G as [G|G].
apply IHS with (m:=n); auto.
apply IH with (n:=n); try exact G.
intro k.
apply IHS with (m:=n) (l:=k).
auto.
intro l.
apply G with (n:=length l); auto.
Qed.
Lemma app_nil_head : forall A:Type, forall x:list A, x = nil ++ x.
Proof. simpl; reflexivity. Qed.
Lemma length_not_nil: forall A:Type, forall l:list A,
l <> nil <-> length l <> 0.
Proof.
intros.
split; intros H; contradict H;
[ rewrite length_nil | rewrite <- length_nil ];
assumption.
Qed.
Lemma hd_nth: forall A:Type, forall l:list A, forall v:A,
hd v l = nth 0 l v.
Proof.
destruct l; simpl; auto.
Qed.
Lemma last_nth: forall A:Type, forall l:list A, forall v:A,
last l v = nth (length l - 1) l v.
Proof.
induction l as [|w ws IHl]; simpl. auto.
intros; rewrite IHl.
destruct ws as [|u us]; simpl; auto.
destruct (length (us)); auto.
Qed.
Lemma hd_last_rev: forall A:Type, forall l:list A, forall v:A,
hd v l = last (rev l) v.
Proof.
intros.
induction l as [|w ws IHl]. simpl; auto.
rewrite hd_nth.
rewrite last_nth.
rewrite rev_nth; simpl.
assert (w::nil = rev(w::nil)) as H; simpl; auto.
rewrite H.
rewrite <- distr_rev; rewrite rev_length.
rewrite <- app_comm_cons; rewrite <- app_nil_head.
assert (length ws - (length (w::ws) - 1) = 0);
destruct ws; simpl; auto; try omega.
assert (length ws - length ws = 0) as J; auto; rewrite J.
auto.
rewrite app_length; rewrite rev_length.
destruct ws; simpl; [auto | omega].
Qed.
Lemma hd_rev_last: forall A:Type, forall l:list A, forall v:A,
hd v (rev l) = last l v.
Proof.
intros.
rewrite hd_last_rev; rewrite rev_involutive; auto.
Qed.
Lemma hd_app: forall A:Type, forall l k: list A, forall d:A,
l <> nil -> hd d (l++k) = hd d l.
Proof.
intros.
destruct l; [ contradict H | simpl ]; auto.
Qed.
Lemma last_app: forall A:Type, forall l k: list A, forall d:A,
k <> nil -> last (l++k) d = last k d.
Proof.
intros.
rewrite <- ? hd_rev_last.
rewrite distr_rev.
apply hd_app.
contradict H; rewrite <- rev_involutive with (l:=k); rewrite H; auto.
Qed.
Lemma hd_indep: forall A:Type, forall l:list A, forall a b:A,
l <> nil -> hd a l = hd b l.
Proof.
intros A l a b H.
induction l; [ contradict H | simpl ]; auto.
Qed.
Lemma last_indep: forall A:Type, forall l:list A, forall a b:A,
l <> nil -> last l a = last l b.
Proof.
intros.
rewrite <- rev_involutive with (l:=l).
rewrite <- ? hd_last_rev.
apply hd_indep.
contradict H.
rewrite <- rev_involutive with (l:=l). rewrite H; auto.
Qed.
Lemma nth_0: forall A:Type, forall l:list A, forall d:A,
nth 0 l d = hd d l.
Proof.
intros; destruct l; simpl; auto.
Qed.
Lemma nth_last: forall A:Type, forall l:list A, forall d:A,
nth (length l-1) l d = last l d.
Proof.
intros.
induction l as [|a l IHl].
simpl; auto.
destruct l as [|a0 l].
simpl; auto.
simpl length in *.
transitivity (nth (S (length l) - 1) (a0::l) d).
simpl; rewrite <- minus_n_O; auto.
rewrite IHl.
firstorder.
Qed.
Lemma firstn_length_nt: forall A:Type, forall l:list A, forall n:nat,
n <= length l -> length (firstn n l) = n.
Proof.
intros.
rewrite firstn_length.
rewrite Min.min_l; omega.
Qed.
Lemma firstn_app: forall A:Type, forall l k:list A, forall n:nat,
length l = n -> firstn n (l++k) = l.
Proof.
intros A l k.
induction l as [|b bs IHl]; intros n H;
destruct n. simpl; auto.
contradict H; simpl; auto.
simpl in H. contradict H; auto.
simpl.
rewrite IHl.
auto. simpl in H. auto.
Qed.
Lemma skipn_app: forall A:Type, forall l k:list A, forall n:nat,
length l = n -> skipn n (l++k) = k.
Proof.
intros A l k.
induction l as [|b bs IHl]; intros n H;
destruct n. simpl; auto.
contradict H; simpl; auto.
simpl in H. contradict H; auto.
simpl.
rewrite IHl. auto.
simpl in H. auto.
Qed.
Lemma initial_app_eq: forall A:Type, forall l l' k k':list A,
length l = length l' -> l++k = l'++k' -> l = l'.
Proof.
intros A l l' k k' H G.
rewrite <- firstn_app with (l:=l) (k:=k) (n:=length l); auto.
rewrite <- firstn_app with (l:=l') (k:=k') (n:=length l'); auto.
rewrite H.
f_equal; exact G.
Qed.
Lemma terminal_app_eq: forall A:Type, forall l l' k k':list A,
length k = length k' -> l++k = l'++k' -> k = k'.
Proof.
intros A l l' k k' H G.
rewrite <- skipn_app with (l:=l) (k:=k) (n:= length l); auto.
rewrite <- skipn_app with (l:=l') (k:=k') (n:= length l'); auto.
assert (length (l++k) = length (l'++k')) as K.
f_equal; exact G.
rewrite ? app_length in K.
rewrite H in K.
f_equal.
omega.
exact G.
Qed.
Lemma skipn_length: forall A:Type, forall l:list A, forall n:nat,
n <= length l -> length (skipn n l) = length l - n.
Proof.
intros A l.
induction l.
intros. destruct n.
simpl; omega.
simpl; auto.
intros. destruct n. simpl; auto.
simpl. apply IHl. firstorder.
Qed.
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.
Proof.
intros A l.
induction l; intros;
destruct m; destruct n; simpl; auto.
Qed.
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.
Proof.
intros A l.
induction l; intros m n d H;
destruct m; destruct n; simpl; firstorder.
contradict H; firstorder.
contradict H; firstorder.
Qed.
Lemma skipn_overflow: forall A:Type, forall l:list A, forall n:nat,
n >= length l -> skipn n l = nil.
Proof.
intros A l.
induction l as [|b bs IH]; intros n H;
destruct n as [|n]; simpl; auto.
simpl in H; contradict H; omega.
simpl in H; unfold ge in H; apply le_S_n in H.
firstorder.
Qed.
Proof. simpl; reflexivity. Qed.
Lemma length_not_nil: forall A:Type, forall l:list A,
l <> nil <-> length l <> 0.
Proof.
intros.
split; intros H; contradict H;
[ rewrite length_nil | rewrite <- length_nil ];
assumption.
Qed.
Lemma hd_nth: forall A:Type, forall l:list A, forall v:A,
hd v l = nth 0 l v.
Proof.
destruct l; simpl; auto.
Qed.
Lemma last_nth: forall A:Type, forall l:list A, forall v:A,
last l v = nth (length l - 1) l v.
Proof.
induction l as [|w ws IHl]; simpl. auto.
intros; rewrite IHl.
destruct ws as [|u us]; simpl; auto.
destruct (length (us)); auto.
Qed.
Lemma hd_last_rev: forall A:Type, forall l:list A, forall v:A,
hd v l = last (rev l) v.
Proof.
intros.
induction l as [|w ws IHl]. simpl; auto.
rewrite hd_nth.
rewrite last_nth.
rewrite rev_nth; simpl.
assert (w::nil = rev(w::nil)) as H; simpl; auto.
rewrite H.
rewrite <- distr_rev; rewrite rev_length.
rewrite <- app_comm_cons; rewrite <- app_nil_head.
assert (length ws - (length (w::ws) - 1) = 0);
destruct ws; simpl; auto; try omega.
assert (length ws - length ws = 0) as J; auto; rewrite J.
auto.
rewrite app_length; rewrite rev_length.
destruct ws; simpl; [auto | omega].
Qed.
Lemma hd_rev_last: forall A:Type, forall l:list A, forall v:A,
hd v (rev l) = last l v.
Proof.
intros.
rewrite hd_last_rev; rewrite rev_involutive; auto.
Qed.
Lemma hd_app: forall A:Type, forall l k: list A, forall d:A,
l <> nil -> hd d (l++k) = hd d l.
Proof.
intros.
destruct l; [ contradict H | simpl ]; auto.
Qed.
Lemma last_app: forall A:Type, forall l k: list A, forall d:A,
k <> nil -> last (l++k) d = last k d.
Proof.
intros.
rewrite <- ? hd_rev_last.
rewrite distr_rev.
apply hd_app.
contradict H; rewrite <- rev_involutive with (l:=k); rewrite H; auto.
Qed.
Lemma hd_indep: forall A:Type, forall l:list A, forall a b:A,
l <> nil -> hd a l = hd b l.
Proof.
intros A l a b H.
induction l; [ contradict H | simpl ]; auto.
Qed.
Lemma last_indep: forall A:Type, forall l:list A, forall a b:A,
l <> nil -> last l a = last l b.
Proof.
intros.
rewrite <- rev_involutive with (l:=l).
rewrite <- ? hd_last_rev.
apply hd_indep.
contradict H.
rewrite <- rev_involutive with (l:=l). rewrite H; auto.
Qed.
Lemma nth_0: forall A:Type, forall l:list A, forall d:A,
nth 0 l d = hd d l.
Proof.
intros; destruct l; simpl; auto.
Qed.
Lemma nth_last: forall A:Type, forall l:list A, forall d:A,
nth (length l-1) l d = last l d.
Proof.
intros.
induction l as [|a l IHl].
simpl; auto.
destruct l as [|a0 l].
simpl; auto.
simpl length in *.
transitivity (nth (S (length l) - 1) (a0::l) d).
simpl; rewrite <- minus_n_O; auto.
rewrite IHl.
firstorder.
Qed.
Lemma firstn_length_nt: forall A:Type, forall l:list A, forall n:nat,
n <= length l -> length (firstn n l) = n.
Proof.
intros.
rewrite firstn_length.
rewrite Min.min_l; omega.
Qed.
Lemma firstn_app: forall A:Type, forall l k:list A, forall n:nat,
length l = n -> firstn n (l++k) = l.
Proof.
intros A l k.
induction l as [|b bs IHl]; intros n H;
destruct n. simpl; auto.
contradict H; simpl; auto.
simpl in H. contradict H; auto.
simpl.
rewrite IHl.
auto. simpl in H. auto.
Qed.
Lemma skipn_app: forall A:Type, forall l k:list A, forall n:nat,
length l = n -> skipn n (l++k) = k.
Proof.
intros A l k.
induction l as [|b bs IHl]; intros n H;
destruct n. simpl; auto.
contradict H; simpl; auto.
simpl in H. contradict H; auto.
simpl.
rewrite IHl. auto.
simpl in H. auto.
Qed.
Lemma initial_app_eq: forall A:Type, forall l l' k k':list A,
length l = length l' -> l++k = l'++k' -> l = l'.
Proof.
intros A l l' k k' H G.
rewrite <- firstn_app with (l:=l) (k:=k) (n:=length l); auto.
rewrite <- firstn_app with (l:=l') (k:=k') (n:=length l'); auto.
rewrite H.
f_equal; exact G.
Qed.
Lemma terminal_app_eq: forall A:Type, forall l l' k k':list A,
length k = length k' -> l++k = l'++k' -> k = k'.
Proof.
intros A l l' k k' H G.
rewrite <- skipn_app with (l:=l) (k:=k) (n:= length l); auto.
rewrite <- skipn_app with (l:=l') (k:=k') (n:= length l'); auto.
assert (length (l++k) = length (l'++k')) as K.
f_equal; exact G.
rewrite ? app_length in K.
rewrite H in K.
f_equal.
omega.
exact G.
Qed.
Lemma skipn_length: forall A:Type, forall l:list A, forall n:nat,
n <= length l -> length (skipn n l) = length l - n.
Proof.
intros A l.
induction l.
intros. destruct n.
simpl; omega.
simpl; auto.
intros. destruct n. simpl; auto.
simpl. apply IHl. firstorder.
Qed.
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.
Proof.
intros A l.
induction l; intros;
destruct m; destruct n; simpl; auto.
Qed.
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.
Proof.
intros A l.
induction l; intros m n d H;
destruct m; destruct n; simpl; firstorder.
contradict H; firstorder.
contradict H; firstorder.
Qed.
Lemma skipn_overflow: forall A:Type, forall l:list A, forall n:nat,
n >= length l -> skipn n l = nil.
Proof.
intros A l.
induction l as [|b bs IH]; intros n H;
destruct n as [|n]; simpl; auto.
simpl in H; contradict H; omega.
simpl in H; unfold ge in H; apply le_S_n in H.
firstorder.
Qed.
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).
Proof.
intros A l P Psym.
assert (forall l, list_prop_pairwise l P -> list_prop_pairwise (rev l) P) as T.
intros k H.
destruct k as [|b bs].
simpl; auto.
destruct bs as [|c cs].
simpl; auto.
unfold list_prop_pairwise.
intros pos posl a.
rewrite rev_length in posl.
simpl in posl.
rewrite ? rev_nth; simpl length; try omega.
apply Psym.
replace (S (S (length cs)) - S pos) with (S (S (length cs)) - S (pos + 1) + 1); try omega.
apply H.
simpl length; omega.
split.
apply T.
rewrite <- rev_involutive with (l:=l);
rewrite rev_involutive at 1.
apply T.
Qed.
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.
Proof.
firstorder.
Qed.
Lemma sublist_skipn: forall A:Type, forall l:list A, forall n:nat,
skipn n l = sublist n (length l) l.
Proof.
intros.
unfold sublist.
replace (firstn (length l) l) with l; auto.
induction l;
simpl; try f_equal; auto.
Qed.
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.
Proof.
intros A l.
induction l as [|b bs IH];
intros m n k H;
destruct m; destruct n; destruct k;
simpl; auto.
contradict H; omega.
unfold sublist. simpl.
f_equal.
rewrite ? sublist_firstn.
apply IH; omega.
unfold sublist; simpl; auto.
contradict H; omega.
contradict H; omega.
unfold sublist. simpl.
apply IH; omega.
Qed.
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.
Proof.
intros A l m n H.
unfold sublist.
rewrite skipn_length; rewrite firstn_length_nt; omega.
Qed.
Lemma sublist_degenerate: forall A:Type, forall l:list A, forall m n:nat,
n <= m \/ m >= length l -> sublist m n l = nil.
Proof.
intros A l m n H.
assert (length (sublist m n l) = 0).
unfold sublist.
rewrite skipn_overflow; simpl; auto.
compare n (length l); intro G.
rewrite firstn_length_nt; omega.
apply nat_total_order in G.
rewrite firstn_length.
destruct G;
[ rewrite Min.min_l | rewrite Min.min_r]; omega.
apply length_nil; assumption.
Qed.
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.
Proof.
intros A l n k d H G.
assert ( length (sublist n k l) = 1) as L.
rewrite sublist_length; try omega.
assert (forall m:list A, length m = 1 -> m = nth 0 m d :: nil) as K.
intros m M.
destruct m as [|b bs].
simpl in M; contradict M; omega.
simpl in M.
injection M.
intro N.
apply length_nil in N.
rewrite N; simpl; auto.
rewrite K with (m:=sublist n k l); try exact L.
unfold sublist.
rewrite skipn_nth.
f_equal.
rewrite <- plus_n_O.
apply firstn_nth; try omega.
Qed.
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.
Proof.
intros A n m l k H.
induction n as [|n IH].
simpl; auto.
assert (m <= n \/ m > n) as G; try omega.
destruct G.
rewrite <- ? sublist_app with (m:=m) (n:=n) (k:=S n); try omega.
rewrite IH; try omega.
f_equal.
unfold sublist; f_equal.
rewrite <- firstn_skipn with (n:=S n) (l:=l).
rewrite app_ass.
rewrite firstn_app; try rewrite firstn_length_nt; try omega.
rewrite firstn_skipn; auto.
rewrite ? sublist_degenerate; auto; omega.
Qed.
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.
Proof.
intros A l k.
induction l as [|b bs IH];
intros m n H.
rewrite <- app_nil_head; f_equal; simpl; omega.
assert (m<= n \/ m > n) as G; try omega.
destruct G.
unfold sublist; simpl.
destruct n; simpl.
rewrite ? skipn_overflow; auto; simpl; try omega.
destruct m.
contradict H; simpl; omega.
simpl; simpl in H.
apply IH; try omega.
rewrite ? sublist_degenerate; auto; try omega.
Qed.
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.
Proof.
intros.
rewrite <- sublist_app with (m:=m) (n:=m+1); try omega.
rewrite sublist_singleton with (d:=d); try omega.
rewrite <- app_comm_cons; rewrite app_nil_head; auto.
Qed.
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.
Proof.
intros A l n m.
induction m;
intros k d H.
destruct n.
contradict H; omega.
simpl in *.
rewrite <- sublist_firstn.
rewrite firstn_nth; auto; exact H.
assert (S m > length l \/ S m <= length l) as G; try omega.
destruct G.
rewrite sublist_degenerate; try omega.
rewrite ? nth_overflow; auto; simpl; omega.
transitivity (nth (k+1) (sublist m n l) d).
rewrite <- sublist_app with (m:=m) (n:=S m); try omega.
rewrite app_nth2; try rewrite sublist_length; try omega.
f_equal; omega.
rewrite IHm with (k:=k+1).
f_equal; omega.
omega.
Qed.
Lemma sublist_full: forall A:Type, forall l:list A, forall n:nat,
n >= length l -> sublist 0 n l = l.
Proof.
intros A l.
unfold sublist.
induction l as [| a l IH];
intros n H;
simpl in *;
destruct n; simpl; auto.
contradict H; omega.
rewrite IH; auto; omega.
Qed.
Lemma sublist_sublist_front: forall A:Type, forall l k:list A, forall n:nat,
length l = n -> sublist 0 n (l ++ k) = l.
Proof.
intros.
unfold sublist; simpl.
apply firstn_app; assumption.
Qed.
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.
Proof.
intros.
unfold sublist.
rewrite sublist_firstn.
rewrite <- sublist_app with (n:=m); try omega.
rewrite <- sublist_firstn.
rewrite firstn_app; try omega.
rewrite skipn_app; try omega.
rewrite app_sublist2; try omega.
replace (m-length l) with 0; try omega.
apply sublist_full; omega.
Qed.
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.
Proof.
intros.
assert (n > length l \/ n <= length l) as G; try omega.
destruct G.
rewrite sublist_full; try omega.
rewrite sublist_degenerate; try omega.
rewrite app_nil_end; auto.
rewrite <- firstn_skipn with (n:=n).
rewrite sublist_firstn.
f_equal.
rewrite sublist_skipn.
rewrite <- sublist_app with (m:=n) (n:=length l); try omega.
rewrite sublist_degenerate with (m:=length l) (n:=k); try omega.
rewrite app_nil_end; auto.
Qed.
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.
Proof.
firstorder.
Qed.
Lemma sublist_skipn: forall A:Type, forall l:list A, forall n:nat,
skipn n l = sublist n (length l) l.
Proof.
intros.
unfold sublist.
replace (firstn (length l) l) with l; auto.
induction l;
simpl; try f_equal; auto.
Qed.
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.
Proof.
intros A l.
induction l as [|b bs IH];
intros m n k H;
destruct m; destruct n; destruct k;
simpl; auto.
contradict H; omega.
unfold sublist. simpl.
f_equal.
rewrite ? sublist_firstn.
apply IH; omega.
unfold sublist; simpl; auto.
contradict H; omega.
contradict H; omega.
unfold sublist. simpl.
apply IH; omega.
Qed.
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.
Proof.
intros A l m n H.
unfold sublist.
rewrite skipn_length; rewrite firstn_length_nt; omega.
Qed.
Lemma sublist_degenerate: forall A:Type, forall l:list A, forall m n:nat,
n <= m \/ m >= length l -> sublist m n l = nil.
Proof.
intros A l m n H.
assert (length (sublist m n l) = 0).
unfold sublist.
rewrite skipn_overflow; simpl; auto.
compare n (length l); intro G.
rewrite firstn_length_nt; omega.
apply nat_total_order in G.
rewrite firstn_length.
destruct G;
[ rewrite Min.min_l | rewrite Min.min_r]; omega.
apply length_nil; assumption.
Qed.
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.
Proof.
intros A l n k d H G.
assert ( length (sublist n k l) = 1) as L.
rewrite sublist_length; try omega.
assert (forall m:list A, length m = 1 -> m = nth 0 m d :: nil) as K.
intros m M.
destruct m as [|b bs].
simpl in M; contradict M; omega.
simpl in M.
injection M.
intro N.
apply length_nil in N.
rewrite N; simpl; auto.
rewrite K with (m:=sublist n k l); try exact L.
unfold sublist.
rewrite skipn_nth.
f_equal.
rewrite <- plus_n_O.
apply firstn_nth; try omega.
Qed.
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.
Proof.
intros A n m l k H.
induction n as [|n IH].
simpl; auto.
assert (m <= n \/ m > n) as G; try omega.
destruct G.
rewrite <- ? sublist_app with (m:=m) (n:=n) (k:=S n); try omega.
rewrite IH; try omega.
f_equal.
unfold sublist; f_equal.
rewrite <- firstn_skipn with (n:=S n) (l:=l).
rewrite app_ass.
rewrite firstn_app; try rewrite firstn_length_nt; try omega.
rewrite firstn_skipn; auto.
rewrite ? sublist_degenerate; auto; omega.
Qed.
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.
Proof.
intros A l k.
induction l as [|b bs IH];
intros m n H.
rewrite <- app_nil_head; f_equal; simpl; omega.
assert (m<= n \/ m > n) as G; try omega.
destruct G.
unfold sublist; simpl.
destruct n; simpl.
rewrite ? skipn_overflow; auto; simpl; try omega.
destruct m.
contradict H; simpl; omega.
simpl; simpl in H.
apply IH; try omega.
rewrite ? sublist_degenerate; auto; try omega.
Qed.
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.
Proof.
intros.
rewrite <- sublist_app with (m:=m) (n:=m+1); try omega.
rewrite sublist_singleton with (d:=d); try omega.
rewrite <- app_comm_cons; rewrite app_nil_head; auto.
Qed.
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.
Proof.
intros A l n m.
induction m;
intros k d H.
destruct n.
contradict H; omega.
simpl in *.
rewrite <- sublist_firstn.
rewrite firstn_nth; auto; exact H.
assert (S m > length l \/ S m <= length l) as G; try omega.
destruct G.
rewrite sublist_degenerate; try omega.
rewrite ? nth_overflow; auto; simpl; omega.
transitivity (nth (k+1) (sublist m n l) d).
rewrite <- sublist_app with (m:=m) (n:=S m); try omega.
rewrite app_nth2; try rewrite sublist_length; try omega.
f_equal; omega.
rewrite IHm with (k:=k+1).
f_equal; omega.
omega.
Qed.
Lemma sublist_full: forall A:Type, forall l:list A, forall n:nat,
n >= length l -> sublist 0 n l = l.
Proof.
intros A l.
unfold sublist.
induction l as [| a l IH];
intros n H;
simpl in *;
destruct n; simpl; auto.
contradict H; omega.
rewrite IH; auto; omega.
Qed.
Lemma sublist_sublist_front: forall A:Type, forall l k:list A, forall n:nat,
length l = n -> sublist 0 n (l ++ k) = l.
Proof.
intros.
unfold sublist; simpl.
apply firstn_app; assumption.
Qed.
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.
Proof.
intros.
unfold sublist.
rewrite sublist_firstn.
rewrite <- sublist_app with (n:=m); try omega.
rewrite <- sublist_firstn.
rewrite firstn_app; try omega.
rewrite skipn_app; try omega.
rewrite app_sublist2; try omega.
replace (m-length l) with 0; try omega.
apply sublist_full; omega.
Qed.
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.
Proof.
intros.
assert (n > length l \/ n <= length l) as G; try omega.
destruct G.
rewrite sublist_full; try omega.
rewrite sublist_degenerate; try omega.
rewrite app_nil_end; auto.
rewrite <- firstn_skipn with (n:=n).
rewrite sublist_firstn.
f_equal.
rewrite sublist_skipn.
rewrite <- sublist_app with (m:=n) (n:=length l); try omega.
rewrite sublist_degenerate with (m:=length l) (n:=k); try omega.
rewrite app_nil_end; auto.
Qed.
Written by P. Christopher Staecker
This page has been generated by coqdoc