Programming with recursion operators

Computer Aided Formal Reasoning
Exercise 2
Deadline: Monday, 25 November 1996

Please submit your module(s) by Email to <>

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