Advanced exercises

Computer Aided Formal Reasoning
Exercise 3
Deadline: Friday,13 December 1996

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

  1. Implement the abstract data type of arrays (available here) using lists. You might want to look at lib_adt_basics, the library module which defines ADT operations.

    1. Define functions div:nat->nat->nat and mod:nat->nat->nat which, when given arguments n and k compute the integer part of n divided by k and the remainder. Since n divided by zero is undefined, you can either exclude it directly by defining your function so that div n k is really n divided by (suc k) (and similarly for mod) or you can return some other value (like n). If you choose the first option, remove the assumption Lt zero k from the following problems.

    2. Prove {k,n:nat}(Lt zero k) -> Lt (mod n k) k .

    3. Extra credit: Prove {k:nat}{n:nat}(Lt zero k) -> Eq n (plus (mod n k) (times k (div n k))).

    Hint: you may wish to look at the libraries on boolean valued relations and all order relations.
Computer Aided Formal Reasoning