(* 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).