4. Combining tactics
In this last section we cover examples involving division.
The key tactic here is called field_simp:
it clears denominators of fractions,
which gets us back to a setting in which ring or polyrith can be applied.
4.1. Basics of the field_simp tactic
Given a ring expression with division or inversion,
the field_simp tactic will clear any denominators for which it can determine that that denominator is nonzero.
Here is an example: we prove that if \(a\) and \(b\) are rational numbers, with \(a\)
nonzero, then \(b = a ^ 2 + 3 a\) implies \(\tfrac{b}{a} - a = 3\). Check that if you
delete the hypothesis that \(a \ne 0\) then field_simp fails to do anything useful.
example (a b : ℚ) (ha : a ≠ 0) (H : b = a ^ 2 + 3 * a) : b / a - a = 3 := by
field_simp
linear_combination H
In the following problem we prove that the unit circle admits a rational parametrization:
In this problem, the denominator, \(t ^ 2 + 1\), is “obviously positive”:
it is the sum of a square and a strictly positive number.
In such a situation field_simp will find the nonzeroness of the denominator automatically without us providing it.
example (t : ℝ) : ((t ^ 2 - 1) / (t ^ 2 + 1)) ^ 2 + (2 * t / (t ^ 2 + 1)) ^ 2 = 1 := by
field_simp
ring
Let’s tweak that problem to make it a bit harder. Suppose we want to prove the identity
which is valid whenever \((m,n)\ne (0,0)\).
In this problem, field_simp cannot automatically prove the nonzeroness of the denominator, \(m ^ 2 + n ^ 2\).
We need to provide a proof of the nonzeroness explicitly.
Notice the use of contraposition and of (n)linarith in proving the nonzeroness hypothesis;
these are both common ingredients.
Again, check that if you comment out the justification that \(m ^ 2 + n ^ 2 \ne 0\),
then field_simp fails to trigger.
example (m n : ℝ) (hmn : (m, n) ≠ 0) :
((m ^ 2 - n ^ 2) / (m ^ 2 + n ^ 2)) ^ 2 + (2 * m * n / (m ^ 2 + n ^ 2)) ^ 2 = 1 := by
have : m ^ 2 + n ^ 2 ≠ 0 := by
contrapose! hmn
ext <;> dsimp <;> nlinarith
field_simp
ring
In the following problem we prove that if \(x\) is a primitive fifth root of unity, then \(x+1/x\) satisfies the quadratic equation
Here the denominator nonzeroness for field_simp is established by a contradiction argument:
if \(x^5=0\) and \(x=0\) then polyrith can produce a numeric contradiction.
Notice also that the nonzeroness hypothesis \(x\ne 1\) turns up later,
when we follow the technique from Section 3.1.
Click through each invocation of polyrith to see what it gives you.
example {x : ℂ} (hx : x ^ 5 = 1) (hx' : x ≠ 1) : (x + 1 / x) ^ 2 + (x + 1 / x) - 1 = 0 := by
have : x ≠ 0 := by
intro h₀
have : (1 : ℂ) = 0 := by polyrith
norm_num at this
field_simp
rw [← sub_ne_zero] at hx'
apply mul_left_cancel₀ hx'
polyrith
Here is an exercise. Let \(f:\mathbb{R}\to \mathbb{R}\) be the function
Away from the bad inputs \(x=0,1\), show that the triple composition of this function is the identity.
noncomputable def f : ℝ → ℝ := fun x => (1 - x)⁻¹
example {x : ℝ} (h₁ : x ≠ 1) (h₀ : x ≠ 0) : f (f (f x)) = x := by
dsimp [f]
sorry
4.2. Stereographic projection
In this section we construct stereographic projection as a bijection between the unit circle (minus
its north pole) and the real line. The formulas for both directions of the bijection are
fractions, so we will use field_simp repeatedly.
We introduce the notation 𝕊 for the unit circle in ℝ × ℝ, defined as the subtype of points
\((x,y)\) such that \(x^2+y^2=1\).
The forward direction of the bijection is the map
/-- Stereographic projection, forward direction. This is a map from `ℝ × ℝ` to `ℝ`. It is
smooth away from the horizontal line `v.2 = 1`. It restricts on the unit circle to the
stereographic projection. -/
def stereoToFun (p : 𝕊) : ℝ := 2 * p.val.1 / (1 - p.val.2)
The backward direction of the bijection is the map
Here we encounter our first proof obligation. We want to prove this is well-defined as a map from
\(\mathbb{R}\) to the circle, so we must prove that the norm-square of this expression is 1.
Fill in the proof below, using field_simp.
In this case there is no need to justify that the denominator, \(w^2+4\), is nonzero:
it is clearly strictly positive, so field_simp finds the nonzeroness automatically.
/-- Stereographic projection, reverse direction. This is a map from `ℝ` to the unit circle
`𝕊` in `ℝ × ℝ`. -/
def stereoInvFun (w : ℝ) : 𝕊 where
val := (w ^ 2 + 4)⁻¹ • (4 * w, w ^ 2 - 4)
property := by
dsimp
sorry
And in fact, since the bijection is going to be a map from \(\mathbb{R}\) to the circle
minus the north pole, we must also prove that this expression is not equal to \((0,1)\).
Fill in the proof below, using field_simp to simplify the expressions h₁ and h₂.
Then find a contradiction.
theorem stereoInvFun_ne_north_pole (w : ℝ) : stereoInvFun w ≠ (⟨(0, 1), by simp⟩ : 𝕊) := by
refine Subtype.coe_ne_coe.1 ?_
dsimp
rw [Prod.mk.inj_iff]
rintro ⟨h₁, h₂⟩
sorry
Now comes the hardest part, proving that the given expression is a left inverse for the forward direction.
There are two different denominator expressions which appear:
\(1-y\) and \(\left(\frac{2x}{1 - y}\right) ^ 2 + 4\).
You will need to prove the nonzeroness of the first one explicitly.
For the second, the nonzeroness will be proved automatically by field_simp,
since it is clearly strictly positive.
theorem stereo_left_inv {p : 𝕊} (hp : (p : ℝ × ℝ) ≠ (0, 1)) :
stereoInvFun (stereoToFun p) = p := by
ext1
obtain ⟨⟨x, y⟩, pythag⟩ := p
dsimp at pythag hp ⊢
rw [Prod.mk.inj_iff] at hp ⊢
sorry
The right inverse proof is much easier,
it’s another case where field_simp can check the denominator-nonzeroness silently.
theorem stereo_right_inv (w : ℝ) : stereoToFun (stereoInvFun w) = w := by
dsimp
sorry
Putting all these facts together with a bit of Lean abstract nonsense gives the bijection.
/-- Stereographic projection, as a bijection to `ℝ` from the complement of `(0, 1)` in the
unit circle `𝕊` in `ℝ × ℝ`. -/
def stereographicProjection : ({(⟨(0, 1), by simp⟩ : 𝕊)}ᶜ : Set 𝕊) ≃ ℝ where
toFun := stereoToFun ∘ (·)
invFun w := ⟨stereoInvFun w, stereoInvFun_ne_north_pole w⟩
left_inv p := Subtype.coe_injective <| stereo_left_inv (Subtype.coe_injective.ne p.prop)
right_inv w := stereo_right_inv w
4.3. A binomial coefficient identity
In this section we prove the following identity involving binomial coefficients:
Proposition
For all natural numbers \(i\) and \(j\),
This identity can be discovered by applying the “Gosper algorithm” to the right-hand side. It turns up in Mathlib in the proof that the recursive definition of the Catalan numbers agrees with the definition by binomial coefficients.
The “central binomial coefficient” expressions \({2n \choose n}\) are available in Mathlib under the name
#check @Nat.centralBinom
-- Nat.centralBinom : ℕ → ℕ
and the following easy identity, relating successive central binomial coefficients, is available
in Mathlib under the name Nat.succ_mul_centralBinom_succ.
Lemma
For all natural numbers \(n\),
The technique of the proof is pretty clear. One should invoke the above lemma twice, once to turn
all \({2(i+1)\choose i+1}\) into \({2i\choose i}\) and once to turn all
\({2(j+1)\choose j+1}\) into \({2j\choose j}\). We should therefore first state these two
applications of the lemma, then use field_simp to clear denominators and then polyrith to
figure out the coefficients with which to combine them. field_simp will check along the way
that all the denominators we want to clear are nonzero (since they are all of the form
“natural number plus one”).
There is one main complication. The lemma Nat.succ_mul_centralBinom_succ concerns natural numbers,
whereas our goal (which involves divisions) is stated
as an equality of rational numbers. So each of the applications of the above lemmas will need to
be cast – try using the tactic qify for this.
example {i j : ℕ} :
((i + 1).centralBinom : ℚ)
* j.centralBinom * (i - j + 1) / (2 * (i + j + 1) * (i + j + 2))
- i.centralBinom * (j + 1).centralBinom
* (i - j - 1) / (2 * (i + j + 1) * (i + j + 2))
= i.centralBinom / (i + 1) * (j.centralBinom / (j + 1)) := by
have h₁ := i.succ_mul_centralBinom_succ
have h₂ := j.succ_mul_centralBinom_succ
sorry