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.

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.