18 - Our Own Definition

At the start of Part III we used Mathlib's definition of odd and even numbers.

Here we'll create our own definition of triangle numbers.

Task

The following picture illustrates triangle numbers. The first few are 1, 3, 6, 10, 15, 21 and 28. 

In general, the $n$th triangle number is 

$$\frac{n \cdot (n+1)}{2}$$

We saw previously the Mathlib definition of Odd didn't produce the $n$th odd number. Instead the definition is a proposition about a supplied number. So Odd 3 is true, but Odd 4 is false.

Our task is to create a definition of triangle numbers that is a proposition, true only if the supplied number is actually a triangle number.

Maths

A proposition for a triangle number $T$ could be:

$$\exists n\in\mathbb{N}\quad[\;T=\frac{n\cdot(n+1)}{2}\;]$$

This proposition is only true if $T$ is a triangle number. That is, if $T$ can be expressed in the form $n\cdot(n+1)/2$ for some natural number $n$.

When working with natural numbers, we should be cautious about dividing them. In this case division is safe because either $n$ or $(n+1)$ is an even number, and so $n \cdot (n+1)$ is divisible by $2$. 

Even so, let's avoid division of natural numbers as good practice. We'll adjust the proposition to the equivalent:

$$\exists n\in\mathbb{N}\quad[\;2 T=n\cdot(n+1)\;]$$

That is, $T$ is a triangle number if $2 T$ can be expressed in the form $n\cdot(n+1)$ for some natural number $n$.

Code

The following Lean code creates a definition of triangle numbers.

-- 18 - Our Own Definition

import Mathlib.Tactic

def Triangle (a : ℕ) : Prop := ∃ n, 2 * a = n * (n + 1)

example : Triangle 10 := by
  dsimp [Triangle]
  use 4

The keyword def signals we're about to create a named definition. Here the name is Triangle.

After that is a declaration of variables, here a as a natural number. The round brackets require anyone using the definition to provide a as a parameter.

The Prop specifies that Triangle will be a proposition, a statement that can be true or false. 

After the := is the actual detail of the definition of a triangle number, ∃ n, 2 * a = n * (n + 1). 

The following picture summarises the structure of simple definitions.

When creating our own definitions, it is considerate to provide a minimal example that illustrates how to use the definition. 

Here the example is a proof of Triangle 10, a proposition that says $10$ is a triangle number. The dsimp [Triangle] unfolds the definition in the Infoview. Because the definition is a “there exists” statement, the proof is resolved by a simple use 4.

Infoview

Placing the cursor before dsimp [Triangle] in the illustrative example shows the proof objective.

⊢ Triangle 10

Moving the cursor to the start of the next line shows the goal with the definition of Triangle unfolded.

⊢ ∃ n, 20 = n * (n + 1)

Types & Terms

Let's take a first peek at the hierarchy of objects in Lean.

Compare the definition of Triangle with a definition of Triple that I just made up:

def Triangle (a : ℕ) : Prop := ∃ n, 2 * a = n * (n + 1)

def Triple (a : ℕ) : ℕ := 3 * a

The type of Triangle is Prop, a proposition. The type of Triple is ℕ, a natural number.

We say the detail ∃ n, 2 * a = n * (n + 1) is a term of type Prop. Similarly, 3 * a is a term of type ℕ.

Appendix A illustrates the hierarchy of objects in Lean and Mathlib. The diagram there shows 13 is a term of type ℕ. What may be surprising is that proofs are terms of type Prop.

Knowing this isn't crucial at this stage of our learning, but it can help us read and write Lean proofs with an additional level of understanding.

---

Easy Exercise

Create a definition of square numbers named Square. It should be a proposition which is only true if a given number can be written in the form $n^{2}$, for some natural number $n$.

Write a proof showing 25 is a square number, illustrating the use of Square.

Appendix B - Libraries

Packaging your own lemmas and theorems into a library is a tidier way of maintaining them, and making them available for others to use.

Library

