The fast_bound Tactic: Kernel-Verified Dyadic Arithmetic

This tactic uses the Dyadic backend to prove bounds within the Lean kernel. Unlike interval_bound, which uses native_decide (relying on the compiler/runtime), fast_bound uses decide, which reduces the proof term in the kernel.

This is made possible because Dyadic arithmetic avoids the expensive GCD computations of Rat that typically make kernel reduction infeasible for deep expressions.

Main tactics

• fast_bound - Prove bounds using Dyadic arithmetic with kernel verification
• fast_bound n - Specify precision in bits (default: 53)

Verification Trust Level

Tactic	Verification	Trust
interval_bound	native_decide	Lean Compiler + Runtime
fast_bound	decide	Lean Kernel only

The kernel is the smallest trusted component of Lean. By using decide, fast_bound provides proofs that are verified by this minimal trusted base.

When to use fast_bound

Use fast_bound instead of interval_bound when:

1. Maximum trust: You need proofs verified by the kernel, not the compiler
2. Deep expressions: Nested transcendentals like sin(sin(sin(x)))
3. Many multiplications: Polynomials with many terms
4. Audit requirements: Security-critical code that needs minimal TCB

Example

-- Proves using only kernel reduction (no compiler trust)
example : ∀ x ∈ Set.Icc (0 : ℝ) 1, x * x + Real.sin x ≤ 2 := by
  fast_bound

-- Higher precision for tight bounds
example : ∀ x ∈ Set.Icc (0 : ℝ) 1, Real.exp x ≤ 2.72 := by
  fast_bound 100

Bridge Theorems for Dyadic Kernel Verification

theorem LeanCert.Tactic.verify_upper_bound_dyadic (e : Core.Expr) (hsupp : Core.ExprSupportedCore e) (lo hi : ℚ) (hle : lo ≤ hi) (c : ℚ) (prec : ℤ) (depth : ℕ) (h_prec : prec ≤ 0) (hdom : Engine.evalDomainValidDyadic e (fun (x : ℕ) => Core.IntervalDyadic.ofIntervalRat { lo := lo, hi := hi, le := hle } prec) { precision := prec, taylorDepth := depth }) (h_check : (Engine.evalIntervalDyadic e (fun (x : ℕ) => Core.IntervalDyadic.ofIntervalRat { lo := lo, hi := hi, le := hle } prec) { precision := prec, taylorDepth := depth }).upperBoundedBy c = true) (x : ℝ) : x ∈ Set.Icc ↑lo ↑hi → Core.Expr.eval (fun (x_1 : ℕ) => x) e ≤ ↑c

Bridge theorem: Verify upper bound on Set.Icc using Dyadic arithmetic. This connects the decidable boolean upperBoundedBy to the semantic property.

theorem LeanCert.Tactic.verify_lower_bound_dyadic (e : Core.Expr) (hsupp : Core.ExprSupportedCore e) (lo hi : ℚ) (hle : lo ≤ hi) (c : ℚ) (prec : ℤ) (depth : ℕ) (h_prec : prec ≤ 0) (hdom : Engine.evalDomainValidDyadic e (fun (x : ℕ) => Core.IntervalDyadic.ofIntervalRat { lo := lo, hi := hi, le := hle } prec) { precision := prec, taylorDepth := depth }) (h_check : (Engine.evalIntervalDyadic e (fun (x : ℕ) => Core.IntervalDyadic.ofIntervalRat { lo := lo, hi := hi, le := hle } prec) { precision := prec, taylorDepth := depth }).lowerBoundedBy c = true) (x : ℝ) : x ∈ Set.Icc ↑lo ↑hi → ↑c ≤ Core.Expr.eval (fun (x_1 : ℕ) => x) e

Bridge theorem: Verify lower bound on Set.Icc using Dyadic arithmetic.

Tactic Implementation

inductive LeanCert.Tactic.KernelVerifyResult : Type

Reasons why kernel verification might not be used.

• success : KernelVerifyResult
• nativeExpression : KernelVerifyResult
• boundsNotDefeq : KernelVerifyResult
• boundCheckFailed : KernelVerifyResult
• parseError : KernelVerifyResult
• unsupportedGoal : KernelVerifyResult

