Library ListFacts

Require Import types.
Require Import Coq.Lists.List.
Require Import Arith.
Require Import Coq.Logic.Classical.
Require Import Coq.omega.Omega.

Lemma removelast_different: forall (A:Type) (l:list A) (x:A),
x::l<>removelast (x::l).

Lemma cons_different: forall (A:Type) (l:list A) (x:A),
l<>x::l.

Lemma removelast_lengthle: forall (A:Type) (l:list A),
length (removelast l)<=length l.

Lemma removelast_length: forall (A:Type) (l:list A) (x:A),
length (removelast (x::l))=length l.

Lemma cons_in: forall (A:Type) (l:list A) (a b:A),
List.In a (b::l)->b=a\/List.In a l.

Lemma list_last_cons2: forall (A:Type) (l:list A) (x y z:A),
last (x::y::l) z=last (y::l) z.

Lemma list_last_cons: forall (A:Type) (l:list A) (x y:A),
last (x::l) y=last l x.

Lemma list_last_In: forall (A:Type) (l:list A) (x:A),
List.In (last l x) (x::l).

Lemma list_last_other: forall (A:Type) (l:list A) (x y z:A),
last (x::l) y=last (x::l) z.

Lemma list_last_Incons: forall (A:Type) (l:list A) (x y:A),
List.In (last (x::l) y) (x::l).

Lemma list_last_app: forall (A:Type) (l m:list A) (x y z:A),
last (l++ x::m) y=last(x::m) z.

Fixpoint listpairs (A:Type) (l:list A) {struct l}:list (A*A):=
match l with
|nil=>nil
|a::t => match t with
  |nil=>nil
  |b::_=>(a,b)::listpairs A t
  end
end.

Definition listpairscycle (A:Type) (l:list A):list (A*A):=
match l with
|nil=>nil
|h::t=>(listpairs A l)++((last l h,h)::nil)
end.

Lemma listpairs_cons: forall (A:Type) (l:list A) (x y:A),
listpairs A (x::y::l)=(x,y)::listpairs A (y::l).

Lemma listpairscycle_break: forall (A:Type) (l:list A) (x:A),
listpairscycle A (x::l)=listpairs A (x::l++x::nil).

Lemma listpairs_Inexbef: forall (A:Type) (l:list A) (x:A),
List.In x l->(exists y:A, List.In (y,x) (listpairs A l))\/hd x l=x.

Lemma listpairscycle_Inexbef: forall (A:Type) (l:list A) (x:A),
List.In x l->exists y:A, List.In (y,x) (listpairscycle A l).

Lemma listpairs_double:forall (A:Type) (l:list A) (x y:A),
List.In (x,y) (listpairs A (l))->
List.In x l /\ List.In y l.

Lemma listpairscycle_double:forall (A:Type) (l:list A) (x y:A),
List.In (x,y) (listpairscycle A (l))->
List.In x l /\ List.In y l.

Lemma listpairscycle_doublesame:forall (A:Type) (l:list A) (x y z:A),
List.In (x,x) (listpairscycle A (y::z::l))-> List.In x (z::l).

Lemma listpairscycle_head:forall (A:Type) (l:list A) (x y:A),
List.In (x,y) (listpairscycle A (x::l))->
List.In y l \/ (l=nil/\x=y).

Lemma AlistIndec: forall (A:Type),
(forall x y:A,{x=y}+{x<>y})->
forall (l:list A) (x:A), {List.In x l}+{~List.In x l}.

Lemma count_occ_le: forall (A : Type)
(DEC:forall x y : A, {x = y} + {x <> y}) (l:list A) (x y:A),
count_occ DEC l y<=count_occ DEC (x::l) y.

Lemma In_nth: forall (A:Type) (l:list A) (x:A),
List.In x l-> exists n:nat,
nth_error l n=value x.

Lemma count_occ_app: forall (A:Type)
(DEC:forall x y : A, {x = y} + {x <> y}) (l m:list A) (x:A),
count_occ DEC (l++m) x=count_occ DEC l x + count_occ DEC m x.

