Root Finding Tactic

The root_bound tactic proves ∀ x ∈ I, f x ≠ 0 using interval arithmetic.

def LeanCert.Tactic.Auto.rootBoundCore (taylorDepth : ℕ) : Lean.Elab.Tactic.TacticM Unit

The main root_bound tactic implementation

Equations

• One or more equations did not get rendered due to their size.

def LeanCert.Tactic.Auto.rootBoundCore.getAst (func : Lean.Expr) : Lean.Elab.Tactic.TacticM Lean.Expr

Try to extract AST from an Expr.eval application, or reify if it's a raw expression

Equations

• One or more equations did not get rendered due to their size.

def LeanCert.Tactic.Auto.rootBoundCore.tryConvertSetIccForRootBound (interval : Lean.Expr) : Lean.MetaM (Option Lean.Expr)

Try to convert Set.Icc to IntervalRat for root_bound

Equations

• One or more equations did not get rendered due to their size.

def LeanCert.Tactic.Auto.rootBoundCore.proveForallNeZero (goal : Lean.MVarId) (interval func : Lean.Expr) (taylorDepth : ℕ) : Lean.Elab.Tactic.TacticM Unit

Prove ∀ x ∈ I, f x ≠ 0 using verify_no_root

Equations

• One or more equations did not get rendered due to their size.

def LeanCert.Tactic.Auto.tacticRoot_bound_ : Lean.ParserDescr

The root_bound tactic.

Automatically proves root-related properties using interval arithmetic.

Usage:

• root_bound - uses default Taylor depth of 10
• root_bound 20 - uses Taylor depth of 20

Supports goals of the form:

• ∀ x ∈ I, f x ≠ 0 (proves no root exists in interval)

Equations

• One or more equations did not get rendered due to their size.