05 - Inequalities

In the first post, we only used inequalities at the final step of each proof, to establish $4>1$ and $4<10$. These were simple numerical comparisons.

Here we have inequalities as the hypotheses of the theorem we want to prove. 

Task

Given the facts

$$\begin{align}b & = a^{2} \\ a & \geq 2 \end{align}$$

our task is to show

$$b\geq4$$

where $a$ and $b$ are natural numbers.

Maths

Let's pause and consider what's different about this task compared to the first chapter. 

Here the conclusion holds for any $a \geq 2$. In the first chapter a was very specifically constrained to $a=4$. So this theorem is much broader in scope. 

The first post's proof concluded with $4>1$, justified by a simple numerical comparison. We can't do that here because $b$ in $b \geq 4$ could be any one of an infinity of natural numbers. 

Let's write out a proof.

$$\begin{align} b&=a^{2}&&\text{given fact}\tag{1}\label{5.1}\\a&\geq2&&\text{given fact}\tag{2}\label{5.2}\\&&&\\b&=a^{2}&&\text{using fact }(\ref{5.1})\\&\geq(2)^{2}&&\text{using fact }(\ref{5.2})\\&=4&&\text{using arithmetic}\tag*{\(\Box\)} \end{align}$$

Let's break it down:

• We first list the given facts, $b=a^{2}$ and $a\geq2$.
• We start with the expression we want to prove something about, $b$. We say this is $a^{2}$ justified by the first given fact.
• Our aim is to express $b$ as a comparison to $4$, so we want to resolve $a$.
• The second fact $a\geq2$ gives us $a^{2}\geq(2)^{2}$.
• Finally, we say $(2)^{2}=4$, giving us the desired conclusion.

It is easy to misread the proof as stating $b=4$. The correct reading is that $b=a^{2}$, and $a^{2}\geq(2)^{2}$, and finally $(2)^{2}=4$. We can tie this chain of inequalities together, and summarise them as $b\geq4$. 

Code

The following Lean program proves $b\geq4$ given $b=a^{2}$ and $a\geq2$.

-- 05 - Simple Inequality

import Mathlib.Tactic

example {a b : ℕ} (h1 : b = a^2) (h2: a ≥ 2) : b ≥ 4 := by
  calc
    b = a^2 := by rw [h1]
    _ ≥ (2)^2 := by rel [h2]
    _ = 4 := by norm_num

The second hypothesis, the proof objective, and one of the lines in the proof body uses an inequality ≥ rather than an equality =. Aside from that, there's nothing structurally different about this proof. 

The rel tactic is new. It is used to justify statements about relations, such as “greater than or equal to”. 

Here the rel tactic is combining a^2 and the hypothesis a ≥ 2 to give a^2 ≥ (2)^2. 

---

Easy Exercise

Write a Lean program to prove $a<c$ if we know $a<b$ and $b\leq c$, where $a$, $b$ and $c$ are natural numbers.

04 - Simple Algebra

Task

We now take a step up, and require Lean to do some algebra.

Our task is to show the following is true

$$(a+b)(a-b)=a^{2}-b^{2}$$

We'll assume $a$ and $b$ are integers.

Maths

Let's try to write out a proof, aiming to show and justify each step.

$$\begin{align}(a+b)(a-b)&=a^{2}-ab+ba-b^{2}&&\text{by algebra}\\&=a^{2}-b^{2}&&\text{by algebra}\tag*{\(\Box\)}\end{align}$$

This proof is much simpler than our previous ones. There is no need for any hypotheses, there are no substitutions, and no arithmetic. 

• We start with the expression we want to prove something about, $(a+b)(a-b)$.
• We expand out the brackets, multiplying every combination of terms inside the brackets, to give $a^{2}-ab+ba-b^{2}$.
• We collect like terms, and find that $ba$ and $-ba$ cancel out, to give the desired result $a^{2}-b^{2}$.

All we needed for this proof was basic algebra, specifically, multiplying out brackets, and collecting like terms.

Code

The following Lean program proves (a+b)(a-b)=a^{2}-b^{2}. 

-- 04 - Simple Algebra

import Mathlib.Tactic

example {a b : ℤ} : (a - b) * (a + b) = a^2 - b^2 := by
  calc
    (a - b) * (a + b) = a^2 - a*b + a*b - b^2 := by ring
    _ = a^2 - b^2 := by ring

Notice the line stating the theorem has no hypotheses to declare. It goes straight from the variable types to the statement we want to prove.

The proof itself starts with the expression we want to prove something about, (a - b) * (a + b), and states that this is equal to a^2 - a*b + a*b - b^2. This is justified by the ring tactic, which can do basic algebra. The final line of the proof states the previous expression is equivalent to a^2 - b^2, again justified by the ring tactic.

The first use of the ring tactic was to justify multiplying out the brackets. The second use of the ring tactic was to justify collecting like terms, and cancelling the -a*b and +a*b terms. 

We could have combined both steps into one, using the ring tactic just once, but it wouldn't have made clear to us what the ring tactic can do. Let's try it anyway. Our code should look like the following.

  calc
    (a - b) * (a + b) = a^2 - b^2 := by ring

Intentional Error

What would happen if $a$ and $b$ were natural numbers, not integers? Let's try it.

Change the variable type declaration from {a b : ℤ} to {a b : ℕ}.

The Infoview now shows errors, indicating that the ring tactic failed. Why is this?

If $a$ and $b$ are natural numbers, then $(a-b)$ doesn't make sense when $b>a$, because natural numbers can't be negative integers. 

This illustrates one of the benefits of Lean. It can catch apparently small assumptions that end up invalidating our results.

---

Exercise

Write a Lean program to prove $(a+b)^{2}=a^{2}+b^{2}$ if we know $ab=0$, where $a$ and $b$ are integers.

This will require both the ring and rewrite tactics.