(* Third assignment for the course G54DTP. *) (* Venanzio Capretta, March 2011. *) 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 := match v with vnull => tt | vcons n x v' => (x,vector_tuple v') end. Fixpoint tuple_vector (A:Set)(n:nat): Tuple A n -> Vector A n := match n return Tuple A n -> Vector A n with O => fun _ => vnull A | S n' => fun t => vcons (fst t) (tuple_vector A n' (snd t)) end. (* 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 := match t with dleaf => nil | dnode z n t1 t2 => z :: dflatten t1 ++ dflatten t2 end. (* 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 := match n with O => O | S n' => S (dsize n' + dsize n') end. Print Vector. Print fst. Fixpoint dvector (n:nat)(t:dTree n): Vector Z (dsize n) := match t in dTree n return Vector Z (dsize n) with dleaf => vnull Z | dnode z n t1 t2 => vcons z (vapp (dvector t1) (dvector t2)) end. (* PART 3 *) (* Define the function returning the label of the root of a tree. *) Fixpoint droot (n:nat)(t: dTree (S n)) : Z := match t with dleaf => tt | dnode z n t1 t2 => z end. (* Define the function returning the left subtree. *) Fixpoint dleft (n:nat)(t: dTree (S n)): dTree n := match t with dleaf => tt | dnode z n t1 t2 => t1 end. (* Define the function returning the right subtree. *) Fixpoint dright (n:nat)(t: dTree (S n)): dTree n := match t with dleaf => tt | dnode z n t1 t2 => t2 end. (* Define the addition operation for trees. *) Fixpoint dadd (n:nat): dTree n -> dTree n -> dTree n := match n return dTree n -> dTree n -> dTree n with O => fun _ _ => dleaf | S n' => fun t1 t2 => dnode (droot t1 + droot t2) (dadd (dleft t1) (dleft t2)) (dadd (dright t1) (dright t2)) end. (* 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 := match n return Vector Z (n+m) -> Vector Z n * Vector Z m with O => fun v => (vnull Z, v) | S n' => fun v => let (v1,v2) := vsplit n' m (vtail v) in (vcons (vhead v) v1, v2) end. (* Define a function that creates a tree from a vector of correct size. *) Fixpoint vdtree (n:nat): Vector Z (dsize n) -> dTree n := match n return Vector Z (dsize n) -> dTree n with O => fun _ => dleaf | S n' => fun v => let (t1,t2) := vsplit (dsize n') (dsize n') (vtail v) in dnode (vhead v) (vdtree n' t1) (vdtree n' t2) end. (* PART 5 *) (* Define an inductive predicate on lists of naturals, that is satisfied whenever the list is in increasing order. *) Inductive IncList : list nat -> Prop := inc_nil : IncList nil | inc_single : forall x, IncList (x::nil) | inc_twocons : forall (x y:nat)(l:list nat), x<=y -> IncList (y::l) -> IncList (x::y::l). Lemma inc_example : IncList (2::5::5::6::9::nil). Proof. repeat (apply inc_twocons; repeat (apply le_n || apply le_S)). apply inc_single. Qed.