1. Basics of polyrith
1.1. Housekeeping
You should be reading this tutorial simultaneously with scrolling through the associated Lean files. This will let you see the goal state of the Lean code and do the exercises.
Head over to the tutorial’s GitHub repository, https://github.com/hrmacbeth/computations_in_lean, to download the repository to your own computer or to open it in the cloud on Gitpod.
1.2. Basics of the linear_combination tactic
How do you do algebra in Lean? Let’s consider a concrete problem.
Problem
Let \(a\) and \(b\) be complex numbers and suppose that \(a - 5b = 4\) and \(b + 2 = 3\). Show that \(a = 9\).
One way to solve this on paper is by a “calculation block”, and this translates directly, if painstakingly, to Lean.
example {a b : ℂ} (h₁ : a - 5 * b = 4) (h₂ : b + 2 = 3) : a = 9 :=
calc a = (a - 5 * b) + 5 * b : by ring
... = 4 + 5 * b : by rw [h₁]
... = -6 + 5 * (b + 2) : by ring
... = -6 + 5 * 3 : by rw [h₂]
... = 9 : by ring
Implicitly, when we write a calculation like this on paper, we tend to alternate “rearrangement
steps” (done in Lean with ring) and “substitution steps” (done in Lean with rw).
Another method: You might be familiar with the linarith tactic, for deducing implications among
linear inequalities. If we were working over a linear ordered field such as \(\mathbb{R}\) or
\(\mathbb{Q}\), this tactic would be a great way to solve this problem.
example {a b : ℝ} (h₁ : a - 5 * b = 4) (h₂ : b + 2 = 3) : a = 9 :=
by linarith
But over \(\mathbb{C}\), which has no order, we could only invoke linarith by first taking
real and imaginary parts of both sides – and over a general field this wouldn’t work at all.
In this section we will introduce a tactic, linear_combination, which is well-adapted to
algebra over general commutative rings. This is a very new tactic, contributed to mathlib in
January 2022 by Brown undergraduate Abby Goldberg. Here is how our example is solved using
linear_combination.
example {a b : ℂ} (h₁ : a - 5 * b = 4) (h₂ : b + 2 = 3) : a = 9 :=
by linear_combination h₁ + 5 * h₂
The tactic linear_combination works by finding coefficients with which LHS - RHS of the goal is
a linear combination of LHS - RHS of the hypotheses. Here LHS - RHS of h₁ is \(a-5b-4\),
LHS - RHS of h₂ is \(b-1\), and LHS - RHS of the goal is \(a-9\). It is indeed true
that
linear_combination is a great tactic to use when your intuition for a problem is to “add
something to both sides” or “divide both sides by something” or “add two equations”.
Problem
Let \(m\) and \(n\) be integers and suppose that \(m - n = 0\). Show that \(m = n\).
example {m n : ℤ} (h : m - n = 0) : m = n :=
by linear_combination h
Problem
Let \(K\) be a field of characteristic zero, let \(s\in K\), and suppose that \(3s+1 = 4\). Show that \(s = 1\).
example {K : Type*} [field K] [char_zero K] {s : K} (hs : 3 * s + 1 = 4) : s = 1 :=
by linear_combination 1/3 * hs
Problem
Let \(p\) and \(q\) be complex numbers and suppose that \(p+2q=4\) and \(p-2q=2\). Show that \(2p = 6\).
example {p q : ℂ} (h₁ : p + 2 * q = 4) (h₂ : p - 2 * q = 2) : 2 * p = 6 :=
by linear_combination h₁ + h₂
Here are a lot of exercises. Do them until you get bored, then go on to the next section.
example {x y : ℤ} (h₁ : 2 * x + y = 4) (h₂ : x + y = 1) : x = 3 :=
sorry
example {r s : ℝ} (h₁ : r + 2 * s = -1) (h₂ : s = 3) : r = -7 :=
sorry
example {c : ℚ} (h₁ : 4 * c + 1 = 3 * c - 2) : c = -3 :=
sorry
example {x y : ℤ} (h₁ : x - 3 * y = 5) (h₂ : y = 3) : x = 14 :=
sorry
example {x y : ℤ} (h₁ : 2 * x - y = 4) (h₂ : y - x + 1 = 2) : x = 5 :=
sorry
example {x y : ℝ} (h₁ : x = 3) (h₂ : y = 4 * x - 3) : y = 9 :=
sorry
example {a b c : ℝ} (h₁ : a + 2 * b + 3 * c = 7) (h₂ : b + 2 * c = 3) (h₃ : c = 1) :
a = 2 :=
sorry
example {a b : ℝ} (h₁ : a + 2 * b = 4) (h₂ : a - b = 1) : a = 2 :=
sorry
example {u v : ℚ} (h₁ : u + 2 * v = 4) (h₂ : u - 2 * v = 6) : u = 5 :=
sorry
example {u v : ℚ} (h₁ : 4 * u + v = 3) (h₂ : v = 2) : u = 1 / 4 :=
sorry
1.3. linear_combination for nonlinear equations
Despite the name, where linear_combination really comes into its own is in solving nonlinear
equations: polynomial equations of degree greater than one. For example, consider the following
calculation, which comes up in studying the twisted cubic.
Problem
Let \(x, y, z, w\) be complex numbers and suppose that \(xz=y^2\) and \(yw=z^2\). Show that \(z(xw-yz)=0\).
This can be solved by exhibiting \(z(xw-yz)\) as an element of the ideal generated by \(xz-y^2\) and \(yw-z^2\):
example {x y z w : ℂ} (h₁ : x * z = y ^ 2) (h₂ : y * w = z ^ 2) : z * (x * w - y * z) = 0 :=
by linear_combination w * h₁ + y * h₂
Even on a problem where your intuition is to use rw, the tactic linear_combination can
probably do it.
Problem
Let \(a\) and \(b\) be rational numbers and suppose that \(a = b\). Show that \(a ^ 2 = b ^ 2\).
example {a b : ℚ} (h : a = b) : a ^ 2 = b ^ 2 :=
by linear_combination (a + b) * h
Problem
Let \(a\) and \(b\) be rational numbers and suppose that \(a = b\). Show that \(a ^ 3 = b ^ 3\).
example {a b : ℚ} (h : a = b) : a ^ 3 = b ^ 3 :=
by linear_combination (a ^ 2 + a * b + b ^ 2) * h
Do you see the pattern?
Importantly, linear_combination strictly subsumes the tactic ring. In fact, ring
amounts to doing a linear_combination of no hypotheses!
Problem
Let \(m\) and \(n\) be integers. Show that
example (m n : ℤ) : (m ^ 2 - n ^ 2) ^ 2 + (2 * m * n) ^ 2 = (m ^ 2 + n ^ 2) ^ 2 :=
by { linear_combination }
Try the following examples, until you get bored.
example {x y : ℝ} (h₁ : x + 3 = 5) (h₂ : 2 * x - y * x = 0) : y = 2 :=
sorry
example {x y : ℝ} (h₁ : x - y = 4) (h₂ : x * y = 1) : (x + y) ^ 2 = 20 :=
sorry
example {a b c d e f : ℤ} (h₁ : a * d = b * c) (h₂ : c * f = d * e) :
d * (a * f - b * e) = 0 :=
sorry
example {u v : ℝ} (h₁ : u + 1 = v) : u ^ 2 + 3 * u + 1 = v ^ 2 + v - 1 :=
sorry
example {z : ℝ} (h₁ : z ^ 2 + 1 = 0) : z ^ 4 + z ^ 3 + 2 * z ^ 2 + z + 3 = 2 :=
sorry
example {p q r : ℚ} (h₁ : p + q + r = 0) (h₂ : p * q + p * r + q * r = 2) :
p ^ 2 + q ^ 2 + r ^ 2 = -4 :=
sorry
1.4. Basics of the polyrith tactic
Surprise! None of the work we did in the last two sections finding the coefficients for
linear_combination by hand was necessary. A brand new tactic, polyrith, contributed to
mathlib in July 2022 by Brown undergraduate Dhruv Bhatia, will obtain them from the Sage function
MPolynomial_libsingular.lift,
so long as you have an internet connection.
(The tactic also requires that your python3 have the requests package installed. This is
probably already the case, but if you encounter bugs that look like they might be caused by this,
install the package by running python3 -m pip install requests at the command line.)
Here is polyrith being let loose on all the examples from the previous two sections. In each
case, click on the blue “Try this” underline, to replace the polyrith invocation (which will
query Sage each time) with an automatically-computed linear_combination which stores its result.
example {a b : ℂ} (h₁ : a - 5 * b = 4) (h₂ : b + 2 = 3) : a = 9 :=
by polyrith
example {m n : ℤ} (h : m - n = 0) : m = n :=
by polyrith
example {K : Type*} [field K] [char_zero K] {s : K} (hs : 3 * s + 1 = 4) : s = 1 :=
by polyrith
example {p q : ℂ} (h₁ : p + 2 * q = 4) (h₂ : p - 2 * q = 2) : 2 * p = 6 :=
by polyrith
example {x y z w : ℂ} (h₁ : x * z = y ^ 2) (h₂ : y * w = z ^ 2) : z * (x * w - y * z) = 0 :=
by polyrith
example {a b : ℚ} (h : a = b) : a ^ 2 = b ^ 2 :=
by polyrith
example {a b : ℚ} (h : a = b) : a ^ 3 = b ^ 3 :=
by polyrith
example (m n : ℤ) : (m ^ 2 - n ^ 2) ^ 2 + (2 * m * n) ^ 2 = (m ^ 2 + n ^ 2) ^ 2 :=
by polyrith