14.3. Polynomial and rational syntax
Polynomial expressions may use numerals, the quantified variable, +, -,
*, negation, natural powers, and division by rational constants. The first
example exercises all of these arithmetic forms. The tactic clears rational
denominators before constructing its certificate:
example : ∀ x : ℝ,
-(2 * x - 1) ^ 2 / 3 + 1 / 5 ≤ 1 / 5 := ⊢ ∀ (x : ℝ), -(2 * x - 1) ^ 2 / 3 + 1 / 5 ≤ 1 / 5
All goals completed! 🐙
example : ∀ x : ℝ,
(x < 0 ∨ x ≥ 0) ∧
(x ≤ 0 ∨ x > 0) ∧
(x = 0 ∨ x ≠ 0) := ⊢ ∀ (x : ℝ), (x < 0 ∨ x ≥ 0) ∧ (x ≤ 0 ∨ x > 0) ∧ (x = 0 ∨ x ≠ 0)
All goals completed! 🐙
The coefficients may be any exact rationals, but bounded endpoints must be
dyadic rationals. Thus 1 / 3 is valid as a coefficient and is not valid as
an endpoint. An endpoint is supported exactly when its reduced denominator is
a power of two.
The proposition must contain exactly one quantified real variable and no other
free variables. Nested quantifiers, symbolic coefficients, division by an
expression containing the variable, and non-polynomial functions such as
Real.sin are outside the supported fragment. The tactic reports which of
these conditions failed.