Main Interval Bound Tactics

Core interval bound proving: intervalBoundCore, certify_bound, certify_bound. Also includes shadow diagnostics for error reporting.

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)")

Dyadic Backend Helper

structure LeanCert.Tactic.Auto.DyadicBoundOutcome : Type

Runtime facts from a retained checked-Dyadic bound proof.

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

@[instance_reducible]

instance LeanCert.Tactic.Auto.instInhabitedDyadicBoundOutcome : Inhabited DyadicBoundOutcome

Equations

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

structure LeanCert.Tactic.Auto.IntervalBoundOutcome : Type

Runtime facts from the retained direct-bound proof. Both Dyadic success and the checked Rational fallback retain their checker, Golden Theorem, and verification event.

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

@[instance_reducible]

instance LeanCert.Tactic.Auto.instInhabitedIntervalBoundOutcome : Inhabited IntervalBoundOutcome

Equations

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

inductive LeanCert.Tactic.Auto.IntervalBoundFailure : Type

Expected non-successes from the direct interval-bound portfolio.

• unsupported (expression detail : String) : IntervalBoundFailure
• inconclusive (detail : String) : IntervalBoundFailure
• transportFailure (detail : String) : IntervalBoundFailure
• internalFailure (detail : String) : IntervalBoundFailure

@[instance_reducible]

instance LeanCert.Tactic.Auto.instInhabitedIntervalBoundFailure : Inhabited IntervalBoundFailure

Equations

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

def LeanCert.Tactic.Auto.instReprIntervalBoundFailure.repr : IntervalBoundFailure → ℕ → Std.Format

Equations

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

@[instance_reducible]

instance LeanCert.Tactic.Auto.instReprIntervalBoundFailure : Repr IntervalBoundFailure

Equations

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

def LeanCert.Tactic.Auto.tryDyadicBoundImpl (goal : Lean.MVarId) (reified : Meta.ReifyReport) (boundRat : Lean.Expr) (intervalInfo : IntervalInfo) (taylorDepth : ℕ) (isStrict isLower : Bool) (precision : ℤ := -80) : Lean.Elab.Tactic.TacticM (Except IntervalBoundFailure (Option DyadicBoundOutcome))

Try to prove a forall-bound goal using the Dyadic backend. Returns metadata if the entire goal was closed, none otherwise. Uses the checked Dyadic evaluator for arbitrary expressions.

Equations

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

Main Tactic Implementation

def LeanCert.Tactic.Auto.intervalBoundCore (taylorDepth : ℕ) (useDyadic : Bool := true) : Lean.Elab.Tactic.TacticM Unit

The main certify_bound tactic implementation

Equations

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

def LeanCert.Tactic.Auto.intervalBoundCore.proveForallLe (useDyadic : Bool) (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 (useDyadic : Bool) (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 (useDyadic : Bool) (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 (useDyadic : Bool) (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.intervalBoundRationalCoreTyped (taylorDepth : ℕ) : Lean.Elab.Tactic.TacticM (Except IntervalBoundFailure IntervalBoundOutcome)

Direct typed Rational implementation. It performs one checker closure and returns the observation from that closure; failure classification never reruns the numerical checker.

Equations

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

def LeanCert.Tactic.Auto.intervalBoundCoreTypedAt (precision : ℤ) (taylorDepth : ℕ) (rationalFallback : Bool := true) : Lean.Elab.Tactic.TacticM (Except IntervalBoundFailure IntervalBoundOutcome)

Direct typed bound attempt at an explicit Dyadic precision and Taylor depth. The Rational fallback runs only after that Dyadic attempt is inconclusive. Rational proof construction runs once on success.

Equations

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

def LeanCert.Tactic.Auto.intervalBoundCoreTyped (taylorDepth : ℕ) : Lean.Elab.Tactic.TacticM (Except IntervalBoundFailure IntervalBoundOutcome)

Compatibility entry point retaining the historical fixed -80 Dyadic attempt before Rational fallback. New adaptive callers should use intervalBoundAdaptiveCoreTyped.

Equations

• LeanCert.Tactic.Auto.intervalBoundCoreTyped taylorDepth = LeanCert.Tactic.Auto.intervalBoundCoreTypedAt (-80) taylorDepth

def LeanCert.Tactic.Auto.intervalBoundAdaptiveCoreTyped (policy : NumericalRefinementPolicy) : Lean.Elab.Tactic.TacticM (Except IntervalBoundFailure IntervalBoundOutcome)

Try coordinated Dyadic stages in increasing refinement order, then run the Rational fallback once at the final Taylor depth. Each attempt is isolated in the original tactic state.

Equations

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

Tactic Syntax

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

Core of certify_bound. Without an explicit Taylor depth, Dyadic precision and Taylor depth increase together. With an explicit depth, only Dyadic precision is refined. Rational fallback runs once after the final Dyadic stage.

Equations

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

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

The certify_bound tactic.

Automatically proves bounds on expressions using interval arithmetic.

Usage:

• certify_bound - coordinates increasing Dyadic precision and Taylor depth
• certify_bound 20 - fixes Taylor depth at 20 while refining Dyadic precision
• certify_bound (trust := kernel) - kernel-only certificate verification (likewise native, auto; defaults to the leancert.trust option)

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

Equations

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