Homework #8

Due Mon, 19 Mar @ 5:00 PM

1. Using an accumulator-style definition of product, prove (in ACL2):

   (product (append xs ys)) = (* (product xs) (product ys))

2. Use accumulator-style to develop a program largest that produces the biggest number in a non-empty list of numbers. Prove (in ACL2) that the result it delivers is

   1. larger than or equal to all of the members of the list, and

   2. contained in the list.

   For the second theorem, you'll probably need to prevent ACL2 from using the definition of the membership predicate. To do that, use a hint like:

   (defthm Theorem-2
     ... the-theorem ...
     :hints (("Goal" :in-theory (disable member-equal))))

3. Develop an accumulator-style reverse; call it rev so you don't collide with the built-in reverse.

   Prove that (rev (rev xs)) = xs for xs:List[Any].

4. Convince ACL2 that quick sort is equivalent to insertion sort.