CS 8803 Computational Logic
Spring 2005

Homework 6, Due 4/20/2005 before class

Read chapters 8, 9, and 10. Try some of the exercises in chapter 11 to gain some experience using ACL2.

Your homework assignment consists of two problems. Send me the ACL2 proof scripts by 4:30PM on April 20th. You can work in pairs, but everyone should understand all the proofs.

1. This exercise will require you to build a simple library for reasoning about "flat" sets. A flat 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 using ACL2.

   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)))

2. 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:

   
   (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)))))))
   
   

   and here is the definition of a permutation.

   
   (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))))))
   
   

   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)
   
   

   Define insertion the function isort (insertion sort) and prove the following theorems.

   
   (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)))