Quantifier elimination for real closed fields

11 fully proved1 ready to prove2 statement formalized1 ready to state

Syntax

InductiveTerms of the language of ordered rings#✓fully proved

Terms are built from variables \(x_i\), one for each natural number \(i\) (a de Bruijn index), and integer constants \(k \in \mathbb{Z}\), using addition \(s + t\), multiplication \(s \cdot t\) and negation \(-t\).

inductive Term where
  | var : Nat → Term
  | const : Int → Term
  | add : Term → Term → Term
  | mul : Term → Term → Term
  | neg : Term → Term
  deriving DecidableEq, Repr, Inhabited

Used by 5

Used byEvaluation of terms · Formulas of the language of ordered rings · Satisfaction of formulas over the reals · A real number is a square exactly when it is nonnegative · Quantifier-free formulas

InductiveFormulas of the language of ordered rings#✓fully proved

Formulas are built from the atomic formulas \(s < t\) and \(s = t\), for terms \(s\) and \(t\), and falsity \(\bot\), by implication \(\varphi \to \psi\) and universal quantification \(\forall \varphi\), which binds de Bruijn index \(0\) in \(\varphi\). Negation, truth, disjunction, conjunction and existential quantification are defined from these.

inductive Formula where
  | lt : Term → Term → Formula
  | eq : Term → Term → Formula
  /-- Falsity. -/
  | fals : Formula
  | imp : Formula → Formula → Formula
  /-- Universal quantification; binds de Bruijn index `0` in the body. -/
  | all : Formula → Formula
  deriving DecidableEq, Repr, Inhabited

Uses 1 · Used by 11

Statement usesTerms of the language of ordered rings

Used byConjunction of formulas · Existential quantification of formulas · Satisfaction of formulas over the reals · A real number is a square exactly when it is nonnegative · Quantifier elimination preserves truth · Quantifier-free formulas · Quantifier elimination yields quantifier-free formulas · Negation of a formula · Disjunction of formulas · Quantifier elimination over the reals · The true formula

DefinitionNegation of a formula#✓fully proved

The negation \(\neg\varphi\) of a formula \(\varphi\) is the formula \(\varphi \to \bot\).

def not (φ : Formula) : Formula := .imp φ .fals

Uses 1 · Used by 5

Statement usesFormulas of the language of ordered rings

Used byConjunction of formulas · Existential quantification of formulas · A real number is a square exactly when it is nonnegative · Disjunction of formulas · The true formula

DefinitionThe true formula#✓fully proved

The formula \(\top\) is the negation \(\neg\bot\) of falsity, that is, the formula \(\bot \to \bot\).

def tru : Formula := .not .fals

Uses 2

Statement usesFormulas of the language of ordered rings · Negation of a formula

DefinitionDisjunction of formulas#✓fully proved

The disjunction \(\varphi \lor \psi\) of formulas \(\varphi\) and \(\psi\) is the formula \(\neg\varphi \to \psi\).

def or (φ ψ : Formula) : Formula := .imp φ.not ψ

Uses 2

Statement usesFormulas of the language of ordered rings · Negation of a formula

DefinitionConjunction of formulas#✓fully proved

For formulas \(\varphi\) and \(\psi\), the conjunction \(\varphi \wedge \psi\) is the formula \(\neg(\varphi \to \neg\psi)\).

def and (φ ψ : Formula) : Formula := (φ.imp ψ.not).not

Uses 2

Statement usesFormulas of the language of ordered rings · Negation of a formula

DefinitionExistential quantification of formulas#✓fully proved

For a formula \(\varphi\), the formula \(\exists \varphi\) is \(\neg \forall \neg \varphi\); it binds de Bruijn index \(0\) in \(\varphi\).

def ex (φ : Formula) : Formula := φ.not.all.not

Uses 2 · Used by 1

Statement usesFormulas of the language of ordered rings · Negation of a formula

Used byA real number is a square exactly when it is nonnegative

Semantics

DefinitionExtending an environment#✓fully proved