In your project's lakefile.lean file, add a reference to the Lean file which contains your lemmas. 

lean_lib MyLeanLemmas

Replace MyLeanLemmas with the name you want for your own library.

Using A Library

To use the lemmas in the MyLeanLemmas library, we simply use import at the top of our lean program.

import Mathlib.Tactic

import MyLeanLemmas

It is a good habit to import additional libraries after any official Mathlib libraries. 

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$.

16 - Writing Our Own Lemma

Mathlib has many lemmas and theorems for us to use. We can also write our own.

Here we'll create a small but convenient lemma about the natural numbers.

Task

If we pick a natural number $b$, then any other natural number $a$ must be less than or equal to $b$, or greater than or equal to $b+1$. 

The following illustrates this idea.

By the definition of natural numbers, $b+1$ is the successor of $b$, so we can be sure a is not in the “gap” from b to b+1.

Our task is to create a lemma for natural numbers $a$ and $b$ that says

$$\boxed{a\le b\;\lor\;b+1\le a}$$

Let's bring this to life with an example. If we say $b=7$, but leave $a$ unspecified, the lemma tells us that either $a\le7$ or $8\le a$, which makes sense.

Maths

To prove our lemma we'll try to make use of lemmas that also exist in Mathlib, not only to shorten the proof, but also to ease the transition to a Lean proof.

$$\begin{align}a\le b\;&\lor\;b+1\le a&&\text{proof objective, }a,b\in\mathbb{N}\\&&&\\a\le b\;&\lor\;b<a&&\text{known lemma, }a,b\in\mathbb{N}\tag{1}\label{16.1}\\m+1\le n&\iff m<n&&\text{known lemma, }m,n\in\mathbb{N}\tag{2}\label{16.2}\\&&&\\a\le b\;&\lor\;b+1\le a&&\text{apply lemma }(\ref{16.2})\text{ to }(\ref{16.1})\tag*{\(\Box\)}\end{align}$$

Lemma (1) is already very close to our proof objective. It says that $a\le b\lor b<a$ for any natural numbers $a$ and $b$. 

Lemma (2) says that $m+1\le n$ is equivalent to $m<n$, for natural numbers $m$ and $n$. It lets us rewrite $b<a$ as $b+1\le a$, which immediately gives us the proof objective.

Both lemmas (1) and (2) exist in Mathlib.

Code

The following Lean code creates a lemma that says either $a\le b$ or $b+1\le a$, for natural numbers $a$ and $b$. 

-- 16 - Writing 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 {c : ℕ} :  c ≤ 2 ∨ 3 ≤ c  := by
  exact Nat.le_or_succ_le c 2

The lemma header starts with lemma Nat.le_or_succ_le to tell Lean we want to create a new lemma named Nat.le_or_succ_le. 

The Nat. prefix is conventional for lemmas about natural numbers. The rest of the name le_or_succ_le tries to follow the naming convention to describe what the lemma is about. 

The Lean proofs we've previously explored started with example and no name. They can be thought of as anonymous lemmas, anonymous because there was no need to refer to them after they'd been proved.

The remainder of the header declares a and b as natural numbers, and states the lemma's proposal a ≤ b ∨ b + 1 ≤ a. The round brackets around the variables (a b : ℕ) require anyone using the lemma to always provide a and b as parameters.

Our lemma is proved in just two lines of code by making effective use of existing Mathlib lemmas:

• The first line of the proof rewrites the goal using a Mathlib lemma Nat.add_one_le_iff. Let's check its header:

• 
  theorem add_one_le_iff : n + 1 ≤ m ↔ n < m :=

The rw tactic is akin to “find and replace”, so it looks at the goal a ≤ b ∨ b + 1 ≤ a and finds b + 1 ≤ a matches the left hand side of the Nat.add_one_le_iff lemma. The matched b + 1 ≤ a is  rewritten with the right hand side of the lemma b < a.

• As we'll see in the Infoview, the goal is now a ≤ b ∨ b < a.
• The final line of the proof applies another Mathlib lemma le_or_lt. Let's check its header:

