Saturday, November 23, 2024

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}\ne7$$


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}\ne7$.

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

$$\begin{align}n^{2}&\ne7&&\text{proof objective}\\&&&\\n\le m&\lor m+1\le n&&\text{our lemma, for }m,n\in\mathbb{N}\tag{1}\label{17.1}\\&&&\\n\le2&\lor3\le n&&\text{lemma (\ref{17.1}) with }m=2\tag{2}\label{17.2}\\&&&\\\text{case }n\le2&&&\text{using }(\ref{17.2})\\n^{2}&\le4&&\\&<7&&\\n^{2}&\ne7&&\text{lemma }a < b\implies a\ne b\tag{3}\label{17.3}\\&&&\\\text{case }n\ge3&&&\text{using }(\ref{17.2})\\n^{2}&\ge9&&\\&>7&&\\n^{2}&\ne7&&\text{lemma }a > b\implies a\ne b\tag{4}\label{17.4}\\&&&\\n&\ne7&&\text{conclusion of both cases}\tag*{\(\Box\)}\end{align}$$

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\le2$ or $3\le n$. 

This is a disjunction of two cases, $n\le2$ and $n\ge3$. 

  • The first case $n\le2$ means $n^{2}\le4$, which also means $n^{2}<7$. The conclusion $n^{2}\ne7$ seem obvious, but we do need to justify it. We can use a tiny lemma $a<b\implies a\ne b$.
  • The second case $n\ge3$ means $n^{2}\ge9$, which also means $n^{2}>7$. Using another small lemma $a>b\implies a\ne b$, we conclude $n^{2}\ne7$.

Both cases lead to $n^{2}\ne7$, completing the proof.


Code

The following Lean program proves $n^{2}\ne7$ 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}\ne7$. 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}\ne10$, for any natural number $n$.


at