Induction Practice
------------------
These notes contain examples of structural induction principles and induction proofs.  To benefit from them, you'll have to try to do the proofs yourself and then check your work.


Tree ::= Atom | (cons Tree Tree)

SIP:  all a:Atom.(p? a)
      all x,y:Tree.(p? x) & (p? y) -> (p? (cons x y))
      -----------------------------------------------
      all x:Tree.(p? x)

;; Tree -> Tree
;; flip a tree about its root.
(defun mirror (tree)
  (cond ((atom tree) tree)
	((consp tree)
	 (cons (mirror (cdr tree))
	       (mirror (car tree))))))

Theorem 1:  all x:Tree.(mirror (mirror x)) = x.
Proof:  We proceed by structural induction on x.
;; Note: the SIP is applicable because we take p? to be:
;;   (defun p? (x) (equal (mirror (mirror x)) x))

(1) case x = a, an arbitrary Atom.
    (mirror (mirror a)) = (mirror a) = a   [use defn of mirror twice]

(2) case x = (cons left right).
    Assume (mirror (mirror left))  = left and
	   (mirror (mirror right)) = right.

    (mirror (mirror (cons left right)))
      = (mirror (cons (mirror right) (mirror left)))  [defn of mirror]
      = (cons (mirror (mirror left))
	      (mirror (mirror right)))		      [defn of mirror]
      = (cons left right)			      [Induction Hypotheses]

Thus, using the structural induction principle for Tree, we conclude
  all x:Tree.(mirror (mirror x)) = x.

Q.E.D.

Theorem 2:  all x:Tree.(mirror (mirror (mirror x))) = (mirror x).
Proof:  Trivial:  apply the last theorem.  Q.E.D.

If you didn't think of the easy proof, that's okay.  Induction works too.

Proof #2:  We proceed by structural induction on x.
;; The SIP applies if we take
;; (defun p? (x) (equal (mirror (mirror (mirror x))) (mirror x)))

(1) case x = a.  Use the defn of mirror twice:
    (mirror (mirror (mirror a)))
      = (mirror (mirror a))
      = (mirror a)

(2) case x = (cons left right).
    Assume (mirror (mirror (mirror left)))  = (mirror left)
       and (mirror (mirror (mirror right))) = (mirror right).

    (mirror (mirror (mirror (cons left right))))
      = (mirror (mirror (cons (mirror right)		[defn mirror]
			      (mirror left))))		
      = (mirror (cons (mirror (mirror left))		[defn mirror]
		      (mirror (mirror right))))
      = (cons (mirror (mirror (mirror right)))		[defn mirror]
	      (mirror (mirror (mirror left))))
      = (cons right left)				[Induction Hypotheses]
      = (mirror (cons left right))			[defn mirror]

Thus, by the structural induction principle for Tree, we conclude
  all x:Tree. (mirror (mirror (mirror x))) = (mirror x).

Q.E.D.


HW 3, #2
--------
LoN ::= nil | (cons Number LoN)
SIP:  (p? nil)
      all xs:LoN.[(p? xs) -> all n:Number.(p? (cons n xs))]
      -----------------------------------------------------
      all x:LoN.(p? LoN)

;; sum-list : List[Number] -> Number
(defun sum-list (xs)
  (if (endp xs)
      0
    (+ (car xs) (sum-list (cdr xs)))))

;; append : List[X] List[X] -> List[X]
(defun append (xs ys)
  (if (endp xs)
      ys
    (cons (car xs) (append (cdr xs) ys))))

Theorem 3: all xs,ys:LoN.
           (sum-list (append xs ys)) = (+ (sum-list xs) (sum-list ys))
Proof:  Let ys be an arbitrary LoN, and proceed by structural induction on xs.
;; Note:  the SIP applies if we take
;; (defun p? (X) (equal (sum-list (append X ys)) (+ (sum-list X) ys)))

(1) case xs = nil.  
    (sum-list (append nil ys))
      = (sum-list ys)			  [defn of append]
      = (+ 0 (sum-list ys))		  [0 + a = a]
      = (+ (sum-list nil) (sum-list ys))  [defn of sum-list]

(2) case xs = (cons n zs), for arbitrary n:Number.
    Assume (sum-list (append zs ys)) = (+ (sum-list zs) (sum-list ys)).

    (sum-list (append (cons n zs) ys))		    
      = (sum-list (cons n (append zs ys)))	    [defn of append]
      = (+ n (sum-list (append zs ys)))		    [defn of sum-list]
      = (+ n (sum-list zs) (sum-list ys))	    [Induction Hypothesis]
      = (+ (sum-list (cons n zs)) (sum-list ys))    [defn of sum-list]

Thus, by structural induction for LoN,
  all xs,ys:LoN.(sum-list (append xs ys)) = (+ (sum-list xs) (sum-list ys))

Q.E.D.

;; Even Expressions
;; Even = Numbers divisible by 2.
EExp ::= (make-num Even) | (make-add EExp EExp) | (make-mul EExp EExp)

SIP:  all n:Even.(p? n)
      all e1,e2:EExp.[(p? e1) & (p? e2) -> (p? (make-add e1 e2))]
      all e1,e2:EExp.[(p? e1) & (p? e2) -> (p? (make-mul e1 e2))]
      -----------------------------------------------------------
      all e:EExp.(p? e)

;; evaluate : EExp -> Number
;; simplify an expression to its value
(defun evaluate (eexp)
  (cond ((num? eexp) (num-value eexp))
	((add? eexp) 
	 (+ (evaluate (add-left eexp)) 
	    (evaluate (add-right eexp))))
	((mul? eexp)
	 (* (evaluate (mul-left eexp))
	    (evaluate (mul-right eexp))))))

;; This theorem says that evaluate produces an even number for every EExp.
Theorem 4:  all e:EExp.(evenp (evaluate e))
Proof:  We proceed by structural induction on e.
;; The SIP applies because we take p? to be
;; (defun p? (e) (evenp (evaluate e)))

(1) case e = (make-num n) for arbitrary n:Even.
    We calculate:
    (evenp n)                            [assumption]
      = (evenp (evaluate (make-num n)))  [defn of evaluate]

(2) case e = (make-add el er).
    Assume (evenp (evaluate el)) /\ (evenp (evaluate er)).

    (evenp (evaluate el)) /\ (evenp (evaluate er))  [Induction Hypothesis]
      = (evenp (+ (evaluate el) (evaluate er)))	    [+ of evens is even]
      = (evenp (evaluate (make-add el er)))	    [defn of evaluate]

(3) case e = (make-mul el er).
    Assume (evenp (evaluate el)) /\ (evenp (evaluate er)).

    (evenp (evaluate el)) /\ (evenp (evaluate er))  [Induction Hypothesis]
      = (evenp (* (evaluate el) (evaluate er)))	    [* of evens is even]
      = (evenp (evaluate (make-mul el er)))	    [defn of evaluate]

Thus, by structural induction on EExp, 
  all e:EExp.(evenp (evaluate e)).

Q.E.D.