4. Combining tactics
In this last section we cover examples where several tactics need to be combined to complete a computation.
We will start with a discussion of the tactic field_simp, which is used in working with
fractions; it clears denominators so that ring or polyrith can be applied.
Later we will give two extended examples in which polyrith and field_simp are combined as
needed with norm_cast (and variants), to deal with casts among different number systems
(\(\mathbb{N}\), \(\mathbb{Z}\), \(\mathbb{Q}\), \(\mathbb{R}\),
\(\mathbb{C}\)) and with (n)linarith (to prove inequalities). But we will not give a
detailed description of these other tactics.
4.1. Basics of the field_simp tactic
Let us turn to field_simp. Given a ring expression with division or inversion, this tactic
will clear any denominators for which there is a proof in context 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 :=
begin
field_simp,
linear_combination H,
end
In the following problem we prove that the unit circle admits a rational parametrization:
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 :=
begin
have : m ^ 2 + n ^ 2 ≠ 0,
{ contrapose! hmn,
have hm : m = 0 := by nlinarith,
have hn : n = 0 := by nlinarith,
simp [hm, hn] },
field_simp,
ring,
end
In the following problem we prove that if \(x\) is a primitive fifth root of unity, then \(x+1/x\) satisfies the quadratic equation
We have another use of contraposition in proving one of the nonzeroness hypotheses. In the other,
we assume the goal did equal zero, and deduce a numeric contradiction with norm_num.
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 :=
begin
have : x ≠ 0,
{ intros h₀,
have : (1:ℂ) = 0 := by polyrith,
norm_num at this, },
field_simp,
have h₁ : x - 1 ≠ 0,
{ contrapose! hx',
polyrith },
apply mul_left_cancel₀ h₁,
polyrith,
end
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 : ℝ → ℝ := λ x, (1 - x)⁻¹
example {x : ℝ} (h₁ : x ≠ 1) (h₀ : x ≠ 0) : f (f (f x)) = x :=
begin
dsimp [f],
sorry,
end
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 set of points
\((x,y)\) such that \(x^2+y^2=1\).
The forward direction of the bijection is the map
def stereo_to_fun (p : 𝕊) : ℝ := 2 * p.1.1 / (1 - p.1.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 and a justification that the denominator is nonzero.
def stereo_inv_fun (w : ℝ) : 𝕊 :=
⟨(w ^ 2 + 4)⁻¹ • (4 * w, w ^ 2 - 4),
begin
dsimp,
sorry,
end⟩
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 and a justification that the denominator is nonzero
to simplify the expression h. Then find a contradiction.
lemma stereo_inv_fun_ne_north_pole (w : ℝ) :
stereo_inv_fun w ≠ (⟨(0, 1), by simp⟩ : 𝕊) :=
begin
refine subtype.ne_of_val_ne _,
dsimp,
rw [prod.mk.inj_iff],
intros h,
sorry,
end
Now comes the hardest part, proving that the given expression is a left inverse for the forward direction. The denominators that appear are complicated, and you may have quite a bit of work in proving them nonzero.
lemma stereo_left_inv {p : 𝕊} (hp : (p : ℝ × ℝ) ≠ (0, 1)) :
stereo_inv_fun (stereo_to_fun p) = p :=
begin
ext1,
obtain ⟨⟨x, y⟩, pythag⟩ := p,
dsimp at pythag hp ⊢,
rw prod.mk.inj_iff at hp ⊢,
sorry,
end
The right inverse proof is much easier, only one denominator and we’ve seen it before.
lemma stereo_right_inv (w : ℝ) : stereo_to_fun (stereo_inv_fun w) = w :=
begin
dsimp,
sorry,
end
Putting all these facts together with a bit of Lean abstract nonsense gives the bijection.
def stereographic_projection : ({(⟨(0, 1), by simp⟩ : 𝕊)}ᶜ : set 𝕊) ≃ ℝ :=
{ to_fun := stereo_to_fun ∘ coe,
inv_fun := λ w, ⟨stereo_inv_fun w, stereo_inv_fun_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.central_binom -- nat.central_binom : ℕ → ℕ
and the following easy identity, relating successive central binomial coefficients, is available
in mathlib under the name nat.succ_mul_central_binom_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 require proofs that
all the denominators we want to clear are nonzero, but this is easy since they are all of the form
“natural number plus one”:
#check nat.succ_ne_zero -- nat.succ_ne_zero : ∀ (n : ℕ), n.succ ≠ 0
There is one main complication. The lemmas nat.succ_mul_central_binom_succ and
nat.succ_ne_zero concern 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 exact_mod_cast for this.
example {i j : ℕ} :
((i + 1).central_binom:ℚ) * j.central_binom * (i - j + 1) / (2 * (i + j + 1) * (i + j + 2))
- i.central_binom * (j + 1).central_binom * (i - j - 1) / (2 * (i + j + 1) * (i + j + 2))
= i.central_binom / (i + 1) * (j.central_binom / (j + 1)) :=
begin
have h₁ : ((i:ℚ) + 1) * (i + 1).central_binom = 2 * (2 * i + 1) * i.central_binom,
{ sorry },
have h₂ : ((j:ℚ) + 1) * (j + 1).central_binom = 2 * (2 * j + 1) * j.central_binom,
{ sorry },
have : (i:ℚ) + j + 1 ≠ 0,
{ sorry },
have : (i:ℚ) + j + 2 ≠ 0,
{ sorry },
have : (i:ℚ) + 1 ≠ 0,
{ sorry },
have : (j:ℚ) + 1 ≠ 0,
{ sorry },
sorry,
end