Subdivision-aware Bound Proving

The interval_bound_subdiv tactic uses interval subdivision when the direct approach is too coarse. Candidate evaluation and certificate verification are separate: search evaluates each node once, while every retained leaf closes one fixed Boolean certificate exactly once.

inductive LeanCert.Tactic.Auto.SubdivisionComparison : Type

Comparison certified by a subdivision proof tree.

• upper : SubdivisionComparison
• lower : SubdivisionComparison
• strictUpper : SubdivisionComparison
• strictLower : SubdivisionComparison

@[instance_reducible]

instance LeanCert.Tactic.Auto.instDecidableEqSubdivisionComparison : DecidableEq SubdivisionComparison

Equations

• LeanCert.Tactic.Auto.instDecidableEqSubdivisionComparison x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

def LeanCert.Tactic.Auto.instReprSubdivisionComparison.repr : SubdivisionComparison → ℕ → Std.Format

Equations

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

@[instance_reducible]

instance LeanCert.Tactic.Auto.instReprSubdivisionComparison : Repr SubdivisionComparison

Equations

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

@[instance_reducible]

instance LeanCert.Tactic.Auto.instInhabitedSubdivisionComparison : Inhabited SubdivisionComparison

Equations

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

structure LeanCert.Tactic.Auto.SubdivisionExecution : Type

Runtime facts retained by one successful subdivision proof tree.

• verification : VerificationUsage
• deepestDepthUsed : ℕ
• boxesExamined : ℕ
• certifiedLeaves : ℕ
• leafPaths : List Core.DyadicPath

  Canonically ordered root-to-leaf subdivision addresses.

• frontierChecked : Bool

  True only after the completed flat frontier passes the structural checker. Path-to-proof correspondence is maintained by the subdivision recursion.

@[instance_reducible]

instance LeanCert.Tactic.Auto.instInhabitedSubdivisionExecution : Inhabited SubdivisionExecution

Equations

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

structure LeanCert.Tactic.Auto.SubdivisionProof : Type

A proof together with the execution facts that produced it.

• proof : Lean.Expr
• enclosure : Core.IntervalRat
• execution : SubdivisionExecution

structure LeanCert.Tactic.Auto.SubdivisionOutcome : Type

Reported result of the public subdivision strategy. Every retained leaf uses the Rational interval backend.

• comparison : SubdivisionComparison
• taylorDepth : ℕ
• maxDepth : ℕ
• finalEnclosure : Core.IntervalRat
• execution : SubdivisionExecution
• checker : Lean.Name
• verifier : Lean.Name

@[instance_reducible]

instance LeanCert.Tactic.Auto.instInhabitedSubdivisionOutcome : Inhabited SubdivisionOutcome

Equations

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

inductive LeanCert.Tactic.Auto.SubdivisionFailure : Type

Typed failures from recursive subdivision.

• unsupported (expression detail : String) : SubdivisionFailure
• domainObstruction (domain : Lean.Expr) (operation detail : String) : SubdivisionFailure
• exhausted (maxDepth boxesExamined deepestDepth : ℕ) (bestEnclosure : Option Core.IntervalRat) : SubdivisionFailure
• rejected (checker : Lean.Name) (detail : String) : SubdivisionFailure
• transportFailure (detail : String) : SubdivisionFailure
• internalFailure (detail : String) : SubdivisionFailure

@[instance_reducible]

instance LeanCert.Tactic.Auto.instInhabitedSubdivisionFailure : Inhabited SubdivisionFailure

Equations

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

@[instance_reducible]

instance LeanCert.Tactic.Auto.instReprSubdivisionFailure : Repr SubdivisionFailure

Equations

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

def LeanCert.Tactic.Auto.instReprSubdivisionFailure.repr : SubdivisionFailure → ℕ → Std.Format

Equations

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

unsafe def LeanCert.Tactic.Auto.intervalBoundSubdivCoreTyped (depth : Option ℕ) (maxSubdiv : ℕ) : Lean.Elab.Tactic.TacticM (Except SubdivisionFailure SubdivisionOutcome)

Typed and exception-total subdivision entry point. Every non-success restores the complete caller tactic state.

Equations

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

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

The interval_bound_subdiv tactic.

Equations

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

unsafe def LeanCert.Tactic.Auto.elabIntervalBoundSubdiv : Lean.Elab.Tactic.Tactic

Equations

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