Global Optimization Tactic

The opt_bound tactic handles goals using global branch-and-bound optimization.

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.

inductive LeanCert.Tactic.Auto.OptimizationDirection : Type

Runtime facts from the retained global-optimization certificate.

• upper : OptimizationDirection
• lower : OptimizationDirection

@[instance_reducible]

instance LeanCert.Tactic.Auto.instDecidableEqOptimizationDirection : DecidableEq OptimizationDirection

Equations

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

@[instance_reducible]

instance LeanCert.Tactic.Auto.instReprOptimizationDirection : Repr OptimizationDirection

Equations

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

def LeanCert.Tactic.Auto.instReprOptimizationDirection.repr : OptimizationDirection → ℕ → Std.Format

Equations

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

@[instance_reducible]

instance LeanCert.Tactic.Auto.instInhabitedOptimizationDirection : Inhabited OptimizationDirection

Equations

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

structure LeanCert.Tactic.Auto.OptBoundOutcome : Type

• direction : OptimizationDirection
• checker : Lean.Name
• verifier : Lean.Name
• verification : VerificationUsage
• maxIterations : ℕ
• tolerance : ℚ
• useMonotonicity : Bool
• taylorDepth : ℕ

@[instance_reducible]

instance LeanCert.Tactic.Auto.instInhabitedOptBoundOutcome : Inhabited OptBoundOutcome

Equations

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

inductive LeanCert.Tactic.Auto.OptBoundFailure : Type

• unsupported (expression detail : String) : OptBoundFailure
• rejected (detail : String) : OptBoundFailure
• transportFailure (detail : String) : OptBoundFailure
• internalFailure (detail : String) : OptBoundFailure

@[instance_reducible]

instance LeanCert.Tactic.Auto.instInhabitedOptBoundFailure : Inhabited OptBoundFailure

Equations

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

@[instance_reducible]

instance LeanCert.Tactic.Auto.instReprOptBoundFailure : Repr OptBoundFailure

Equations

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

def LeanCert.Tactic.Auto.instReprOptBoundFailure.repr : OptBoundFailure → ℕ → Std.Format

Equations

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

unsafe def LeanCert.Tactic.Auto.optBoundCoreTyped (maxIters : ℕ) (useMonotonicity : Bool) (taylorDepth : ℕ) : Lean.Elab.Tactic.TacticM (Except OptBoundFailure OptBoundOutcome)

Typed opt_bound implementation. The upper and lower theorem interpretations are transactional, and only the retained certificate contributes verification telemetry.

Equations

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

unsafe def LeanCert.Tactic.Auto.optBoundCoreTyped.hasBinders (count : ℕ) (type : Lean.Expr) : Lean.MetaM Bool

Equations

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

unsafe def LeanCert.Tactic.Auto.optBoundCoreTyped.stripBinders (count : ℕ) (type : Lean.Expr) : Lean.MetaM (Option Lean.Expr)

Equations

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

unsafe def LeanCert.Tactic.Auto.optBoundCoreTyped.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.optBoundTac : 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.

unsafe def LeanCert.Tactic.Auto.elabOptBound : Lean.Elab.Tactic.Tactic

Equations

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