Library Array_old_eqtype

Require Import axiomtypes.

Require Import Arith.

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: forall (A:Type) (m n:nat),
array A m=array A n<->m=n.

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}}.

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.

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_type: forall (A:Type) (m:nat) (a:array A m)
(n:nat) (b:array A n) (x:A), a==b -> x::a==x::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.

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)}.

Section arrays_lists.

Require Import List.

Fixpoint array_as_list (A:Type) (n:nat) (a:array A n):list A:=
match a with
|Top.nil => nil
|Top.cons 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 (Top.cons 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 (Top.app a b)=
array_as_list a ++ array_as_list b.

End arrays_lists.