Point Inequality Tactic (interval_decide)

The interval_decide tactic proves point inequalities like Real.exp 1 ≤ 3.

def LeanCert.Tactic.Auto.proveClosedExpressionBound (goal : Lean.MVarId) (goalType : Lean.Expr) (taylorDepth : ℕ) : Lean.Elab.Tactic.TacticM Unit

Try to prove a closed expression bound directly using certificate verification.

Equations

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

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

The interval_decide tactic implementation.

Equations

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

Depth estimation helpers

partial def LeanCert.Tactic.Auto.intervalDecideWithConnectives (depth : Option ℕ) : Lean.Elab.Tactic.TacticM Unit

Recursively handle conjunctions and disjunctions, then apply intervalDecideSingle

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

Equations

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