Maximums and Minimums

Purpose of exercise

Activities

Terminology

Requirements

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

Properties

  1. If xs is a non-empty true-list of rational numbers, then (maximum xs) is a rational number
  2. The value (maximum xs) occurs in the list xs
  3. The value (maximum xs) is at least as large as any element in xs
  4. If xs is a non-empty true-list of measure pairs, then (minimum-pair xs) is a measure-pair
  5. If xs is a non-empty true-list of measure-pairs, then (minimum-pair xs) is an element of xs
  6. 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

Note