Read chapters 8, 9, and 10 of CAR. Try some of the exercises in chapter 11 to gain some experience using ACL2s.
Your homework assignment consists of two problems. Send your proof scripts to the grader and cc me by 11:59PM on December 2nd. You can work in pairs, but everyone should understand all the proofs. Also, all the proofs should use "ACL2s" mode of the ACL2 Sedan.
(1 2 1)has two elements:
(in a x)returns
(=< x y)returns
tif every element in
(== x y)returns
yhave exactly the same elements and
(== '(1 2 1) '(2 1)).
(set-union x y)are exactly those that are either in
(set-intersection x y)are exactly those that are both in
Prove the following theorems using ACL2.
Define insertion sort so that it sorts any list of ACL2 objects. Note that the ACL2 universe can be totally ordered, so here is the definition of ordered:
and here is the definition of a permutation.
(defun <<= (x y) (lexorder x y)) (defun orderedp (x) (cond ((atom x) (null x)) (t (or (null (cdr x)) (and (<<= (car x) (cadr x)) (orderedp (cdr x)))))))
Prove the following theorems:
(defun in (a X) (cond ((atom X) nil) ((equal a (car X)) t) (t (in a (cdr X))))) (defun remove-el (a x) (cond ((atom x) nil) ((equal a (car x)) (cdr x)) (t (cons (car x) (remove-el a (cdr x)))))) (defun perm (x y) (cond ((atom x) (atom y)) (t (and (in (car x) y) (perm (cdr x) (remove-el (car x) y))))))
Define insertion the function isort (insertion sort) and prove the following theorems.
(defequiv perm) (defcong perm perm (append x y) 1) (defcong perm perm (append x y) 2) (defcong perm perm (cons x y) 2) (defcong perm perm (remove-el x y) 2) (defcong perm equal (in x y) 2)
(defthm ordered-sort (orderedp (isort x))) (defthm perm-sort (perm (isort x) x)) (defthm main (equal (perm x y) (equal (isort x) (isort y)))) (defthm main2 (implies (and (orderedp x) (perm x y)) (equal (isort y) x))) (defthm main3 (implies (and (orderedp x) (orderedp y) (perm x y)) (equal x y)))
Last modified: Sun Mar 19 15:45:28 EST 2006