14.1. Introduction
rcf decides statements about one real variable. Give it a sentence such as
∀ x : ℝ, x⁴ − 4x + 3 ≥ 0 or ∃ x ∈ (1, 2], x³ − x − 1 = 0: one universal or
existential quantifier over ℝ, or over a half-open interval Set.Ioc a b
with dyadic endpoints, followed by any Boolean combination of polynomial
equations and inequalities with rational coefficients. If the sentence is
true, rcf proves it. If it is false, rcf reports that, and for a universal
sentence names an interval on which the body fails.
This is Tarski's decision procedure in its simplest case. The real roots of the polynomials in the sentence cut the line into finitely many intervals and points, each polynomial keeps a constant sign on each piece, and so a statement about every real number, or about some real number, becomes a finite check. The tactic performs that check with exact integer arithmetic: it isolates the roots with certified Sturm counts, records the sign of each polynomial on each piece, and hands the kernel a certificate containing those signs and counts. The kernel replays the certificate by evaluation, never repeats the search, and the resulting proof uses no axiom beyond the three that Mathlib always uses.
The tactics Mathlib already provides do something different. nlinarith and
positivity are heuristics: they succeed on many true inequalities of this
shape, may need hints such as sq_nonneg (x - 1) supplied by hand, and give
no verdict when they fail. polyrith proves equalities only. decide does
not apply to quantifiers over ℝ. None of them proves an existential
statement without a named witness, and the witness in the cubic above is
irrational. rcf needs neither hints nor a witness, and on this fragment it
always answers.
Import HexRCF and write rcf at the goal. Here it proves that the Chebyshev
polynomial T₅ is bounded by one on (−1, 1] and attains the bound, that a
cubic has a root in a dyadic interval and none outside it, and that a quartic
is nonnegative with equality at exactly one point. Each is one call:
example : ∀ x : ℝ, x ^ 2 + 1 > 0 := ⊢ ∀ (x : ℝ), x ^ 2 + 1 > 0
All goals completed! 🐙
example : ∀ x : ℝ, x ∈ Set.Ioc (-1 : ℝ) 1 →
-1 ≤ 16 * x ^ 5 - 20 * x ^ 3 + 5 * x ∧
16 * x ^ 5 - 20 * x ^ 3 + 5 * x ≤ 1 := ⊢ ∀ x ∈ Set.Ioc (-1) 1, -1 ≤ 16 * x ^ 5 - 20 * x ^ 3 + 5 * x ∧ 16 * x ^ 5 - 20 * x ^ 3 + 5 * x ≤ 1
All goals completed! 🐙
example : ∃ x : ℝ, x ∈ Set.Ioc (-1 : ℝ) 1 ∧
16 * x ^ 5 - 20 * x ^ 3 + 5 * x = 1 := ⊢ ∃ x ∈ Set.Ioc (-1) 1, 16 * x ^ 5 - 20 * x ^ 3 + 5 * x = 1
All goals completed! 🐙
-- The real root of x³ − x − 1 lies in (21/16, 43/32], and
-- nothing outside that interval is a root.
example : ∃ x : ℝ, x ^ 3 - x - 1 = 0 ∧
21 / 16 < x ∧ x ≤ 43 / 32 := ⊢ ∃ x, x ^ 3 - x - 1 = 0 ∧ 21 / 16 < x ∧ x ≤ 43 / 32
All goals completed! 🐙
example : ∀ x : ℝ, x ^ 3 - x - 1 = 0 →
21 / 16 < x ∧ x ≤ 43 / 32 := ⊢ ∀ (x : ℝ), x ^ 3 - x - 1 = 0 → 21 / 16 < x ∧ x ≤ 43 / 32
All goals completed! 🐙
-- x⁴ − 4x + 3 = (x − 1)² (x² + 2x + 3) is nonnegative,
-- and zero only at x = 1.
example : ∀ x : ℝ, x ^ 4 - 4 * x + 3 ≥ 0 := ⊢ ∀ (x : ℝ), x ^ 4 - 4 * x + 3 ≥ 0
All goals completed! 🐙
example : ∀ x : ℝ, x ^ 4 - 4 * x + 3 = 0 → x = 1 := ⊢ ∀ (x : ℝ), x ^ 4 - 4 * x + 3 = 0 → x = 1
All goals completed! 🐙
The statement that the cubic has exactly one real root mentions two variables and is outside this fragment; HexRealRoots proves counts of that kind.