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

Ceiling/Floor Preprocessing

Goals involving ⌈e⌉₊ (Nat.ceil) cannot be reified into the Expr AST because it has no constructor for ceiling. Instead we reduce to a pure real inequality:

• ⌈e⌉₊ + k ≤ n ⟹ prove e ≤ ↑(n - k) by interval_decide, then close via Nat.ceil_le + omega.

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.