Multivariate Bound Tactic

The multivariate_bound tactic proves bounds on multivariate expressions.

inductive LeanCert.Tactic.Auto.MultivariateBoundDirection : Type

Runtime facts from the retained multivariate global-bound certificate.

• upper : MultivariateBoundDirection
• lower : MultivariateBoundDirection

@[instance_reducible]

instance LeanCert.Tactic.Auto.instDecidableEqMultivariateBoundDirection : DecidableEq MultivariateBoundDirection

Equations

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

def LeanCert.Tactic.Auto.instReprMultivariateBoundDirection.repr : MultivariateBoundDirection → ℕ → Std.Format

Equations

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

@[instance_reducible]

instance LeanCert.Tactic.Auto.instReprMultivariateBoundDirection : Repr MultivariateBoundDirection

Equations

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

@[instance_reducible]

instance LeanCert.Tactic.Auto.instInhabitedMultivariateBoundDirection : Inhabited MultivariateBoundDirection

Equations

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

structure LeanCert.Tactic.Auto.MultivariateBoundOutcome : Type

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

@[instance_reducible]

instance LeanCert.Tactic.Auto.instInhabitedMultivariateBoundOutcome : Inhabited MultivariateBoundOutcome

Equations

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

inductive LeanCert.Tactic.Auto.MultivariateBoundFailure : Type

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

@[instance_reducible]

instance LeanCert.Tactic.Auto.instInhabitedMultivariateBoundFailure : Inhabited MultivariateBoundFailure

Equations

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

@[instance_reducible]

instance LeanCert.Tactic.Auto.instReprMultivariateBoundFailure : Repr MultivariateBoundFailure

Equations

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

def LeanCert.Tactic.Auto.instReprMultivariateBoundFailure.repr : MultivariateBoundFailure → ℕ → Std.Format

Equations

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

unsafe def LeanCert.Tactic.Auto.multivariateBoundCoreTyped (maxIters : ℕ) (tolerance : ℚ) (useMonotonicity : Bool) (taylorDepth : ℕ) : Lean.Elab.Tactic.TacticM (Except MultivariateBoundFailure MultivariateBoundOutcome)

Typed multivariate-bound implementation.

Equations

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

unsafe def LeanCert.Tactic.Auto.multivariateBoundCoreTyped.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.

unsafe def LeanCert.Tactic.Auto.multivariateBoundCoreTyped.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.

unsafe def LeanCert.Tactic.Auto.multivariateBoundCoreTyped.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.

unsafe def LeanCert.Tactic.Auto.multivariateBoundCoreTyped.proveMultivariateLe (goal : Lean.MVarId) (vars : Array VarIntervalInfo) (func bound : Lean.Expr) (maxIters : ℕ) (tolerance : ℚ) (useMonotonicity : Bool) (taylorDepth : ℕ) : Lean.Elab.Tactic.TacticM (Except MultivariateBoundFailure VerificationEvent)

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.

unsafe def LeanCert.Tactic.Auto.multivariateBoundCoreTyped.proveMultivariateGe (goal : Lean.MVarId) (vars : Array VarIntervalInfo) (func bound : Lean.Expr) (maxIters : ℕ) (tolerance : ℚ) (useMonotonicity : Bool) (taylorDepth : ℕ) : Lean.Elab.Tactic.TacticM (Except MultivariateBoundFailure VerificationEvent)

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.multivariateBoundTac : 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.

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

Equations

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