An environment is a map \(e : \mathbb{N} \to \mathbb{R}\) that assigns a real number to each de Bruijn index. For \(x \in \mathbb{R}\), the extension of \(e\) by \(x\) sends index \(0\) to \(x\) and index \(i + 1\) to \(e(i)\) for every \(i \in \mathbb{N}\).

def cons (x : ℝ) (env : Nat → ℝ) : Nat → ℝ
  | 0 => x
  | i + 1 => env i

Used by 1

Used bySatisfaction of formulas over the reals

DefinitionEvaluation of terms#✓fully proved

Given an environment \(e : \mathbb{N} \to \mathbb{R}\), the value of a term in \(\mathbb{R}\) is defined by recursion on the term: the variable with de Bruijn index \(i\) has value \(e(i)\), the integer constant \(k\) has value \(k\), and the value of a sum, product or negation of terms is the sum, product or negation in \(\mathbb{R}\) of the values of its parts.

def Term.eval (env : Nat → ℝ) : Term → ℝ
  | .var i => env i
  | .const k => (k : ℝ)
  | .add a b => a.eval env + b.eval env
  | .mul a b => a.eval env * b.eval env
  | .neg a => -a.eval env

Uses 1 · Used by 1

Statement usesTerms of the language of ordered rings

Used bySatisfaction of formulas over the reals

DefinitionSatisfaction of formulas over the reals#✓fully proved

Let \(e : \mathbb{N} \to \mathbb{R}\) be an environment. Whether a formula holds under \(e\) is defined by recursion on the formula: \(s < t\) holds when the value of \(s\) under \(e\) is less than the value of \(t\) under \(e\); \(s = t\) holds when these values are equal; \(\bot\) never holds; \(\varphi \to \psi\) holds when \(\varphi\) holding under \(e\) implies \(\psi\) holding under \(e\); and \(\forall \varphi\) holds when, for every \(x \in \mathbb{R}\), \(\varphi\) holds under the extension of \(e\) by \(x\).

def Formula.Holds (env : Nat → ℝ) : Formula → Prop
  | .lt a b => a.eval env < b.eval env
  | .eq a b => a.eval env = b.eval env
  | .fals => False
  | .imp φ ψ => φ.Holds env → ψ.Holds env
  | .all φ => ∀ x : ℝ, φ.Holds (cons x env)

Uses 4 · Used by 2

Statement usesFormulas of the language of ordered rings · Terms of the language of ordered rings · Evaluation of terms · Extending an environment

Used byA real number is a square exactly when it is nonnegative · Quantifier elimination preserves truth

DefinitionQuantifier-free formulas#✓fully proved

A formula is quantifier free if it contains no universal quantifier \(\forall\).

def Formula.IsQF : Formula → Prop
  | .lt _ _ => True
  | .eq _ _ => True
  | .fals => True
  | .imp φ ψ => φ.IsQF ∧ ψ.IsQF
  | .all _ => False

Uses 2 · Used by 1

Statement usesFormulas of the language of ordered rings · Terms of the language of ordered rings

Used byQuantifier elimination yields quantifier-free formulas

The problem

DefinitionQuantifier elimination over the reals#●ready to state

Quantifier elimination is a map sending each formula \(\varphi\) of the language of ordered rings to a formula \(\operatorname{qe}(\varphi)\), subject to two requirements: \(\operatorname{qe}(\varphi)\) is quantifier free, and for every environment \(e : \mathbb{N} \to \mathbb{R}\) assigning a real number to each variable, \(\operatorname{qe}(\varphi)\) holds in \(\mathbb{R}\) under \(e\) if and only if \(\varphi\) does.

The formula \(\operatorname{qe}(\varphi)\) may mention additional variables, but only vacuously.

public def_wanted qe (φ : Formula) : Formula

Sources

• Tarski, 'A Decision Method for Elementary Algebra and Geometry' (1951); Collins, 'Quantifier elimination for real closed fields by cylindrical algebraic decomposition' (1975); Mahboubi, 'Programming and certifying a CAD algorithm in the Coq system' (2006); Cohen and Mahboubi, 'Formal proofs in real algebraic geometry: from ordered fields to quantifier elimination' (2012). Problem rcf_quantifier_elimination of the lean-eval benchmark.

