CS 3220 Processor Design
Fall 2002

Instructor: Pete Manolios

Homework 4, Due 11/8/2002 (before midnight)

This will be a group project. Groups of size 2-4 are allowed. Please form groups on your own (perhaps by using the newsgroup). The goal of this homework is to familiarize you with proving theorems using paper and pencil (i.e., without the theorem prover). We will look at functions that manipulate sets because they are relatively simple and also tend to be useful to have around. Make sure that you have read chapters 6 and 7 of the Computer Aided Reasoning book.

A set is a list of ACL2 objects. An object is in a set if it is one of its elements. For example the list (1 2 1) has two elements: 1 and 2.

  1. Define in so that (in a x) returns t if a is in x and nil otherwise.
  2. Define =< so that (=< x y) returns t if every element in x is in y and nil otherwise.
  3. Define == so that (== x y) returns t if x and y have exactly the same elements and nil otherwise, e.g., (== '(1 2 1) '(2 1)).
  4. Define set-union so that the elements in (set-union x y) are exactly those that are either in x or in y.
  5. Define set-intersection so that the elements in (set-intersection x y) are exactly those that are both in x and in y.
Prove the following theorems. You do not have to justify propositional reasoning in your proofs: you can just say "by propositional logic" or something similar. Also, basic arithmetic facts do not have to be justified. By this I mean any of the standard number theory and algebra you learned in high school can be used without proof. Also, you can use the fact that acl2-count and len always return a natural number, so that both (e0-ordinalp (acl2-count x)) and (e0-ordinalp (len x)) are theorems.
  1. (=< x x) (reflexivity of =<).
  2. (== x x) (reflexivity of ==).
  3. (implies (== x y) (== y x)) (symmetry of ==).
  4. (implies (and (=< x y) (=< y z)) (=< x z)) (transitivity of =<).
  5. (implies (and (== x y) (== y z)) (== x z)) (transitivity of ==).
  6. (=< x (set-union x y))
  7. (== (set-union x y) (set-union y x))
  8. (iff (in a (set-union x y)) (or (in a x) (in a y)))
  9. (== (set-union (set-union x y) z) (set-union x (set-union y z)))
  10. (=< (set-intersection x y) x)
  11. (== (set-intersection x y) (set-intersection y x))
  12. (iff (in a (set-intersection x y)) (and (in a x) (in a y)))
  13. (== (set-intersection (set-intersection x y) z) (set-intersection x (set-intersection y z)))
Send one file, either text, pdf, or postscript, with your answers via email to both Vernard (vernard@cc) and myself.