Automated Interval Arithmetic Tactics

This file provides smart tactics that automatically:

1. Reify Lean expressions to LeanCert AST (Phase 1)
2. Generate ExprSupportedCore proofs (Phase 2)
3. Apply the appropriate verification theorem and close the goal (Phase 3)

Main tactics

• interval_bound - Automatically prove bounds using interval arithmetic

Usage

-- Automatically proves the bound
example : ∀ x ∈ I01, x * x + Real.sin x ≤ 2 := by
  interval_bound

-- With custom Taylor depth for exp
example : ∀ x ∈ I01, Real.exp x ≤ 3 := by
  interval_bound { taylorDepth := 20 }

Design notes

The tactic detects the goal structure:

• ∀ x ∈ I, f x ≤ c → uses verify_upper_bound
• ∀ x ∈ I, c ≤ f x → uses verify_lower_bound

opaque leancert.debug : Lean.Option Bool

def isLeanCertDebugEnabled : Lean.CoreM Bool

Check if LeanCert debug mode is enabled

Equations

• isLeanCertDebugEnabled = do let __do_lift ← Lean.getOptions pure (Lean.KVMap.getBool __do_lift `leancert.debug)

Goal Normalization

theorem LeanCert.Tactic.Auto.forall_arrow_of_Icc {α : Type u_1} [Preorder α] {lo hi : α} {P : α → Prop} : (∀ x ∈ Set.Icc lo hi, P x) → ∀ (x : α), lo ≤ x → x ≤ hi → P x

Bridge: Set.Icc bound to arrow chain (lo ≤ x → x ≤ hi).

theorem LeanCert.Tactic.Auto.forall_arrow_of_Icc_rev {α : Type u_1} [Preorder α] {lo hi : α} {P : α → Prop} : (∀ x ∈ Set.Icc lo hi, P x) → ∀ x ≤ hi, lo ≤ x → P x

Bridge: Set.Icc bound to reversed arrow chain (x ≤ hi → lo ≤ x).

theorem LeanCert.Tactic.Auto.forall_and_of_Icc {α : Type u_1} [Preorder α] {lo hi : α} {P : α → Prop} : (∀ x ∈ Set.Icc lo hi, P x) → ∀ (x : α), lo ≤ x ∧ x ≤ hi → P x

Bridge: Set.Icc bound to conjunctive domain (lo ≤ x ∧ x ≤ hi).

theorem LeanCert.Tactic.Auto.forall_and_of_Icc_rev {α : Type u_1} [Preorder α] {lo hi : α} {P : α → Prop} : (∀ x ∈ Set.Icc lo hi, P x) → ∀ (x : α), x ≤ hi ∧ lo ≤ x → P x

Bridge: Set.Icc bound to reversed conjunctive domain (x ≤ hi ∧ lo ≤ x).

def LeanCert.Tactic.Auto.intervalNormCore : Lean.Elab.Tactic.TacticM Unit

Normalize common goal patterns for interval tactics.

Equations

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

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

The interval_norm tactic.

Normalizes inequalities, subtraction, rational division, and domain syntax to reduce goal-shape variation before parsing.

Equations

• LeanCert.Tactic.Auto.intervalNormTac = Lean.ParserDescr.node `LeanCert.Tactic.Auto.intervalNormTac 1024 (Lean.ParserDescr.nonReservedSymbol "interval_norm" false)

def LeanCert.Tactic.Auto.elabIntervalNorm : Lean.Elab.Tactic.Tactic

Equations

• LeanCert.Tactic.Auto.elabIntervalNorm x✝ = LeanCert.Tactic.Auto.intervalNormCore

Rational Extraction Helpers

Utilities for extracting rational numbers from Lean expressions representing real number literals or coercions.

partial def LeanCert.Tactic.Auto.extractRatFromReal (e : Lean.Expr) : Lean.MetaM (Option ℚ)

Try to extract a rational value from a Lean expression that represents a real number. Handles: Rat.cast, OfNat.ofNat, Nat.cast, Int.cast, negations, and divisions. Also handles direct ℚ expressions as a fallback.

partial def LeanCert.Tactic.Auto.extractRatFromReal.tryExtract (e : Lean.Expr) : Lean.MetaM (Option ℚ)

def LeanCert.Tactic.Auto.mkIntervalRat (loExpr hiExpr : Lean.Expr) (lo hi : ℚ) : Lean.MetaM Lean.Expr

Build an IntervalRat expression from two rational expressions and their Lean representations

Equations

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

Goal Analysis

Utilities for analyzing the goal structure to determine which theorem to apply.

structure LeanCert.Tactic.Auto.IntervalInfo : Type

Information about interval source

• intervalRat : Lean.Expr

  The IntervalRat expression to use in proofs

• fromSetIcc : Option (ℚ × ℚ × Lean.Expr × Lean.Expr × Lean.Expr × Lean.Expr × Lean.Expr)

  If converted from Set.Icc, contains (lo, hi, loRatExpr, hiRatExpr, leProof, origLoExpr, origHiExpr)

def LeanCert.Tactic.Auto.instReprIntervalInfo.repr : IntervalInfo → ℕ → Std.Format

Equations

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

instance LeanCert.Tactic.Auto.instReprIntervalInfo : Repr IntervalInfo

Equations

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

inductive LeanCert.Tactic.Auto.BoundGoal : Type

Result of analyzing a bound goal

• forallLe (varName : Lean.Name) (interval : IntervalInfo) (func bound : Lean.Expr) : BoundGoal

  ∀ x ∈ I, f x ≤ c

• forallGe (varName : Lean.Name) (interval : IntervalInfo) (func bound : Lean.Expr) : BoundGoal

  ∀ x ∈ I, c ≤ f x

• forallLt (varName : Lean.Name) (interval : IntervalInfo) (func bound : Lean.Expr) : BoundGoal

  ∀ x ∈ I, f x < c

• forallGt (varName : Lean.Name) (interval : IntervalInfo) (func bound : Lean.Expr) : BoundGoal

  ∀ x ∈ I, c < f x

instance LeanCert.Tactic.Auto.instReprBoundGoal : Repr BoundGoal

Equations

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

def LeanCert.Tactic.Auto.instReprBoundGoal.repr : BoundGoal → ℕ → Std.Format

Equations

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

def LeanCert.Tactic.Auto.parseBoundGoal (goal : Lean.Expr) : Lean.MetaM (Option BoundGoal)

Try to parse a goal as a bound goal

Equations

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

def LeanCert.Tactic.Auto.parseBoundGoal.findSome (cands : List Lean.Expr) (f : Lean.Expr → Lean.MetaM (Option BoundGoal)) : Lean.MetaM (Option BoundGoal)

Equations

• One or more equations did not get rendered due to their size.
• LeanCert.Tactic.Auto.parseBoundGoal.findSome [] f = pure none

def LeanCert.Tactic.Auto.parseBoundGoal.getLeArgs (e : Lean.Expr) : Lean.MetaM (Option (Lean.Expr × Lean.Expr))

Extract (lhs, rhs) from an LE.le application.

Equations

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

def LeanCert.Tactic.Auto.parseBoundGoal.extractLowerBound (e x : Lean.Expr) : Lean.MetaM (Option Lean.Expr)

Extract lower bound lo from lo ≤ x.

Equations

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

def LeanCert.Tactic.Auto.parseBoundGoal.extractUpperBound (e x : Lean.Expr) : Lean.MetaM (Option Lean.Expr)

Extract upper bound hi from x ≤ hi.

Equations

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

def LeanCert.Tactic.Auto.parseBoundGoal.extractBoundsFromAnd (memTy x : Lean.Expr) : Lean.MetaM (Option (Lean.Expr × Lean.Expr))

Extract bounds from conjunction form lo ≤ x ∧ x ≤ hi.

Equations

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

def LeanCert.Tactic.Auto.parseBoundGoal.mkIntervalInfoFromBounds (loExpr hiExpr : Lean.Expr) : Lean.MetaM (Option IntervalInfo)

Build IntervalInfo from explicit lo/hi bounds.

Equations

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

def LeanCert.Tactic.Auto.parseBoundGoal.extractInterval (memTy x : Lean.Expr) : Lean.MetaM (Option IntervalInfo)

Extract the interval from a membership expression

Equations

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

def LeanCert.Tactic.Auto.parseBoundGoal.tryConvertSetIcc (interval : Lean.Expr) : Lean.MetaM (Option IntervalInfo)

Try to convert a Set.Icc expression to an IntervalRat with full info

Equations

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

Diagnostic Helpers for Shadow Computation

def LeanCert.Tactic.Auto.runShadowDiagnostic (boundGoal : Option BoundGoal) (_goalType : Lean.Expr) : Lean.Elab.Tactic.TacticM Lean.MessageData

Run shadow computation to diagnose why a proof failed

Equations

• One or more equations did not get rendered due to their size.
• LeanCert.Tactic.Auto.runShadowDiagnostic boundGoal _goalType = pure (Lean.toMessageData "(Could not parse goal for diagnostics)")

Shared Diagnostic Helpers

def LeanCert.Tactic.Auto.formatGoalContext (goalType : Lean.Expr) : Lean.MetaM Lean.MessageData

Format goal context for diagnostic output, showing both normal and detailed forms

Equations

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

def LeanCert.Tactic.Auto.analyzeGoalStructure (goalType : Lean.Expr) : Lean.MetaM Lean.MessageData

Analyze goal structure and report what was found vs expected

Equations

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

def LeanCert.Tactic.Auto.suggestNextActions (failureType : String) : Lean.MessageData

Suggest next actions based on failure type

Equations

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

def LeanCert.Tactic.Auto.mkDiagnosticReport (tacticName : String) (goalType : Lean.Expr) (failureType : String) (additionalInfo : Option Lean.MessageData := none) : Lean.MetaM Lean.MessageData

Create a full diagnostic report for a failed tactic

Equations

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

Main Tactic Implementation

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

The main interval_bound tactic implementation

Equations

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

def LeanCert.Tactic.Auto.intervalBoundCore.extractRatBound (bound : Lean.Expr) : Lean.Elab.Tactic.TacticM Lean.Expr

Try to extract the rational from a bound expression (possibly coerced to ℝ)

Equations

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

def LeanCert.Tactic.Auto.intervalBoundCore.getAst (func : Lean.Expr) : Lean.Elab.Tactic.TacticM Lean.Expr

Try to extract AST from an Expr.eval application, or reify if it's a raw expression

Equations

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

def LeanCert.Tactic.Auto.intervalBoundCore.getSupportProof (ast : Lean.Expr) : Lean.Elab.Tactic.TacticM (Lean.Expr × Bool)

Try to generate ExprSupportedCore proof, falling back to ExprSupportedWithInv if needed. Returns (supportProof, useWithInv) where useWithInv is true if we used WithInv.

Equations

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

def LeanCert.Tactic.Auto.intervalBoundCore.proveForallLe (goal : Lean.MVarId) (intervalInfo : IntervalInfo) (func bound : Lean.Expr) (taylorDepth : ℕ) : Lean.Elab.Tactic.TacticM Unit

Prove ∀ x ∈ I, f x ≤ c

Equations

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

def LeanCert.Tactic.Auto.intervalBoundCore.proveForallGe (goal : Lean.MVarId) (intervalInfo : IntervalInfo) (func bound : Lean.Expr) (taylorDepth : ℕ) : Lean.Elab.Tactic.TacticM Unit

Prove ∀ x ∈ I, c ≤ f x

Equations

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

def LeanCert.Tactic.Auto.intervalBoundCore.proveForallLt (goal : Lean.MVarId) (intervalInfo : IntervalInfo) (func bound : Lean.Expr) (taylorDepth : ℕ) : Lean.Elab.Tactic.TacticM Unit

Prove ∀ x ∈ I, f x < c

Equations

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

def LeanCert.Tactic.Auto.intervalBoundCore.proveForallGt (goal : Lean.MVarId) (intervalInfo : IntervalInfo) (func bound : Lean.Expr) (taylorDepth : ℕ) : Lean.Elab.Tactic.TacticM Unit

Prove ∀ x ∈ I, c < f x

Equations

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

Tactic Syntax

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

The certify_bound tactic.

Automatically proves bounds on expressions using interval arithmetic.

Usage:

• certify_bound - uses adaptive precision (tries depths 10, 15, 20, 25, 30)
• certify_bound 20 - uses fixed Taylor depth of 20

Supports goals of the form:

• ∀ x ∈ I, f x ≤ c
• ∀ x ∈ I, c ≤ f x
• ∀ x ∈ I, f x < c
• ∀ x ∈ I, c < f x

Note: interval_bound is an alias for backward compatibility.

Equations

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

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

Backward-compatible alias for certify_bound

Equations

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

Multivariate Bounds Tactic

The multivariate_bound tactic handles goals with multiple quantified variables:

• ∀ x ∈ I, ∀ y ∈ J, f(x, y) ≤ c
• ∀ x ∈ I, ∀ y ∈ J, c ≤ f(x, y)

This uses the global optimization theorems (verify_global_upper_bound/verify_global_lower_bound) from Validity/Bounds.lean, which operate over Box (List IntervalRat) domains.

structure LeanCert.Tactic.Auto.VarIntervalInfo : Type

Information about a quantified variable and its interval

• varName : Lean.Name

  Variable name

• varType : Lean.Expr

  Variable type

• intervalRat : Lean.Expr

  Extracted interval (lo, hi rationals and their expressions)

• loExpr : Lean.Expr

  Original lower bound expression for Set.Icc

• hiExpr : Lean.Expr

  Original upper bound expression for Set.Icc

• lo : ℚ

  Low bound as rational

• hi : ℚ

  High bound as rational

instance LeanCert.Tactic.Auto.instReprVarIntervalInfo : Repr VarIntervalInfo

Equations

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

def LeanCert.Tactic.Auto.instReprVarIntervalInfo.repr : VarIntervalInfo → ℕ → Std.Format

Equations

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

instance LeanCert.Tactic.Auto.instInhabitedVarIntervalInfo : Inhabited VarIntervalInfo

Equations

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

def LeanCert.Tactic.Auto.instInhabitedVarIntervalInfo.default : VarIntervalInfo

Equations

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

inductive LeanCert.Tactic.Auto.MultivariateBoundGoal : Type

Result of analyzing a multivariate bound goal

• forallLe (vars : Array VarIntervalInfo) (func bound : Lean.Expr) : MultivariateBoundGoal

  ∀ x₁ ∈ I₁, ..., ∀ xₙ ∈ Iₙ, f(x₁,...,xₙ) ≤ c

• forallGe (vars : Array VarIntervalInfo) (func bound : Lean.Expr) : MultivariateBoundGoal

  ∀ x₁ ∈ I₁, ..., ∀ xₙ ∈ Iₙ, c ≤ f(x₁,...,xₙ)

instance LeanCert.Tactic.Auto.instReprMultivariateBoundGoal : Repr MultivariateBoundGoal

Equations

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

def LeanCert.Tactic.Auto.instReprMultivariateBoundGoal.repr : MultivariateBoundGoal → ℕ → Std.Format

Equations

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

def LeanCert.Tactic.Auto.parseMultivariateBoundGoal (goal : Lean.Expr) : Lean.MetaM (Option MultivariateBoundGoal)

Recursively parse a multivariate bound goal, collecting variables and intervals. This processes all quantifiers within nested withLocalDeclD scopes so that fvars remain valid for mkLambdaFVars.

Equations

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

partial def LeanCert.Tactic.Auto.parseMultivariateBoundGoal.findSome (cands : List Lean.Expr) (f : Lean.Expr → Lean.MetaM (Option MultivariateBoundGoal)) : Lean.MetaM (Option MultivariateBoundGoal)

partial def LeanCert.Tactic.Auto.parseMultivariateBoundGoal.collect (extractLowerBound extractUpperBound : Lean.Expr → Lean.Expr → Lean.MetaM (Option Lean.Expr)) (extractBoundsFromAnd : Lean.Expr → Lean.Expr → Lean.MetaM (Option (Lean.Expr × Lean.Expr))) (mkVarIntervalInfoFromBounds : Lean.Expr → Lean.Expr → Lean.Expr → Lean.MetaM (Option VarIntervalInfo)) (memCandidates : Lean.Expr → Lean.MetaM (Array Lean.Expr)) (e : Lean.Expr) (acc : Array VarIntervalInfo) (fvars : Array Lean.Expr) : Lean.MetaM (Option MultivariateBoundGoal)

def LeanCert.Tactic.Auto.mkBoxExpr (infos : Array VarIntervalInfo) : Lean.MetaM Lean.Expr

Build a Box expression (List IntervalRat) from an array of VarIntervalInfo

Equations

• LeanCert.Tactic.Auto.mkBoxExpr infos = Lean.Meta.mkListLit (Lean.mkConst `LeanCert.Core.IntervalRat) (Array.map (fun (x : LeanCert.Tactic.Auto.VarIntervalInfo) => x.intervalRat) infos).toList

def LeanCert.Tactic.Auto.multivariateBoundCore (maxIters : ℕ) (tolerance : ℚ) (useMonotonicity : Bool) (taylorDepth : ℕ) : Lean.Elab.Tactic.TacticM Unit

The main multivariate_bound tactic implementation

Equations

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

def LeanCert.Tactic.Auto.multivariateBoundCore.extractRatBound (bound : Lean.Expr) : Lean.Elab.Tactic.TacticM Lean.Expr

Extract rational bound from possible coercion (reusing logic from intervalBoundCore)

Equations

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

def LeanCert.Tactic.Auto.multivariateBoundCore.getVarExprs (vars : Array VarIntervalInfo) : Lean.Elab.Tactic.TacticM (Array Lean.Expr)

Fetch local variable expressions in the order of VarIntervalInfo.

Equations

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

def LeanCert.Tactic.Auto.multivariateBoundCore.mkEnvExpr (varsListExpr : Lean.Expr) : Lean.Elab.Tactic.TacticM Lean.Expr

Build an environment function ρ from a list of variables.

Equations

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

def LeanCert.Tactic.Auto.multivariateBoundCore.proveMultivariateLe (goal : Lean.MVarId) (vars : Array VarIntervalInfo) (func bound : Lean.Expr) (maxIters : ℕ) (tolerance : ℚ) (useMonotonicity : Bool) (taylorDepth : ℕ) : Lean.Elab.Tactic.TacticM Unit

Prove ∀ x₁ ∈ I₁, ..., ∀ xₙ ∈ Iₙ, f(x) ≤ c using verify_global_upper_bound

Equations

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

def LeanCert.Tactic.Auto.multivariateBoundCore.proveMultivariateGe (goal : Lean.MVarId) (vars : Array VarIntervalInfo) (func bound : Lean.Expr) (maxIters : ℕ) (tolerance : ℚ) (useMonotonicity : Bool) (taylorDepth : ℕ) : Lean.Elab.Tactic.TacticM Unit

Prove ∀ x₁ ∈ I₁, ..., ∀ xₙ ∈ Iₙ, c ≤ f(x) using verify_global_lower_bound

Equations

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

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

The multivariate_bound tactic.

Automatically proves bounds on multivariate expressions using global optimization.

Usage:

• multivariate_bound - uses defaults (1000 iterations, tolerance 1/1000, Taylor depth 10)
• multivariate_bound 2000 - uses 2000 iterations

Supports goals of the form:

• ∀ x ∈ I, ∀ y ∈ J, f(x,y) ≤ c
• ∀ x ∈ I, ∀ y ∈ J, c ≤ f(x,y)

Equations

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

Global Optimization Tactic

The opt_bound tactic handles goals of the form:

• ∀ ρ, Box.envMem ρ B → (∀ i, i ≥ B.length → ρ i = 0) → c ≤ Expr.eval ρ e
• ∀ ρ, Box.envMem ρ B → (∀ i, i ≥ B.length → ρ i = 0) → Expr.eval ρ e ≤ c

This uses global branch-and-bound optimization with optional monotonicity pruning.

partial def LeanCert.Tactic.Auto.skipForallsAux (e : Lean.Expr) : Lean.MetaM Lean.Expr

Skip through foralls (from ≥ binder notation) to get to the final comparison

inductive LeanCert.Tactic.Auto.GlobalBoundGoal : Type

Result of analyzing a global bound goal

• globalGe (box expr bound : Lean.Expr) : GlobalBoundGoal

  ∀ ρ ∈ B, (zero extension) → c ≤ f(ρ)

• globalLe (box expr bound : Lean.Expr) : GlobalBoundGoal

  ∀ ρ ∈ B, (zero extension) → f(ρ) ≤ c

instance LeanCert.Tactic.Auto.instReprGlobalBoundGoal : Repr GlobalBoundGoal

Equations

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

def LeanCert.Tactic.Auto.instReprGlobalBoundGoal.repr : GlobalBoundGoal → ℕ → Std.Format

Equations

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

def LeanCert.Tactic.Auto.isExprEval (e : Lean.Expr) : Bool

Check if expression is Expr.eval (checking both short and full names)

Equations

• LeanCert.Tactic.Auto.isExprEval e = (e.getAppFn.isConstOf `LeanCert.Core.Expr.eval || e.getAppFn.isConstOf `LeanCert.Core.Expr.eval)

def LeanCert.Tactic.Auto.isExprEvalName (name : Lean.Name) : Bool

Check if name ends with Expr.eval

Equations

• LeanCert.Tactic.Auto.isExprEvalName name = `Expr.eval.isSuffixOf name

def LeanCert.Tactic.Auto.parseSimpleBoundGoal (goal : Lean.Expr) : Lean.MetaM (Option GlobalBoundGoal)

Try to parse an already-intro'd goal as a global optimization bound. After intro ρ hρ hzero, the goal should be a comparison: Expr.eval ρ e ≤ c or c ≤ Expr.eval ρ e

Equations

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

def LeanCert.Tactic.Auto.mkGlobalOptConfigExpr (maxIters : ℕ) (tolerance : ℚ) (useMonotonicity : Bool) (taylorDepth : ℕ) : Lean.MetaM Lean.Expr

Build a GlobalOptConfig expression

Equations

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

def LeanCert.Tactic.Auto.optBoundCore (maxIters : ℕ) (useMonotonicity : Bool) (taylorDepth : ℕ) : Lean.Elab.Tactic.TacticM Unit

The main opt_bound tactic implementation

Equations

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

def LeanCert.Tactic.Auto.optBoundCore.proveSupport (goal : Lean.MVarId) : Lean.Elab.Tactic.TacticM Unit

Prove ExprSupportedCore goal by generating the proof

Equations

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

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

The opt_bound tactic.

Automatically proves global bounds on expressions over boxes using branch-and-bound optimization.

Usage:

• opt_bound - uses defaults (1000 iterations, no monotonicity, Taylor depth 10)
• opt_bound 2000 - uses 2000 iterations
• opt_bound 1000 mono - enables monotonicity pruning

Supports goals of the form:

• ∀ ρ, Box.envMem ρ B → (∀ i, i ≥ B.length → ρ i = 0) → c ≤ Expr.eval ρ e
• ∀ ρ, Box.envMem ρ B → (∀ i, i ≥ B.length → ρ i = 0) → Expr.eval ρ e ≤ c

Equations

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

Root Finding Tactic

The root_bound tactic handles goals related to root finding:

• ∀ x ∈ I, f x ≠ 0 (no root exists) - uses verify_no_root

inductive LeanCert.Tactic.Auto.RootGoal : Type

Result of analyzing a root finding goal

• forallNeZero (varName : Lean.Name) (interval func : Lean.Expr) : RootGoal

  ∀ x ∈ I, f x ≠ 0

instance LeanCert.Tactic.Auto.instReprRootGoal : Repr RootGoal

Equations

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

def LeanCert.Tactic.Auto.instReprRootGoal.repr : RootGoal → ℕ → Std.Format

Equations

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

def LeanCert.Tactic.Auto.parseRootGoal (goal : Lean.Expr) : Lean.MetaM (Option RootGoal)

Try to parse a goal as a root finding goal

Equations

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

def LeanCert.Tactic.Auto.parseRootGoal.getLeArgs (e : Lean.Expr) : Lean.MetaM (Option (Lean.Expr × Lean.Expr))

Equations

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

def LeanCert.Tactic.Auto.parseRootGoal.extractLowerBound (e x : Lean.Expr) : Lean.MetaM (Option Lean.Expr)

Equations

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

def LeanCert.Tactic.Auto.parseRootGoal.extractUpperBound (e x : Lean.Expr) : Lean.MetaM (Option Lean.Expr)

Equations

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

def LeanCert.Tactic.Auto.parseRootGoal.extractBoundsFromAnd (memTy x : Lean.Expr) : Lean.MetaM (Option (Lean.Expr × Lean.Expr))

Equations

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

def LeanCert.Tactic.Auto.parseRootGoal.mkIntervalRatFromBounds (loExpr hiExpr : Lean.Expr) : Lean.MetaM (Option Lean.Expr)

Equations

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

def LeanCert.Tactic.Auto.parseRootGoal.extractInterval (memTy x : Lean.Expr) : Lean.MetaM (Option Lean.Expr)

Extract the interval from a membership expression

Equations

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

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

The main root_bound tactic implementation

Equations

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

def LeanCert.Tactic.Auto.rootBoundCore.getAst (func : Lean.Expr) : Lean.Elab.Tactic.TacticM Lean.Expr

Try to extract AST from an Expr.eval application, or reify if it's a raw expression

Equations

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

def LeanCert.Tactic.Auto.rootBoundCore.tryConvertSetIccForRootBound (interval : Lean.Expr) : Lean.MetaM (Option Lean.Expr)

Try to convert Set.Icc to IntervalRat for root_bound

Equations

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

def LeanCert.Tactic.Auto.rootBoundCore.proveForallNeZero (goal : Lean.MVarId) (interval func : Lean.Expr) (taylorDepth : ℕ) : Lean.Elab.Tactic.TacticM Unit

Prove ∀ x ∈ I, f x ≠ 0 using verify_no_root

Equations

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

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

The root_bound tactic.

Automatically proves root-related properties using interval arithmetic.

Usage:

• root_bound - uses default Taylor depth of 10
• root_bound 20 - uses Taylor depth of 20

Supports goals of the form:

• ∀ x ∈ I, f x ≠ 0 (proves no root exists in interval)

Equations

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

Point Inequality Tactic (interval_decide)

The interval_decide tactic proves point inequalities like Real.exp 1 ≤ 3 by transforming them into singleton interval bounds ∀ x ∈ Set.Icc c c, f x ≤ b and using the existing interval_bound machinery.

def LeanCert.Tactic.Auto.parsePointIneq (goal : Lean.Expr) : Lean.MetaM (Option (Lean.Expr × Lean.Expr × Bool × Bool))

Parse a point inequality goal and extract lhs, rhs, and inequality type. Returns (lhs, rhs, isStrict, isReversed) where:

• isStrict: true for < or >, false for ≤ or ≥
• isReversed: true for ≥ or > (need to flip the comparison)

Equations

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

partial def LeanCert.Tactic.Auto.collectConstants (e : Lean.Expr) : Lean.MetaM (List ℚ)

Try to collect all constant rational values from an expression. Returns the list of rational constants found (for building the singleton interval).

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. For goals like Real.pi ≤ 4 where the expression doesn't contain any variables, we can directly use verify_upper_bound/verify_lower_bound with a singleton interval.

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. Transforms f(c) ≤ b into ∀ x ∈ [c,c], f(x) ≤ b and uses interval_bound.

Equations

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

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

Equations

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

Subdivision-aware bound proving

The interval_bound_subdiv tactic uses interval subdivision when the direct approach fails. This helps with tight bounds where interval arithmetic has excessive width due to the dependency problem (when a variable appears multiple times, we lose correlation).

Subdivision works because:

1. Narrower intervals → tighter bounds
2. May subdivide near critical points, reducing dependency

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

The interval_bound_subdiv tactic.

Like interval_bound, but uses interval subdivision when the direct approach fails. This can help with tight bounds where the dependency problem causes excessive width.

Usage:

• interval_bound_subdiv - uses default Taylor depth 10 and max subdivision depth 3
• interval_bound_subdiv 20 - uses Taylor depth 20
• interval_bound_subdiv 20 5 - uses Taylor depth 20 and max subdivision depth 5

Equations

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

Adaptive Branch-and-Bound Tactic

The interval_bound_adaptive tactic uses branch-and-bound global optimization for bound verification. Unlike interval_bound_subdiv which does subdivision at the proof level (many native_decide calls), this tactic does subdivision at the computation level (single native_decide).

This is more efficient for cases requiring many subdivisions.

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

The interval_bound_adaptive tactic.

Uses branch-and-bound global optimization for bound verification. This does adaptive subdivision at the computation level (single native_decide) rather than at the proof level (multiple native_decide calls).

Usage:

• interval_bound_adaptive - uses default max iterations (200)
• interval_bound_adaptive 500 - uses 500 max iterations

More efficient than interval_bound_subdiv for cases requiring many subdivisions.

Equations

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

Unified Interval Tactic

The interval_auto tactic automatically routes to the appropriate tactic based on goal structure:

• Point inequalities (e.g., Real.pi ≤ 4) → interval_decide
• Quantified bounds (e.g., ∀ x ∈ I, f x ≤ c) → interval_bound

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.