17 - Using Our Own Lemma

In the last post we created our own lemma. 

Here we'll make use of that lemma to prove a disequality. 

Task

For any natural number $n$, show that

$$n^2\ne 7$$

Maths

Intuitively, we can see that small n leads to an $n^2$ less than 7, and large $n$ results in $n^2$ larger than 7. 

So a proof strategy is to split the natural number sequence into two, so that all the smaller numbers result in $n^2<7$, and all the larger numbers in $n^2>7$. If every possible choice for $n$ leads to either $n^2<7$ or $n^2>7$, then clearly $n^2\ne 7$.

Let's write this out in small steps as preparation for a Lean proof.

$$\begin{array}{rlrl}{n}^2& \ne 7& & \text{proof objective}\\ & & & \\ \text{(1)}& n\le m& \vee m+1\le n& & \text{our lemma, for }m,n\in \mathbb{N}& & & \\ \text{(2)}& n\le 2& \vee 3\le n& & \text{lemma (}\text{1}\text{) with }m=2& & & \\ \text{case }n\le 2& & & \text{using }(\text{2})\\ n^2& \le 4& & \\ & <7& & \\ \text{(3)}& n^2& \ne 7& & \text{lemma }a<b⟹a\ne b& & & \\ \text{case }n\ge 3& & & \text{using }(\text{2})\\ n^2& \ge 9& & \\ & >7& & \\ \text{(4)}& n^2& \ne 7& & \text{lemma }a>b⟹a\ne b& & & \\ ◻& n& \ne 7& & \text{conclusion of both cases}\end{array}$$

We use our lemma (1) to split the natural numbers into two sets, so that for any $n\in \mathbb{N}$ we have either $n\le 2$ or $3\le n$. 

This is a disjunction of two cases, $n\le 2$ and $n\ge 3$. 

• The first case $n\le 2$ means $n^2\le 4$, which also means $n^2<7$. The conclusion $n^2\ne 7$ seem obvious, but we do need to justify it. We can use a tiny lemma $a<b⟹a\ne b$.
• The second case $n\ge 3$ means $n^2\ge 9$, which also means $n^2>7$. Using another small lemma $a>b⟹a\ne b$, we conclude $n^2\ne 7$.

Both cases lead to $n^2\ne 7$, completing the proof.

Code

The following Lean program proves $n^2\ne 7$ for any natural number n using our lemma. 

-- 17 - Using Our Own Lemma

import Mathlib.Tactic

---

lemma Nat.le_or_succ_le (a b : ℕ): a ≤ b ∨ b + 1 ≤ a := by
  rw [Nat.add_one_le_iff]
  exact le_or_lt a b

---

example {n : ℕ} :  n^2 ≠ 7  := by
  have h := Nat.le_or_succ_le n 2
  obtain ha | hb := h
  · apply ne_of_lt
    calc
      n^2 ≤ 2^2 := by rel [ha]
      _ < 7 := by norm_num
  · apply ne_of_gt
    calc
      n^2 ≥ 3^2 := by rel [hb]
      _ > 7 := by norm_num

The code is separated into two sections by comment dashes. 

The first section is a copy of the lemma we developed in the last chapter, Nat.le_or_succ_le.

The second section is the Lean proof that $n^2\ne 7$. Let's break it down.

• Our lemma Nat.le_or_succ_le with parameters n and 2, gives us n ≤ 2 ∨ 2 + 1 ≤ n. We capture this as hypothesis h using have. 
• That hypothesis h is a disjunction, so we use obtain to split it into two cases, n ≤ 2 and 2 + 1 ≤ n.
• The first case starts by changing the goal from n^2 ≠ 7 to n^2 < 7 by applying a Mathlib lemma ne_of_lt. Its definition confirms that if we can prove n^2 < 7 then we've proven n^2 ≠ 7:

lemma ne_of_lt (h : a < b) : a %$\ne$% b :=

We then use a calc section to show n^2 ≤ 2^2 from the current case n ≤ 2 , then 2^2 < 7, all of which resolves the goal n^2 < 7.

• The second case is similar. It starts by changing the goal from n^2 ≠ 7 to n^2 > 7 by applying a Mathlib lemma ne_of_gt. Its definition confirms that if we can prove n^2 > 7 then we've proven n^2 ≠ 7:

lemma ne_of_gt (h : b < a) : a %$\ne$% b :=

Again, we use a calc section to show n^2 ≥ 3^2 from the current case 2 + 1 ≤ n , then 3^2 > 7, all of which resolves the goal n^2 > 7.

Libraries of Lemmas

If our lemma Nat.le_or_succ_le is used in several proofs, then having a copy accompanying each can become a little untidy, and make it more difficult to maintain. 

In the wider world of software, re-usable code is packaged into libraries. We can do the same with Lean lemmas and theorems. Appendix B explains briefly how to do this.

---

Easy Exercise

Write a Lean proof to show that $n^3\ne 10$, for any natural number $n$.