Monday, July 1, 2024

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.


at