Library Array

Require Import types.

Require Import Arith.
Require Import Omega.
Require Import Recdef.

Require Import Range.


Section Arrays.


Inductive array (A:Type):nat->Type:=
|nil : array A 0
|cons : forall n:nat, A -> array A n -> array A (S n).

Definition length (A:Type) (n:nat) (a:array A n):= n.

Definition head (A:Type) (n:nat) (a:array A n):=
match a with
|nil => error
|cons n' h b=> value h
end.

Definition hd (A:Type) (n:nat) (x:A) (a:array A n):=
match a with
|nil => x
|cons n' h b=> h
end.

Lemma head_hd: forall (A:Type) (n:nat) (x:A) (a:array A n),
n>0 -> head A n a=value (hd A n x a).

Definition tail (A:Type) (n:nat) (a:array A n):array A (pred n).
Defined.

Definition headS (A:Type) (n:nat) (a:array A (S n)):=
match a with
|cons n' h b=>h
end.

Definition tailS (A:Type) (n:nat) (a:array A (S n)):array A n:=
match a with
|nil => nil
|cons n' h b=> b
end.



Axiom array_typeequality_down: forall (A:Type) (m n:nat),
array A m=array A n->m=n.

Lemma array_typeequality_up: forall (A:Type) (m n:nat),
m=n->array A m=array A n.

Lemma array_typeequality: forall (A:Type) (m n:nat),
array A m=array A n<->m=n.

Lemma array_rewrite_dependent: forall (A B:Type) (m n:nat)
(a:array A m) (b:array A n)
(f:forall n:nat,array A n->B), a==b-> f m a=f n b.

Lemma array_rewrite_dependent_Prop: forall (A:Type) (m n:nat)
(a:array A m) (b:array A n)
(P:forall n:nat,array A n->Prop), a==b-> P m a->P n b.

Lemma array_nil_n0: forall (A:Type) (n:nat) (a:array A n),
a==nil A -> n=0.

Lemma array_n0_nil: forall (A:Type) (n:nat) (a:array A n),
n=0 -> a==nil A.

Lemma array_0_nil: forall (A:Type) (a:array A 0),
a=nil A.

Theorem array_destruct: forall (A:Type) (n:nat) (a:array A n), n<>0->
{a_body:array A (pred n) &
 {a_head:A & a==cons A (pred n) a_head a_body}}.

Theorem array_destructS: forall (A:Type) (n:nat) (a:array A (S n)),
{a_body:array A n & {a_head:A & a=cons A n a_head a_body}}.
Ltac array_destructS a:=
 let a_body:=fresh a "_body"
 with a_head:=fresh a "_head"
 with aH:=fresh a "H"
 with X:=fresh
 in
assert(X:=array_destructS _ _ a);
destruct X as [a_body X];
destruct X as [a_head aH].

Lemma array_1_head: forall (A:Type) (a:array A 1),
{h|cons A 0 h (nil A)=a}.

Lemma array_S_ht: forall (A:Type) (n:nat) (a:array A (S n)),
a=cons A n (headS A n a) (tailS A n a).

Lemma tailS0_nil: forall (A:Type) (a:array A 1),
tailS A 0 a = nil A.

Lemma tailsequal: forall (A:Type) (n:nat) (a:array A (S n)),
tail A (S n) a=tailS A n a.

Lemma tailS_tail: forall (A:Type) (n:nat) (a:array A (S n)),
tailS A n a=tail A (S n) a.

Lemma headS_hd: forall (A:Type) (n:nat) (x:A) (a:array A (S n)),
headS A n a=hd A (S n) x a.

Lemma tail1_nil: forall (A:Type) (a:array A 1),
tail A 1 a = nil A.

Lemma single_notnil: forall (A:Type) (x:A),
~(cons A 0 x (nil A) == nil A).

Lemma cons_headS_tailS: forall (A:Type) (n:nat)
(a:array A (S n)),
cons A n (headS A n a) (tailS A n a)=a.

Lemma cons_hd_tail: forall (A:Type) (n:nat) (x:A)
(a:array A n), n>0 ->
cons A (pred n) (hd A n x a) (tail A n a)==a.

Lemma head_and_body: forall (A:Type) (n:nat)
(a b:array A n), head A n a=head A n b->
tail A n a=tail A n b-> a=b.


Inductive appending (A:Type) (p:nat) (a:array A p) (q:nat) (b:array A q)
(r:nat) (c:array A r):Prop:=
|appending_nil: r=p+q -> a==nil A -> c==b -> appending A p a q b r c
|appending_intro: r=p+q -> p>0 -> head A p a=head A r c ->
 appending A (pred p) (tail A p a) q b (pred r) (tail A r c)
 -> appending A p a q b r c.

