$$ \newcommand{\setmin}{\mathbin{\backslash}} \newcommand{\symmdiff}{\mathbin{∆}} $$

6  Mathematical Induction

6.1. Proof by Mathematical Induction

Section 6.1 of HTPI introduces a new proof technique called mathematical induction. It is used for proving statements of the form ∀ (n : Nat), P n. Here is how it works (HTPI p. 273):

To prove a goal of the form ∀ (n : Nat), P n:

First prove P 0, and then prove ∀ (n : Nat), P n → P (n + 1). The first of these proofs is sometimes called the base case and the second the induction step.

For an explanation of why this strategy works to establish the truth of ∀ (n : Nat), P n, see HTPI. Here we focus on using mathematical induction in Lean.

To use mathematical induction in a Lean proof, we will use the tactic by_induc. If the goal has the form ∀ (n : Nat), P n, then the by_induc tactic leaves the list of givens unchanged, but it replaces the goal with the goals for the base case and induction step. Thus, the effect of the tactic can be summarized as follows:

>> ⋮
⊢ ∀ (n : Nat), P n

case Base_Case
>> ⋮
⊢ P 0
case Induction_Step
>> ⋮
⊢ ∀ (n : Nat), P n → P (n + 1)

To illustrate proof by mathematical induction in Lean, we turn first to Example 6.1.2 in HTPI, which gives a proof of the statement \(\forall n \in \mathbb{N} (3 \mid (n^3 - n))\). For reasons that we will explain a little later, we will prove a slightly different theorem: \(\forall n \in \mathbb{N} (3 \mid (n^3 + 2n))\). Here is a proof of the theorem, modeled on the proof in Example 6.1.2 of HTPI (HTPI pp. 276–277).

For every natural number \(n\), \(3 \mid (n^3 + 2n)\).

Proof. We use mathematical induction.

Base Case: If \(n = 0\), then \(n^3 + 2n = 0 = 3 \cdot 0\), so \(3 \mid (n^3 + 2n)\).

Induction Step: Let \(n\) be an arbitrary natural number and suppose \(3 \mid (n^3 + 2n)\). Then we can choose an integer \(k\) such that \(3k = n^3 + 2n\). Thus, \[\begin{align*} (n+1)^3 + 2(n+1) &= n^3 + 3n^2 + 3n + 1 + 2n + 2\\ &= (n^3 + 2n) + 3n^2 + 3n + 3\\ &= 3k + 3n^2 + 3n + 3\\ &= 3(k + n^2 + n + 1). \end{align*}\] Therefore \(3 \mid ((n+1)^3 + 2(n+1))\), as required.  □

Now let’s try writing the same proof in Lean. We start, of course, with the by_induc tactic.

theorem Like_Example_6_1_2 :
    ∀ (n : Nat), 3 ∣ n ^ 3 + 2 * n := by
  by_induc
  **done::

case Base_Case
⊢ 3 ∣ 0 ^ 3 + 2 * 0
case Induction_Step
⊢ ∀ (n : ℕ),
>>  3 ∣ n ^ 3 + 2 * n →
>>  3 ∣ (n + 1) ^ 3 +
>>      2 * (n + 1)

The base case is easy: The define tactic tells us that the goal means ∃ (c : Nat), 0 ^ 3 + 2 * 0 = 3 * c, and then apply Exists.intro 0 changes the goal to 0 ^ 3 + 2 * 0 = 3 * 0. Both sides are definitionally equal to 0, so rfl finishes off the base case. For the induction step, we begin, as in the HTPI proof, by introducing an arbitrary natural number n and assuming 3 ∣ n ^ 3 + 2 * n. This assumption is called the inductive hypothesis, so in the Lean proof we give it the identifier ih. Our goal now is to prove 3 ∣ (n + 1) ^ 3 + 2 * (n + 1).

theorem Like_Example_6_1_2 :
    ∀ (n : Nat), 3 ∣ n ^ 3 + 2 * n := by
  by_induc
  · -- Base Case
    define
    apply Exists.intro 0
    rfl
    done
  · -- Induction Step
    fix n : Nat
    assume ih : 3 ∣ n ^ 3 + 2 * n
    **done::
  done

case Induction_Step
n : ℕ
ih : 3 ∣ n ^ 3 + 2 * n
⊢ 3 ∣ (n + 1) ^ 3 +
>>      2 * (n + 1)

The rest of the Lean proof follows the model of the HTPI proof: we use the inductive hypothesis to introduce a k such that n ^ 3 + 2 * n = 3 * k, and then we use a calculational proof to show that (n + 1) ^ 3 + 2 * (n + 1) = 3 * (k + n ^ 2 + n + 1).

theorem Like_Example_6_1_2 :
    ∀ (n : Nat), 3 ∣ n ^ 3 + 2 * n := by
  by_induc
  · -- Base Case
    define         --Goal : ∃ (c : Nat), 0 ^ 3 + 2 * 0 = 3 * c
    apply Exists.intro 0
    rfl
    done
  · -- Induction Step
    fix n : Nat
    assume ih : 3 ∣ n ^ 3 + 2 * n
    define at ih   --ih : ∃ (c : Nat), n ^ 3 + 2 * n = 3 * c
    obtain (k : Nat) (h1 : n ^ 3 + 2 * n = 3 * k) from ih
    define         --Goal : ∃ (c : Nat), (n + 1) ^ 3 + 2 * (n + 1) = 3 * c
    apply Exists.intro (k + n ^ 2 + n + 1)
    show (n + 1) ^ 3 + 2 * (n + 1) = 3 * (k + n ^ 2 + n + 1) from
      calc (n + 1) ^ 3 + 2 * (n + 1)
        _ = n ^ 3 + 2 * n + 3 * n ^ 2 + 3 * n + 3 := by ring
        _ = 3 * k + 3 * n ^ 2 + 3 * n + 3 := by rw [h1]
        _ = 3 * (k + n ^ 2 + n + 1) := by ring
    done
  done

Next we’ll look at Example 6.1.1 in HTPI, which proves that for every natural number \(n\), \(2^0 + 2^1 + \cdots + 2^n = 2^{n+1} - 1\). Once again, we will change the theorem slightly before proving it in Lean. What we will prove is that for every \(n\), \((2^0 + 2^1 + \cdots + 2^n) + 1 = 2^{n+1}\). To understand this theorem you must be able to recognize what the “\(\cdots\)” stands for. A human reader will probably realize that the numbers being added up here are the numbers of the form \(2^i\), where \(i\) runs through all of the natural numbers from 0 to \(n\). But Lean can’t be expected to figure out this pattern, so we must be more explicit.

Section 6.3 of HTPI introduces the explicit notation that mathematicians usually use for such sums. If \(f\) is a function whose domain is the natural numbers, then \[ \sum_{i=0}^n f(i) = f(0) + f(1) + \cdots + f(n). \] More generally, if \(k \le n\) then \[ \sum_{i=k}^n f(i) = f(k) + f(k+1) + \cdots + f(n). \]

The notation we will use in Lean for this sum is Sum i from k to n, f i. Thus, a mathematician would state our theorem like this:

For every natural number \(n\), \[ \left(\sum_{i=0}^n 2^i\right) + 1 = 2^{n+1}. \]

And to state the same theorem in Lean, we will write:

theorem Like_Example_6_1_1 :
    ∀ (n : Nat), (Sum i from 0 to n, 2 ^ i) + 1 = 2 ^ (n + 1)

We will have more to say later about how the notation Sum i from k to n, f i is defined. But to use the notation in a proof, we will just need to know a few theorems. The #check command will tell us the meanings of the theorems sum_base, sum_step, and sum_from_zero_step:

@sum_base : ∀ {A : Type} [inst : AddZeroClass A] {k : ℕ} {f : ℕ → A},
            Sum i from k to k, f i = f k

@sum_step : ∀ {A : Type} [inst : AddZeroClass A] {k n : ℕ} {f : ℕ → A},
            k ≤ n → Sum i from k to n + 1, f i =
              (Sum i from k to n, f i) + f (n + 1)

@sum_from_zero_step :
            ∀ {A : Type} [inst : AddZeroClass A] {n : ℕ} {f : ℕ → A},
            Sum i from 0 to n + 1, f i =
              (Sum i from 0 to n, f i) + f (n + 1)

As usual, we don’t need to pay too much attention to the implicit arguments in the first line of each statement. What is important is that sum_base can be used to prove any statement of the form

Sum i from k to k, f i = f k

and sum_step proves any statement of the form

k ≤ n → Sum i from k to n + 1, f i = (Sum i from k to n, f i) + f (n + 1).

In the case k = 0, we have the simpler theorem sum_from_zero_step, which proves

Sum i from 0 to n + 1, f i = (Sum i from 0 to n, f i) + f (n + 1).

With that preparation, we can start on the proof. Once again we begin with the by_induc tactic. Our goal for the base case is (Sum i from 0 to 0, 2 ^ i) + 1 = 2 ^ (0 + 1). To deal with the term Sum i from 0 to 0, 2 ^ i, we use that fact that sum_base proves Sum i from 0 to 0, 2 ^ i = 2 ^ 0. It follows that the tactic rewrite [sum_base] will change the goal to 2 ^ 0 + 1 = 2 ^ (0 + 1). Of course, this means 2 = 2, so rfl finishes the base case. For the induction step, we start by introducing an arbitrary natural number n and assuming the inductive hypothesis.

theorem Like_Example_6_1_1 :
    ∀ (n : Nat), (Sum i from 0 to n, 2 ^ i) + 1 = 2 ^ (n + 1) := by
  by_induc
  · -- Base Case
    rewrite [sum_base]
    rfl
    done
  · -- Induction Step
    fix n : Nat
    assume ih : (Sum i from 0 to n, 2 ^ i) + 1 = 2 ^ (n + 1)
    **done::
  done

Our goal is now (Sum i from 0 to n + 1, 2 ^ i) + 1 = 2 ^ (n + 1 + 1), and we use a calculational proof to prove this. Often the key to the proof of the induction step is to find a relationship between the inductive hypothesis and the goal. In this case, that means finding a relationship between Sum i from 0 to n, 2 ^ i and Sum i from 0 to n + 1, 2 ^ i. The relationship we need is given by the theorem sum_from_zero_step. The tactic rewrite [sum_from_zero_step] will replace Sum i from 0 to n + 1, 2 ^ i with (Sum i from 0 to n, 2 ^ i) + 2 ^ (n + 1). The rest of the calculation proof involves straightforward algebra, handled by the ring tactic, together with an application of the inductive hypothesis.

theorem Like_Example_6_1_1 :
    ∀ (n : Nat), (Sum i from 0 to n, 2 ^ i) + 1 = 2 ^ (n + 1) := by
  by_induc
  · -- Base Case
    rewrite [sum_base]
    rfl
    done
  · -- Induction Step
    fix n : Nat
    assume ih : (Sum i from 0 to n, 2 ^ i) + 1 = 2 ^ (n + 1)
    show (Sum i from 0 to n + 1, 2 ^ i) + 1 = 2 ^ (n + 1 + 1) from
      calc (Sum i from 0 to n + 1, 2 ^ i) + 1
        _ = (Sum i from 0 to n, 2 ^ i) + 2 ^ (n + 1) + 1 := by
              rw [sum_from_zero_step]
        _ = (Sum i from 0 to n, 2 ^ i) + 1 + 2 ^ (n + 1) := by ring
        _ = 2 ^ (n + 1) + 2 ^ (n + 1) := by rw [ih]
        _ = 2 ^ (n + 1 + 1) := by ring
    done
  done

The last example in Section 6.1 of HTPI gives a proof of the statement \(\forall n \ge 5 (2^n > n^2)\). The proof is by mathematical induction, but since we are only interested in natural numbers greater than or equal to 5, it uses 5 in the base case instead of 0. Here are the theorem and proof from HTPI (HTPI p. 278):