Uses 1 · Used by 2

Statement usesFormulas of the language of ordered rings

Used byQuantifier elimination preserves truth · Quantifier elimination yields quantifier-free formulas

TheoremQuantifier elimination yields quantifier-free formulas#●statement formalized

Let \(\mathrm{qe}\) be the quantifier elimination map on formulas. For every formula \(\varphi\), the formula \(\mathrm{qe}(\varphi)\) is quantifier free.

public theorem_wanted isQF_qe (φ : Formula) : (❰qe❱ φ).IsQF

Sources

• Tarski, 'A Decision Method for Elementary Algebra and Geometry' (1951); Collins, 'Quantifier elimination for real closed fields by cylindrical algebraic decomposition' (1975); Mahboubi, 'Programming and certifying a CAD algorithm in the Coq system' (2006); Cohen and Mahboubi, 'Formal proofs in real algebraic geometry: from ordered fields to quantifier elimination' (2012). Problem rcf_quantifier_elimination of the lean-eval benchmark.

Uses 3

Statement usesFormulas of the language of ordered rings · Quantifier-free formulas · Quantifier elimination over the reals

TheoremQuantifier elimination preserves truth#●statement formalized

Let \(\mathrm{qe}\) be the quantifier elimination map on formulas. For every formula \(\varphi\) and every environment \(e : \mathbb{N} \to \mathbb{R}\), the formula \(\mathrm{qe}(\varphi)\) holds in \(\mathbb{R}\) under \(e\) if and only if \(\varphi\) holds in \(\mathbb{R}\) under \(e\).

Together with the statement that \(\mathrm{qe}(\varphi)\) is always quantifier free, this is Tarski's quantifier elimination theorem, stated for \(\mathbb{R}\).

public theorem_wanted holds_qe (φ : Formula) (env : Nat → ℝ) :
    (❰qe❱ φ).Holds env ↔ φ.Holds env

Sources

• Tarski, 'A Decision Method for Elementary Algebra and Geometry' (1951); Collins, 'Quantifier elimination for real closed fields by cylindrical algebraic decomposition' (1975); Mahboubi, 'Programming and certifying a CAD algorithm in the Coq system' (2006); Cohen and Mahboubi, 'Formal proofs in real algebraic geometry: from ordered fields to quantifier elimination' (2012). Problem rcf_quantifier_elimination of the lean-eval benchmark.

Uses 3

Statement usesFormulas of the language of ordered rings · Satisfaction of formulas over the reals · Quantifier elimination over the reals

TheoremA real number is a square exactly when it is nonnegative#●ready to prove

For every environment \(e : \mathbb{N} \to \mathbb{R}\), the formula \(\exists x.\ x \cdot x = a\) holds under \(e\) if and only if the formula \(\neg(a < 0)\) holds under \(e\). In the first formula the bound variable \(x\) is de Bruijn index \(0\) and \(a\) is index \(1\); in the second \(a\) is index \(0\); in both, \(a\) denotes \(e(0)\). Thus \(e(0)\) is a square in \(\mathbb{R}\) exactly when \(e(0) \ge 0\).

This checks the semantics and the de Bruijn convention against a known fact.

public theorem_wanted holds_ex_sq (env : Nat → ℝ) :
    (Formula.ex (.eq (.mul (.var 0) (.var 0)) (.var 1))).Holds env ↔
      (Formula.not (.lt (.var 0) (.const 0))).Holds env

Sources

• Tarski, 'A Decision Method for Elementary Algebra and Geometry' (1951); Collins, 'Quantifier elimination for real closed fields by cylindrical algebraic decomposition' (1975); Mahboubi, 'Programming and certifying a CAD algorithm in the Coq system' (2006); Cohen and Mahboubi, 'Formal proofs in real algebraic geometry: from ordered fields to quantifier elimination' (2012). Problem rcf_quantifier_elimination of the lean-eval benchmark.

Uses 5

Statement usesFormulas of the language of ordered rings · Satisfaction of formulas over the reals · Existential quantification of formulas · Negation of a formula · Terms of the language of ordered rings

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.