Common Proving Utilities

Shared utilities for proving bounds across all interval tactics.

def LeanCert.Tactic.Auto.tryCloseWith (tacs : List (Lean.TSyntax `tactic)) : Lean.Elab.Tactic.TacticM Bool

Try to close a goal with a sequence of tactics

Equations

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

def LeanCert.Tactic.Auto.standardCloseTactics : Lean.Elab.Tactic.TacticM (List (Lean.TSyntax `tactic))

Standard tactics for closing side goals

Equations

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

def LeanCert.Tactic.Auto.tryCloseGoal : Lean.Elab.Tactic.TacticM Bool

Try to close the current goal using standard tactics

Equations

• LeanCert.Tactic.Auto.tryCloseGoal = do let tacs ← LeanCert.Tactic.Auto.standardCloseTactics LeanCert.Tactic.Auto.tryCloseWith tacs

def LeanCert.Tactic.Auto.tryCloseRpowSideGoal : Lean.Elab.Tactic.TacticM Bool

Try to close side goals generated by reifying x ^ q as exp (log x * q).

Equations

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

def LeanCert.Tactic.Auto.closeAllSideGoals (tacticName : String) : Lean.Elab.Tactic.TacticM Unit

Close all remaining side goals

Equations

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

def LeanCert.Tactic.Auto.extractRatBound (bound : Lean.Expr) : Lean.Elab.Tactic.TacticM Lean.Expr

Extract rational bound from possible coercion

Equations

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

def LeanCert.Tactic.Auto.getAstWithReport (func : Lean.Expr) : Lean.Elab.Tactic.TacticM Meta.ReifyReport

Extract an AST and retain the definitions unfolded while reifying it.

Equations

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

def LeanCert.Tactic.Auto.getSupportProof (ast : Lean.Expr) : Lean.Elab.Tactic.TacticM (Lean.Expr × Bool)

Get a core support proof when available. Checked evaluators need no support proof; their branch receives an unused placeholder.

Equations

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

def LeanCert.Tactic.Auto.mkBoxExpr (infos : Array VarIntervalInfo) : Lean.MetaM Lean.Expr

Build a Box expression (List IntervalRat) from an array of VarIntervalInfo

Equations

• LeanCert.Tactic.Auto.mkBoxExpr infos = Lean.Meta.mkListLit (Lean.mkConst `LeanCert.Core.IntervalRat) (Array.map (fun (x : LeanCert.Tactic.Auto.VarIntervalInfo) => x.intervalRat) infos).toList

def LeanCert.Tactic.Auto.certCheckSucceeds (checkFn : Lean.Expr) : Lean.Elab.Tactic.TacticM Bool

Check if a certificate check will succeed (without throwing)

Equations

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

def LeanCert.Tactic.Auto.getSubdivBounds (intervalInfo : IntervalInfo) : Lean.Elab.Tactic.TacticM (Option (ℚ × ℚ × Lean.Expr × Lean.Expr × Lean.Expr × Bool))

Extract bounds from IntervalInfo for subdivision

Equations

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

def LeanCert.Tactic.Auto.getLiteral? (e : Lean.Expr) : Lean.Elab.Tactic.TacticM (Option ℚ)

Extract a rational literal from an expression

Equations

• LeanCert.Tactic.Auto.getLiteral? e = liftM (LeanCert.Meta.Numeral.toRatFolded? e)