• 
  lemma le_or_lt (a b : α) : a ≤ b ∨ b < a :=
  

  This lemma le_or_lt says that, given two numbers a and b, then a ≤ b ∨ b < a. This matches our current goal exactly, so we can use exact to resolve it and complete the proof.

Notice how the header of the Mathlib lemma le_or_lt (a b : α) uses round brackets requiring us to provide a and b when we use it.

Infoview

Placing the cursor before rw [Nat.add_one_le_iff] shows the original proof goal.

⊢ a ≤ b ∨ b + 1 ≤ a

Moving the cursor to the start of the next line shows the rewritten goal.

⊢ a ≤ b ∨ b < a

Minimal Example

When writing your own lemmas, it is considerate to provide a minimal example showing how to use them. 

The minimal example here illustrates how to use our lemma to prove $c\le2\lor3\le c$ for any natural number $c$.  

With a set to c, and b set to 2, our lemma becomes c ≤ 2 ∨ 3 ≤ c. This matches the proof goal exactly, allowing us to use exact to complete the proof neatly in one line.

Forwards & Backwards

Comparing the maths and Lean proofs, we can see they are similar, but not quite the same.

• The maths proof starts with a lemma $a\le b\lor b<a$ and uses another lemma to arrive at the goal $a\le b\lor b+1\le a$.
• The Lean proof starts with the goal $a\le b\lor b+1\le a$ and uses another lemma to  arrive at an equivalent statement, which happens to be a known lemma $a\le b\lor b<a$.

The proofs go in opposite directions. Where one starts, the other finishes.

Starting with the proof objective and resolving it down to known true facts, rather than building up from known facts to a proof objective, will be a little more common with Lean proofs because many of the tactics bias towards operating on the current goal.

Just for interest, the following is a Lean proof which follows the same path as the maths proof.

lemma Nat.le_or_succ_le (a b: ℕ): a ≤ b ∨ b + 1 ≤ a := by
  have h : a ≤ b ∨ b < a := le_or_lt a b
  rw [← Nat.succ_le] at h
  exact h

The left arrow in rw [← Nat.succ_le] selects the reverse direction of the bidirectional lemma.

---

Easy Exercise

Write a lemma for integers $a$ and $b$ that says

$$a\le b\;\lor\;b+1\le a$$

Create a minimal example illustrating how your lemma can prove the following for any integer $c$.

$$c\le-5\;\lor\;-4\le c$$

15 - Zero Product

Some lemmas are bidirectional implications. To apply them, we need to decide which of the two directions match our task.

Here we'll apply such a lemma to help solve an equation.

Task

Given the zero product

$$(p-1)\cdot(q-2)=0$$

show that

$$p=1\text{ or }q=2$$

where $p$ and $q$ are rational numbers.

Maths

It is common knowledge that the product of two numbers, $a$ and $b$, is zero, if and only if, one or the other is zero. 

We'll think of this as a lemma,

$$a\cdot b=0\iff(a=0)\lor(b=0)$$

A statement of the form $P\iff Q$ is equivalent to both of the following being true:

• $P\implies Q$
• $Q\implies P$

We say “$P$ is true if and only if $Q$ is true” or “$P$ is true iff $Q$ is true.”

So our lemma is equivalent to the following two statements:

• $a\cdot b=0\implies(a=0)\lor(b=0)$
• $(a=0)\lor(b=0)\implies a\cdot b=0$

The antecedent of the first matches our hypothesis $(p-1)\cdot(q-2)=0$, so applying it gives us a disjunction.

$$(p-1=0)\lor(q-2=0)$$

We could conclude $p=1$ or $q=2$ just by looking at this, but to write a Lean proof we'll need to plan out more detail.

