Advanced exercises

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

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.

2. 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.