Programming with recursion operators

Please submit your module(s) by Email to <jlu@dcs.ed.ac.uk>

For this assignment, you will want to use the libraries pertaining to booleans (lib_bool,lib_bool_funs,and lib_bool_thms) natural numbers (lib_nat) and lists (lib_list_basics). You can browse these libraries on the web.

1. Write the following functions in Lego, using the appropriate recursion operators:
   1. sum_list: (list nat) -> nat (add the elements of a list)

   2. iszero : nat -> bool (true if the argument is zero, false otherwise)

   3. is_one : nat -> bool (true if the argument is suc zero, false otherwise -- hint: use iszero)

   4. contains_zero :(list nat) -> bool ; (true if the list contains a zero)

   5. zero_list :(list nat) -> bool ; (true if the list is either empty or consists entirely of zeroes)

2. Prove the following properties of your functions:
   1. iszero_eq_zero : {n:nat}(is_true (iszero n)) -> Eq n zero;

   2. is_one_eq_one : {n:nat}(is_true (is_one n)) -> Eq n one;

   3. sum_zero_list_is_zero : {l:list nat}(is_true (zero_list l)) -> Eq (sum_list l) zero;

   Hint: induction is often the best way to prove things about inductively defined functions.