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.
- Define in so that (in a x) returns
t if a is in x and nil
otherwise.
- Define =< so that (=< x y) returns
t if every element in x is in y and nil
otherwise.
- 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)).
- Define set-union so that the elements in
(set-union x y) are exactly those that are either
in x or in y.
- 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.
- (=< x x) (reflexivity of =<).
- (== x x) (reflexivity of ==).
- (implies (== x y) (== y x))
(symmetry of ==).
- (implies (and (=< x y) (=< y z)) (=< x z))
(transitivity of =<).
- (implies (and (== x y) (== y z)) (== x z))
(transitivity of ==).
- (=< x (set-union x y))
- (== (set-union x y) (set-union y x))
- (iff (in a (set-union x y)) (or (in a x) (in a y)))
- (== (set-union (set-union x y) z) (set-union x (set-union y z)))
- (=< (set-intersection x y) x)
- (== (set-intersection x y) (set-intersection y x))
- (iff (in a (set-intersection x y)) (and (in a x) (in a y)))
- (== (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.