Assignment #1: COS 441

Due by midnight on Wednesday September 24.  Either hand in in class or
deliver to Rob's office.  You mail also email a completed assignment
to him at rdockins@princeton.edu.  Please put "COS 441 A1" in the
subject line of any such email.

0. (a) [0 Points] Subscribe to the course mailing list.  All students
   in COS 441 are required to sign up for the class mailing list.  If
   you have questions about assignments or other information you can
   send email to cos441 "atsign" lists.cs.princeton.edu.

To subscribe to the list go to
https://lists.cs.princeton.edu/mailman/listinfo/cos441.

  (b) [0 Points] The next assignment will involve some programming in
  SML.  Get yourself prepared for next week by: 
  
  (1) Finding a reference manual for SML either online or in the bookstore
             (see course home page for details) 
  (2) Figuring out how to install and run the SML compiler, 
             (see course home page for details) 
  (3) Writing the "hello world" program that prints out "hello world".

One of the important elements of this class is learning how to write
down proofs of properties in a clear, precise and exacting fashion.
You will be graded both on correctness and clarity of your proofs.
Hand-waving is not acceptable! Normally, you will lay out your proofs
in a similar way as in this document.  In particular, always remember
to state the proof methodology you are using in your proof ("Induction
on ...").  Points will be automatically deducted from answers in which
the proof methodology is not stated clearly.

There are 15 points to gain on this assignment.

Use the following inductive definitions of natural numbers,
addition and lists from class:

                    |- n nat
-----------         -------------
|- Z nat            |- S n nat

 
|- n nat            |- add n1 n2 n3      
-------------       -------------------------
|- add Z n n        |- add (S n1) n2 (S n3)

                       |- n nat    |- l list
-----------            -----------------------
|- nil list            |- cons (n,l) list


1. (a) [1 Point] Define a judgement |- length l n that is valid when n is the
length of l.

(b) [1 Point] Given your definition, prove that this judgement is valid:

    |- length (cons (S S Z, cons (Z, nil)))  (S S Z)


2. [1 Point] Define a judgement |- sum l n that is valid when n is the
sum of all of the elements of l. For example:

    |- sum (cons (S Z, cons (S Z, Nil))  (S S Z)

is valid.


3. [3 Points] Inductively define multiplication as the repeated
addition of natural numbers.  Here is the judgment form:

    |- mult n1 n2 n3

The following should be valid judgments (among many others of course):

    |- mult Z (S Z) Z

    |- mult (S Z) (S Z) (S Z)

    |- mult (S S Z) (S S Z) (S S S S Z)


4. [2 Points] Convert the following recursive equations into an 
inductively defined relation in our notation

    fact(0) = 1
    fact(n+1) = (n+1) * fact(n)


5. [2 Points] Prove Lemma 1.

Lemma 1:  For all n such that |- n nat,
|- add n Z n is valid.


6.  [2 Points] Prove Lemma 2.

Lemma 2:  For all n1, n2, n3,
if |- add n1 n2 n3 then |- add n1 (S n2) (S n3). 


7.  [3 Points] Prove that addition is commutative.  In other words, prove
theorem 3.

Theorem 3: For all n1, n2, n3,
if |- add n1 n2 n3 then |- add n2 n1 n3.

Hint: You may want to use Lemma 1 and/or Lemma 2.  Define and prove
other auxiliary lemmas if you need to.