## Maximums and Minimums

### Purpose of exercise

- Practice writing equation-based programs
- Practice specifying correctness properties
- Use DrACuLa DoubleCheck for predicate-based, random testing
- Certify correctness properties using ACL2

### Activities

- Define the functions required below (here are some
predefined functions that you might find helpful)
- Package the functions in a book and certify it
- Define the predicates required below and package them in another book (the
"test book")
- Package DoubleCheck tests for the properties stated below in the test
book, and run some tests
- Convert the DoubleCheck predicates to ACL2 theorems, package them in another book (the "verification book"), and certify it

### Terminology

*measure pair:* a two-element list whose first element, a rational
number, is the *measure* of its other element
*true-list*: nil or (cons x xs), where xs is a true-list

### Requirements

- Define a function,
*maximum*, that delivers the largest value
in a non-empty list of rational numbers.
- Define a function,
*min-pair*, that delivers the smaller of two
measure-pairs.
- Define a function,
*minimium-pair*, that delivers the smallest
measure-pair from a non-empty list of measure-pairs.
- Define a predicate,
*measure-pairp*, that is true if and only
if its argument is a measure-pair.
- Define a predicate,
*measure-pair-listp*, that is true if and
only if its argument is a true-list of measure-pairs.

### Properties

- If xs is a non-empty true-list of rational numbers, then (maximum xs) is a
rational number
- The value (maximum xs) occurs in the list xs
- The value (maximum xs) is at least as
large as any element in xs
- If xs is a non-empty true-list of measure pairs, then (minimum-pair xs) is
a measure-pair
- If xs is a non-empty true-list of measure-pairs, then (minimum-pair xs) is an
element of xs
- If xs is a true-list of measure-pairs, then no element of xs has a smaller
measure than (minimum-pair xs)

### ACL2 functions useful in this exercise

- max
- true-listp
- rationalp
- rational-listp
- member-equal

### Note

- The ACL2 intrinsic
*member* is more efficient *member-equal*,
but member-equal can check for the occurrence of any kind of value in a
list, while member is reliable only for numbers, characters, and symbols.