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