Core Types for Interval Tactics

This module defines the core data structures used by interval arithmetic tactics:

• IntervalInfo: Information about an interval source
• BoundGoal: Result of analyzing a univariate bound goal
• VarIntervalInfo: Information about a quantified variable and its interval
• MultivariateBoundGoal: Result of analyzing a multivariate bound goal
• GlobalBoundGoal: Result of analyzing a global optimization bound goal
• RootGoal: Result of analyzing a root finding goal

opaque LeanCert.Tactic.Auto.leancert.debug : Lean.Option Bool

def LeanCert.Tactic.Auto.isLeanCertDebugEnabled : Lean.CoreM Bool

Check if LeanCert debug mode is enabled

Equations

• LeanCert.Tactic.Auto.isLeanCertDebugEnabled = do let __do_lift ← Lean.getOptions pure (__do_lift.getBool `leancert.debug)

structure LeanCert.Tactic.Auto.IntervalInfo : Type

Information about interval source

• intervalRat : Lean.Expr

  The IntervalRat expression to use in proofs

• fromSetIcc : Option (ℚ × ℚ × Lean.Expr × Lean.Expr × Lean.Expr × Lean.Expr × Lean.Expr)

  If converted from Set.Icc, contains (lo, hi, loRatExpr, hiRatExpr, leProof, origLoExpr, origHiExpr)

@[instance_reducible]

instance LeanCert.Tactic.Auto.instReprIntervalInfo : Repr IntervalInfo

Equations

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

def LeanCert.Tactic.Auto.instReprIntervalInfo.repr : IntervalInfo → ℕ → Std.Format

Equations

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

inductive LeanCert.Tactic.Auto.BoundGoal : Type

Result of analyzing a bound goal

• forallLe (varName : Lean.Name) (interval : IntervalInfo) (func bound : Lean.Expr) : BoundGoal

  ∀ x ∈ I, f x ≤ c

• forallGe (varName : Lean.Name) (interval : IntervalInfo) (func bound : Lean.Expr) : BoundGoal

  ∀ x ∈ I, c ≤ f x

• forallLt (varName : Lean.Name) (interval : IntervalInfo) (func bound : Lean.Expr) : BoundGoal

  ∀ x ∈ I, f x < c

• forallGt (varName : Lean.Name) (interval : IntervalInfo) (func bound : Lean.Expr) : BoundGoal

  ∀ x ∈ I, c < f x

def LeanCert.Tactic.Auto.instReprBoundGoal.repr : BoundGoal → ℕ → Std.Format

Equations

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

@[instance_reducible]

instance LeanCert.Tactic.Auto.instReprBoundGoal : Repr BoundGoal

Equations

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

structure LeanCert.Tactic.Auto.VarIntervalInfo : Type

Information about a quantified variable and its interval

• varName : Lean.Name

  Variable name

• varType : Lean.Expr

  Variable type

• intervalRat : Lean.Expr

  Extracted interval (lo, hi rationals and their expressions)

• loExpr : Lean.Expr

  Original lower bound expression for Set.Icc

• hiExpr : Lean.Expr

  Original upper bound expression for Set.Icc

• lo : ℚ

  Low bound as rational

• hi : ℚ

  High bound as rational

@[instance_reducible]

instance LeanCert.Tactic.Auto.instReprVarIntervalInfo : Repr VarIntervalInfo

Equations

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

def LeanCert.Tactic.Auto.instReprVarIntervalInfo.repr : VarIntervalInfo → ℕ → Std.Format

Equations

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

@[instance_reducible]

instance LeanCert.Tactic.Auto.instInhabitedVarIntervalInfo : Inhabited VarIntervalInfo

Equations

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

inductive LeanCert.Tactic.Auto.MultivariateBoundGoal : Type

Result of analyzing a multivariate bound goal

• forallLe (vars : Array VarIntervalInfo) (func bound : Lean.Expr) : MultivariateBoundGoal

  ∀ x₁ ∈ I₁, ..., ∀ xₙ ∈ Iₙ, f(x₁,...,xₙ) ≤ c

• forallGe (vars : Array VarIntervalInfo) (func bound : Lean.Expr) : MultivariateBoundGoal

  ∀ x₁ ∈ I₁, ..., ∀ xₙ ∈ Iₙ, c ≤ f(x₁,...,xₙ)

def LeanCert.Tactic.Auto.instReprMultivariateBoundGoal.repr : MultivariateBoundGoal → ℕ → Std.Format

Equations

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

@[instance_reducible]

instance LeanCert.Tactic.Auto.instReprMultivariateBoundGoal : Repr MultivariateBoundGoal

Equations

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

inductive LeanCert.Tactic.Auto.GlobalBoundGoal : Type

Result of analyzing a global bound goal

• globalGe (box expr bound : Lean.Expr) : GlobalBoundGoal

  ∀ ρ ∈ B, (zero extension) → c ≤ f(ρ)

• globalLe (box expr bound : Lean.Expr) : GlobalBoundGoal

  ∀ ρ ∈ B, (zero extension) → f(ρ) ≤ c

def LeanCert.Tactic.Auto.instReprGlobalBoundGoal.repr : GlobalBoundGoal → ℕ → Std.Format

Equations

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

@[instance_reducible]

instance LeanCert.Tactic.Auto.instReprGlobalBoundGoal : Repr GlobalBoundGoal

Equations

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

inductive LeanCert.Tactic.Auto.RootGoal : Type

Result of analyzing a root finding goal

• forallNeZero (varName : Lean.Name) (interval func : Lean.Expr) : RootGoal

  ∀ x ∈ I, f x ≠ 0

@[instance_reducible]

instance LeanCert.Tactic.Auto.instReprRootGoal : Repr RootGoal

Equations

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

def LeanCert.Tactic.Auto.instReprRootGoal.repr : RootGoal → ℕ → Std.Format

Equations

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