Root Finding Tactic

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

structure LeanCert.Tactic.Auto.RootBoundOutcome : Type

Runtime facts from a retained no-root certificate.

• checker : Lean.Name
• verifier : Lean.Name
• verification : VerificationUsage
• taylorDepth : ℕ

@[instance_reducible]

instance LeanCert.Tactic.Auto.instInhabitedRootBoundOutcome : Inhabited RootBoundOutcome

Equations

• LeanCert.Tactic.Auto.instInhabitedRootBoundOutcome = { default := LeanCert.Tactic.Auto.instInhabitedRootBoundOutcome.default }

inductive LeanCert.Tactic.Auto.RootBoundFailure : Type

Expected and invariant failures from no-root certification.

• unsupported (expression detail : String) : RootBoundFailure
• rejected (detail : String) : RootBoundFailure
• transportFailure (detail : String) : RootBoundFailure
• internalFailure (detail : String) : RootBoundFailure

@[instance_reducible]

instance LeanCert.Tactic.Auto.instInhabitedRootBoundFailure : Inhabited RootBoundFailure

Equations

• LeanCert.Tactic.Auto.instInhabitedRootBoundFailure = { default := LeanCert.Tactic.Auto.instInhabitedRootBoundFailure.default }

@[instance_reducible]

instance LeanCert.Tactic.Auto.instReprRootBoundFailure : Repr RootBoundFailure

Equations

• LeanCert.Tactic.Auto.instReprRootBoundFailure = { reprPrec := LeanCert.Tactic.Auto.instReprRootBoundFailure.repr }

def LeanCert.Tactic.Auto.instReprRootBoundFailure.repr : RootBoundFailure → ℕ → Std.Format

Equations

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

def LeanCert.Tactic.Auto.rootBoundCoreTyped (taylorDepth : ℕ) : Lean.Elab.Tactic.TacticM (Except RootBoundFailure RootBoundOutcome)

Typed root-bound implementation. Every non-success restores the caller's complete tactic state.

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.