Definition appaux (A:Type) (m:nat) (a:array A m) (n:nat) (b:array A n):
{c:array A (m+n) & appending A m a n b (m+n) c}.
Qed.

Definition app(A:Type) (m:nat) (a:array A m) (n:nat) (b:array A n):array A (m+n).
Defined.


Theorem app_is_appending: forall (A:Type)
(m:nat) (a:array A m) (n:nat) (b:array A n),
appending A m a n b (m+n) (app A m a n b).

End Arrays.

Implicit Arguments cons [A n].
Implicit Arguments app [A m n].
Infix "::" := cons (at level 60, right associativity) : array_scope.
Infix "++" := app (right associativity, at level 60) : array_scope.
Implicit Arguments headS [A n].
Implicit Arguments tailS [A n].

Ltac array_destructS a:=
 let a_body:=fresh a "_body"
 with a_head:=fresh a "_head"
 with aH:=fresh a "H"
 with X:=fresh
 in
assert(X:=array_destructS _ _ a);
destruct X as [a_body X];
destruct X as [a_head aH].

Open Local Scope array_scope.

Check (app (nil nat) (nil nat)).
Check ((nil nat) ++ (nil nat)).
Print plus_assoc.

Lemma array_assoc: forall (A:Type) (p q r:nat),
 array A (p+(q+r))=array A ((p+q)+r).

Lemma app_nil_l: forall (A:Type) (n:nat) (a:array A n),
nil A ++ a = a.


Lemma app_single_l: forall (A:Type) (n:nat) (a:array A n) (x:A),
(x :: nil A) ++ a = x::a.

Lemma cons_JMeq_type: forall (A B:Type) (AB:A=B),
@cons A==@cons B.

Lemma cons_JMeq_length: forall (A B:Type) (m n:nat) (AB:A=B) (Emn:m=n),
@cons A m==@cons B n.

Lemma cons_type: forall (A:Type) (m:nat) (a:array A m)
(n:nat) (b:array A n) (x:A), a==b -> x::a==x::b.
Lemma cons_maptype: forall (A B:Type) (m n:nat)
(AB:A=B) (Emn:m=n)
(F:(A->array A m->array A (S m))=(B->array B n->array B (S n))),
maptype F (@cons A m)=@cons B n.

Lemma cons_maptype_apply: forall (A B:Type) (m n:nat) (a:array A m)
(x:A) (E:A=B) (FS:(array A (S m))=(array B (S n)))
(F:(array A m)=(array B n)),
maptype FS (x::a)=(maptype E x) :: maptype F a.

Lemma decons_head: forall (A:Type) (n:nat) (t:array A n) (ha hb:A),
ha::t=hb::t->ha=hb.

Lemma decons_tail: forall (A:Type) (n:nat) (a b:array A n)
(h:A), h::a=h::b->a=b.

Lemma decons: forall (A:Type) (n:nat) (a b:array A n)
(ha hb:A), ha::a=hb::b->ha=hb/\a=b.

Lemma cons_untype: forall (A:Type) (m:nat) (a:array A m)
(n:nat) (b:array A n) (ha hb:A), ha::a==hb::b -> ha=hb /\ a==b.

Theorem unique_appending: forall (A:Type)
(p:nat) (a:array A p) (q:nat) (b:array A q)
(r:nat) (c:array A r) (s:nat) (d:array A s),
appending A p a q b r c->
appending A p a q b s d->
c==d.

Theorem app_from_appending: forall (A:Type)
(p:nat) (a:array A p) (q:nat) (b:array A q)
(r:nat) (c:array A r),
appending A p a q b r c-> a++b==c.

Theorem app_S: forall (A:Type) (p:nat) (a:array A p)
 (q:nat) (b:array A q) (r:nat) (c:array A r) (x:A),
c==a++b -> x::c==(x::a)++b.


Theorem consapp_ass: forall (A:Type) (p:nat) (a:array A p)
 (q:nat) (b:array A q) (x:A),
(x::a) ++ b=x::(a++b).

Theorem app_ass : forall (A:Type) (p:nat) (a:array A p)
 (q:nat) (b:array A q) (r:nat) (c:array A r),
(a ++ b) ++ c == a ++ b ++ c.

Lemma app_nil_r: forall (A:Type) (n:nat) (a:array A n),
a++nil A == a.

Fixpoint array_homogeneous (A:Type) (n:nat) (x:A)
:array A n:=
match n with
|0 => nil A
|S p=> @cons A p x (array_homogeneous A p x)
end.