instance LeanCert.Tactic.instDecidableEqKernelVerifyResult : DecidableEq KernelVerifyResult

Equations

• LeanCert.Tactic.instDecidableEqKernelVerifyResult x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

def LeanCert.Tactic.extractOrReifyAst (func : Lean.Expr) : Lean.Elab.Tactic.TacticM (Lean.Expr × Bool)

Try to extract AST from a function that may be Core.Expr.eval or a raw expression. Returns (ast, isExprEval) where isExprEval indicates if goal was in Expr.eval form.

Equations

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

def LeanCert.Tactic.fastBoundKernel (prec : ℤ) (taylorDepth : ℕ) : Lean.Elab.Tactic.TacticM KernelVerifyResult

Core implementation of fast_bound with kernel verification. Returns a result indicating success or reason for fallback.

Equations

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

Main Tactic

def LeanCert.Tactic.tacticCertify_kernel_ : Lean.ParserDescr

The certify_kernel tactic. Proves bounds using Dyadic arithmetic with kernel verification when possible.

Trust Levels

Mode	Verification	When Used
Kernel	decide	Goal in Core.Expr.eval form
Fallback	native_decide	General expressions

Kernel verification provides maximum trust (only the Lean kernel is trusted). Fallback mode trusts the Lean compiler and runtime in addition to the kernel.

Kernel Verification

For goals expressed using Core.Expr.eval, the tactic uses kernel-verified arithmetic via decide. This requires the goal's interval bounds to be definitionally equal to rational casts:

open LeanCert.Core

-- This uses kernel verification (Expr.eval form)
example : ∀ x ∈ Set.Icc (0 : ℝ) 1,
    Expr.eval (fun _ => x) (Expr.mul (Expr.var 0) (Expr.var 0)) ≤ 2 := by
  certify_kernel

General Usage

For native Lean expressions, the tactic falls back to certify_bound which uses native_decide:

-- This falls back to native_decide
example : ∀ x ∈ Set.Icc (0 : ℝ) 1, x * x ≤ 2 := by
  certify_kernel

Usage:

• certify_kernel - Use default precision (53 bits)
• certify_kernel n - Use n bits of precision

Note: fast_bound is an alias for backward compatibility.

Equations

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

def LeanCert.Tactic.tacticFast_bound_ : Lean.ParserDescr

Backward-compatible alias for certify_kernel

Equations

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

Convenience Variants

def LeanCert.Tactic.tacticCertify_kernel_precise : Lean.ParserDescr

certify_kernel with high precision (100 bits). Use when you need tighter bounds at the cost of speed.

Equations

• LeanCert.Tactic.tacticCertify_kernel_precise = Lean.ParserDescr.node `LeanCert.Tactic.tacticCertify_kernel_precise 1024 (Lean.ParserDescr.nonReservedSymbol "certify_kernel_precise" false)

def LeanCert.Tactic.tacticFast_bound_precise : Lean.ParserDescr

Backward-compatible alias

Equations

• LeanCert.Tactic.tacticFast_bound_precise = Lean.ParserDescr.node `LeanCert.Tactic.tacticFast_bound_precise 1024 (Lean.ParserDescr.nonReservedSymbol "fast_bound_precise" false)

def LeanCert.Tactic.tacticCertify_kernel_quick : Lean.ParserDescr

certify_kernel with low precision (30 bits). Use when you need maximum speed and can tolerate wider bounds.

Equations

• LeanCert.Tactic.tacticCertify_kernel_quick = Lean.ParserDescr.node `LeanCert.Tactic.tacticCertify_kernel_quick 1024 (Lean.ParserDescr.nonReservedSymbol "certify_kernel_quick" false)

def LeanCert.Tactic.tacticFast_bound_quick : Lean.ParserDescr

Backward-compatible alias

Equations

• LeanCert.Tactic.tacticFast_bound_quick = Lean.ParserDescr.node `LeanCert.Tactic.tacticFast_bound_quick 1024 (Lean.ParserDescr.nonReservedSymbol "fast_bound_quick" false)