(* First assignment for the course G54DTP. *) (* Venanzio Capretta, February 2011. *) (* INSTRUCTIONS: you must complete this file by replacing every question mark with a correct definition satisfying the requirements specified in the comment before each incomplete definition. You are not allowed to modify any other part of the file. There are 10 exercises, each one is worth 1 point. *) (* PART 1 *) (* Non-recursive functions. *) Require Import ZArith. Open Scope Z_scope. (* Define the function on the integer that maps x to x^2-4x+3. *) Definition quad_fun : Z -> Z := ? (* Define the function on the integers that maps x to x^3+x-1. *) Definition cub_fun (x:Z) : Z := ? (* PART 2 *) (* Recursive functions. *) Open Scope nat_scope. (* Define the function on natural numbers that adds the first n squares: (square_sum n) = 0^2 + 1^2 + 2^2 + ... + n^2. *) Fixpoint square_sum (n:nat): nat := ? (* Define a function that computes the binomial coefficients. Remember that the binomial coefficients satisfy the following equalities: (binomial n 0) = 1 for every n (binomial n k) = (binomial (n-1) (k-1)) + (binomial (n-1) k) if k<=n We will assume by convention that (binomial n k) = 0 if k>n. *) Fixpoint binomial (n k:nat): nat := ? (* PART 3 *) (* Functions on lists *) Require Import List. Set Implicit Arguments. Open Scope Z_scope. (* Define the function that adds all the elements of a list. For example: list_sum (2::-3::1::9::2::nil) = 2+(-3)+1+9+2 = 11. *) Fixpoint list_sum (l:list Z): Z := ? (* Define the function that reverses the order of a list: reverse (2::-3::1::9::2::nil) = 2::9::1::-3::2::nil. The function is defined in terms of an auxiliary function that takes two arguments and appends the reverse of the first to the second: reverse_aux (5::2::7::nil) (-3::6::nil) =7::2::5::-3::6::nil. *) Fixpoint reverse_aux (A:Set)(l lacc: list A): list A := ? Definition reverse (A:Set)(l:list A): list A := reverse_aux l nil. (* PART 4 *) (* Functions on trees. *) (* Here is again the definition of search trees. *) Inductive STree : Set := leaf : STree | node : Z -> STree -> STree -> STree. (* Define the function that adds all the values in the labels of a tree. *) Fixpoint tree_sum (t:STree): Z := ? Require Import Max. (* max is the function that computes the maximum of two naturals. *) Check max. (* Define the function that computes the depth of a tree, that is, the maximum length of a path from the root to a leaf. *) Fixpoint tree_depth (t:STree): nat := ? (* PART 5 *) (* More advanced definitions on trees. *) (* Define the function that construct the mirror image of a tree: every node must go the opposite side. For example: mirror (node 4 (node 2 (node 1 nil nil) (node 7 nil nil)) (node 9 (node 6 nil nil) (node 3 nil nil))) = node 4 (node 9 (node 3 nil nil) (node 6 nil nil)) (node 2 (node 7 nil nil) (node 1 nil nil)) *) Fixpoint mirror (t:STree): STree := ? (* We repeat the definition of the insertion of a new element in a tree. *) Fixpoint tree_insert (x:Z)(t:STree): STree := match t with leaf => node x leaf leaf | node y ltr rtr => if (Z_le_gt_dec x y) then (node y (tree_insert x ltr) rtr) else (node y ltr (tree_insert x rtr)) end. (* Using the definition above, define the function that "merges" two search trees, that is, computes a tree containing all the values from the two imput trees. Assuming that the input trees are correctly ordered, also the result must be correctly ordered. *) Fixpoint tree_merge (t1 t2: STree): STree := ?