Goal Parsing for Interval Tactics

This module provides utilities for parsing goal structure to determine which theorem to apply. Handles:

• Univariate bound goals
• Multivariate bound goals
• Root finding goals
• Point inequalities

Univariate Goal Parsing

def LeanCert.Tactic.Auto.parseBoundGoal (goal : Lean.Expr) : Lean.MetaM (Option BoundGoal)

Try to parse a goal as a bound goal

Equations

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

def LeanCert.Tactic.Auto.parseBoundGoal.findSome (cands : List Lean.Expr) (f : Lean.Expr → Lean.MetaM (Option BoundGoal)) : Lean.MetaM (Option BoundGoal)

Equations

• One or more equations did not get rendered due to their size.
• LeanCert.Tactic.Auto.parseBoundGoal.findSome [] f = pure none

def LeanCert.Tactic.Auto.parseBoundGoal.getLeArgs (e : Lean.Expr) : Lean.MetaM (Option (Lean.Expr × Lean.Expr))

Extract (lhs, rhs) from an LE.le application.

Equations

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

def LeanCert.Tactic.Auto.parseBoundGoal.extractLowerBound (e x : Lean.Expr) : Lean.MetaM (Option Lean.Expr)

Extract lower bound lo from lo ≤ x.

Equations

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

def LeanCert.Tactic.Auto.parseBoundGoal.extractUpperBound (e x : Lean.Expr) : Lean.MetaM (Option Lean.Expr)

Extract upper bound hi from x ≤ hi.

Equations

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

def LeanCert.Tactic.Auto.parseBoundGoal.extractBoundsFromAnd (memTy x : Lean.Expr) : Lean.MetaM (Option (Lean.Expr × Lean.Expr))

Extract bounds from conjunction form lo ≤ x ∧ x ≤ hi.

Equations

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

def LeanCert.Tactic.Auto.parseBoundGoal.mkIntervalInfoFromBounds (loExpr hiExpr : Lean.Expr) : Lean.MetaM (Option IntervalInfo)

Build IntervalInfo from explicit lo/hi bounds.

Equations

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

def LeanCert.Tactic.Auto.parseBoundGoal.extractInterval (memTy x : Lean.Expr) : Lean.MetaM (Option IntervalInfo)

Extract the interval from a membership expression

Equations

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

def LeanCert.Tactic.Auto.parseBoundGoal.tryConvertSetIcc (interval : Lean.Expr) : Lean.MetaM (Option IntervalInfo)

Try to convert a Set.Icc expression to an IntervalRat with full info

Equations

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

Multivariate Goal Parsing

def LeanCert.Tactic.Auto.parseMultivariateBoundGoal (goal : Lean.Expr) : Lean.MetaM (Option MultivariateBoundGoal)

Recursively parse a multivariate bound goal, collecting variables and intervals. This processes all quantifiers within nested withLocalDeclD scopes so that fvars remain valid for mkLambdaFVars.

Equations

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

partial def LeanCert.Tactic.Auto.parseMultivariateBoundGoal.findSome (cands : List Lean.Expr) (f : Lean.Expr → Lean.MetaM (Option MultivariateBoundGoal)) : Lean.MetaM (Option MultivariateBoundGoal)

partial def LeanCert.Tactic.Auto.parseMultivariateBoundGoal.collect (extractLowerBound extractUpperBound : Lean.Expr → Lean.Expr → Lean.MetaM (Option Lean.Expr)) (extractBoundsFromAnd : Lean.Expr → Lean.Expr → Lean.MetaM (Option (Lean.Expr × Lean.Expr))) (mkVarIntervalInfoFromBounds : Lean.Expr → Lean.Expr → Lean.Expr → Lean.MetaM (Option VarIntervalInfo)) (memCandidates : Lean.Expr → Lean.MetaM (Array Lean.Expr)) (e : Lean.Expr) (acc : Array VarIntervalInfo) (fvars : Array Lean.Expr) : Lean.MetaM (Option MultivariateBoundGoal)

Point Inequality Parsing

def LeanCert.Tactic.Auto.parsePointIneq (goal : Lean.Expr) : Lean.MetaM (Option (Lean.Expr × Lean.Expr × Bool × Bool))

Parse a point inequality goal and extract lhs, rhs, and inequality type. Returns (lhs, rhs, isStrict, isReversed) where:

• isStrict: true for < or >, false for ≤ or ≥
• isReversed: true for ≥ or > (need to flip the comparison)

Equations

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

partial def LeanCert.Tactic.Auto.collectConstants (e : Lean.Expr) : Lean.MetaM (List ℚ)

Try to collect all constant rational values from an expression. Returns the list of rational constants found (for building the singleton interval).

Root Finding Goal Parsing

def LeanCert.Tactic.Auto.parseRootGoal (goal : Lean.Expr) : Lean.MetaM (Option RootGoal)

Try to parse a goal as a root finding goal

Equations

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

def LeanCert.Tactic.Auto.parseRootGoal.getLeArgs (e : Lean.Expr) : Lean.MetaM (Option (Lean.Expr × Lean.Expr))

Equations

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

def LeanCert.Tactic.Auto.parseRootGoal.extractLowerBound (e x : Lean.Expr) : Lean.MetaM (Option Lean.Expr)

Equations

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

def LeanCert.Tactic.Auto.parseRootGoal.extractUpperBound (e x : Lean.Expr) : Lean.MetaM (Option Lean.Expr)

Equations

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

def LeanCert.Tactic.Auto.parseRootGoal.extractBoundsFromAnd (memTy x : Lean.Expr) : Lean.MetaM (Option (Lean.Expr × Lean.Expr))

Equations

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

def LeanCert.Tactic.Auto.parseRootGoal.mkIntervalRatFromBounds (loExpr hiExpr : Lean.Expr) : Lean.MetaM (Option Lean.Expr)

Equations

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

def LeanCert.Tactic.Auto.parseRootGoal.extractInterval (memTy x : Lean.Expr) : Lean.MetaM (Option Lean.Expr)

Extract the interval from a membership expression

Equations

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

Global Optimization Goal Parsing

def LeanCert.Tactic.Auto.isExprEval (e : Lean.Expr) : Bool

Check if expression is Expr.eval (checking both short and full names)

Equations

• LeanCert.Tactic.Auto.isExprEval e = (e.getAppFn.isConstOf `LeanCert.Core.Expr.eval || e.getAppFn.isConstOf `LeanCert.Core.Expr.eval)

def LeanCert.Tactic.Auto.isExprEvalName (name : Lean.Name) : Bool

Check if name ends with Expr.eval

Equations

• LeanCert.Tactic.Auto.isExprEvalName name = `Expr.eval.isSuffixOf name

def LeanCert.Tactic.Auto.parseSimpleBoundGoal (goal : Lean.Expr) : Lean.MetaM (Option GlobalBoundGoal)

Try to parse an already-intro'd goal as a global optimization bound. After intro ρ hρ hzero, the goal should be a comparison: Expr.eval ρ e ≤ c or c ≤ Expr.eval ρ e

Equations

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