The rcf tactic proves closed propositions about exactly one quantified real
variable by exact decision. Its input is one universal or existential
quantifier over ℝ, or over a half-open interval Set.Ioc a b, with no other
free variables. The quantifier body may use Boolean combinations of
comparisons between univariate polynomials with rational coefficients.
The computation uses exact integer and rational arithmetic. It isolates the
real roots that can change an atom's sign, evaluates the formula on the
resulting cells, and emits a certificate for Lean's kernel to check. No
floating-point approximation occurs.
Quantification over the whole real line may be universal or existential. The
body can combine equalities, inequalities, conjunctions, disjunctions,
negations, and implications:
/-- A universal sentence over the real line. -/
example:∀x:ℝ,x^2≤1→x^4-x^2≤0:=⊢ ∀(x:ℝ),x^2≤1→x^4-x^2≤0All goals completed! 🐙/-- An existential sentence over the real line. -/
example:∃x:ℝ,x^3-x-1=0∧1<x∧x<2:=⊢ ∃x,x^3-x-1=0∧1<x∧x<2All goals completed! 🐙
The bounded forms use Set.Ioc a b, which denotes (a, b]. The lower
endpoint is excluded and the upper endpoint is included:
/-- Universal quantification over `(0, 1]`. -/
example:∀x:ℝ,x∈Set.Ioc(0:ℝ)1→x>0:=⊢ ∀x∈Set.Ioc01,x>0All goals completed! 🐙/-- Existential quantification over `(0, 1]`.
The upper endpoint is a witness. -/
example:∃x:ℝ,x∈Set.Ioc(0:ℝ)1∧x=1:=⊢ ∃x∈Set.Ioc01,x=1All goals completed! 🐙
An interval is empty when a ≥ b. Universal statements on an empty
interval are true, while existential statements are false. These examples
also show that the lower endpoint is not part of a nonempty interval:
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:
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.
The tactic constructs proofs only for true sentences. For a false universal
sentence it identifies a cell on which the body is false:
example:∀x:ℝ,x^2>0:=⊢ ∀(x:ℝ),x^2>0rcf: the universal sentence is false on the root cell isolated in (-2, 2]⊢ ∀(x:ℝ),x^2>0
rcf: the universal sentence is false on the root cell isolated in (-2, 2]
For a false existential sentence it reports that all relevant cells were
checked and that none supplies a witness:
example:∃x:ℝ,x^2+1=0:=⊢ ∃x,x^2+1=0rcf: the existential sentence is false. Every relevant decomposition
cell was checked and found false, so there is no witness⊢ ∃x,x^2+1=0
rcf: the existential sentence is false. Every relevant decomposition
cell was checked and found false, so there is no witness
A supported sentence may be false even though reification and certified
decision both succeed. Such a checked false verdict never becomes a proof
term: rcf reports the relevant false-sentence diagnostic above. An
out-of-fragment goal is different: reification fails before the decision
procedure runs. Both are ordinary tactic failures, so tactic combinators may
fall through to another method. Here the unquantified goal is outside the
fragment and norm_num handles it:
Only Set.Ioc is accepted directly. If a goal uses a closed interval
Set.Icc, separate the lower endpoint from the remaining half-open interval.
For a predicate φ the exact rewrites are:
∀ x ∈ Set.Icc a b, φ x becomes
(a ≤ b → φ a) ∧ ∀ x ∈ Set.Ioc a b, φ x.
∃ x ∈ Set.Icc a b, φ x becomes
a ≤ b ∧ (φ a ∨ ∃ x ∈ Set.Ioc a b, φ x).
For an open interval Set.Ioo, exclude the upper endpoint from Set.Ioc:
∀ x ∈ Set.Ioo a b, φ x becomes
∀ x ∈ Set.Ioc a b, x ≠ b → φ x.
∃ x ∈ Set.Ioo a b, φ x becomes
∃ x ∈ Set.Ioc a b, φ x ∧ x ≠ b.
After the endpoint proposition has been handled separately, rcf can prove
the remaining singly quantified part. This worked closed-interval example
checks the lower endpoint separately and sends the Set.Ioc tail to rcf:
Most users only need the rcf tactic. Programs that construct or inspect
sentences directly use the reflected language below. A comparison applies to
one integer polynomial, formulas combine comparisons, and a sentence adds the
one quantifier supported by the decision procedure.
A quantifier-free formula under exactly one real or bounded-real
quantifier. Bounded quantifiers use the half-open convention (a,b] inherited
from real-root isolations.
Interpret a reflected sentence as a Lean proposition.
The #p[...] literal lists coefficients in ascending degree order and
normalizes away trailing zeros. This direct construction represents
∀ x : ℝ, x² + 1 > 0 and sends it through the same compiled decision
procedure used by the tactic:
The four certificate shapes correspond to empty bounded domains, formulas
with no nonconstant atom polynomial, root-free carriers, and positive-root
cell decompositions:
HexRCF is classified as a Mathlib-facing library because its reifier, tactic,
real semantics, and soundness theorem use Mathlib. There is no separate
HexRCFMathlib library. By contrast, HexRCF.DecisionCheck exposes the
complete compiled search, certificate construction, replay, and
Hex.RCF.decide path, with a mechanically checked Mathlib-free import
closure. The soundness theorem remains on the Mathlib-facing side of this
boundary.
Certificate construction runs as compiled elaboration code. That search is
not trusted. The tactic embeds its reflected sentence and a literal
Hex.RCF.Certificate, reduces the public Boolean checker
Hex.RCF.Certificate.check, and applies the soundness theorem
Hex.RCF.check_sound. Lean's kernel also checks the reifier's proof
that the reflected sentence is equivalent to the source goal.
The public soundness boundary can be used independently of the tactic:
Hex.RCF.Certificate.replay? distinguishes malformed evidence (none), a checked
false verdict (some false), and a checked true verdict (some true).
Hex.RCF.Certificate.check accepts only the last case. The convenience function
Hex.RCF.decide returns some true only after this checker accepts the
certificate. Advanced clients can use Hex.RCF.build? to retain the
certificate and its diagnostic or proof-producing verdict. A successfully
checked false sentence produces some false. Neither Hex.RCF.check_sound nor the
tactic turns some false into a proof of a negation.
A none from Hex.RCF.decide means the compiled path did not produce a
checker-accepted certificate. It does not mean that the sentence is false.
The kernel replays polynomial identities, signs, root counts, endpoint
comparisons, and Boolean folds on literal data. It does not repeat root
isolation, polynomial gcd computation, or interval refinement. The emitted
proof uses ordinary kernel reduction and does not use native_decide:
theoremrcf_square_nonnegative:∀x:ℝ,x^2≥0:=⊢ ∀(x:ℝ),x^2≥0All goals completed! 🐙'rcf_square_nonnegative' depends on axioms: [propext,Classical.choice,Quot.sound]#printaxiomsrcf_square_nonnegative
'rcf_square_nonnegative' depends on axioms: [propext,Classical.choice,Quot.sound]
HexPolyZ provides the dense integer polynomial
operations used to normalize atoms and check polynomial identities.
HexRealRoots provides the exact real-root isolator
used by HexRCF during compiled certificate construction. The generalized
multiplication-only Sturm certificates in HexRCF are kernel-replay
evidence for the resulting root-count facts, not a separate compiled
isolation algorithm.