Automated Interval Arithmetic Tactics

This module re-exports the interval arithmetic tactic suite:

• interval_bound - Prove bounds using interval arithmetic
• interval_decide - Prove point inequalities
• interval_auto - Unified entry point (recommended)
• multivariate_bound - Prove bounds on multivariate expressions
• opt_bound - Prove bounds using global optimization
• root_bound - Prove non-existence of roots
• interval_bound_subdiv - Prove bounds with subdivision
• interval_bound_adaptive - Prove bounds with adaptive precision

The infrastructure (types, parsing, normalization, extraction, diagnostics, common proving utilities) lives in LeanCert.Tactic.IntervalAuto.Basic.

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

Unified tactic that handles both point inequalities and quantified bounds.

• interval_auto - uses adaptive precision
• interval_auto 20 - uses fixed Taylor depth of 20

This is the recommended entry point for interval arithmetic proofs.

Equations

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