(* First assignment for the course G54DTP. *) (* Venanzio Capretta, February 2011. *) (* PART 1 *) (* Non-recursive functions. *) Require Import ZArith. Open Scope Z_scope. Definition quad_fun : Z -> Z := fun x:Z => x*x - 4*x + 3. Definition cub_fun (x:Z) : Z := x*x*x + x - 1. (* PART 2 *) (* Recursive functions. *) Open Scope nat_scope. Fixpoint square_sum (n:nat): nat := match n with O => 0 | S n' => (square_sum n') + n*n end. Fixpoint binomial (n k:nat): nat := match n with O => match k with O => 1 | S k' => 0 end | S n' => match k with O => 1 | S k' => (binomial n' k') + (binomial n' k) end end. (* PART 3 *) (* Functions on lists *) Require Import List. Set Implicit Arguments. Open Scope Z_scope. Fixpoint list_sum (l:list Z): Z := match l with nil => 0 | cons x l' => x + (list_sum l') end. Fixpoint reverse_aux (A:Set)(l lacc: list A): list A := match l with nil => lacc | cons x l' => reverse_aux l' (x::lacc) end. Definition reverse (A:Set)(l:list A): list A := reverse_aux l nil. (* PART 4 *) (* Functions on trees. *) Inductive STree : Set := leaf : STree | node : Z -> STree -> STree -> STree. Fixpoint tree_sum (t:STree): Z := match t with leaf => 0 | node x tl tr => x + (tree_sum tl) + (tree_sum tr) end. Require Import Max. Check max. Fixpoint tree_depth (t:STree): nat := match t with leaf => O | node x tl tr => S (max (tree_depth tl) (tree_depth tr)) end. (* PART 5 *) Fixpoint mirror (t:STree): STree := match t with leaf => leaf | node x tl tr => node x (mirror tr) (mirror tl) end. 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. Fixpoint tree_merge (t1 t2: STree): STree := match t1 with leaf => t2 | node x tl tr => tree_merge tl (tree_merge tr (tree_insert x t2)) end.