Advanced exercises
Computer Aided Formal Reasoning
Exercise 3
Deadline: Friday,13 December 1996
Please submit your module(s) by Email to <jlu@dcs.ed.ac.uk>
 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.

 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.
 Prove
{k,n:nat}(Lt zero k) > Lt (mod n k) k
.

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