This homework was a bit too difficult for a week's effort during finals preparation, as we found out. Here is my solution to the game and proofs.
Here is a simple graphical program in ACL2s.
(include-book "graphics" :dir :acl2s :ttags :all) (defun presenter (conf pr) (declare (ignore conf)) (fill-oval 0 0 1 1 :red pr)) (set-configuration-presenter 'presenter) (set-initial-configuration (list 0)) (big-bang)
You will be presenting proofs of the following theorems using ACL2s in recursion and induction mode.
Given:
(defun matcol (A i)
(if (endp A)
nil
(cons (nth i A) (matcol (cdr A) i))))
(defun matcol*-acc (A i acc)
(if (endp A)
(rev acc)
(matcol*-acc (cdr A) i (cons (nth i A) acc))))
(defun matcol* (A i)
(matcol*-acc A i nil))
(defun sum-n (n)
(if (zp n)
0
(+ n (sum-n (- n 1)))))
(defun sum-n*-acc (n acc)
(if (zp n)
acc
(sum-n*-acc (- n 1) (+ n acc))))
(defun sum-n* (n)
(sum-n*-acc n 0))
Prove:
1. (equal (sum-n* n) (sum-n n)) 2. (equal (matcol* A i) (matcol A i))
We will be going through another mini version of the homework, answering questions and perhaps having you present your solutions. The lab exercises are here, and extra problems are here. I tried to make them easy, but not too much so. Try these if you feel the current proofs are really mindless. Update: (2009-Oct-31 15:52) solutions to the extra problems are here
Today we will be going through a mini version of the homework. You are expected to give solutions during the lab. The initial code for this lab is here.
I have written up a few more examples for you to solve. Solutions will be posted Tuesday. Download here (Update Oct20 15:37: Errors in last two problems corrected). Solutions here.
I expect you to have solutions ready for this lab. If you can't solve the problems, then do your best and be prepared to explain what you did and where you got stuck.
1. Substitution.
For each pair of ACL2 terms, give a substitution that instantiates the first to the second. Notice that it doesn't matter if you do not know how certain functions are defined (eg, mapcons) because it is irrelevant for this exercise.
a. (append a b)
(append x (append y z))
b. (append a b)
(append (mapcons n x) (append y z))
c. (mapcons a (append b c))
(mapcons (+ 1 (append x y)) (append (reverse z) z))
d. (append a (append b c))
(append (append (mapcons x y) (reverse z)) (append y (cons x w)))
e. (+ (- x y) z (* x w))
(+ (- (+ w y) (/ x y)) (* (expt 2 z) (expt 3 x)) (* (+ w y) x))
2. Prove the following >First, recall the following definitions. len and app will be used in problem 3 too.
(defun len (x)
(if (endp x)
0
(+ 1 (len (cdr x)))))
(defun app (x y)
(if (endp x)
y
(cons (car x) (app (cdr x) y))))
Second, assume that the following is a theorem (you don't have to prove it).
(= (len (app x y))
(+ (len x) (len y)))
Prove that the following is a theorem:
(= (len (app x y))
(len (app y x)))
3. Length of append
Assume that the following is a theorem (you don't have to prove it).
(natp (len y))
Prove that the following is a theorem:
(and (implies (endp x)
(= (len (app x y))
(+ (len x) (len y))))
(implies (and (consp x)
(= (len (app (cdr x) y))
(+ (len (cdr x)) (len y))))
(= (len (app x y))
(+ (len x) (len y)))))
Address common mistakes made on the second test.
Review for the test on propositional logic. A review exercise / quick overview is available here.
Address common mistakes made on the first test.
Addressing questions on homework and class material in preparation for the exam on Wednesday.
Today we will be focusing on getting everyone set up with the latest version of ACL2 Sedan. In the remaining time I expect you to present solutions to the following exercises, so please come prepared.
length - the function contract is list -> natural. obvious behavior - if the list is (a_0 a_1 ... a_n) return n. Example: ACL2>(length '(1 2 3)) 3 reverse - the function contract is list -> list the nth item of the input list should be the (- (length list) n 1)th item of the output list. Example: ACL2>(reverse '(1 2 3 4)) (LIST 4 3 2 1) sum-list - the function contract is list -> number again the behavior should be obvious, but I expect that if given a list of numbers (a_0 a_1 ... a_n) that your function will return (+ a_0 a_1 ... a_n) Example: ACL2>(sum-list '(1 2 4 8 16)) 31 rotate - the function contract is list -> natural -> list rotates a list i places to the left. Given a list of elements (a_0 a_1 ... a_n), return (a_i a_i+1 ... a_n a_0 a_1 ... a_i - 1). Example: ACL2>(rotate '(1 2 3 4 5 6) 3) (LIST 4 5 6 1 2 3)Example Solutions