Problem 1: Power Hour

Consider the following Racket definition

(define pow
  (lambda (x y)
    (if (zero? y)
        1
        (* x (pow x (- y 1))))))

Prove the following claim using mathematical induction. You may take the shortcut of evaluating a recursive function call directly to the branch that it selects in a single step.

In your proof, you can assume that the following lemma about pow holds:

In your proof, make sure to be explicit where you invoke both this lemma and your induction hypothesis.

Problem 2: Down By More Than One

Consider the following recursive Racket definitions:

(define even?
  (lambda (n)
    (cond [(zero? n) #t]
          [(= n 1)   #f]
          [else      (even? (- n 2))])))

(define iterate
  (lambda (f x n)
    (if (zero? n)
        x
        (iterate f (f x) (- n 1)))))

For this problem, you may take the shortcut of evaluating a recursive function call directly to the branch that it selects in a single step.

1. First prove the following auxiliary claim about even:

   Lemma: For any natural number n, if (even? n) and n is not zero then (<= 2 n).

2. Consider the following claim about iterate:

   For all natural numbers n and booleans b, if (even? n) then (iterate not b n) ≡ b.

   In a sentence or two, describe at a high-level why this claim is correct.

3. Formally prove this claim, using the auxiliary claim from part (a).

Problem 3: Absolute Reasoning

Consider the following code snippet, which computes \(|x-y|\):

# x and y are previously defined

if x < y:
    z = y - x
else:
    z = x - y

Prove the following claim about this code using our conditional rule:

Note that to prove this, it is sufficient to show that the proposition is a postcondition of this code without any required preconditions.