$$\begin{align}(p-1)\cdot(q-2)&=0&&\text{hypothesis}\tag{1}\label{15.1}\\&&&\\a\cdot b=0&\iff(a=0)\lor(b=0)&&\text{existing lemma}\tag{2}\label{15.2}\\&&&\\(p-1=0)&\lor(q-2=0)&&\text{apply lemma }(\ref{15.2})\text{ to }(\ref{15.1})\tag{3}\label{15.3}\\&&&\\\text{case }p-1=0&&&\text{using }(\ref{15.3})\\p&=1&&\text{add 1 to both sides}\\&&&\\\text{case }q-2=0&&&\text{using }(\ref{15.3})\\q&=2&&\text{add 2 to both sides}\\&&&\\(p=1)&\lor(q=2)&&\text{conclusion}\tag*{\(\Box\)}\end{align}$$

The key step is applying the lemma (2) to the hypothesis (1) to derive a new intermediate result (3).

This intermediate result is a disjunction $(p-1=0)\lor(q-2=0)$, and so the proof proceeds as a proof by cases.

Code

The following Lean program proves that $p=1$ or $q=2$ given $(p-1)\cdot(q-2)=0$, where $p,q\in\mathbb{Q}$.

-- 15 - Using Lemmas: Multiplied Factors Equal Zero

import Mathlib.Tactic

example {p q : ℚ} (h : (p - 1) * (q - 2) = 0) : p = 1 ∨ q = 2 := by
  apply mul_eq_zero.mp at h
  obtain hp | hq := h
  · left
    linarith
  · right
    linarith

Mathlib has a lemma mul_eq_zero which expresses the idea we want to use, that $a\cdot b=0\iff(a=0)\lor(b=0)$. 

It's a good habit to look up the header of any lemma we plan to use. This allows us to check the lemma works as we imagine it does.

theorem mul_eq_zero : a * b = 0 ↔ a = 0 ∨ b = 0 :=

The first line of the proof applies mul_eq_zero to hypothesis h, but the lemma name has a .mp appended.

• Adding .mp to a bidirectional lemma selects the forward direction. 
• Adding .mpr to a bidirectional lemma selects the reverse direction.

The mp is “modus ponens”, terminology from the field of logic for the process of reaching a conclusion using an implication.

The Infoview will confirm the hypothesis has been replaced with the equivalent disjunction p - 1 = 0 ∨ q - 2 = 0.

The proof then proceeds as a proof by cases.

• The obtain instruction splits the hypotheses h into two cases, p - 1 = 0 and q - 2 = 0. We then use focussing dots to organise the sub-proofs for each of these cases.
• The first case uses left to state our intention to prove the left side of the disjunctive proof goal, p = 1. The linarith tactic can perform an “add a number to both sides” to justify the goal p = 1 from the current hypotheses, one of which is hp : p - 1 = 0.
• The second case is almost the same, but we use right to state our intention to prove the right side of the disjunctive proof goal, q = 2.

Both cases, p - 1 = 0 and q - 2 = 0, confirm the same disjunctive proof goal, so the proof is complete.

Replacing A Hypothesis?

In the maths proof we derived an intermediate result from the hypothesis, but in the Lean code the hypothesis was replaced.

Mathematically, the original hypothesis (1) always holds. The lemma allows us to derive an equivalent, but more useful, intermediate result (3). Because it is equivalent, we could replace the original hypothesis, but that's not how we write maths proofs.

In the Lean proof, the apply tactic does actually replace the original hypothesis. This is valid only because the new hypothesis is equivalent to the original. If we wanted to preserve the original hypothesis, we could use have to create a new intermediate result.

Infoview

Placing the cursor before apply mul_eq_zero.mp at h shows the original hypothesis.

h : (p - 1) * (q - 2) = 0

Moving the cursor to the beginning of the next line shows the hypothesis has been replaced.

h : p - 1 = 0 ∨ q - 2 = 0

---

Easy Exercise

Write a Lean program to prove $(p-1)\cdot(q-2)\ne0$ given $p-1\ne0$ and $q-2\ne0$, where $p$ and $q$ are rational numbers.

Use the lemma mul_ne_zero_iff. Look up the lemma's header to understand what it actually says, then decide in which direction to apply it.