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