Lemma listpairs_app: forall (A:Type) (l m:list A) (a b:A),
listpairs A ((a::l)++(b::m))=
listpairs A (a::l)++(last (a::l) a,b)::(listpairs A (b::m)).
SearchAbout cons.
Qed.

Fixpoint rotatelist (A:Type) (l:list A):=
match l with
|nil=>nil
|a::m=>m++a::nil
end.

Fixpoint rotatelistn (A:Type) (l:list A) (n:nat):=
match n with
|O=>l
|S p=>rotatelistn A (rotatelist A l) p
end.

Lemma rotatelist_cons: forall (A:Type) (l:list A) (x:A),
rotatelist A (x::l)=l++x::nil.

Lemma rotatelistn_cons: forall (A:Type) (l:list A) (n:nat),
rotatelistn A l (S n)=rotatelistn A (rotatelist A l) n.

Lemma rotatelistn_plus: forall (A:Type) (l:list A) (m n:nat),
rotatelistn A l (m+n)=rotatelistn A (rotatelistn A l n) m.

Lemma rotatelistn_comm: forall (A:Type) (l:list A) (m n:nat),
rotatelistn A (rotatelistn A l n) m=rotatelistn A (rotatelistn A l m) n.

Lemma rotatelistn_rotatelist: forall (A:Type) (l:list A) (n:nat),
rotatelistn A (rotatelist A l) n=rotatelist A (rotatelistn A l n).

Lemma rotatelistn_nil: forall (A:Type) (n:nat),
rotatelistn A nil n=nil.

Lemma rotatelist_nilinv: forall (A:Type) (l:list A),
rotatelist A l=nil->l=nil.

Lemma rotatelistn_nilinv: forall (A:Type) (l:list A) (n:nat),
rotatelistn A l n=nil->l=nil.

Lemma rotatelistn_single: forall (A:Type) (x:A) (n:nat),
rotatelistn A (x::nil) n=x::nil.

Lemma rotatelist_length: forall (A:Type) (l:list A),
length (rotatelist A l)=length l.

Lemma rotatelistn_length: forall (A:Type) (l:list A) (n:nat),
length (rotatelistn A l n)=length l.

Lemma list_ntherror_out: forall (A:Type) (l:list A) (n:nat),
length l <=n <-> nth_error l n=error.

Lemma list_ntherror_outR: forall (A:Type) (l:list A) (n:nat),
length l <=n -> nth_error l n=error.

Lemma list_nth_out: forall (A:Type) (l:list A) (x:A) (n:nat),
length l <=n -> nth n l x=x.

Lemma list_ntherror_inR: forall (A:Type) (l:list A) (n:nat),
n<length l -> exists x:A, nth_error l n=value x.

Lemma list_ntherror_inL: forall (A:Type) (l:list A) (x:A) (n:nat),
nth_error l n=value x -> n<length l.

Lemma list_ntherror_nth: forall (A:Type) (l:list A) (x:A) (n:nat),
n<length l -> nth_error l n=value (nth n l x).

Lemma list_eq_ntherror_to_nth: forall (A:Type) (l m:list A) (x:A) (n:nat),
nth_error l n=nth_error m n -> nth n l x=nth n m x.

Lemma list_eq_nth_to_ntherror: forall (A:Type) (l m:list A) (x y:A) (n:nat),
n<length l -> n<length m -> nth n l x=nth n m y->nth_error l n=nth_error m n.

Lemma rotatelist_ntherror: forall (A:Type) (l:list A) (x:A) (n:nat),
n<length l->
nth_error (rotatelist A (x::l)) n=nth_error l n.

Lemma rotatelist_ntherrorS: forall (A:Type) (l:list A) (n:nat),
S n<length l->
nth_error (rotatelist A l) n=nth_error l (S n).

Lemma rotatelistn_app: forall (A:Type) (l m:list A),
rotatelistn A (l++m) (length l)=m++l.

