Nat-Nat Problems

Problem 1. Write the functions max and monus, where

    (claim max
      (-> Nat Nat Nat))

is the usual max function, e.g.,

    > (max 3 7)
    (the Nat 7)

and where

    (claim monus
      (-> Nat Nat Nat))

is zero-truncated subtraction, e.g.,

    > (monus 7 3)
    (the Nat 4)
    > (monus 3 7)
    (the Nat 0)

Problem 2. The max and min definitions (along with the max-monus-theorem) follow a similar programming pattern in defining a binary function on Nat via a recursion on both arguments simultaneously. Define a function rec-Nat-Nat that captures this recursion, and use it to give alternative definitions of max and monus along with min and diff, where diff gives the distance between two Nats, e.g.,

    > (diff 7 3)
    (the Nat 4)
    > (diff 3 7)
    (the Nat 4)

Problem 3. Prove the following theorem relating max and monus:

    (claim max-monus-theorem
        (Pi ((m Nat)
             (n Nat))
            (= Nat (max m n) (+ m (monus n m)))))

Note: This is a hard problem, and requires persistence and planning.

Problem 4. The emergence of rec-Nat-Nat raises an intriguing possibility. The proof of the commutativity of + typically requires first proving a couple of theorems that essentially symmetrize it, i.e.,

    (claim +zero
        (Pi ((m Nat))
            (= Nat (+ m 0) m)))

and

    (claim +succ
        (Pi ((m Nat)
             (n Nat))
            (= Nat (+ m (add1 n)) (add1 (+ m n)))))

An attractive possibility is to define plus via rec-Nat-Nat, an alternative definition of addition which is already symmetric, based on the following equations for addition:

    0 + 0 = 0
    m + 0 = m
    0 + n = n
    (m+1) + (n+1) = 2 + (m+n)

With this definition, the hard case of proving commutativity is in showing that if

    m + n = n + m

then

    (m+1) + (n+1) = (n+1) + (m+1).

But this is easy to argue directly:

    (m+1) + (n+1)
    = 2 + (m+n)         definition of +
    = 2 + (n+m)         inductive hypothesis
    = (n+1) + (m+1)     definition of +

Formalizing this approach first requires generalizing rec-Nat-Nat to ind-Nat-Nat, and giving a simple formal proof of comm-plus.

Problem 5. Prove that plus and + are the same function, and use this to infer that the usual addition is commutative via comm-plus.

Problem 6. Formulate another theorem, along the lines of max-monus-theorem of Problem 3, but relating min, max, and diff, and use ind-Nat-Nat to prove it.