Lemma array_noninhabited: forall (A:Type) (n:nat)
(a:array A n), ~ inhabited A -> n=0.

Lemma array_single_type: forall (A:Type) (n:nat) (a:array A n),
n=1 -> {h:A|a==h::(nil A)}.

Lemma array_single:forall (A:Type) (a:array A 1),
{h:A|a=h::(nil A)}.

Print nat_destruct.

Qed.
Check array_Function_ind.
Check array_Function_equation.

Lemma array_Function0: forall (A B:Type)
(head:nat->B->A) (x:B),
array_Function A B 0 head x=nil A.

Lemma array_FunctionS: forall (A B:Type) (n:nat)
(head:nat->B->A) (x:B),
array_Function A B (S n) head x=
head (S n) x::array_Function A B n head x.

Fixpoint nth (A:Type) (p:nat) (default:A)
(n:nat) (a:array A p) : A :=
match n,nat_destruct p with
| O, (inleft N) =>
  let (p',E):=N in
  let E':=array_typeequality_up A p (S p') E in
  headS (maptype E' a)
| S m,(inleft N) =>
  let (p',E):=N in
  let E':=array_typeequality_up A p (S p') E in
  nth A p' default m (tailS (maptype E' a))
|_,_ => default
end.
Implicit Arguments nth[A p].

Fixpoint nth_error (A:Type) (p:nat)
(n:nat) (a:array A p) : Exc A :=
match n,nat_destruct p with
| O, (inleft N) =>
  let (p',E):=N in
  let E':=array_typeequality_up A p (S p') E in
  value (headS (maptype E' a))
| S m,(inleft N) =>
  let (p',E):=N in
  let E':=array_typeequality_up A p (S p') E in
  nth_error A p' m (tailS (maptype E' a))
|_,_ => error
end.
Implicit Arguments nth_error[A p].

Definition nth_range (A:Type) (p:nat) (I:{k|k<p})
(a:array A p):A.
Defined.
Implicit Arguments nth_range[A p].

Theorem nth_out: forall (A:Type) (p:nat) (default:A)
(n:nat) (a:array A p),
n>=p -> nth default n a=default.

Theorem nth_error_out: forall (A:Type) (p n:nat) (a:array A p),
n>=p -> nth_error n a=error.

Theorem nth_error_eq: forall (A:Type) (p:nat) (default:A)
(n:nat) (a:array A p), n<p ->
nth_error n a = value (nth default n a).

Lemma nth_anydefault: forall (A:Type) (p:nat) (d1 d2:A)
(n:nat) (a:array A p), n<p ->
nth d1 n a = nth d2 n a.

Lemma nth_range_eq: forall (A:Type) (p:nat) (d:A)
(n:nat) (H:n<p) (a:array A p),
nth_range (exist _ n H) a=nth d n a.

Fixpoint array_from_func_aux (A:Type) (n:nat) (f:nat->A)
(s:nat) :array A n:=
match n return array A n with
|O=>nil A
|S n'=>f s ::(array_from_func_aux A n' f (S s))
end.

Definition array_from_func (A:Type) (n:nat) (f:nat->A):
array A n:= array_from_func_aux A n f 0.
Implicit Arguments array_from_func[A].

