Point Inequality Tactic (interval_decide)

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

structure LeanCert.Tactic.Auto.PointInequalityOutcome : Type

Runtime facts from a retained point-inequality certificate.

• checker : Lean.Name
• verifier : Lean.Name
• verification : VerificationUsage
• dyadic : Bool
• precision : Option ℤ
• taylorDepth : ℕ

@[instance_reducible]

instance LeanCert.Tactic.Auto.instInhabitedPointInequalityOutcome : Inhabited PointInequalityOutcome

Equations

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

inductive LeanCert.Tactic.Auto.PointInequalityFailure : Type

Expected non-successes from the direct point solver. Transport failures are kept distinct because the router treats them as implementation errors rather than numerical rejection.

• unsupported (expression detail : String) : PointInequalityFailure
• rejected (detail : String) : PointInequalityFailure
• inconclusive (detail : String) : PointInequalityFailure
• transportFailure (detail : String) : PointInequalityFailure
• internalFailure (detail : String) : PointInequalityFailure

@[instance_reducible]

instance LeanCert.Tactic.Auto.instInhabitedPointInequalityFailure : Inhabited PointInequalityFailure

Equations

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

def LeanCert.Tactic.Auto.proveClosedExpressionBoundTyped (goal : Lean.MVarId) (goalType : Lean.Expr) (taylorDepth : ℕ) (precision : ℤ := -80) (rationalFallback : Bool := true) : Lean.Elab.Tactic.TacticM (Except PointInequalityFailure PointInequalityOutcome)

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.proveClosedExpressionBoundAdaptiveTyped (goal : Lean.MVarId) (goalType : Lean.Expr) (policy : NumericalRefinementPolicy) : Lean.Elab.Tactic.TacticM (Except PointInequalityFailure PointInequalityOutcome)

Coordinate Dyadic precision and Taylor depth for a closed point inequality. The Rational fallback runs only in the final stage.

Equations

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

def LeanCert.Tactic.Auto.intervalDecideCoreWithPolicy (policy : NumericalRefinementPolicy) : Lean.Elab.Tactic.TacticM Unit

Point-inequality implementation under one coordinated refinement policy.

Equations

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

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

Compatibility entry point with fixed Taylor depth and adaptive Dyadic precision.

Equations

• LeanCert.Tactic.Auto.intervalDecideCore taylorDepth = LeanCert.Tactic.Auto.intervalDecideCoreWithPolicy (LeanCert.Tactic.NumericalRefinementPolicy.fixedTaylor taylorDepth 0)

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.