http://www.cs.nott.ac.uk/~pszvc/g54dtp/vectors.v

vector-types.coq

(* Introduction to dependent types using vectors. 
    Venanzio Capretta, February 2011.             *)

(* This tells Coq to implicitely deduce some arguments. *)

Set Implicit Arguments.

(* Family of finite types: (Finite n) has exactly n elements. *)

Inductive Finite: nat -> Set :=
  finz: forall n, Finite (S n)
| fins: forall n, Finite n -> Finite (S n).

Check (finz 3).
Check (fins (fins (finz 3))).

(* This function turns an element of a finite type
   to the curresponding natural number. *)

Fixpoint fin_to_nat (n:nat)(i:Finite n): nat :=
match i with
  finz n => O
| fins n i' => S (fin_to_nat i')
end.

Eval compute in (fin_to_nat (fins (fins (finz 3)))).

(* (Vector A n) is the type of vectors of length n
   whose elements are of type A. *)
 
Inductive Vector (A:Set): nat -> Set :=
  vnull: Vector A 0
| vcons: forall n, A -> Vector A n -> Vector A (S n).

Check (vcons 7 (vcons 1 (vcons 4 (vnull nat)))).

(* Sum of the elements of a vector of natural numbers. *)

Fixpoint vsum (n:nat)(v:Vector nat n): nat :=
match v with
  vnull => O
| vcons n x v' => x + (vsum v')
end.

Eval compute in (vsum (vcons 7 (vcons 1 (vcons 4 (vnull nat))))).

(* Appending two vectors. *)

Fixpoint vapp (A:Set)(n1:nat)(v1:Vector A n1)(n2:nat)(v2:Vector A n2):
  Vector A (n1+n2) :=
match v1 with
  vnull => v2
| vcons n x v1' => vcons x (vapp v1' v2)
end.

Definition v1 := vcons 7 (vcons 2 (vcons 4 (vnull nat))).
Definition v2 := vcons 8 (vcons 3 (vnull nat)).

Check v1.
Check v2.

Eval compute in (vapp v1 v2).
Eval compute in (Vector nat (3+2)).

(* Type of the first element of a vector. *)

Definition vhType (A:Set)(n:nat): Set :=
match n with
  O => unit
| S n' => A
end.

(* First element of a vector, if it exists. *)

Definition vhead (A:Set)(n:nat)(v:Vector A n): vhType A n :=
match v with
  vnull => tt
| vcons n x v' => x
end.

Definition vector_head (A:Set)(n:nat)(v:Vector A (S n)): A :=
  vhead v.

(* Type of the tail of a vector. *)

Definition vtType (A:Set)(n:nat): Set :=
match n with
  O => unit
| S n' => Vector A n'
end.

(* Part of the vector after the head. *)

Definition vtail (A:Set)(n:nat)(v:Vector A n): vtType A n :=
match v with
  vnull => tt
| vcons n' x v' => v'
end.

Definition vector_tail (A:Set)(n:nat)(v:Vector A (S n)): Vector A n :=
  vtail v.

(* Pointwise addition of two vectors of equal length. *)
(* This time we do recursion on the number n.
   Since the result type depend on it, we must specify
   this fact by giving a "return" specification in the match. *)

Fixpoint vadd (n:nat): Vector nat n -> Vector nat n -> Vector nat n :=
match n return (Vector nat n -> Vector nat n -> Vector nat n) with
  O => fun _ _ => vnull nat
| (S n) => fun v1 v2 => vcons ((vhead v1)+(vhead v2))
                                                 (vadd (vtail v1) (vtail v2))
end.

Definition v3 := vcons 5 (vcons 9 (vcons 0 (vnull nat))).

Eval compute in (vadd v1 v3).