Lemma rotatelistn_periodic: forall (A:Type) (l:list A),
rotatelistn A l (length l)=l.

Lemma rotatelistn_ntherror: forall (A:Type) (l:list A) (m n:nat),
m+n<length l->
nth_error (rotatelistn A l n) m=nth_error l (m+n).

Lemma rotatelist_hderror: forall (A:Type) (l:list A) (x y:A),
hd_error (rotatelist A (x::y::l))=hd_error (y::l).

Lemma list_hd_nth: forall (A:Type) (l:list A) (x:A),
hd x l=nth 0 l x.

Lemma list_hderror_ntherror: forall (A:Type) (l:list A),
hd_error l=nth_error l 0.

Lemma rotatelistn_hderror: forall (A:Type) (l:list A) (n:nat),
n<length l->
hd_error (rotatelistn A l n)=nth_error l n.


Lemma rotatelist_listpairscycle: forall (A:Type) (l:list A),
listpairscycle A (rotatelist A l)=
rotatelist _ (listpairscycle A l).

Lemma rotatelistn_listpairscycle: forall (A:Type) (l:list A) (n:nat),
listpairscycle A (rotatelistn A l n)=
rotatelistn _ (listpairscycle A l) n.

Lemma rotatelist_count: forall (A:Type)
(DEC:forall x y : A, {x = y} + {x <> y}) (l:list A) (x:A),
count_occ DEC (rotatelist A l) x=count_occ DEC l x.

Lemma rotatelistn_count: forall (A:Type)
(DEC:forall x y : A, {x = y} + {x <> y}) (l:list A) (x:A) (n:nat),
count_occ DEC (rotatelistn A l n) x=count_occ DEC l x.

Lemma rotatelist_InR: forall (A:Type) (l:list A) (x:A),
List.In x l->List.In x (rotatelist A l).

Lemma rotatelist_InL: forall (A:Type) (l:list A) (x:A),
List.In x (rotatelist A l)->List.In x l.

Lemma rotatelistn_InR: forall (A:Type) (l:list A) (x:A) (n:nat),
List.In x l->List.In x (rotatelistn A l n).

Lemma rotatelistn_InL: forall (A:Type) (l:list A) (x:A) (n:nat),
List.In x (rotatelistn A l n)->List.In x l.

Lemma listpairs_length: forall (A:Type) (l:list A) (x:A),
length (listpairs A (x::l))=length l.

Lemma listpairscycle_length: forall (A:Type) (l:list A),
length (listpairscycle A l)=length l.

Lemma rotatelist_to: forall (A:Type) (l:list A) (x:A),
List.In x l->exists n:nat, hd x (rotatelistn A l n)=x.

Lemma rotatelist_topair: forall (A:Type) (l:list A) (pair:A*A),
List.In pair (listpairscycle A l) ->
exists n:nat, hd pair (listpairscycle _ (rotatelistn A l n))=pair.

Lemma listpairs_nth : forall (A:Type) (l:list A) (x y:A) (n:nat),
S n<length l->nth n (listpairs A l) (x,y)=
(nth n l x,nth (S n) l y).

Lemma listpairscycle_nth : forall (A:Type) (l:list A) (x y:A) (n:nat),
S n<length l->nth n (listpairscycle A l) (x,y)=
(nth n l x,nth (S n) l y).

Lemma listpairscycle_last : forall (A:Type) (l:list A) (x y:A),
last (listpairscycle A l) (x,y)=(last l x,hd y l).

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

Lemma listpairscycle_fst : forall (A:Type) (l:list A) (x y:A) (n:nat),
n<length l-> fst(nth n (listpairscycle A l) (x,y))=nth n l x.

Lemma listpairscycle_consecutive : forall (A:Type) (l:list A)
(a b b' c:A) (pair:A*A) (n:nat),
S n<length l->
(nth n (listpairscycle A l) pair=(a,b) /\
nth (S n) (listpairscycle A l) pair=(b',c) )
->b=b'.