(* Third assignment for the course G54DTP. *) (* Venanzio Capretta, March 2011. *) (* Each part is worth 2 points. *) Require Import ZArith. Require Import List. Set Implicit Arguments. (* Recall the definition of vectors. *) Inductive Vector (A:Set): nat -> Set := vnull: Vector A 0 | vcons: forall n, A -> Vector A n -> Vector A (S n). (* The function that appends 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. (* PART 1 *) (* A different way of defining vectors is by a recursive tuple type. *) Fixpoint Tuple (A:Set)(n:nat): Set := match n with O => unit | S n' => (A*(Tuple A n'))%type end. (* Define functions that transform vectors to tuples and viceversa. *) Fixpoint vector_tuple (A:Set)(n:nat)(v:Vector A n): Tuple A n := ? Fixpoint tuple_vector (A:Set)(n:nat): Tuple A n -> Vector A n := ? (* PART 2 *) (* Binary trees of fixed depth with integer labels on the nodes. *) Inductive dTree : nat -> Set := dleaf : dTree O | dnode : Z -> forall n, dTree n -> dTree n -> dTree (S n). (* Define the function that returns the list of labels of a tree. *) Fixpoint dflatten (n:nat)(t:dTree n): list Z := ? (* Define the function that returns the vector of labels of a tree. First you need to define a function that gives the size of the vector. *) Fixpoint dsize (n:nat): nat := ? Fixpoint dvector (n:nat)(t:dTree n): Vector Z (dsize n) := ? (* PART 3 *) (* Define the function returning the label of the root of a tree. *) Fixpoint droot (n:nat)(t: dTree (S n)) : Z := ? (* Define the function returning the left subtree. *) Fixpoint dleft (n:nat)(t: dTree (S n)): dTree n := ? (* Define the function returning the right subtree. *) Fixpoint dright (n:nat)(t: dTree (S n)): dTree n := ? (* Define the addition operation for trees. *) Fixpoint dadd (n:nat): dTree n -> dTree n -> dTree n := ? (* PART 4 *) Require Import Min. (* Recall the definitions of head and tail of a vector. *) Definition vhead (A:Set)(n:nat)(v:Vector A (S n)): A := match v with vnull => tt | vcons n x v' => x end. Definition vtail (A:Set)(n:nat)(v:Vector A (S n)): Vector A n := match v with vnull => tt | vcons n x v' => v' end. (* Define a function that splits a vector in two parts of specified sizes. *) Fixpoint vsplit (n m:nat): Vector Z (n+m) -> Vector Z n * Vector Z m := ? (* Define a function that creates a tree from a vector of correct size. *) Fixpoint vdtree (n:nat): Vector Z (dsize n) -> dTree n := ? (* PART 5 *) (* Define an inductive predicate on list of naturals, that is satisfied whenever the list is in increasing order. *) Inductive IncList : list nat -> Prop := ? (* If you defined it correctly, you should be able to prove the following lemma. *) Lemma inc_example : IncList (2::5::5::6::9::nil). Proof. ? Qed.