Solutions for homework 3, proofs as described in class
Question 1:
See official answer sheet on the web page
http://www.ccs.neu.edu/course/csu290/assignments.html
----------------------------------------------------------------------
Question 2:
Assuming
(= (length (append x y))
(+ (length x) (length y)))
prove
(= (length (append x y))
(length (append y x)))
Proof:
(= (length (append x y)) (length (append y x)))
by assumption: (length (append a b)) = (+ (length a) (length b))
(= (+ (length x) (length y)) (length (append y x)))
by arithmetic: + is commutative, i.e. a+b = b+a
(= (+ (length y) (length x)) (length (append y x)))
by assumption: (length (append a b)) = (+ (length a) (length b))
(= (length (append y x)) (length (append y x)))
----------------------------------------------------------------------
Question 3:
Assuming
(natp (length y))
prove
(and (implies (endp x)
(= (length (append x y))
(+ (length x) (length y))))
(implies (and (not (endp x))
(= (length (append (cdr x) y))
(+ (length (cdr x)) (length y))))
(= (length (append x y))
(+ (length x) (length y)))))
Written in the notation from class, this is just:
(endp x) => (= (length (append x y))
(+ (length x) (length y)))
/\
(not (endp x)) /\ (= (length (append (cdr x) y))
(+ (length (cdr x)) (length y)))
=> (= (length (append x y))
(+ (length x) (length y)))
We saw that to prove something of the form F/\G, it suffices to prove
F and G separately. So let's first prove
(endp x) => (= (length (append x y))
(+ (length x) (length y)))
by definition of append
(endp x) => (= (length (if (endp x) y (cons (car x) (append (cdr x) y))))
(+ (length x) (length y)))
by endp and if axioms
(endp x) => (= (length y)
(+ (length x) (length y)))
by definition of length (we figure that length x is 0, right,
since x is endp?)
(endp x) => (= (length y)
(+ (if (endp x) 0 (+ 1 (length (cdr x)))) (length y)))
by endp and if axioms
(endp x) => (= (length y)
(+ 0 (length y)))
by arithmetic
(endp x) => (= (length y)
(length y))
Now, we prove the other conjunct:
(not (endp x)) /\ (= (length (append (cdr x) y))
(+ (length (cdr x)) (length y)))
=> (= (length (append x y))
(+ (length x) (length y)))
Let C be the context (not (endp x)) /\ (= (length (append (cdr x) y))
(+ (length (cdr x)) (length y)))
where A1 : (not (endp x))
A2 : (= (length (append (cdr x) y))
(+ (length (cdr x)) (length y)))
So we must prove
C => (= (length (append x y))
(+ (length x) (length y)))
by definition of append
C => (= (length (if (endp x) y (cons (car x) (append (cdr x) y))))
(+ (length x) (length y)))
by A1 and if axiom
C => (= (length (cons (car x) (append (cdr x) y)))
(+ (length x) (length y)))
by definition of length
C => (= (if (endp (cons (car x) (append (cdr x) y)))
0
(+ 1 (length (cdr (cons (car x) (append (cdr x) y))))))
(+ (length x) (length y)))
by endp and if axioms (recall that (endp (cons a b)) is false
C => (= (+ 1 (length (cdr (cons (car x) (append (cdr x) y)))))
(+ (length x) (length y)))
by cdr axiom
C => (= (+ 1 (length (append (cdr x) y)))
(+ (length x) (length y)))
by A2
C => (= (+ 1 (+ (length (cdr x)) (length y)))
(+ (length x) (length y)))
by definition of length
C => (= (+ 1 (+ (length (cdr x)) (length y)))
(+ (if (endp x) 0 (+ 1 (length (cdr x)))) (length y)))
by A1 and if axiom
C => (= (+ 1 (+ (length (cdr x)) (length y)))
(+ (+ 1 (length (cdr x))) (length y)))
by arithmetic (associativity of +)
C => (= (+ 1 (+ (length (cdr x)) (length y)))
(+ 1 (+ (length (cdr x)) (length y))))
----------------------------------------------------------------------
Question 4:
Prove
(and (implies (endp x)
(= (length (suffixes x))
(+ 1 (length x))))
(implies (and (not (endp x))
(= (length (suffixes (cdr x)))
(+ 1 (length (cdr x)))))
(= (length (suffixes x))
(+ 1 (length x)))))
Again, translating:
(endp x) => (= (length (suffixes x))
(+ 1 (length x)))
/\
(not (endp x)) /\ (= (length (suffixes (cdr x)))
(+ 1 (length (cdr x))))
=> (= (length (suffixes x))
(+ 1 (length x)))
We prove each conjunct separately. The proofs are very similar to
those in Question 3.
(endp x) => (= (length (suffixes x))
(+ 1 (length x)))
by definition of suffixed
(endp x) => (= (length (if (endp x) (list nil) (cons x (suffixes (cdr x)))))
(+ 1 (length x)))
by endp and if axioms
(endp x) => (= (length (list nil))
(+ 1 (length x)))
by definition of length (remember that (list nil) is just
(cons nil nil))
(endp x) => (= (if (endp (cons nil nil)) 0 (+ 1 (length (cdr (cons nil nil)))))
(+ 1 (length x)))
by endp and if axioms
(endp x) => (= (+ 1 (length (cdr (cons nil nil))))
(+ 1 (length x)))
by cdr axioms
(endp x) => (= (+ 1 (length nil))
(+ 1 (length x)))
by definition of length (applied twice), endp and if axioms
(endp x) => (= (+ 1 0)
(+ 1 0))
To prove the second conjuntion, let C be the context
(not (endp x)) /\ (= (length (suffixes (cdr x)))
(+ 1 (length (cdr x))))
And let A1 : (not (endp x))
A2: (= (length (suffixes (cdr x)))
(+ 1 (length (cdr x))))
C => (= (length (suffixes x))
(+ 1 (length x)))
by definition of suffixed
C => (= (length (if (endp x) (list nil) (cons x (suffixes (cdr x)))))
(+ 1 (length x)))
by A1 and if axiom
C => (= (length (cons x (suffixes (cdr x))))
(+ 1 (length x)))
by definition of elngth
C => (= (if (endp (cons x (suffixes (cdr x))))
0
(+ 1 (length (cdr (cons x (suffixes (cdr x)))))))
(+ 1 (length x)))
by endp and if axioms
C => (= (+ 1 (length (cdr (cons x (suffixes (cdr x))))))
(+ 1 (length x)))
by cdr axiom and A2
C => (= (+ 1 (+ 1 (length (cdr x))))
(+ 1 (length x)))
by definition of length
C => (= (+ 1 (+ 1 (length (cdr x))))
(+ 1 (if (endp x) 0 (+ 1 (length (cdr x))))))
by A1 and if axiom
C => (= (+ 1 (+ 1 (length (cdr x))))
(+ 1 (+ 1 (length (cdr x)))))
----------------------------------------------------------------------
Question 5:
Prove
(and (implies (endp x)
(= (length (mapcons a x))
(length x)))
(implies (and (not (endp x))
(= (length (mapcons a (cdr x)))
(length (cdr x))))
(= (length (mapcons a x))
(length x))))
Same deal as above. First we translate:
(endp x) => (= (length (mapcons a x))
(length x))
/\
(not (endp x)) /\ (= (length (mapcons a (cdr x)))
(length (cdr x)))
=> (= (length (mapcons a x))
(length x))
Then we prove each conjunct separately.
(endp x) => (= (length (mapcons a x))
(length x))
by definition of mapcons
(endp x) => (= (length (if (endp x) nil (cons (cons a (car x))
(mapcons a (cdr x)))))
(length x))
by endp and if axioms
(endp x) => (= (length nil)
(length x))
by definition of length (applied twice), endp and if axioms
(endp x) => (= 0 0)
Now, to prove the second conjunct, let C be the context
(not (endp x)) /\ (= (length (mapcons a (cdr x)))
(length (cdr x)))
and let A1 : (not (endp x))
A2 : (= (length (mapcons a (cdr x)))
(length (cdr x)))
C => (= (length (mapcons a x))
(length x))
by definition of mapcons
C => (= (length (if (endp x) nil (cons (cons a (car x))
(mapcons a (cdr x)))))
(length x))
by A1 and if axiom
C => (= (length (cons (cons a (car x))
(mapcons a (cdr x))))
(length x))
by definition of length
C => (= (if (endp (cons (cons a (car x)) (mapcons a (cdr x))))
0
(+ 1 (length (cdr (cons (cons a (car x))
(mapcons a (cdr x)))))))
(length x))
by endp, if, and cdr axioms
C => (= (+ 1 (length (mapcons a (cdr x))))
(length x))
by A2
C => (= (+ 1 (length (cdr x)))
(length x))
by definition of length
C => (= (+ 1 (length (cdr x)))
(if (endp x) 0 (+ 1 (length (cdr x)))))
by A1 and if axiom
C => (= (+ 1 (length (cdr x)))
(+ 1 (length (cdr x))))
----------------------------------------------------------------------
Question 6:
Assuming
(= (sum (append x y))
(+ (sum x) (sum y)))
prove
(endp x) => (= (sum (reverse x))
(sum x)))
/\
(not (endp x)) /\ (= (sum (reverse (cdr x)))
(sum (cdr x)))
=> (= (sum (reverse x))
(sum x))
(I've done the conversion already.)
Again, this is a conjunction, so we prove each conjunct separately.
First:
(endp x) => (= (sum (reverse x))
(sum x)))
by definition of reverse
(endp x) => (= (sum (if (endp x) nil (append (reverse (cdr x))
(list (car x)))))
(sum x))
by endp and if axioms
(endp x) => (= (sum nil)
(sum x))
by definition of sum (applied twice), endp and if axioms
(endp x) => (= 0 0)
Now, for the other conjunct. Let C be the context
(not (endp x)) /\ (= (sum (reverse (cdr x)))
(sum (cdr x)))
and let A1 : (not (endp x))
A2 : (= (sum (reverse (cdr x)))
(sum (cdr x)))
C => (= (sum (reverse x))
(sum x))
by definition of reverse
C => (= (sum (if (endp x) nil (append (reverse (cdr x))
(list (car x)))))
(sum x))
by A1 and if axiom
C => (= (sum (append (reverse (cdr x))
(list (car x))))
(sum x))
by our assumption - this is the tricky bit, we use the assumption
instead of expanding append...
C => (= (+ (sum (reverse (cdr x)))
(sum (list (car x))))
(sum x))
by A2
C => (= (+ (sum (cdr x))
(sum (list (car x))))
(sum x))
by definition of sum (and remembering that (list (car x)) is just
(cons (car x) nil))
C => (= (+ (sum (cdr x))
(if (endp (cons (car x) nil))
0
(+ (car (cons (car x) nil))
(sum (cdr (cons (car x) nil))))))
(sum x))
by endp and if axioms; and car and cdr axioms
C => (= (+ (sum (cdr x))
(+ (car x)
(sum nil)))
(sum x))
by definiition of sum, endp and if axioms
(this gives us that (sum nil) is 0) and arithmtic (+ a 0) = a
C => (= (+ (sum (cdr x))
(car x))
(sum x))
by definition of sum
C => (= (+ (sum (cdr x))
(car x))
(if (endp x) 0 (+ (car x) (sum (cdr x)))))
by A1 and if axiom
C => (= (+ (sum (cdr x))
(car x))
(+ (car x) (sum (cdr x))))
by arithemtic (associativity of +)
C => (= (+ (car x) (sum (cdr x)))
(+ (car x) (sum (cdr x))))
----------------------------------------------------------------------
Question 7:
Assuming
(= (length (append x y))
(+ (length x) (length y)))
/\
(= (length (mapcons a x))
(length x)))
prove
(endp x) => (= (length (powerlist x))
(expt 2 (length x)))
/\
(not (endp x)) /\ (= (length (powerlist (cdr x)))
(expt 2 (length (cdr x))))
=> (= (length (powerlist x))
(expt 2 (length x)))
Again, we prove this conjunction by proving each conjunct separately.
First conjunct:
(endp x) => (= (length (powerlist x))
(expt 2 (length x)))
by definition of powerlist
(endp x) => (= (length (if (endp x)
(list nil)
(append (powerlist (cdr x))
(mapcons (car x) (powerlist (cdr x))))))
(expt 2 (length x)))
by endp and if axioms
(endp x) => (= (length (list nil))
(expt 2 (length x)))
by definitio of length, and knowing that (list nil) is just (cons nil nil)
(endp x) => (= (if (endp (cons nil nil)) 0 (+ 1 (length (cdr (cons nil nil)))))
(expt 2 (length x)))
by endp and if axioms
(endp x) => (= (+ 1 (length (cdr (cons nil nil))))
(expt 2 (length x)))
by cdr axiom
(endp x) => (= (+ 1 (length nil))
(expt 2 (length x)))
by definition of length; endp and if axioms and arithmetic (+ 1 0) = a
(endp x) => (= 1
(expt 2 (length x)))
by definition of length
(endp x) => (= 1
(expt 2 (if (endp x) 0 (+ 1 (length (cdr x))))))
by endp and if axiom
(endp x) => (= 1
(expt 2 0))
by arithmetic
(endp x) => (= 1 1)
Now, the second conjunct. (Chances are, we are going to need our assumptions here, so let's name them.)
A1 : (= (length (append x y))
(+ (length x) (length y)))
A2 : (= (length (mapcons a x))
(length x)))
Let C be the context of the formula to be proved:
(not (endp x)) /\ (= (length (powerlist (cdr x)))
(expt 2 (length (cdr x))))
and let A3 : (not (endp x))
A4 : (= (length (powerlist (cdr x)))
(expt 2 (length (cdr x))))
C => (= (length (powerlist x))
(expt 2 (length x)))
by definition of powerlist
C => (= (length (if (endp x)
(list nil)
(append (powerlist (cdr x))
(mapcons (car x) (powerlist (cdr x))))))
(expt 2 (length x)))
by A3 and if axiom
C => (= (length (append (powerlist (cdr x))
(mapcons (car x) (powerlist (cdr x)))))
(expt 2 (length x)))
by A1 (instead of expanding a bunch of stuff)
C => (= (+ (length (powerlist (cdr x)))
(length (mapcons (car x) (powerlist (cdr x)))))
(expt 2 (length x)))
by A2 (again, instead of expanding a bunch of stuff)
C => (= (+ (length (powerlist (cdr x)))
(length (powerlist (cdr x))))
(expt 2 (length x)))
by arithmetic
C => (= (* 2 (length (powerlist (cdr x))))
(expt 2 (length x)))
by A4
C => (= (* 2 (expt 2 (length (cdr x))))
(expt 2 (length x)))
by definition of length
C => (= (* 2 (expt 2 (length (cdr x))))
(expt 2 (if (endp x) 0 (+ 1 (length (cdr x))))))
by A3 and if axiom
C => (= (* 2 (expt 2 (length (cdr x))))
(expt 2 (+ 1 (length (cdr x)))))
by arithmetic ( 2 * 2^a = 2^(a+1) )
C => (= (expt 2 (+ 1 (length (cdr x))))
(expt 2 (+ 1 (length (cdr x)))))