Definition array_from_funcrange_aux_head (m n n':nat)
(H:n<=m) (E:n=S n'):lowrangt m.
Defined.
Definition array_from_funcrange_aux_head2 (m n':nat)
(HS:S n'<=m):lowrangt m.
Defined.
Lemma array_from_funcrange_aux_head_eq: forall (m n n':nat)
(H:n<=m) (HS:S n'<=m) (E:n=S n'),
array_from_funcrange_aux_head m n n' H E=
array_from_funcrange_aux_head2 m n' HS.
Lemma array_from_funcrange_aux_H: forall (m n n':nat) (H:n<=m)
(E:n=S n'), n'<=m.
Qed.

Definition array_from_funcrange (A:Type) (n:nat)
(f:{k:nat|k<n}->A):
array A n:= array_from_funcrange_aux A n n (le_refl n) f.
Implicit Arguments array_from_funcrange[A].

Lemma array_from_funcrange_aux_destruct0: forall (A:Type)
(m:nat) (H:0<=m) (f:{k:nat|k<m}->A),
array_from_funcrange_aux A m 0 H f=nil A.

Lemma array_from_funcrange_aux_destructS: forall (A:Type)
(m n:nat) (H:n<=m) (HS:S n<=m) (f:{k:nat|k<m}->A),
array_from_funcrange_aux A m (S n) HS f=
f (array_from_funcrange_aux_head2 m n HS)::
array_from_funcrange_aux A m n H f.

Theorem array_from_func_aux_eq: forall (A:Type) (m n:nat)
(f:nat->A) (H:n<=m),
array_from_funcrange_aux A m n H (natfunc_lowrangt f m)=

array_from_func_aux A n f (m-n).

Theorem array_from_func_eq: forall (A:Type) (n:nat)
(f:nat->A),
array_from_funcrange n (natfunc_lowrangt f n)=

array_from_func n f.

Theorem array_from_func_nth_aux: forall (A:Type) (n:nat) (f:nat->A)
(s:nat) (default:A) (i:nat),
i<n->nth default i (array_from_func_aux A n f s)=f (s+i).

Theorem array_from_func_nth_error_aux:
forall (A:Type) (n:nat) (f:nat->A) (s:nat) (i:nat),
i<n->nth_error i (array_from_func_aux A n f s)=value (f (s+i)).

Theorem array_from_func_nth: forall (A:Type) (n:nat) (f:nat->A)
(default:A) (i:nat),
i<n->nth default i (array_from_func n f)=f i.

Theorem array_from_func_nth_error:
forall (A:Type) (n:nat) (f:nat->A) (i:nat),
i<n->nth_error i (array_from_func n f)=value(f i).

Theorem array_from_func_nth_range:
forall (A:Type) (n:nat) (f:nat->A) (I:{i|i<n}),
nth_range I (array_from_func n f)=f (proj1_sig I).

Lemma array_from_funcrange_nth_range_aux2: forall (n m:nat)
(I:{k|k<n}) (H:n<=m), {k|k<m}.
Theorem array_from_funcrange_nth_range_aux:
forall (A:Type) (m n:nat) (H:n<=m) (f:{k|k<m}->A)
(I:{k|k<n}),
nth_range I (array_from_funcrange_aux A m n H f)=
f (array_from_funcrange_nth_range_aux2 n m I H).
Theorem array_from_funcrange_nth_range:
forall (A:Type) (n:nat) (f:{k|k<n}->A) (I:{k|k<n}),
nth_range I (array_from_funcrange n f)=f I.

Theorem array_from_funcrange_nth_error_aux:
forall (A:Type) (m n:nat) (H:n<=m) (f:nat->A) (i:nat),
i<n->nth_error i (array_from_funcrange_aux A m n H

(natfunc_lowrangt f m))
=value (f (m-n+i)).

Theorem array_from_funcrange_nth_error:
forall (A:Type) (n:nat) (f:nat->A) (i:nat),
i<n->nth_error i (array_from_funcrange n

(natfunc_lowrangt f n))
=value (f i).

Theorem nth_error_equality: forall (A:Type) (n:nat)
(a b:array A n),
(forall m:nat, nth_error m a=nth_error m b)->a=b.

Theorem nth_equality: forall (A:Type) (n:nat) (d:A)
(a b:array A n),
(forall m:nat, nth d m a=nth d m b)->a=b.

Theorem nth_range_equality: forall (A:Type) (n:nat)
(a b:array A n),
(forall I:{i|i<n}, nth_range I a=nth_range I b)->a=b.

Theorem array_from_func_extensionality: forall (A:Type)
(n:nat) (f g:nat->A) (EXT:forall m:nat, f m= g m),
array_from_func n f=array_from_func n g.

Theorem array_from_funcrange_extensionality: forall (A:Type)
(n:nat) (f g:nat->A) (EXT:forall m, f m= g m),
array_from_funcrange n (natfunc_lowrangt f n)

=array_from_funcrange n (natfunc_lowrangt g n).

Theorem array_from_funcrange_extensionalityR: forall (A:Type)
(n:nat) (f g:{k|k<n}->A) (EXT:forall m, f m= g m),
array_from_funcrange n f
=array_from_funcrange n g.

Theorem array_homogeneous_nth: forall (A:Type)
(n:nat) (x d:A) (i:nat), i<n->
nth d i (array_homogeneous A n x)=x.

Corollary array_homogeneous_nth_same: forall (A:Type)
(n:nat) (x:A) (i:nat),
nth x i (array_homogeneous A n x)=x.

Theorem array_homogeneous_nth_range: forall (A:Type)
(n:nat) (x:A) (I:{k|k<n}),
nth_range I (array_homogeneous A n x)=x.

Theorem array_homogeneous_app: forall (A:Type) (m n:nat) (x:A),
array_homogeneous A (m + n) x =
(array_homogeneous A m x) ++ array_homogeneous A n x.

Theorem app_headS: forall (A:Type) (m n:nat)
(a:array A (S m)) (b:array A n),
headS (a++b) = headS a.

Theorem app_tailS: forall (A:Type) (m n:nat)
(a:array A (S m)) (b:array A n),
tailS (a++b) = tailS a ++ b.

Theorem app_headS_tailS: forall (A:Type) (n:nat)
(a:array A (S n)), (headS a::nil A) ++ tailS a=a.

Theorem app_nth_left: forall (A:Type) (m n:nat)
(a:array A m) (b:array A n) (d:A) (i:nat),i<m->
nth d i (a++b)=nth d i a.

Theorem app_nth_right: forall (A:Type) (m n:nat)
(a:array A m) (b:array A n) (d:A) (i:nat) (Hl:i>=m) (Hr:i<m+n),
nth d i (a++b)=nth d (i-m) b.

Theorem nth_headS: forall (A:Type) (n:nat) (a:array A (S n)) (d:A),
nth d 0 a=headS a.

Theorem nth_tailS: forall (A:Type) (n:nat) (a:array A (S n)) (d:A) (i:nat),
nth d (S i) a=nth d i (tailS a).

Theorem nth_error_headS: forall (A:Type) (n:nat) (a:array A (S n)),
nth_error 0 a=value (headS a).

Theorem nth_error_tailS: forall (A:Type) (n:nat) (a:array A (S n)) (i:nat),
nth_error (S i) a=nth_error i (tailS a).

Theorem nth_range_headS: forall (A:Type) (n:nat) (a:array A (S n))
(H:0<S n),
nth_range (exist _ 0 H) a=headS a.

Theorem nth_range_tailS: forall (A:Type) (n:nat) (a:array A (S n))
(i:nat) (Hi:S i<S n),
nth_range (exist _ (S i) Hi) a=
nth_range (exist _ i (lt_S_n i n Hi)) (tailS a).

Section Cutting.
 Variable A : Type.

Theorem array_cut: forall (c n:nat) (Hc:c<=n) (a:array A n),
 {l:array A c&{r:array A (n-c)|l++r==a}}.


End Cutting.

Theorem app_equality: forall (A:Type) (m n:nat)
(l1 l2:array A m) (r1 r2:array A n),
l1++r1=l2++r2->l1=l2/\r1=r2.

Lemma array_from_func_back: forall (A:Type) (n:nat) (f:nat->A),
array_from_func (n+1) f=array_from_func n f++ f n::nil A.

Theorem nth_range_JMequality: forall (A:Type) (m n:nat) (E:m=n)
(a:array A m) (b:array A n),
(forall (I:{i|i<m}) (J:{j|j<n}), I==J-> nth_range I a=nth_range J b)
->a==b.

Lemma array_from_funcrange_back: forall (A:Type) (n:nat)
(f:{k|k<S n}->A),
array_from_funcrange (S n) f==
array_from_funcrange n (lowrangt_prevfunc f)
 ++ f (exist _ n (lt_n_Sn n))::nil A.

Lemma array_to_arrayfromfunc: forall (A:Type) (n:nat)
(a:array A n) (d:A),
a=array_from_func n (fun i:nat=>nth d i a).

Lemma array_to_arrayfromfuncrange: forall (A:Type) (n:nat)
(a:array A n),
a=array_from_funcrange n (fun I:{i|i<n}=>nth_range I a).

Section arrays_lists.

Definition arraynil:=nil.
Definition arraycons:=cons.
Definition arrayapp:=app.
Definition array_app_nil_l:=app_nil_l.
Implicit Arguments arraycons [A n].
Implicit Arguments arrayapp [A m n].
Require Import List.
Definition listnil:=@Coq.Lists.List.nil.
Definition listcons:=@Coq.Lists.List.cons.

Fixpoint array_as_list (A:Type) (n:nat) (a:array A n):list A:=
match a with
|arraynil => nil
|arraycons nb h b => h::(array_as_list A nb b)
end.
Implicit Arguments array_as_list [A n].

Lemma array_as_list_cero: forall (A:Type) (a:array A 0)
(x:A), array_as_list a=nil.

Theorem array_list_cons:forall (A:Type) (n:nat) (a:array A n) (h:A),
array_as_list (arraycons h a)=h::array_as_list a.

Theorem array_list_app: forall (A:Type) (m:nat) (a:array A m)
 (n:nat) (b:array A n) (x:A),
array_as_list (arrayapp a b)=
array_as_list a ++ array_as_list b.


End arrays_lists.