# Programming with recursion operators

Computer Aided Formal Reasoning
Exercise 2

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.

Computer Aided Formal Reasoning