Next: Vector Basics Up: Vectors Previous: Vectors

## Vector Definitions

Vectors are another datatype parameterised over nat but this time vect n is the collection of lists of length n. With this datatype we can define the (family of) total functions ``nth'' for any natural number n which take an element of the finite set and a list of length n and returns the appropriate element of the list. In this file we prove that the ``nth'' function defined here is equivalent (modulo the appropriate conversions) to the ``nth'' function in the list library.

``` ** Module lib_vectors Imports lib_finite lib_list_length
\$vect : (Type)->nat->Type(vect)
\$vnil : {A:Type}vect A zero
\$vcons : {A:Type}A->{n|nat}(vect A n)->vect A (suc n)
\$vect_elim :
{A:Type}{C_vect:{n|nat}(vect A n)->TYPE}(C_vect (vnil A))->
({a:A}{n|nat}{v:vect A n}(C_vect v)->C_vect (vcons A a v))->{n|nat}
{z:vect A n}C_vect z
[[A:Type][C_vect:{n|nat}(vect A n)->TYPE][f_vnil:C_vect (vnil A)]
[f_vcons:{a:A}{n|nat}{v:vect A n}(C_vect v)->C_vect (vcons A a v)][a:A]
[n|nat][v:vect A n]
vect_elim A C_vect f_vnil f_vcons (vnil A)  ==>  f_vnil
|| vect_elim A C_vect f_vnil f_vcons (vcons A a v)  ==>
f_vcons a v (vect_elim A C_vect f_vnil f_vcons v)]

vect_elim'_lemma = ... :
{A:Type}{n:nat}{m:vect A (suc n)}{P:(vect A (suc n))->Type}
({a:A}{m'6:vect A n}P (vcons A a m'6))->P m
vect_rec = ... :
{A:Type}{C|Type}C->(A->{n|nat}(vect A n)->C->C)->{n|nat}(vect A n)->
C
vect_iter = ... :
{A:Type}{C|Type}C->(nat->A->C->C)->{n|nat}(vect A n)->C
vect_ind = ... :
{A:Type}{P:{n:nat}(vect A n)->Prop}(P (vnil A))->
({a:A}{n|nat}{v:vect A n}(P v)->P (vcons A a v))->{n|nat}
{z:vect A n}P z
vnil_lemma = ... :
{A:Type}{n:nat}{v:vect A n}
nat_elim|([x:nat](vect A x)->Prop)
([v'4:vect A zero]Eq v'4 (vnil A))
([x:nat][_:(vect A x)->Prop][_:vect A (suc x)]trueProp) n v
vect_zero_eq_vnil = ... : {A:Type}{v:vect A zero}Eq v (vnil A)
vect_head = ... : {A:Type}{n|nat}(vect A (suc n))->A
vect_tail = ... : {A:Type}{n|nat}(vect A (suc n))->vect A n
cons_inj_lemma1 = ... :
{A:Type}{a,b:A}{n:nat}{v:vect A n}(Eq (vcons A a v) (vcons A b v))->
Eq a b
cons_inj_lemma2 = ... :
{A:Type}{a:A}{n:nat}{v,w:vect A n}(Eq (vcons A a v) (vcons A a w))->
Eq v w
{A:Type}{n|nat}{v:vect A (suc n)}
Eq (vcons A (vect_head A v) (vect_tail A v)) v
vect_nth = ... : {A:Type}{n|nat}(fin n)->(vect A n)->A
vect_zip = ... :
{A:Type}{n:nat}(A->A->A)->(vect A n)->(vect A n)->vect A n
vector_to_list = ... : {A:Type}{n|nat}(vect A n)->list A
vector_to_list_resp_cons = ... :
{A:Type}{n|nat}{v:vect A n}{a:A}
Eq (cons|A a (vector_to_list A v)) (vector_to_list A (vcons A a v))
vect_nth_equiv_nth = ... :
{A:Type}{n|nat}{x:fin n}{v:vect A n}{a:A}
Eq (vect_nth A x v) (nth (fin_to_nat x) (vector_to_list A v) a)```

Lego
Fri May 24 19:01:27 BST 1996