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 $\{0,\ldots,n-1\}$ 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_ne = ... :
    {A:Type}{C:{n|nat}(vect A (suc n))->Type}
    ({a:A}{n|nat}{v:vect A n}C (vcons A a v))->{n|nat}{v:vect A (suc n)}
    C 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
  vect_head_cons_tail = ... :
    {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_update = ... : {A:Type}{n|nat}(fin n)->(vect A n)->A->vect A n
  vect_character = ... :
    {A:Type}
    [vect_character_rhs=nat_elim ([n:nat](vect A n)->vect A n)
                         ([_:vect A zero]vnil A)
                         ([x1:nat][_:(vect A x1)->vect A x1]
                          [v:vect A (suc x1)]
                          vcons A (vect_head A v) (vect_tail A v))]
    {n|nat}{v:vect A n}Eq v (vect_character_rhs n v)
  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)