For every natural number \(n \ge 5\), \(2^n > n^2\).

Proof. By mathematical induction.

Base case: When \(n = 5\) we have \(2^n = 32 > 25 = n^2\).

Induction step: Let \(n \ge 5\) be arbitrary, and suppose that \(2^n > n^2\). Then \[\begin{align*} 2^{n+1} &= 2 \cdot 2^n\\ &> 2n^2 &&\text{(inductive hypothesis)}\\ &= n^2 + n^2\\ &\ge n^2 + 5n &&\text{(since $n \ge 5$)}\\ &= n^2 + 2n + 3n\\ &> n^2 + 2n + 1 = (n+1)^2. &&\Box \end{align*}\]

Notice that the sequence of calculations at the end of the proof mixes \(=\), \(>\), and \(\ge\) in a way that establishes the final conclusion \(2^{n+1} > (n+1)^2\). As we’ll see, such a mixture is allowed in calculational proofs in Lean as well.

To write this proof in Lean, there is no need to specify that the base case should be n = 5; the by_induc tactic is smart enough to figure that out on its own, as you can see in the tactic state below. (Notice that, as in HTPI, in Lean we can write ∀ n ≥ k, P n as an abbreviation for ∀ (n : Nat), n ≥ k → P n.)

theorem Example_6_1_3 :
    ∀ n ≥ 5, 2 ^ n > n ^ 2 := by
  by_induc
  **done::

case Base_Case
⊢ 2 ^ 5 > 5 ^ 2
case Induction_Step
⊢ ∀ n ≥ 5,
>>  2 ^ n > n ^ 2 →
>>  2 ^ (n + 1) >
>>      (n + 1) ^ 2

To complete this proof we’ll use two tactics we haven’t used before: decide and linarith. The truth or falsity of the inequality in the base case can be decided by simply doing the necessary arithmetic. The tactic decide can do such calculations, and it proves the base case.

For the induction step, we introduce an arbitrary natural number n, assume n ≥ 5, and assume the inductive hypothesis, 2 ^ n > n ^ 2. Then we use a calculational proof to imitate the reasoning at the end of the HTPI proof. The tactic linarith makes inferences that involve combining linear equations and inequalities. It is able to prove almost all of the inequalities in the calculational proof. The exception is n * n ≥ 5 * n (which is not linear because of the term n * n). So we prove that inequality separately, using a theorem from Lean’s library, Nat.mul_le_mul_right. The command #check @Nat.mul_le_mul_right tells us the meaning of that theorem:

@Nat.mul_le_mul_right : ∀ {n m : ℕ} (k : ℕ), n ≤ m → n * k ≤ m * k

Thus, Nat.mul_le_mul_right n can be used to prove the statement 5 ≤ n → 5 * n ≤ n * n. Lean recognizes x ≥ y as meaning the same thing as y ≤ x, so we can apply this statement to our assumption n ≥ 5 to prove that n * n ≥ 5 * n. Once we have proven that inequality, the linarith tactic can use it to complete the required inequality reasoning.

theorem Example_6_1_3 : ∀ n ≥ 5, 2 ^ n > n ^ 2 := by
  by_induc
  · -- Base Case
    decide
    done
  · -- Induction Step
    fix n : Nat
    assume h1 : n ≥ 5
    assume ih : 2 ^ n > n ^ 2
    have h2 : n * n ≥ 5 * n := Nat.mul_le_mul_right n h1
    show 2 ^ (n + 1) > (n + 1) ^ 2 from
      calc 2 ^ (n + 1)
        _ = 2 * 2 ^ n := by ring
        _ > 2 * n ^ 2 := by linarith
        _ ≥ n ^ 2 + 5 * n := by linarith
        _ > n ^ 2 + 2 * n + 1 := by linarith
        _ = (n + 1) ^ 2 := by ring
    done
  done

Finally, we turn to the question of why we made small changes in two of the examples from HTPI. Perhaps you have guessed by now that we were trying to avoid the use of subtraction. All of the numbers in the examples in this section were natural numbers, and subtraction of natural numbers is problematic. In the natural numbers, 3 - 2 is equal to 1, but what is 2 - 3? Lean’s answer is 0.

++#eval:: 2 - 3     --Answer: 0

In Lean, if a and b are natural numbers and a < b, then a - b is defined to be 0. As a result, the algebraic laws of natural number subtraction are complicated. For example, 2 - 3 + 1 = 0 + 1 = 1, but 2 + 1 - 3 = 3 - 3 = 0, so it is not true that for all natural numbers a, b, and c, a - b + c = a + c - b.

If you thought that the answer to the subtraction problem 2 - 3 was -1, then you automatically switched from the natural numbers to the integers. (Recall that the natural numbers are the numbers 0, 1, 2, …, while the integers are the numbers …, –3, –2, –1, 0, 1, 2, 3, ….) To a human mathematician, this is a perfectly natural thing to do: the natural numbers are a subset of the integers, so 2 and 3 are not only natural numbers but also integers, and we can compute 2 - 3 in the integers.

However, that’s not how things work in Lean. In Lean, different types are completely separate. In particular, Nat and Int are separate types, and therefore the natural numbers are not a subset of the integers. Of course, there is an integer 2, but it is different from the natural number 2. By default, Lean assumes that 2 denotes the natural number 2, but you can specify that you want the integer 2 by writing (2 : Int). Subtraction of integers in Lean is the subtraction you are familiar with, and it has all the algebraic properties you would expect. If we want to use subtraction in the theorems in this section, we are better off using familiar integer subtraction rather than funky natural number subtraction.

To prove the theorem in Example 6.1.1 as it appears in HTPI, we could state the theorem like this:

theorem Example_6_1_1 :
    ∀ (n : Nat), Sum i from 0 to n, (2 : Int) ^ i =
    (2 : Int) ^ (n + 1) - (1 : Int)

The expression Sum i from 0 to n, (2 : Int) ^ i denotes a sum of integers, so it is an integer. Similarly, the right side of the equation is an integer, and the equation asserts the equality of two integers. The subtraction on the right side of the equation is integer subtraction, so we can use the usual algebraic laws to reason about it. In fact, the proof of the theorem in this form is not hard:

theorem Example_6_1_1 :
    ∀ (n : Nat), Sum i from 0 to n, (2 : Int) ^ i =
    (2 : Int) ^ (n + 1) - (1 : Int) := by
  by_induc
  · -- Base Case
    rewrite [sum_base]
    rfl
    done
  · -- Induction Step
    fix n : Nat
    assume ih : Sum i from 0 to n, (2 : Int) ^ i =
        (2 : Int) ^ (n + 1) - (1 : Int)
    show Sum i from 0 to n + 1, (2 : Int) ^ i =
        (2 : Int) ^ (n + 1 + 1) - (1 : Int) from
      calc Sum i from 0 to n + 1, (2 : Int) ^ i
        _ = (Sum i from 0 to n, (2 : Int) ^ i)
            + (2 : Int) ^ (n + 1) := by rw [sum_from_zero_step]
        _ = (2 : Int) ^ (n + 1) - (1 : Int)
            + (2 : Int) ^ (n + 1) := by rw [ih]
        _ = (2 : Int) ^ (n + 1 + 1) - (1 : Int) := by ring
    done
  done

If you change (2 : Int) and (1 : Int) to 2 and 1, then the right side of the equation will be a difference of two natural numbers, and Lean will interpret the subtraction as natural number subtraction. The proof won’t work because the ring tactic is not able to deal with the peculiar algebraic properties of natural number subtraction. (The theorem is still true, but the proof is harder.)

Exercises

theorem Like_Exercise_6_1_1 :
    ∀ (n : Nat), 2 * Sum i from 0 to n, i = n * (n + 1) := sorry

theorem Like_Exercise_6_1_4 :
    ∀ (n : Nat), Sum i from 0 to n, 2 * i + 1 = (n + 1) ^ 2 := sorry

theorem Exercise_6_1_9a : ∀ (n : Nat), 2 ∣ n ^ 2 + n := sorry

theorem Exercise_6_1_13 :
    ∀ (a b : Int) (n : Nat), (a - b) ∣ (a ^ n - b ^ n) := sorry

theorem Exercise_6_1_15 : ∀ n ≥ 10, 2 ^ n > n ^ 3 := sorry

lemma nonzero_is successor :
    ∀ (n : Nat), n ≠ 0 → ∃ (m : Nat), n = m + 1 := sorry

For the next two exercises you will need the following definitions:

def nat_even (n : Nat) : Prop := ∃ (k : Nat), n = 2 * k

def nat_odd (n : Nat) : Prop := ∃ (k : Nat), n = 2 * k + 1

theorem Exercise_6_1_16a1 :
    ∀ (n : Nat), nat_even n ∨ nat_odd n := sorry

--Hint:  You may find the lemma nonzero_is_successor
--from a previous exercise useful, as well as Nat.add_right_cancel.
theorem Exercise_6_1_16a2 :
    ∀ (n : Nat), ¬(nat_even n ∧ nat_odd n) := sorry

6.2. More Examples

We saw in the last section that mathematical induction can be used to prove theorems about calculations involving natural numbers. But mathematical induction has a much wider range of uses. Section 6.2 of HTPI illustrates this by proving two theorems about finite sets.

How can mathematical induction be used to prove a statement about finite sets? To say that a set is finite means that it has \(n\) elements, for some natural number \(n\). Thus, to say that all finite sets have some property, we can say that for every natural number \(n\), every set with \(n\) elements has the property. Since this statement starts with “for every natural number \(n\),” we can use mathematical induction to try to prove it.

What does it mean to say that a set “has \(n\) elements”? Section 6.2 of HTPI says that for the proofs in that section, “an intuitive understanding of this concept will suffice.” Unfortunately, intuition is not Lean’s strong suit! So we’ll need to be more explicit about how to talk about finite sets in Lean.

In Chapter 8, we’ll define numElts A n to be a proposition saying that the set A has n elements, and we’ll prove several theorems involving that proposition. Those theorems make precise and explicit the intuitive ideas that we’ll need in this section. We’ll state those theorems here and use them in our proofs, but you’ll have to wait until Section 8.1½ to see how they are proven. Here are the theorems we’ll need:

theorem zero_elts_iff_empty {U : Type} (A : Set U) :
    numElts A 0 ↔ empty A

theorem one_elt_iff_singleton {U : Type} (A : Set U) :
    numElts A 1 ↔ ∃ (x : U), A = {x}

theorem nonempty_of_pos_numElts {U : Type} {A : Set U} {n : Nat}
    (h1 : numElts A n) (h2 : n > 0) : ∃ (x : U), x ∈ A

theorem remove_one_numElts {U : Type} {A : Set U} {n : Nat} {a : U}
    (h1 : numElts A (n + 1)) (h2 : a ∈ A) : numElts (A \ {a}) n

These theorems should make intuitive sense. The first says that a set has zero elements if and only if it is empty, and the second says that a set has one element if and only if it is a singleton set. The third theorem says that if a set has a positive number of elements, then there is something in the set. And the fourth says that if a set has \(n + 1\) elements and you remove one element, then the resulting set has \(n\) elements. You can probably guess that we’ll be using the last theorem in the induction steps of our proofs.

Our first theorem about finite sets says that if \(R\) is a partial order on \(A\), then every finite, nonempty subset of \(A\) has an \(R\)-minimal element. (This is not true in general for infinite subsets of \(A\). Can you think of an example of an infinite subset of a partially ordered set that has no minimal element?) To say that a set is finite and nonempty we can say that it has \(n\) elements for some \(n \ge 1\). So here’s how we state our theorem in Lean:

theorem Example_6_2_1 {A : Type} (R : BinRel A) (h : partial_order R) :
    ∀ n ≥ 1, ∀ (B : Set A), numElts B n →
      ∃ (x : A), minimalElt R x B

When we use mathematical induction to prove this theorem, the base case will be n = 1. To write the proof for the base case, we start by assuming B is a set with one element. We can then use the theorem one_elt_iff_singleton to conclude that B = {b}, for some b of type A. We need to prove that B has a minimal element, and the only possibility for the minimal element is b. Verifying that minimalElt R b B is straightforward. Here is the proof of the base case:

theorem Example_6_2_1 {A : Type} (R : BinRel A) (h : partial_order R) :
    ∀ n ≥ 1, ∀ (B : Set A), numElts B n →
      ∃ (x : A), minimalElt R x B := by
  by_induc
  · -- Base Case
    fix B : Set A
    assume h2 : numElts B 1
    rewrite [one_elt_iff_singleton] at h2
    obtain (b : A) (h3 : B = {b}) from h2
    apply Exists.intro b
    define         --Goal : b ∈ B ∧ ¬∃ x ∈ B, R x b ∧ x ≠ b
    apply And.intro
    · -- Proof that b ∈ B
      rewrite [h3]    --Goal : b ∈ {b}
      define          --Goal : b = b
      rfl
      done
    · -- Proof that nothing in B is smaller than b
      by_contra h4
      obtain (x : A) (h5 : x ∈ B ∧ R x b ∧ x ≠ b) from h4
      have h6 : x ∈ B := h5.left
      rewrite [h3] at h6   --h6 : x ∈ {b}
      define at h6         --h6 : x = b
      show False from h5.right.right h6
      done
    done
  · -- Induction Step

    **done::
  done

Notice that since the definition of minimalElt R b B involves a negative statement, we found it convenient to use proof by contradiction to prove it.

For the induction step, we assume that n ≥ 1 and that every set with n elements has an R-minimal element. We must prove that every set with n + 1 elements has a minimal element, so we let B be an arbitrary set with n + 1 elements. To apply the inductive hypothesis, we need a set with n elements. So we pick some b ∈ B (using the theorem nonempty_of_pos_numElts) and then remove it from B to get the set B' = B \ {b}. The theorem remove_one_numElts tells us that B' has n elements, so by the inductive hypothesis, we can then let c be a minimal element of B'. We now know about two elements of B: b and c. Which will be a minimal element of B? As explained in HTPI, it depends on whether or not R b c. We’ll prove that if R b c, then b is a minimal element of B, and if not, then c is a minimal element. It will be convenient to prove these last two facts separately as lemmas. The first lemma says that in the situation at this point in the proof, if R b c, then b is an R-minimal element of B. Here is the proof.

lemma Lemma_6_2_1_1 {A : Type} {R : BinRel A} {B : Set A} {b c : A}
    (h1 : partial_order R) (h2 : b ∈ B) (h3 : minimalElt R c (B \ {b}))
    (h4 : R b c) : minimalElt R b B := by
  define at h3
    --h3 : c ∈ B \ {b} ∧ ¬∃ x ∈ B \ {b}, R x c ∧ x ≠ c
  define  --Goal : b ∈ B ∧ ¬∃ x ∈ B, R x b ∧ x ≠ b
  apply And.intro h2    --Goal : ¬∃ x ∈ B, R x b ∧ x ≠ b
  contradict h3.right with h5
  obtain (x : A) (h6 : x ∈ B ∧ R x b ∧ x ≠ b) from h5
  apply Exists.intro x  --Goal : x ∈ B \ {b} ∧ R x c ∧ x ≠ c
  apply And.intro
  · -- Proof that x ∈ B \ {b}
    show x ∈ B \ {b} from And.intro h6.left h6.right.right
    done
  · -- Proof that R x c ∧ x ≠ c
    have Rtrans : transitive R := h1.right.left
    have h7 : R x c := Rtrans x b c h6.right.left h4
    apply And.intro h7
    by_contra h8
    rewrite [h8] at h6  --h6 : c ∈ B ∧ R c b ∧ c ≠ b
    have Rantisymm : antisymmetric R := h1.right.right
    have h9 : c = b := Rantisymm c b h6.right.left h4
    show False from h6.right.right h9
    done
  done

The second lemma says that if ¬R b c, then c is an R-minimal element of B. We’ll leave the proof as an exercise for you:

lemma Lemma_6_2_1_2 {A : Type} {R : BinRel A} {B : Set A} {b c : A}
    (h1 : partial_order R) (h2 : b ∈ B) (h3 : minimalElt R c (B \ {b}))
    (h4 : ¬R b c) : minimalElt R c B := sorry

With this preparation, we are finally ready to give the proof of the induction step of Example_6_2_1:

theorem Example_6_2_1 {A : Type} (R : BinRel A) (h : partial_order R) :
    ∀ n ≥ 1, ∀ (B : Set A), numElts B n →
      ∃ (x : A), minimalElt R x B := by
  by_induc
  · -- Base Case
    ...
  · -- Induction Step
    fix n : Nat
    assume h2 : n ≥ 1
    assume ih : ∀ (B : Set A), numElts B n → ∃ (x : A), minimalElt R x B
    fix B : Set A
    assume h3 : numElts B (n + 1)
    have h4 : n + 1 > 0 := by linarith
    obtain (b : A) (h5 : b ∈ B) from nonempty_of_pos_numElts h3 h4
    set B' : Set A := B \ {b}
    have h6 : numElts B' n := remove_one_numElts h3 h5
    obtain (c : A) (h7 : minimalElt R c B') from ih B' h6
    by_cases h8 : R b c
    · -- Case 1. h8 : R b c
      have h9 : minimalElt R b B := Lemma_6_2_1_1 h h5 h7 h8
      show ∃ (x : A), minimalElt R x B from Exists.intro b h9
      done
    · -- Case 2. h8 : ¬R b c
      have h9 : minimalElt R c B := Lemma_6_2_1_2 h h5 h7 h8
      show ∃ (x : A), minimalElt R x B from Exists.intro c h9
      done
    done
  done

We’ll consider one more theorem from Section 6.2 of HTPI. Example 6.2.2 proves that a partial order on a finite set can always be extended to a total order. Rather than give that proof, we are going to prove the more general theorem that is stated in Exercise 2 in Section 6.2 of HTPI. To explain the theorem in that exercise, it will be helpful to introduce a bit of terminology. Suppose R is a partial order on A and b has type A. We will say that b is R-comparable to everything if ∀ (x : A), R b x ∨ R x b. If B is a set of objects of type A, we say that B is R-comparable to everything if every element of B is R-comparable to everything; that is, if ∀ b ∈ B, ∀ (x : A), R b x ∨ R x b. Finally, we say that another binary relation T extends R if ∀ (x y : A), R x y → T x y. We are going to prove that if R is a partial order on A and B is a finite set of objects of type A, then there is a partial order T that extends R such that B is T-comparable to everything. In other words, we are going to prove the following theorem:

theorem Exercise_6_2_2 {A : Type} (R : BinRel A) (h : partial_order R) :
    ∀ (n : Nat) (B : Set A), numElts B n → ∃ (T : BinRel A),
    partial_order T ∧ (∀ (x y : A), R x y → T x y) ∧
    ∀ x ∈ B, ∀ (y : A), T x y ∨ T y x

In the exercises, we will ask you to show that this implies the theorem in Example 6.2.2.

It will be helpful to begin with a warm-up exercise. We’ll show that a partial order can always be extended to make a single object comparable to everything. In other words, we’ll show that if R is a partial order on A and b has type A, then we can define a partial order T extending R such that b is T-comparable to everything. To define T, we will need to make sure that for every x of type A, either T b x or T x b. If R x b, then since T must extend R, we must have T x b. If ¬R x b, then we will define T so that T b x. But notice that if we follow this plan, then for any x and y, if we have R x b and ¬R y b, then we will have T x b and T b y, and since T must be transitive, we must then have T x y. Summing up, if we have R x y then we must have T x y, and if we have R x b and ¬R y b then we will also need to have T x y. So let’s try defining T x y to mean R x y ∨ (R x b ∧ ¬R y b).

It will be useful to have a name for this relation T. Since it is an extension of R determined by the element b, we will give it the name extendPO R b. Here is the definition of this relation:

def extendPO {A : Type} (R : BinRel A) (b : A) (x y : A) : Prop :=
  R x y ∨ (R x b ∧ ¬R y b)

We need to prove a number of things about extendPO R b. First of all, we need to prove that it is a partial order. We’ll leave most of the details as exercises for you:

lemma extendPO_is_ref {A : Type} (R : BinRel A) (b : A)
    (h : partial_order R) : reflexive (extendPO R b) := sorry

lemma extendPO_is_trans {A : Type} (R : BinRel A) (b : A)
    (h : partial_order R) : transitive (extendPO R b) := sorry

lemma extendPO_is_antisymm {A : Type} (R : BinRel A) (b : A)
    (h : partial_order R) : antisymmetric (extendPO R b) := sorry

lemma extendPO_is_po {A : Type} (R : BinRel A) (b : A)
    (h : partial_order R) : partial_order (extendPO R b) := 
  And.intro (extendPO_is_ref R b h)
    (And.intro (extendPO_is_trans R b h) (extendPO_is_antisymm R b h))

It is easy to prove that extendPO R b extends R:

lemma extendPO_extends {A : Type} (R : BinRel A) (b : A) (x y : A) :
    R x y → extendPO R b x y := by
  assume h1 : R x y
  define
  show R x y ∨ R x b ∧ ¬R y b from Or.inl h1
  done

Finally, we verify that extendPO R b does what it was supposed to do: it makes b comparable with everything:

lemma extendPO_all_comp {A : Type} (R : BinRel A) (b : A)
    (h : partial_order R) :
    ∀ (x : A), extendPO R b b x ∨ extendPO R b x b := by
  have Rref : reflexive R := h.left
  fix x : A
  or_left with h1
  define at h1     --h1 : ¬(R x b ∨ R x b ∧ ¬R b b)
  demorgan at h1   --h1 : ¬R x b ∧ ¬(R x b ∧ ¬R b b)
  define           --Goal : R b x ∨ R b b ∧ ¬R x b
  apply Or.inr
  show R b b ∧ ¬R x b from And.intro (Rref b) h1.left
  done

With this preparation, we can finally return to our theorem Exercise_6_2_2. We will prove it by mathematical induction. In the base case we must show that if B has 0 elements then we can extend R to make everything in B comparable to everything. Of course, no extension is necessary, since it is vacuously true that all elements of B are R-comparable to everything. For the induction step, after assuming the inductive hypothesis, we must prove that if B has n + 1 elements then we can extend R to make all elements of B comparable to everything. As before, we choose b ∈ B and let B' = B \ {b}. By inductive hypothesis, we can find an extension T' of R that makes all elements of B' comparable to everything, so we just have to extend T' further to make b comparable to everything. But as we have just seen, we can do this with extendPO T' b.

theorem Exercise_6_2_2 {A : Type} (R : BinRel A) (h : partial_order R) :
    ∀ (n : Nat) (B : Set A), numElts B n → ∃ (T : BinRel A),
    partial_order T ∧ (∀ (x y : A), R x y → T x y) ∧
    ∀ x ∈ B, ∀ (y : A), T x y ∨ T y x := by
  by_induc
  · -- Base Case
    fix B : Set A
    assume h2 : numElts B 0
    rewrite [zero_elts_iff_empty] at h2
    define at h2     --h2 : ¬∃ (x : A), x ∈ B
    apply Exists.intro R
    apply And.intro h
    apply And.intro
    · -- Proof that R extends R
      fix x : A; fix y : A
      assume h3 : R x y
      show R x y from h3
      done
    · -- Proof that everything in B comparable to everything under R
      fix x : A
      assume h3 : x ∈ B
      contradict h2
      show ∃ (x : A), x ∈ B from Exists.intro x h3
      done
    done
  · -- Induction Step
    fix n : Nat
    assume ih : ∀ (B : Set A), numElts B n → ∃ (T : BinRel A),
      partial_order T ∧ (∀ (x y : A), R x y → T x y) ∧
      ∀ (x : A), x ∈ B → ∀ (y : A), T x y ∨ T y x
    fix B : Set A
    assume h2 : numElts B (n + 1)
    have h3 : n + 1 > 0 := by linarith
    obtain (b : A) (h4 : b ∈ B) from nonempty_of_pos_numElts h2 h3
    set B' : Set A := B \ {b}
    have h5 : numElts B' n := remove_one_numElts h2 h4
    have h6 : ∃ (T : BinRel A), partial_order T ∧
      (∀ (x y : A), R x y → T x y) ∧
      ∀ (x : A), x ∈ B' → ∀ (y : A), T x y ∨ T y x := ih B' h5
    obtain (T' : BinRel A)
      (h7 : partial_order T' ∧ (∀ (x y : A), R x y → T' x y) ∧
      ∀ (x : A), x ∈ B' → ∀ (y : A), T' x y ∨ T' y x) from h6
    have T'po : partial_order T' := h7.left
    have T'extR : ∀ (x y : A), R x y → T' x y := h7.right.left
    have T'compB' : ∀ (x : A), x ∈ B' →
      ∀ (y : A), T' x y ∨ T' y x := h7.right.right
    set T : BinRel A := extendPO T' b
    apply Exists.intro T
    apply And.intro (extendPO_is_po T' b T'po)
    apply And.intro
    · -- Proof that T extends R
      fix x : A; fix y : A
      assume h8 : R x y
      have h9 : T' x y := T'extR x y h8
      show T x y from (extendPO_extends T' b x y h9)
      done
    · -- Proof that everything in B comparable to everything under T
      fix x : A
      assume h8 : x ∈ B
      by_cases h9 : x = b
      · -- Case 1. h9 : x = b
        rewrite [h9]
        show ∀ (y : A), T b y ∨ T y b from extendPO_all_comp T' b T'po
        done
      · -- Case 2. h9 : x ≠ b
        have h10 : x ∈ B' := And.intro h8 h9
        fix y : A
        have h11 : T' x y ∨ T' y x := T'compB' x h10 y
        by_cases on h11
        · -- Case 2.1. h11 : T' x y
          show T x y ∨ T y x from
            Or.inl (extendPO_extends T' b x y h11)
          done
        · -- Case 2.2. h11 : T' y x
          show T x y ∨ T y x from
            Or.inr (extendPO_extends T' b y x h11)
          done
        done
      done
    done
  done

Exercises

lemma Lemma_6_2_1_2 {A : Type} {R : BinRel A} {B : Set A} {b c : A}
    (h1 : partial_order R) (h2 : b ∈ B) (h3 : minimalElt R c (B \ {b}))
    (h4 : ¬R b c) : minimalElt R c B := sorry

lemma extendPO_is_ref {A : Type} (R : BinRel A) (b : A)
    (h : partial_order R) : reflexive (extendPO R b) := sorry

lemma extendPO_is_trans {A : Type} (R : BinRel A) (b : A)
    (h : partial_order R) : transitive (extendPO R b) := sorry

lemma extendPO_is_antisymm {A : Type} (R : BinRel A) (b : A)
    (h : partial_order R) : antisymmetric (extendPO R b) := sorry

theorem Exercise_6_2_3 (A : Type) (R : BinRel A)
    (h : total_order R) : ∀ n ≥ 1, ∀ (B : Set A),
    numElts B n → ∃ (b : A), smallestElt R b B := sorry

--Hint:  First prove that R is reflexive.
theorem Exercise_6_2_4a {A : Type} (R : BinRel A)
    (h : ∀ (x y : A), R x y ∨ R y x) : ∀ n ≥ 1, ∀ (B : Set A),
    numElts B n → ∃ x ∈ B, ∀ y ∈ B, ∃ (z : A), R x z ∧ R z y := sorry

theorem Like_Exercise_6_2_16 {A : Type} (f : A → A)
    (h : one_to_one f) : ∀ (n : Nat) (B : Set A), numElts B n →
    closed f B → ∀ y ∈ B, ∃ x ∈ B, f x = y := sorry

--Hint:  Use Exercise_6_2_2.
theorem Example_6_2_2 {A : Type} (R : BinRel A)
    (h1 : ∃ (n : Nat), numElts {x : A | x = x} n)
    (h2 : partial_order R) : ∃ (T : BinRel A),
      total_order T ∧ ∀ (x y : A), R x y → T x y := sorry

6.3. Recursion

In the last two sections, we saw that we can prove that all natural numbers have some property by proving that 0 has the property, and also that for every natural number \(n\), if \(n\) has the property then so does \(n + 1\). In this section we will see that a similar idea can be used to define a function whose domain is the natural numbers. We can define a function \(f\) with domain \(\mathbb{N}\) by specifying the value of \(f(0)\), and also saying how to compute \(f(n+1)\) if you already know the value of \(f(n)\).

For example, we can define a function \(f : \mathbb{N} \to \mathbb{N}\) as follows:

\(f(0) = 1\);
for every \(n \in \mathbb{N}\), \(f(n+1) = (n+1) \cdot f(n)\).

Here is the same definition written in Lean. (For reasons that will become clear shortly, we have given the function the name fact.)

def fact (k : Nat) : Nat :=
  match k with
    | 0 => 1
    | n + 1 => (n + 1) * fact n

Lean can use this definition to compute fact k for any natural number k. The match statement tells Lean to try to match the input k with one of the two patterns 0 and n + 1, and then to use the corresponding formula after => to compute fact k. For example, if we ask Lean for fact 4, it first checks if 4 matches 0. Since it doesn’t, it goes on to the next line and determines that 4 matches the pattern n + 1, with n = 3, so it uses the formula fact 4 = 4 * fact 3. Of course, now it must compute fact 3, which it does in the same way: 3 matches n + 1 with n = 2, so fact 3 = 3 * fact 2. Continuing in this way, Lean determines that

fact 4 = 4 * fact 3 = 4 * (3 * fact 2) = 4 * (3 * (2 * fact 1))
       = 4 * (3 * (2 * (1 * fact 0))) = 4 * (3 * (2 * (1 * 1))) = 24.

You can confirm this with the #eval command:

#eval fact 4   --Answer: 24

Of course, by now you have probably guessed why we used the name fact for his function: fact k is k factorial—the product of all the numbers from 1 to k.

This style of definition is called a recursive definition. If a function is defined by a recursive definition, then theorems about that function are often most easily proven by induction. For example, here is a theorem about the factorial function. It is Example 6.3.1 in HTPI, and we begin the Lean proof by imitating the proof in HTPI.

theorem ??Example_6_3_1:: : ∀ n ≥ 4, fact n > 2 ^ n := by
  by_induc
  · -- Base Case
    decide
    done
  · -- Induction Step
    fix n : Nat
    assume h1 : n ≥ 4
    assume ih : fact n > 2 ^ n
    show fact (n + 1) > 2 ^ (n + 1) from
      calc fact (n + 1)
        _ = (n + 1) * fact n := by rfl
        _ > (n + 1) * 2 ^ n := sorry
        _ > 2 * 2 ^ n := sorry
        _ = 2 ^ (n + 1) := by ring
    done
  done

There are two steps in the calculational proof at the end that require justification. The first says that (n + 1) * fact n > (n + 1) * 2 ^ n, which should follow from the inductive hypothesis ih : fact n > 2 ^ n by multiplying both sides by n + 1. Is there a theorem that would justify this inference?

This may remind you of a step in Example_6_1_3 where we used the theorem Nat.mul_le_mul_right, which says ∀ {n m : ℕ} (k : ℕ), n ≤ m → n * k ≤ m * k. Our situation in this example is similar, but it involves a strict inequality (> rather than ≥) and it involves multiplying on the left rather than the right. Many theorems about inequalities in Lean’s library contain either le (for “less than or equal to”) or lt (for “less than”) in their names, but they can also be used to prove statements involving ≥ or >. Perhaps the theorem we need is named something like Nat.mul_lt_mul_left. If you type #check @Nat.mul_lt_mul_ into VS Code, a pop-up window will appear listing several theorems that begin with Nat.mul_lt_mul_. There is no Nat.mul_lt_mul_left, but there is a theorem called Nat.mul_lt_mul_of_pos_left, and its meaning is

@Nat.mul_lt_mul_of_pos_left : ∀ {n m k : ℕ},
                                n < m → k > 0 → k * n < k * m

Lean has correctly reminded us that, to multiply both sides of a strict inequality by a number k, we need to know that k > 0. So in our case, we’ll need to prove that n + 1 > 0. Once we have that, we can use the theorem Nat.mul_lt_mul_of_pos_left to eliminate the first sorry.

The second sorry is similar: (n + 1) * 2 ^ n > 2 * 2 ^ n should follow from n + 1 > 2 and 2 ^ n > 0, and you can verify that the theorem that will justify this inference is Nat.mul_lt_mul_of_pos_right.

So we have three inequalities that we need to prove before we can justify the steps of the calculational proof: n + 1 > 0, n + 1 > 2, and 2 ^ n > 0. We’ll insert have steps before the calculational proof to assert these three inequalities. If you try it, you’ll find that linarith can prove the first two, but not the third.

How can we prove 2 ^ n > 0? It is often helpful to think about whether there is a general principle that is behind a statement we are trying to prove. In our case, the inequality 2 ^ n > 0 is an instance of the general fact that if m and n are any natural numbers with m > 0, then m ^ n > 0. Maybe that fact is in Lean’s library:

example (m n : Nat) (h : m > 0) : m ^ n > 0 := by ++apply?::

The apply? tactic comes up with exact Nat.pos_pow_of_pos n h, and #check @Nat.pos_pow_of_pos gives the result

@Nat.pos_pow_of_pos : ∀ {n : ℕ} (m : ℕ), 0 < n → 0 < n ^ m

That means that we can use Nat.pos_pow_of_pos to prove 2 ^ n > 0, but first we’ll need to prove that 2 > 0. We now have all the pieces we need; putting them together leads to this proof:

theorem Example_6_3_1 : ∀ n ≥ 4, fact n > 2 ^ n := by
  by_induc
  · -- Base Case
    decide
    done
  · -- Induction Step
    fix n : Nat
    assume h1 : n ≥ 4
    assume ih : fact n > 2 ^ n
    have h2 : n + 1 > 0 := by linarith
    have h3 : n + 1 > 2 := by linarith
    have h4 : 2 > 0 := by linarith
    have h5 : 2 ^ n > 0 := Nat.pos_pow_of_pos n h4
    show fact (n + 1) > 2 ^ (n + 1) from
      calc fact (n + 1)
        _ = (n + 1) * fact n := by rfl
        _ > (n + 1) * 2 ^ n := Nat.mul_lt_mul_of_pos_left ih h2
        _ > 2 * 2 ^ n := Nat.mul_lt_mul_of_pos_right h3 h5
        _ = 2 ^ (n + 1) := by ring
    done
  done

But there is an easier way. Look at the two “>” steps in the calculational proof at the end of Example_6_3_1. In both cases, we took a known relationship between two quantities and did something to both sides that preserved the relationship. In the first case, the known relationship was ih : fact n > 2 ^ n, and we multiplied both sides by n + 1 on the left; in the second, the known relationship was h3 : n + 1 > 2, and we multiplied both sides by 2 ^ n on the right. To justify these steps, we had to find the right theorems in Lean’s library, and we ended up needing auxiliary positivity facts: h2 : n + 1 > 0 in the first case and h5 : 2 ^ n > 0 in the second. There is a tactic that can simplify these steps: if h is a proof of a statement asserting a relationship between two quantities, then the tactic rel [h] will attempt to prove any statement obtained from that relationship by applying the same operation to both sides. The tactic will try to find a theorem in Lean’s library that says that the operation preserves the relationship, and if the theorem requires auxiliary positivity facts, it will try to prove those facts as well. The rel tactic doesn’t always succeed, but when it does, it saves you the trouble of searching through the library for the necessary theorems. In this case, the tactic allows us to give a much simpler proof of Example_6_3_1:

theorem Example_6_3_1 : ∀ n ≥ 4, fact n > 2 ^ n := by
  by_induc
  · -- Base Case
    decide
    done
  · -- Induction Step
    fix n : Nat
    assume h1 : n ≥ 4
    assume ih : fact n > 2 ^ n
    have h2 : n + 1 > 2 := by linarith
    show fact (n + 1) > 2 ^ (n + 1) from
      calc fact (n + 1)
        _ = (n + 1) * fact n := by rfl
        _ > (n + 1) * 2 ^ n := by rel [ih]
        _ > 2 * 2 ^ n := by rel [h2]
        _ = 2 ^ (n + 1) := by ring
    done
  done

The next example in HTPI is a proof of one of the laws of exponents: a ^ (m + n) = a ^ m * a ^ n. Lean’s definition of exponentiation with natural number exponents is recursive. The definitions Lean uses are essentially as follows:

--For natural numbers b and k, b ^ k = nat_pow b k:
def nat_pow (b k : Nat) : Nat :=
  match k with
    | 0 => 1
    | n + 1 => (nat_pow b n) * b

--For a real number b and a natural number k, b ^ k = real_pow b k:
def real_pow (b : Real) (k : Nat) : Real :=
  match k with
    | 0 => 1
    | n + 1 => (real_pow b n) * b

Let’s prove the addition law for exponents:

theorem Example_6_3_2_cheating : ∀ (a : Real) (m n : Nat),
    a ^ (m + n) = a ^ m * a ^ n := by
  fix a : Real; fix m : Nat; fix n : Nat
  ring
  done

Well, that wasn’t really fair. The ring tactic knows the laws of exponents, so it has no trouble proving this theorem. But we want to know why the law holds, so let’s see if we can prove it without using ring. The following proof is essentially the same as the proof in HTPI:

theorem Example_6_3_2 : ∀ (a : Real) (m n : Nat),
    a ^ (m + n) = a ^ m * a ^ n := by
  fix a : Real; fix m : Nat
    --Goal : ∀ (n : Nat), a ^ (m + n) = a ^ m * a ^ n
  by_induc
  · -- Base Case
    show a ^ (m + 0) = a ^ m * a ^ 0 from
      calc a ^ (m + 0)
        _ = a ^ m := by rfl
        _ = a ^ m * 1 := (mul_one (a ^ m)).symm
        _ = a ^ m * a ^ 0 := by rfl
    done
  · -- Induction Step
    fix n : Nat
    assume ih : a ^ (m + n) = a ^ m * a ^ n
    show a ^ (m + (n + 1)) = a ^ m * a ^ (n + 1) from
      calc a ^ (m + (n + 1))
        _ = a ^ ((m + n) + 1) := by rw [add_assoc]
        _ = a ^ (m + n) * a := by rfl
        _ = (a ^ m * a ^ n) * a := by rw [ih]
        _ = a ^ m * (a ^ n * a) := by rw [mul_assoc]
        _ = a ^ m * (a ^ (n + 1)) := by rfl
    done
  done

Finally, we’ll prove the theorem in Example 6.3.4 of HTPI, which again involves exponentiation with natural number exponents. Here’s the beginning of the proof:

theorem Example_6_3_4 : ∀ (x : Real), x > -1 →
    ∀ (n : Nat), (1 + x) ^ n ≥ 1 + n * x := by
  fix x : Real
  assume h1 : x > -1
  **done::

x : ℝ
h1 : x > -1
⊢ ∀ (n : ℕ),
>>  (1 + x) ^ n ≥
>>    1 + ↑n * x

Look carefully at the goal in the tactic state. Why is there a ↑ before the last n? The reason has to do with types. The variable x has type Real and n has type Nat, so how can Lean multiply n by x? Remember, in Lean, the natural numbers are not a subset of the real numbers. The two types are completely separate, but for each natural number, there is a corresponding real number. To multiply n by x, Lean had to convert n to the corresponding real number, through a process called coercion. The notation ↑n denotes the result of coercing (or casting) n to another type—in this case, Real. Since ↑n and x are both real numbers, Lean can use the multiplication operation on the real numbers to multiply them. (To type ↑ in VSCode, type \uparrow, or just \u.)

As we will see, the need for coercion in this example will make the proof a bit more complicated, because we’ll need to use some theorems about coercions. Theorems about coercion of natural numbers to some other type often have names that start Nat.cast.

Continuing with the proof, since exponentiation is defined recursively, let’s try mathematical induction:

theorem Example_6_3_4 : ∀ (x : Real), x > -1 →
    ∀ (n : Nat), (1 + x) ^ n ≥ 1 + n * x := by
  fix x : Real
  assume h1 : x > -1
  by_induc
  · -- Base Case

    **done::
  · -- Induction Step

    **done::  
  done

case Base_Case
x : ℝ
h1 : x > -1
⊢ (1 + x) ^ 0 ≥
>>  1 + ↑0 * x

You might think that linarith could prove the goal for the base case, but it can’t. The problem is the ↑0, which denotes the result of coercing the natural number 0 to a real number. Of course, that should be the real number 0, but is it? Yes, but the linarith tactic doesn’t know that. The theorem Nat.cast_zero says that ↑0 = 0 (where the 0 on the right side of the equation is the real number 0), so the tactic rewrite [Nat.cast_zero] will convert ↑0 to 0. After that step, linarith can complete the proof of the base case, and we can start on the induction step.

theorem Example_6_3_4 : ∀ (x : Real), x > -1 →
    ∀ (n : Nat), (1 + x) ^ n ≥ 1 + n * x := by
  fix x : Real
  assume h1 : x > -1
  by_induc
  · -- Base Case
    rewrite [Nat.cast_zero]
    linarith
    done
  · -- Induction Step
    fix n : Nat
    assume ih : (1 + x) ^ n ≥ 1 + n * x
    **done::
  done

case Induction_Step
x : ℝ
h1 : x > -1
n : ℕ
ih : (1 + x) ^ n ≥
>>    1 + ↑n * x
⊢ (1 + x) ^ (n + 1) ≥
>>  1 + ↑(n + 1) * x

Once again, there’s a complication caused by coercion. The inductive hypothesis talks about ↑n, but the goal involves ↑(n + 1). What is the relationship between these? Surely it should be the case that ↑(n + 1) = ↑n + 1; that is, the result of coercing the natural number n + 1 to a real number should be one larger than the result of coercing n to a real number. The theorem Nat.cast_succ says exactly that, so rewrite [Nat.cast_succ] will change the ↑(n + 1) in the goal to ↑n + 1. (The number n + 1 is sometimes called the successor of n, and succ is short for “successor.”) With that change, we can continue with the proof. The following proof is modeled on the proof in HTPI.

theorem ??Example_6_3_4:: : ∀ (x : Real), x > -1 →
    ∀ (n : Nat), (1 + x) ^ n ≥ 1 + n * x := by
  fix x : Real
  assume h1 : x > -1
  by_induc
  · -- Base Case
    rewrite [Nat.cast_zero]
    linarith
    done
  · -- Induction Step
    fix n : Nat
    assume ih : (1 + x) ^ n ≥ 1 + n * x
    rewrite [Nat.cast_succ]
    show (1 + x) ^ (n + 1) ≥ 1 + (n + 1) * x from
      calc (1 + x) ^ (n + 1)
        _ = (1 + x) ^ n * (1 + x) := by rfl
        _ ≥ (1 + n * x) * (1 + x) := sorry
        _ = 1 + n * x + x + n * x ^ 2 := by ring
        _ ≥ 1 + n * x + x + 0 := sorry
        _ = 1 + (n + 1) * x := by ring
    done
  done

Note that in the calculational proof, each n or n + 1 that is multiplied by x is really ↑n or ↑n + 1, but we don’t need to say so explicitly; Lean fills in coercions automatically when they are required.

All that’s left is to replace the two occurrences of sorry with justifications. The first sorry step should follow from the inductive hypothesis by multiplying both sides by 1 + x, so a natural attempt to justify it would be by rel [ih]. Unfortunately, we get an error message saying that rel failed. The error message tells us that rel needed to know that 0 ≤ 1 + x, and it was unable to prove it, so we’ll have to provide a proof of that statement ourselves. Fortunately, linarith can handle it (deducing it from h1 : x > -1), and once we fill in that additional step, the rel tactic succeeds.

theorem ??Example_6_3_4:: : ∀ (x : Real), x > -1 →
    ∀ (n : Nat), (1 + x) ^ n ≥ 1 + n * x := by
  fix x : Real
  assume h1 : x > -1
  by_induc
  · -- Base Case
    rewrite [Nat.cast_zero]
    linarith
    done
  · -- Induction Step
    fix n : Nat
    assume ih : (1 + x) ^ n ≥ 1 + n * x
    rewrite [Nat.cast_succ]
    have h2 : 0 ≤ 1 + x := by linarith
    show (1 + x) ^ (n + 1) ≥ 1 + (n + 1) * x from
      calc (1 + x) ^ (n + 1)
        _ = (1 + x) ^ n * (1 + x) := by rfl
        _ ≥ (1 + n * x) * (1 + x) := by rel [ih]
        _ = 1 + n * x + x + n * x ^ 2 := by ring
        _ ≥ 1 + n * x + x + 0 := sorry
        _ = 1 + (n + 1) * x := by ring
    done
  done

For the second sorry step, we’ll need to know that n * x ^ 2 ≥ 0. To prove it, we start with the fact that the square of any real number is nonnegative:

@sq_nonneg : ∀ {α : Type u_1} [inst : LinearOrderedSemiring α]
              [inst_1 : ExistsAddOfLE α]
              (a : α), 0 ≤ a ^ 2

As usual, we don’t need to pay much attention to the implicit arguments; what is important is the last line, which tells us that sq_nonneg x is a proof of x ^ 2 ≥ 0. To get n * x ^ 2 ≥ 0 we just have to multiply both sides by n, which we can justify with the rel tactic, and then one more application of rel will handle the remaining sorry. Here is the complete proof:

theorem Example_6_3_4 : ∀ (x : Real), x > -1 →
    ∀ (n : Nat), (1 + x) ^ n ≥ 1 + n * x := by
  fix x : Real
  assume h1 : x > -1
  by_induc
  · -- Base Case
    rewrite [Nat.cast_zero]
    linarith
    done
  · -- Induction Step
    fix n : Nat
    assume ih : (1 + x) ^ n ≥ 1 + n * x
    rewrite [Nat.cast_succ]
    have h2 : 0 ≤ 1 + x := by linarith
    have h3 : x ^ 2 ≥ 0 := sq_nonneg x
    have h4 : n * x ^ 2 ≥ 0 :=
      calc n * x ^ 2
        _ ≥ n * 0 := by rel [h3]
        _ = 0 := by ring
    show (1 + x) ^ (n + 1) ≥ 1 + (n + 1) * x from
      calc (1 + x) ^ (n + 1)
        _ = (1 + x) ^ n * (1 + x) := by rfl
        _ ≥ (1 + n * x) * (1 + x) := by rel [ih]
        _ = 1 + n * x + x + n * x ^ 2 := by ring
        _ ≥ 1 + n * x + x + 0 := by rel [h4]
        _ = 1 + (n + 1) * x := by ring
    done
  done

Before ending this section, we’ll return to a topic left unexplained before. We can now describe how Sum i from k to n, f i is defined. The key is a function sum_seq, which is defined by recursion:

def sum_seq {A : Type} [AddZeroClass A]
    (m k : Nat) (f : Nat → A) : A :=
  match m with
    | 0 => 0
    | n + 1 => sum_seq n k f + f (k + n)

To get an idea of what this definition means, let’s try evaluating sum_seq 3 k f:

sum_seq 3 k f = sum_seq 2 k f + f (k + 2)
              = sum_seq 1 k f + f (k + 1) + f (k + 2)
              = sum_seq 0 k f + f (k + 0) + f (k + 1) + f (k + 2)
              = 0 + f (k + 0) + f (k + 1) + f (k + 2)
              = f k + f (k + 1) + f (k + 2).

So sum_seq 3 k f adds up three consecutive values of f, starting with f k. More generally, sum_seq n k f adds up a sequence of n consecutive values of f, starting with f k. (The implicit arguments say that the type of the values of f can be any type for which + and 0 make sense.) The notation Sum i from k to n, f i is now defined to be a shorthand for sum_seq (n + 1 - k) k f. We’ll leave it to you to puzzle out why that gives the desired result.

Exercises

theorem Exercise_6_3_4 : ∀ (n : Nat),
    3 * (Sum i from 0 to n, (2 * i + 1) ^ 2) =
    (n + 1) * (2 * n + 1) * (2 * n + 3) := sorry

theorem Exercise_6_3_7b (f : Nat → Real) (c : Real) : ∀ (n : Nat),
    Sum i from 0 to n, c * f i = c * Sum i from 0 to n, f i := sorry

theorem fact_pos : ∀ (n : Nat), fact n ≥ 1 := sorry

--Hint:  Use the theorem fact_pos from the previous exercise.
theorem Exercise_6_3_13a (k : Nat) : ∀ (n : Nat),
    fact (k ^ 2 + n) ≥ k ^ (2 * n) := sorry

--Hint:  Use the theorem in the previous exercise.
--You may find it useful to first prove a lemma:
--∀ (k : Nat), 2 * k ^ 2 + 1 ≥ k
theorem Exercise_6_3_13b (k : Nat) : ∀ n ≥ 2 * k ^ 2,
    fact n ≥ k ^ n := sorry

6. A sequence is defined recursively as follows:

def seq_6_3_15 (k : Nat) : Int :=
  match k with
    | 0 => 0
    | n + 1 => 2 * seq_6_3_15 n + n

Prove the following theorem about this sequence:

theorem Exercise_6_3_15 : ∀ (n : Nat),
    seq_6_3_15 n = 2 ^ n - n - 1 := sorry

7. A sequence is defined recursively as follows:

def seq_6_3_16 (k : Nat) : Nat :=
  match k with
    | 0 => 2
    | n + 1 => (seq_6_3_16 n) ^ 2

Find a formula for seq_6_3_16 n. Fill in the blank in the theorem below with your formula and then prove the theorem.

theorem Exercise_6_3_16 : ∀ (n : Nat),
    seq_6_3_16 n = ___ := sorry

6.4. Strong Induction

In the induction step of a proof by mathematical induction, we prove that a natural number has some property from the assumption that the previous number has the property. Section 6.4 of HTPI introduces a version of mathematical induction in which we get to assume that all smaller numbers have the property. Since this is a stronger assumption, this version of induction is called strong induction. Here is how strong induction works (HTPI p. 304):

To prove a goal of the form ∀ (n : Nat), P n:

Prove that ∀ (n : Nat), (∀ n_1 < n, P n_1) → P n.

To write a proof by strong induction in Lean, we use the tactic by_strong_induc, whose effect on the tactic state can be illustrated as follows.

>> ⋮
⊢ ∀ (n : Nat), P n

>> ⋮
⊢  ∀ (n : Nat),
>>  (∀ n_1 < n, P n_1) → P n

To illustrate this, we begin with Example 6.4.1 of HTPI.

theorem Example_6_4_1 : ∀ m > 0, ∀ (n : Nat),
    ∃ (q r : Nat), n = m * q + r ∧ r < m

Imitating the strategy of the proof in HTPI, we let m be an arbitrary natural number, assume m > 0, and then prove the statement ∀ (n : Nat), ∃ (q r : Nat), n = m * q + r ∧ r < m by strong induction. That means that after introducing an arbitrary natural number n, we assume the inductive hypothesis, which says ∀ n_1 < n, ∃ (q r : Nat), n_1 = m * q + r ∧ r < m.

theorem Example_6_4_1 : ∀ m > 0, ∀ (n : Nat),
    ∃ (q r : Nat), n = m * q + r ∧ r < m := by
  fix m : Nat
  assume h1 : m > 0
  by_strong_induc
  fix n : Nat
  assume ih : ∀ n_1 < n, ∃ (q r : Nat), n_1 = m * q + r ∧ r < m
  **done::

Our goal now is to prove that ∃ (q r : Nat), n = m * q + r ∧ r < m. Although strong induction does not require a base case, it is not uncommon for proofs by strong induction to involve reasoning by cases. The proof in HTPI uses cases based on whether or not n < m. If n < m, then the proof is easy: the numbers q = 0 and r​ = n clearly have the required properties. If ¬n < m, then we can write n as n = k + m, for some natural number k. Since m > 0, we have k < n, so we can apply the inductive hypothesis to k. Notice that if m > 1, then k is not the number immediately preceding n; that’s why this proof uses strong induction rather than ordinary induction.

How do we come up with the number k in the previous paragraph? We’ll use a theorem from Lean’s library. There are two slightly different versions of the theorem—notice that the first ends with m + k and the second ends with k + m:

@Nat.exists_eq_add_of_le : ∀ {m n : ℕ}, m ≤ n → ∃ (k : ℕ), n = m + k

@Nat.exists_eq_add_of_le' : ∀ {m n : ℕ}, m ≤ n → ∃ (k : ℕ), n = k + m

We’ll use the second version in our proof.

theorem Example_6_4_1 : ∀ m > 0, ∀ (n : Nat),
    ∃ (q r : Nat), n = m * q + r ∧ r < m := by
  fix m : Nat
  assume h1 : m > 0
  by_strong_induc
  fix n : Nat
  assume ih : ∀ n_1 < n, ∃ (q r : Nat), n_1 = m * q + r ∧ r < m
  by_cases h2 : n < m
  · -- Case 1. h2 : n < m
    apply Exists.intro 0
    apply Exists.intro n     --Goal : n = m * 0 + n ∧ n < m
    apply And.intro _ h2
    ring
    done
  · -- Case 2. h2 : ¬n < m
    have h3 : m ≤ n := by linarith
    obtain (k : Nat) (h4 : n = k + m) from Nat.exists_eq_add_of_le' h3
    have h5 : k < n := by linarith
    have h6 : ∃ (q r : Nat), k = m * q + r ∧ r < m := ih k h5
    obtain (q' : Nat)
      (h7 : ∃ (r : Nat), k = m * q' + r ∧ r < m) from h6
    obtain (r' : Nat) (h8 : k = m * q' + r' ∧ r' < m) from h7
    apply Exists.intro (q' + 1)
    apply Exists.intro r'     --Goal : n = m * (q' + 1) + r' ∧ r' < m
    apply And.intro _ h8.right
    show n = m * (q' + 1) + r' from
      calc n
        _ = k + m := h4
        _ = m * q' + r' + m := by rw [h8.left]
        _ = m * (q' + 1) + r' := by ring
    done
  done

The numbers q and r in Example_6_4_1 are called the quotient and remainder when n is divided by m. Lean knows how to compute these numbers: if n and m are natural numbers, then in Lean, n / m denotes the quotient when n is divided by m, and n % m denotes the remainder. (The number n % m is also sometimes called n modulo m, or n mod m.) And Lean knows theorems stating that these numbers have the properties specified in Example_6_4_1:

@Nat.div_add_mod : ∀ (m n : ℕ), n * (m / n) + m % n = m

@Nat.mod_lt : ∀ (x : ℕ) {y : ℕ}, y > 0 → x % y < y

By the way, although we are unlikely to want to use the notation n / 0 or n % 0, Lean uses the definitions n / 0 = 0 and n % 0 = n. As a result, the equation n * (m / n) + m % n = m is true even if n = 0. That’s why the theorem Nat.div_add_mod doesn’t include a requirement that n > 0. It is important to keep in mind that division of natural numbers is not the same as division of real numbers. For example, dividing the natural number 5 by the natural number 2 gives a quotient of 2 (with a remainder of 1), so (5 : Nat) / (2 : Nat) is 2, but (5 : Real) / (2 : Real) is 2.5.

There is also a strong form of recursion. As an example of this, here is a recursive definition of a sequence of numbers called the Fibonacci numbers:

def Fib (n : Nat) : Nat :=
  match n with
    | 0 => 0
    | 1 => 1
    | k + 2 => Fib k + Fib (k + 1)

Notice that the formula for Fib (k + 2) involves the two previous values of Fib, not just the immediately preceding value. That is the sense in which the recursion is strong. Not surprisingly, theorems about the Fibonacci numbers are often proven by induction—either ordinary or strong. We’ll illustrate this with a proof by strong induction that ∀ (n : Nat), Fib n < 2 ^ n. This time we’ll need to treat the cases n = 0 and n = 1 separately, since these values are treated separately in the definition of Fib n. And we’ll need to know that if n doesn’t fall into either of those cases, then it falls into the third case: n = k + 2 for some natural number k. Since similar ideas will come up several times in the rest of this book, it will be useful to begin by proving lemmas that will help with this kind of reasoning.

We’ll need two theorems from Lean’s library, the second of which has two slightly different versions:

@Nat.pos_of_ne_zero : ∀ {n : ℕ}, n ≠ 0 → 0 < n

@lt_of_le_of_ne : ∀ {α : Type u_1} [inst : PartialOrder α] {a b : α},
                    a ≤ b → a ≠ b → a < b

@lt_of_le_of_ne' : ∀ {α : Type u_1} [inst : PartialOrder α] {a b : α},
                    a ≤ b → b ≠ a → a < b

If we have h1 : n ≠ 0, then Nat.pos_of_ne_zero h1 is a proof of 0 < n. But for natural numbers a and b, Lean treats a < b as meaning the same thing as a + 1 ≤ b, so this is also a proof of 1 ≤ n. If we also have h2 : n ≠ 1, then we can use lt_of_le_of_ne' to conclude 1 < n, which is definitionally equal to 2 ≤ n. Combining this reasoning with the theorem Nat.exists_eq_add_of_le', which we used in the last example, we can prove two lemmas that will be helpful for reasoning in which the first one or two natural numbers have to be treated separately.

lemma exists_eq_add_one_of_ne_zero {n : Nat}
    (h1 : n ≠ 0) : ∃ (k : Nat), n = k + 1 := by
  have h2 : 1 ≤ n := Nat.pos_of_ne_zero h1
  show ∃ (k : Nat), n = k + 1 from Nat.exists_eq_add_of_le' h2
  done

theorem exists_eq_add_two_of_ne_zero_one {n : Nat}
    (h1 : n ≠ 0) (h2 : n ≠ 1) : ∃ (k : Nat), n = k + 2 := by
  have h3 : 1 ≤ n := Nat.pos_of_ne_zero h1
  have h4 : 2 ≤ n := lt_of_le_of_ne' h3 h2
  show ∃ (k : Nat), n = k + 2 from Nat.exists_eq_add_of_le' h4
  done

With this preparation, we can present the proof:

example : ∀ (n : Nat), Fib n < 2 ^ n := by
  by_strong_induc
  fix n : Nat
  assume ih : ∀ n_1 < n, Fib n_1 < 2 ^ n_1
  by_cases h1 : n = 0
  · -- Case 1. h1 : n = 0
    rewrite [h1]   --Goal : Fib 0 < 2 ^ 0
    decide
    done
  · -- Case 2. h1 : ¬n = 0
    by_cases h2 : n = 1
    · -- Case 2.1. h2 : n = 1
      rewrite [h2]
      decide
      done
    · -- Case 2.2. h2 : ¬n = 1
      obtain (k : Nat) (h3 : n = k + 2) from
        exists_eq_add_two_of_ne_zero_one h1 h2
      have h4 : k < n := by linarith
      have h5 : Fib k < 2 ^ k := ih k h4
      have h6 : k + 1 < n := by linarith
      have h7 : Fib (k + 1) < 2 ^ (k + 1) := ih (k + 1) h6
      rewrite [h3]            --Goal : Fib (k + 2) < 2 ^ (k + 2)
      show Fib (k + 2) < 2 ^ (k + 2) from
        calc Fib (k + 2)
          _ = Fib k + Fib (k + 1) := by rfl
          _ < 2 ^ k + Fib (k + 1) := by rel [h5]
          _ < 2 ^ k + 2 ^ (k + 1) := by rel [h7]
          _ ≤ 2 ^ k + 2 ^ (k + 1) + 2 ^ k := by linarith
          _ = 2 ^ (k + 2) := by ring
      done
    done
  done

As with ordinary induction, strong induction can be useful for proving statements that do not at first seem to have the form ∀ (n : Nat), .... To illustrate this, we’ll prove the well-ordering principle, which says that if a set S : Set Nat is nonempty, then it has a smallest element. We’ll prove the contrapositive: if S has no smallest element, then it is empty. To say that S is empty means ∀ (n : Nat), n ∉ S, and that’s the statement to which we will apply strong induction.

theorem well_ord_princ (S : Set Nat) : (∃ (n : Nat), n ∈ S) →
    ∃ n ∈ S, ∀ m ∈ S, n ≤ m := by
  contrapos
  assume h1 : ¬∃ n ∈ S, ∀ m ∈ S, n ≤ m
  quant_neg                   --Goal : ∀ (n : Nat), n ∉ S
  by_strong_induc
  fix n : Nat
  assume ih : ∀ n_1 < n, n_1 ∉ S  --Goal : n ∉ S
  contradict h1 with h2       --h2 : n ∈ S
    --Goal : ∃ n ∈ S, ∀ m ∈ S, n ≤ m
  apply Exists.intro n        --Goal : n ∈ S ∧ ∀ m ∈ S, n ≤ m
  apply And.intro h2          --Goal : ∀ m ∈ S, n ≤ m
  fix m : Nat
  assume h3 : m ∈ S
  have h4 : m < n → m ∉ S := ih m
  contrapos at h4             --h4 : m ∈ S → ¬m < n
  have h5 : ¬m < n := h4 h3
  linarith
  done

Section 6.4 of HTPI ends with an example of an application of the well-ordering principle. The example gives a proof that \(\sqrt{2}\) is irrational. If \(\sqrt{2}\) were rational, then there would be natural numbers \(p\) and \(q\) such that \(q \ne 0\) and \(p/q = \sqrt{2}\), and therefore \(p^2 = 2q^2\). So we can prove that \(\sqrt{2}\) is irrational by showing that there do not exist natural numbers \(p\) and \(q\) such that \(q \ne 0\) and \(p^2 = 2q^2\).

The proof uses a definition from the exercises of Section 6.1:

def nat_even (n : Nat) : Prop := ∃ (k : Nat), n = 2 * k

We will also use the following lemma, whose proof we leave as an exercise for you:

lemma sq_even_iff_even (n : Nat) : nat_even (n * n) ↔ nat_even n := sorry

And we’ll need another theorem that we haven’t seen before:

@mul_left_cancel_iff_of_pos : ∀ {α : Type u_1} {a b c : α}
                    [inst : MulZeroClass α] [inst_1 : PartialOrder α]
                    [inst_2 : PosMulReflectLE α],
                    0 < a → (a * b = a * c ↔ b = c)

To show that \(\sqrt{2}\) is irrational, we will prove the statement

¬∃ (q p : Nat), p * p = 2 * (q * q) ∧ q ≠ 0

We proceed by contradiction. If this statement were false, then the set

S = {q : Nat | ∃ (p : Nat), p * p = 2 * (q * q) ∧ q ≠ 0}

would be nonempty, and therefore, by the well-ordering principle, it would have a smallest element. We then show that this leads to a contradiction. Here is the proof.

theorem Theorem_6_4_5 :
    ¬∃ (q p : Nat), p * p = 2 * (q * q) ∧ q ≠ 0 := by
  set S : Set Nat :=
    {q : Nat | ∃ (p : Nat), p * p = 2 * (q * q) ∧ q ≠ 0}
  by_contra h1
  have h2 : ∃ (q : Nat), q ∈ S := h1
  have h3 : ∃ q ∈ S, ∀ r ∈ S, q ≤ r := well_ord_princ S h2
  obtain (q : Nat) (h4 : q ∈ S ∧ ∀ r ∈ S, q ≤ r) from h3
  have qinS : q ∈ S := h4.left
  have qleast : ∀ r ∈ S, q ≤ r := h4.right
  define at qinS     --qinS : ∃ (p : Nat), p * p = 2 * (q * q) ∧ q ≠ 0
  obtain (p : Nat) (h5 : p * p = 2 * (q * q) ∧ q ≠ 0) from qinS
  have pqsqrt2 : p * p = 2 * (q * q) := h5.left
  have qne0 : q ≠ 0 := h5.right
  have h6 : nat_even (p * p) := Exists.intro (q * q) pqsqrt2
  rewrite [sq_even_iff_even p] at h6    --h6 : nat_even p
  obtain (p' : Nat) (p'halfp : p = 2 * p') from h6
  have h7 : 2 * (2 * (p' * p')) = 2 * (q * q) := by
    rewrite [←pqsqrt2, p'halfp]
    ring
    done
  have h8 : 2 > 0 := by decide
  rewrite [mul_left_cancel_iff_of_pos h8] at h7
    --h7 : 2 * (p' * p') = q * q
  have h9 : nat_even (q * q) := Exists.intro (p' * p') h7.symm
  rewrite [sq_even_iff_even q] at h9   --h9 : nat_even q
  obtain (q' : Nat) (q'halfq : q = 2 * q') from h9
  have h10 : 2 * (p' * p') = 2 * (2 * (q' * q')) := by
    rewrite [h7, q'halfq]
    ring
    done
  rewrite [mul_left_cancel_iff_of_pos h8] at h10
    --h10 : p' * p' = 2 * (q' * q')
  have q'ne0 : q' ≠ 0 := by
    contradict qne0 with h11
    rewrite [q'halfq, h11]
    rfl
    done
  have q'inS : q' ∈ S := Exists.intro p' (And.intro h10 q'ne0)
  have qleq' : q ≤ q' := qleast q' q'inS
  rewrite [q'halfq] at qleq'        --qleq' : 2 * q' ≤ q'
  contradict q'ne0
  linarith
  done

Exercises

--Hint: Use Exercise_6_1_16a1 and Exercise_6_1_16a2
--from the exercises of Section 6.1.
lemma sq_even_iff_even (n : Nat) :
    nat_even (n * n) ↔ nat_even n := sorry

--This theorem proves that the square root of 6 is irrational
theorem Exercise_6_4_4a :
    ¬∃ (q p : Nat), p * p = 6 * (q * q) ∧ q ≠ 0 := sorry

theorem Exercise_6_4_5 :
    ∀ n ≥ 12, ∃ (a b : Nat), 3 * a + 7 * b = n := sorry

theorem Exercise_6_4_7a : ∀ (n : Nat),
    (Sum i from 0 to n, Fib i) + 1 = Fib (n + 2) := sorry

theorem Exercise_6_4_7c : ∀ (n : Nat),
    Sum i from 0 to n, Fib (2 * i + 1) = Fib (2 * n + 2) := sorry

theorem Exercise_6_4_8a : ∀ (m n : Nat),
    Fib (m + n + 1) = Fib m * Fib n + Fib (m + 1) * Fib (n + 1) := sorry

theorem Exercise_6_4_8d : ∀ (m k : Nat), Fib m ∣ Fib (m * k) := sorry

Hint for #7: Let m be an arbitrary natural number, and then use induction on k. For the induction step, you must prove Fib m ∣ Fib (m * (k + 1)). If m = 0 ∨ k = 0, then this is easy. If not, then use exists_eq_add_one_of_ne_zero to obtain a natural number j such that m * k = j + 1, and therefore m * (k + 1) = j + m + 1, and then apply Exercise_6_4_8a.

def Fib_like (n : Nat) : Nat :=
  match n with
    | 0 => 1
    | 1 => 2
    | k + 2 => 2 * (Fib_like k) + Fib_like (k + 1)

theorem Fib_like_formula : ∀ (n : Nat), Fib_like n = 2 ^ n := sorry

def triple_rec (n : Nat) : Nat :=
  match n with
    | 0 => 0
    | 1 => 2
    | 2 => 4
    | k + 3 => 4 * triple_rec k +
                6 * triple_rec (k + 1) + triple_rec (k + 2)

theorem triple_rec_formula :
    ∀ (n : Nat), triple_rec n = 2 ^ n * Fib n := sorry

10. In this exercise you will prove that the numbers q and r in Example_6_4_1 are unique. It is helpful to prove a lemma first.

lemma quot_rem_unique_lemma {m q r q' r' : Nat}
    (h1 : m * q + r = m * q' + r') (h2 : r' < m) : q ≤ q' := sorry

theorem quot_rem_unique (m q r q' r' : Nat)
    (h1 : m * q + r = m * q' + r') (h2 : r < m) (h3 : r' < m) :
    q = q' ∧ r = r' := sorry

11. Use the theorem in the previous exercise to prove the following characterization of n / m and n % m.

theorem div_mod_char (m n q r : Nat)
    (h1 : n = m * q + r) (h2 : r < m) : q = n / m ∧ r = n % m := sorry

6.5. Closures Again

Section 6.5 of HTPI gives one more application of recursion and induction: another proof of the existence of closures of sets under functions. Recall from Section 5.4 that if f : A → A and B : Set A, then the closure of B under f is the smallest set containing B that is closed under f. In Section 5.4, we constructed the closure of B under f by taking the intersection of all sets containing B that are closed under f. In this section, we construct the closure by starting with the set B and repeatedly taking the image under f. For the motivation for this strategy, see HTPI; here we focus on how to carry out this strategy in Lean.

To talk about repeatedly taking the image of a set under a function, we will need a recursive definition:

def rep_image {A : Type} (f : A → A) (n : Nat) (B : Set A) : Set A :=
  match n with
    | 0 => B
    | k + 1 => image f (rep_image f k B)

According to this definition, rep_image f 0 B = B, rep_image f 1 B = image f B, rep_image f 2 B = image f (image f B), and so on. In other words, rep_image f n B is the result of starting with B and then taking the image under f n times. To make it easier to work with this definition, we state two simple theorems, both of which follow immediately from the definition.

theorem rep_image_base {A : Type} (f : A → A) (B : Set A) :
    rep_image f 0 B = B := by rfl

theorem rep_image_step {A : Type} (f : A → A) (n : Nat) (B : Set A) :
    rep_image f (n + 1) B = image f (rep_image f n B) := by rfl

We will prove that the closure of B under f is the union of the sets rep_image f n B. We will call this the cumulative image of B under f, and we define it as follows:

def cumul_image {A : Type} (f : A → A) (B : Set A) : Set A :=
  {x : A | ∃ (n : Nat), x ∈ rep_image f n B}

To prove that cumul_image f B is the closure of B under f, we first prove a lemma saying that if B ⊆ D and D is closed under f, then for every natural number n, rep_image f n B ⊆ D. We prove it by induction.

lemma rep_image_sub_closed {A : Type} {f : A → A} {B D : Set A}
    (h1 : B ⊆ D) (h2 : closed f D) :
    ∀ (n : Nat), rep_image f n B ⊆ D := by
  by_induc
  · -- Base Case
    rewrite [rep_image_base]          --Goal : B ⊆ D
    show B ⊆ D from h1
    done
  · -- Induction Step
    fix n : Nat
    assume ih : rep_image f n B ⊆ D   --Goal : rep_image f (n + 1) B ⊆ D
    fix x : A
    assume h3 : x ∈ rep_image f (n + 1) B  --Goal : x ∈ D
    rewrite [rep_image_step] at h3
    define at h3    --h3 : ∃ x_1 ∈ rep_image f n B, f x_1 = x
    obtain (b : A) (h4 : b ∈ rep_image f n B ∧ f b = x) from h3
    rewrite [←h4.right]   --Goal : f b ∈ D    
    have h5 : b ∈ D := ih h4.left
    define at h2          --h2 : ∀ x ∈ D, f x ∈ D
    show f b ∈ D from h2 b h5
    done
  done

With this preparation, we can now prove that cumul_image f B is the closure of B under f.

theorem Theorem_6_5_1 {A : Type} (f : A → A) (B : Set A) :
    closure f B (cumul_image f B) := by
  define
  apply And.intro
  · -- Proof that cumul_image f B ∈ {D : Set A | B ⊆ D ∧ closed f D}
    define  --Goal : B ⊆ cumul_image f B ∧ closed f (cumul_image f B)
    apply And.intro
    · -- Proof that B ⊆ cumul_image f B
      fix x : A
      assume h1 : x ∈ B
      define     --Goal : ∃ (n : Nat), x ∈ rep_image f n B
      apply Exists.intro 0
      rewrite [rep_image_base]  --Goal : x ∈ B
      show x ∈ B from h1
      done
    · -- Proof that cumul_image f B closed under f
      define
      fix x : A
      assume h1 : x ∈ cumul_image f B  --Goal : f x ∈ cumul_image f B
      define at h1
      obtain (m : Nat) (h2 : x ∈ rep_image f m B) from h1
      define     --Goal : ∃ (n : Nat), f x ∈ rep_image f n B
      apply Exists.intro (m + 1) --Goal : f x ∈ rep_image f (m + 1) B
      rewrite [rep_image_step]   --Goal : f x ∈ image f (rep_image f m B)
      define     --Goal : ∃ x_1 ∈ rep_image f m B, f x_1 = f x
      apply Exists.intro x  --Goal : x ∈ rep_image f m B ∧ f x = f x
      apply And.intro h2
      rfl
      done
    done
  · -- Proof that cumul_image f B is smallest
    fix D : Set A
    assume h1 : D ∈ {D : Set A | B ⊆ D ∧ closed f D}
    define at h1  --h1 : B ⊆ D ∧ closed f D
    define   --Goal : ∀ ⦃a : A⦄, a ∈ cumul_image f B → a ∈ D
    fix x : A
    assume h2 : x ∈ cumul_image f B  --Goal : x ∈ D
    define at h2  --h2: ∃ (n : Nat), x ∈ rep_image f n B
    obtain (m : Nat) (h3 : x ∈ rep_image f m B) from h2
    have h4 : rep_image f m B ⊆ D :=
      rep_image_sub_closed h1.left h1.right m
    show x ∈ D from h4 h3
    done
  done

Exercises

1. Recall the following definitions from the exercises of Section 5.4:

def closed_family {A : Type} (F : Set (A → A)) (C : Set A) : Prop :=
  ∀ f ∈ F, closed f C

def closure_family {A : Type} (F : Set (A → A)) (B C : Set A) : Prop :=
  smallestElt (sub A) C {D : Set A | B ⊆ D ∧ closed_family F D}

These definitions say that a set is closed under a family of functions if it is closed under all of the functions in the family, and the closure of a set B under a family of functions is the smallest set containing B that is closed under the family.

In this exercise we will use the following additional definitions:

def rep_image_family {A : Type}
    (F : Set (A → A)) (n : Nat) (B : Set A) : Set A :=
  match n with
    | 0 => B
    | k + 1 => {x : A | ∃ f ∈ F, x ∈ image f (rep_image_family F k B)}

def cumul_image_family {A : Type}
    (F : Set (A → A)) (B : Set A) : Set A :=
  {x : A | ∃ (n : Nat), x ∈ rep_image_family F n B}

The following theorems establish that if F : Set (A → A) and B : Set A, then cumul_image_family F B is the closure of B under F. The first two are proven by rfl; the other two are for you to prove.

theorem rep_image_family_base {A : Type}
    (F : Set (A → A)) (B : Set A) : rep_image_family F 0 B = B := by rfl

theorem rep_image_family_step {A : Type}
    (F : Set (A → A)) (n : Nat) (B : Set A) :
    rep_image_family F (n + 1) B =
    {x : A | ∃ f ∈ F, x ∈ image f (rep_image_family F n B)} := by rfl

lemma rep_image_family_sub_closed {A : Type}
    (F : Set (A → A)) (B D : Set A)
    (h1 : B ⊆ D) (h2 : closed_family F D) :
    ∀ (n : Nat), rep_image_family F n B ⊆ D := sorry

theorem Exercise_6_5_3 {A : Type} (F : Set (A → A)) (B : Set A) :
    closure_family F B (cumul_image_family F B) := sorry

The next two exercises concern the following two definitions from Section 5.4:

def closed2 {A : Type} (f : A → A → A) (C : Set A) : Prop :=
  ∀ x ∈ C, ∀ y ∈ C, f x y ∈ C

def closure2 {A : Type} (f : A → A → A) (B C : Set A) : Prop := 
  smallestElt (sub A) C {D : Set A | B ⊆ D ∧ closed2 f D}

They also use the following definition, which extends the idea of the image of a set under a function to functions of two variables:

def image2 {A : Type} (f : A → A → A) (B : Set A) : Set A :=
  {z : A | ∃ (x y : A), x ∈ B ∧ y ∈ B ∧ z = f x y}

2. A natural way to try to find the closure of a set under a function of two variables would be to use the following definitions and theorems:

def rep_image2 {A : Type}
    (f : A → A → A) (n : Nat) (B : Set A) : Set A :=
  match n with
    | 0 => B
    | k + 1 => image2 f (rep_image2 f k B)

theorem rep_image2_base {A : Type} (f : A → A → A) (B : Set A) :
    rep_image2 f 0 B = B := by rfl

theorem rep_image2_step {A : Type}
    (f : A → A → A) (n : Nat) (B : Set A) :
    rep_image2 f (n + 1) B = image2 f (rep_image2 f n B) := by rfl

def cumul_image2 {A : Type} (f : A → A → A) (B : Set A) : Set A :=
  {x : A | ∃ (n : Nat), x ∈ rep_image2 f n B}

We could now try to prove that if f : A → A → A and B : Set A, then cumul_image2 f B is the closure of B under f. However, this approach doesn’t work, because cumul_image2 f B might not be closed under f.

Here is an incorrect informal argument that cumul_image2 f B is closed under f. Suppose x and y are elements of cumul_image2 f B. This means that we can choose some natural number n such that x ∈ rep_image2 f n B and y ∈ rep_image2 f n B. This implies that f x y ∈ image2 f (rep_image2 f n B) = rep_image2 f (n + 1) B, so f x y ∈ cumul_image2 f B.

Find the mistake in this informal argument by trying to turn it into a proof in Lean:

--You won't be able to complete this proof
theorem Exercise_6_5_6 {A : Type} (f : A → A → A) (B : Set A) :
    closed2 f (cumul_image2 f B) := sorry

3. In this exercise, we fix the mistake in the attempted proof in the previous exercise. Instead of repeatedly taking the image of a set, we repeatedly take the union of a set with its image:

def un_image2 {A : Type} (f : A → A → A) (B : Set A) : Set A :=
  B ∪ (image2 f B)

def rep_un_image2 {A : Type}
    (f : A → A → A) (n : Nat) (B : Set A) : Set A :=
  match n with
    | 0 => B
    | k + 1 => un_image2 f (rep_un_image2 f k B)

theorem rep_un_image2_base {A : Type} (f : A → A → A) (B : Set A) :
    rep_un_image2 f 0 B = B := by rfl

theorem rep_un_image2_step {A : Type}
    (f : A → A → A) (n : Nat) (B : Set A) :
    rep_un_image2 f (n + 1) B =
    un_image2 f (rep_un_image2 f n B) := by rfl

def cumul_un_image2 {A : Type}
    (f : A → A → A) (B : Set A) : Set A :=
  {x : A | ∃ (n : Nat), x ∈ rep_un_image2 f n B}

Now prove that if f : A → A → A and B : Set A, then cumul_un_image2 f B is the closure of B under f by completing the following proofs:

theorem Exercise_6_5_8a {A : Type} (f : A → A → A) (B : Set A) :
    ∀ (m n : Nat), m ≤ n →
    rep_un_image2 f m B ⊆ rep_un_image2 f n B := sorry

lemma rep_un_image2_sub_closed {A : Type} {f : A → A → A} {B D : Set A}
    (h1 : B ⊆ D) (h2 : closed2 f D) :
    ∀ (n : Nat), rep_un_image2 f n B ⊆ D := sorry

lemma closed_lemma
    {A : Type} {f : A → A → A} {B : Set A} {x y : A} {nx ny n : Nat}
    (h1 : x ∈ rep_un_image2 f nx B) (h2 : y ∈ rep_un_image2 f ny B)
    (h3 : nx ≤ n) (h4 : ny ≤ n) :
    f x y ∈ cumul_un_image2 f B := sorry

theorem Exercise_6_5_8b {A : Type} (f : A → A → A) (B : Set A) :
    closure2 f B (cumul_un_image2 f B) := sorry

The remaining exercises in this section use the following definitions:

def idExt (A : Type) : Set (A × A) := {(x, y) : A × A | x = y}

def rep_comp {A : Type} (R : Set (A × A)) (n : Nat) : Set (A × A) :=
  match n with
    | 0 => idExt A
    | k + 1 => comp (rep_comp R k) R

def cumul_comp {A : Type} (R : Set (A × A)) : Set (A × A) :=
  {(x, y) : A × A | ∃ n ≥ 1, (x, y) ∈ rep_comp R n}

theorem rep_comp_one {A : Type} (R : Set (A × A)) :
    rep_comp R 1 = R := sorry

theorem Exercise_6_5_11 {A : Type} (R : Set (A × A)) :
    ∀ (m n : Nat), rep_comp R (m + n) =
    comp (rep_comp R m) (rep_comp R n) := sorry

lemma rep_comp_sub_trans {A : Type} {R S : Set (A × A)}
    (h1 : R ⊆ S) (h2 : transitive (RelFromExt S)) :
    ∀ n ≥ 1, rep_comp R n ⊆ S := sorry

theorem Exercise_6_5_14 {A : Type} (R : Set (A × A)) :
    smallestElt (sub (A × A)) (cumul_comp R)
    {S : Set (A × A) | R ⊆ S ∧ transitive (RelFromExt S)} := sorry