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