CS G379 Decision Procedures for Verification
Fall 2007

Homework 5, Due by the end of the day, 12/2/2007

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

   

   Last modified: Sun Mar 19 15:45:28 EST 2006