Discovery Mode: Tactics

This module provides tactics for automatically proving existential goals using discovery algorithms:

• interval_minimize - Prove ∃ m, ∀ x ∈ I, f(x) ≥ m by finding the minimum
• interval_maximize - Prove ∃ M, ∀ x ∈ I, f(x) ≤ M by finding the maximum
• interval_roots - Prove ∃ x ∈ I, f(x) = 0 by finding roots (Stub)

Usage

-- Automatically find and prove a lower bound exists
example : ∃ m : ℚ, ∀ x ∈ I01, x^2 + Real.sin x ≥ m := by
  interval_minimize

-- Find a root (Not fully implemented yet)
example : ∃ x ∈ Icc (-2 : ℝ) 2, x^3 - x = 0 := by
  interval_roots

Implementation

The tactics:

1. Analyze the goal to find the function f and interval I.
2. Reify f to a LeanCert AST.
3. Execute the optimization algorithm (via evalExpr) to find the bound m.
4. Instantiate the existential ∃ m with the found value.
5. Call opt_bound to prove the resulting universal bound.

@[reducible, inline]

abbrev LeanCert.Tactic.Discovery.LExpr : Type

Equations

• LeanCert.Tactic.Discovery.LExpr = LeanCert.Core.Expr

Helper Functions

unsafe def LeanCert.Tactic.Discovery.parseDomainToBox (domainExpr : Lean.Expr) : Lean.MetaM Engine.Optimization.Box

Parse a domain expression into a Box

Equations

• LeanCert.Tactic.Discovery.parseDomainToBox domainExpr = do let e ← Lean.Meta.evalExpr LeanCert.Core.IntervalRat (Lean.mkConst `LeanCert.Core.IntervalRat) domainExpr pure [e]

inductive LeanCert.Tactic.Discovery.ExistentialBoundGoal : Type

Check if the goal is an existential bound: ∃ m, ∀ x ∈ I, f(x) ≥ m or ≤ m

• minimize (varName : Lean.Name) (varType domain func : Lean.Expr) : ExistentialBoundGoal
• maximize (varName : Lean.Name) (varType domain func : Lean.Expr) : ExistentialBoundGoal

def LeanCert.Tactic.Discovery.parseExistentialGoal (goalType : Lean.Expr) : Lean.MetaM (Option ExistentialBoundGoal)

Parse an existential bound goal. Supports goals of the form:

• ∃ m, ∀ x ∈ I, f(x) ≥ m (minimize)
• ∃ M, ∀ x ∈ I, f(x) ≤ M (maximize)

The function f can be:

• A raw Lean expression like x * x + Real.sin x
• An Expr.eval wrapped expression

Auto-reification will convert raw expressions to LeanCert AST.

Equations

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

Helper Functions

def LeanCert.Tactic.Discovery.getAstFromFunc (func : Lean.Expr) : Lean.Elab.Tactic.TacticM Lean.Expr

Try to extract AST from an Expr.eval application, or reify if it's a raw expression. This enables automatic reification - users can write standard math like x * x + sin x without needing to wrap in Expr.eval.

Equations

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

Domain normalization helpers

partial def LeanCert.Tactic.Discovery.extractRatFromReal (e : Lean.Expr) : Lean.MetaM (Option ℚ)

Try to extract a rational value from a Lean expression that represents a real number. Handles: Rat.cast, OfNat.ofNat, Nat.cast, Int.cast, negations, and divisions. Also handles direct ℚ expressions as a fallback.

partial def LeanCert.Tactic.Discovery.extractRatFromReal.tryExtract (e : Lean.Expr) : Lean.MetaM (Option ℚ)

Minimization Tactic

unsafe def LeanCert.Tactic.Discovery.intervalMinimizeCore (taylorDepth : ℕ) : Lean.Elab.Tactic.TacticM Unit

The interval_minimize tactic implementation

Equations

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

def LeanCert.Tactic.Discovery.intervalMinimizeTac : Lean.ParserDescr

The interval_minimize tactic.

Proves goals of the form ∃ m, ∀ x ∈ I, f(x) ≥ m by:

1. Running global optimization to find the minimum m.
2. Instantiating the existential with m.
3. Proving the bound using opt_bound.

Equations

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

unsafe def LeanCert.Tactic.Discovery.elabIntervalMinimize : Lean.Elab.Tactic.Tactic

Equations

• LeanCert.Tactic.Discovery.elabIntervalMinimize stx = LeanCert.Tactic.Discovery.intervalMinimizeCore (match stx[1].getOptional? with | some n => n.toNat | none => 10)

Maximization Tactic

unsafe def LeanCert.Tactic.Discovery.intervalMaximizeCore (taylorDepth : ℕ) : Lean.Elab.Tactic.TacticM Unit

The interval_maximize tactic implementation

Equations

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

def LeanCert.Tactic.Discovery.intervalMaximizeTac : Lean.ParserDescr

The interval_maximize tactic.

Proves goals of the form ∃ M, ∀ x ∈ I, f(x) ≤ M.

Equations

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

unsafe def LeanCert.Tactic.Discovery.elabIntervalMaximize : Lean.Elab.Tactic.Tactic

Equations

• LeanCert.Tactic.Discovery.elabIntervalMaximize stx = LeanCert.Tactic.Discovery.intervalMaximizeCore (match stx[1].getOptional? with | some n => n.toNat | none => 10)

Argmax/Argmin Tactics

inductive LeanCert.Tactic.Discovery.ArgmaxGoal : Type

Result of analyzing an argmax goal

• argmax (varName : Lean.Name) (domain func : Lean.Expr) : ArgmaxGoal

  ∃ x ∈ I, ∀ y ∈ I, f(y) ≤ f(x)

instance LeanCert.Tactic.Discovery.instReprArgmaxGoal : Repr ArgmaxGoal

Equations

• LeanCert.Tactic.Discovery.instReprArgmaxGoal = { reprPrec := LeanCert.Tactic.Discovery.instReprArgmaxGoal.repr }

def LeanCert.Tactic.Discovery.instReprArgmaxGoal.repr : ArgmaxGoal → ℕ → Std.Format

Equations

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

def LeanCert.Tactic.Discovery.parseArgmaxGoal (goal : Lean.Expr) : Lean.MetaM (Option ArgmaxGoal)

Try to parse a goal as an argmax goal: ∃ x ∈ I, ∀ y ∈ I, f(y) ≤ f(x)

Equations

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

def LeanCert.Tactic.Discovery.parseArgmaxGoal.extractIntervalExpr (memExpr x : Lean.Expr) : Lean.MetaM (Option Lean.Expr)

Extract the interval from a membership expression x ∈ I

Equations

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

inductive LeanCert.Tactic.Discovery.ArgminGoal : Type

Result of analyzing an argmin goal

• argmin (varName : Lean.Name) (domain func : Lean.Expr) : ArgminGoal

  ∃ x ∈ I, ∀ y ∈ I, f(x) ≤ f(y)

def LeanCert.Tactic.Discovery.instReprArgminGoal.repr : ArgminGoal → ℕ → Std.Format

Equations

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

instance LeanCert.Tactic.Discovery.instReprArgminGoal : Repr ArgminGoal

Equations

• LeanCert.Tactic.Discovery.instReprArgminGoal = { reprPrec := LeanCert.Tactic.Discovery.instReprArgminGoal.repr }

def LeanCert.Tactic.Discovery.parseArgminGoal (goal : Lean.Expr) : Lean.MetaM (Option ArgminGoal)

Try to parse a goal as an argmin goal: ∃ x ∈ I, ∀ y ∈ I, f(x) ≤ f(y)

Equations

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

def LeanCert.Tactic.Discovery.parseArgminGoal.extractIntervalExpr (memExpr x : Lean.Expr) : Lean.MetaM (Option Lean.Expr)

Extract the interval from a membership expression x ∈ I

Equations

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

def LeanCert.Tactic.Discovery.isExprEvalFunc (func : Lean.Expr) : Lean.MetaM Bool

Check if a function expression is wrapped in Expr.eval

Equations

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

unsafe def LeanCert.Tactic.Discovery.intervalArgmaxCore (taylorDepth : ℕ) : Lean.Elab.Tactic.TacticM Unit

The interval_argmax tactic implementation

Equations

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

def LeanCert.Tactic.Discovery.intervalArgmaxTac : Lean.ParserDescr

The interval_argmax tactic.

Proves goals of the form ∃ x ∈ I, ∀ y ∈ I, f(y) ≤ f(x) by:

1. Running global optimization to find the point x where f is maximized.
2. Instantiating the existential with x.
3. Proving membership x ∈ I.
4. Proving the universal bound using interval arithmetic.

Equations

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

unsafe def LeanCert.Tactic.Discovery.elabIntervalArgmax : Lean.Elab.Tactic.Tactic

Equations

• LeanCert.Tactic.Discovery.elabIntervalArgmax stx = LeanCert.Tactic.Discovery.intervalArgmaxCore (match stx[1].getOptional? with | some n => n.toNat | none => 10)

unsafe def LeanCert.Tactic.Discovery.intervalArgminCore (taylorDepth : ℕ) : Lean.Elab.Tactic.TacticM Unit

The interval_argmin tactic implementation

Equations

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

def LeanCert.Tactic.Discovery.intervalArgminTac : Lean.ParserDescr

The interval_argmin tactic.

Proves goals of the form ∃ x ∈ I, ∀ y ∈ I, f(x) ≤ f(y) by:

1. Running global optimization to find the point x where f is minimized.
2. Instantiating the existential with x.
3. Proving membership x ∈ I.
4. Proving the universal bound using interval arithmetic.

Equations

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

unsafe def LeanCert.Tactic.Discovery.elabIntervalArgmin : Lean.Elab.Tactic.Tactic

Equations

• LeanCert.Tactic.Discovery.elabIntervalArgmin stx = LeanCert.Tactic.Discovery.intervalArgminCore (match stx[1].getOptional? with | some n => n.toNat | none => 10)

Multivariate Minimization/Maximization Tactics

inductive LeanCert.Tactic.Discovery.MultivariateExistentialGoal : Type

Result of analyzing a multivariate existential bound goal

• minimize (varType : Lean.Expr) (vars : Array Auto.VarIntervalInfo) (func : Lean.Expr) : MultivariateExistentialGoal

  ∃ m, ∀ x ∈ I, ∀ y ∈ J, ..., f(...) ≥ m (minimize)

• maximize (varType : Lean.Expr) (vars : Array Auto.VarIntervalInfo) (func : Lean.Expr) : MultivariateExistentialGoal

  ∃ M, ∀ x ∈ I, ∀ y ∈ J, ..., f(...) ≤ M (maximize)

def LeanCert.Tactic.Discovery.parseMultivariateExistentialGoal (goalType : Lean.Expr) : Lean.MetaM (Option MultivariateExistentialGoal)

Parse a multivariate existential bound goal. Supports goals of the form:

• ∃ m, ∀ x ∈ I, ∀ y ∈ J, f(x,y) ≥ m (minimize)
• ∃ M, ∀ x ∈ I, ∀ y ∈ J, f(x,y) ≤ M (maximize)

Equations

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

unsafe def LeanCert.Tactic.Discovery.intervalMinimizeMvCore (taylorDepth : ℕ) : Lean.Elab.Tactic.TacticM Unit

The interval_minimize_mv tactic implementation for multivariate goals

Equations

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

def LeanCert.Tactic.Discovery.intervalMinimizeMvTac : Lean.ParserDescr

The interval_minimize_mv tactic.

Proves multivariate goals of the form ∃ m, ∀ x ∈ I, ∀ y ∈ J, f(x,y) ≥ m by:

1. Running global optimization over the n-dimensional domain.
2. Instantiating the existential with the found minimum.
3. Proving the bound using interval_bound.

Equations

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

unsafe def LeanCert.Tactic.Discovery.elabIntervalMinimizeMv : Lean.Elab.Tactic.Tactic

Equations

• LeanCert.Tactic.Discovery.elabIntervalMinimizeMv stx = LeanCert.Tactic.Discovery.intervalMinimizeMvCore (match stx[1].getOptional? with | some n => n.toNat | none => 10)

unsafe def LeanCert.Tactic.Discovery.intervalMaximizeMvCore (taylorDepth : ℕ) : Lean.Elab.Tactic.TacticM Unit

The interval_maximize_mv tactic implementation for multivariate goals

Equations

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

def LeanCert.Tactic.Discovery.intervalMaximizeMvTac : Lean.ParserDescr

The interval_maximize_mv tactic.

Proves multivariate goals of the form ∃ M, ∀ x ∈ I, ∀ y ∈ J, f(x,y) ≤ M by:

1. Running global optimization over the n-dimensional domain.
2. Instantiating the existential with the found maximum.
3. Proving the bound using interval_bound.

Equations

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

unsafe def LeanCert.Tactic.Discovery.elabIntervalMaximizeMv : Lean.Elab.Tactic.Tactic

Equations

• LeanCert.Tactic.Discovery.elabIntervalMaximizeMv stx = LeanCert.Tactic.Discovery.intervalMaximizeMvCore (match stx[1].getOptional? with | some n => n.toNat | none => 10)

Roots Tactic

inductive LeanCert.Tactic.Discovery.RootExistsGoal : Type

Result of analyzing a root existence goal

• existsRoot (varName : Lean.Name) (interval func : Lean.Expr) : RootExistsGoal

  ∃ x ∈ I, f x = 0

instance LeanCert.Tactic.Discovery.instReprRootExistsGoal : Repr RootExistsGoal

Equations

• LeanCert.Tactic.Discovery.instReprRootExistsGoal = { reprPrec := LeanCert.Tactic.Discovery.instReprRootExistsGoal.repr }

def LeanCert.Tactic.Discovery.instReprRootExistsGoal.repr : RootExistsGoal → ℕ → Std.Format

Equations

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

def LeanCert.Tactic.Discovery.parseRootExistsGoal (goal : Lean.Expr) : Lean.MetaM (Option RootExistsGoal)

Try to parse a goal as a root existence goal: ∃ x ∈ I, f(x) = 0

Equations

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

def LeanCert.Tactic.Discovery.parseRootExistsGoal.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.Discovery.parseRootExistsGoal.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.Discovery.parseRootExistsGoal.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.Discovery.parseRootExistsGoal.extractBoundsFromAnd (memExpr 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.Discovery.parseRootExistsGoal.mkSetIccFromBounds (loExpr hiExpr : Lean.Expr) : Lean.MetaM Lean.Expr

Equations

• LeanCert.Tactic.Discovery.parseRootExistsGoal.mkSetIccFromBounds loExpr hiExpr = Lean.Meta.mkAppM `Set.Icc #[loExpr, hiExpr]

def LeanCert.Tactic.Discovery.parseRootExistsGoal.extractInterval (memExpr x : Lean.Expr) : Lean.MetaM (Option Lean.Expr)

Extract the interval from a membership expression x ∈ I

Equations

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

def LeanCert.Tactic.Discovery.parseRootExistsGoal.extractFuncFromEqZero (eqExpr x : Lean.Expr) : Lean.MetaM (Option Lean.Expr)

Extract function from f(x) = 0

Equations

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

def LeanCert.Tactic.Discovery.intervalRootsCore (taylorDepth : ℕ) : Lean.Elab.Tactic.TacticM Unit

The interval_roots tactic implementation

Equations

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

def LeanCert.Tactic.Discovery.tacticInterval_roots_ : Lean.ParserDescr

The interval_roots tactic.

Proves goals of the form ∃ x ∈ I, f(x) = 0 by:

1. Checking for a sign change at the interval endpoints using interval arithmetic
2. Applying the Intermediate Value Theorem

The tactic automatically:

• Reifies the function to a LeanCert AST
• Generates an ExprSupportedCore proof
• Generates a ContinuousOn proof (automatic for supported expressions)
• Verifies the sign change certificate using native_decide

Usage:

example : ∃ x ∈ Icc (0 : ℝ) 2, x^2 - 2 = 0 := by
  interval_roots

Limitations:

• Only works for expressions in ExprSupportedCore (no log, inv)
• Requires a sign change at the endpoints (IVT condition)
• If there's no sign change, the tactic will fail

Equations

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

Unique Root Tactic

def LeanCert.Tactic.Discovery.parseUniqueRootGoal (goalType : Lean.Expr) : Lean.MetaM (Option (Lean.Name × Lean.Expr × Lean.Expr))

Parse a unique root goal: ∃! x, x ∈ I ∧ f(x) = 0

Equations

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

unsafe def LeanCert.Tactic.Discovery.intervalUniqueRootCore (taylorDepth : ℕ) : Lean.Elab.Tactic.TacticM Unit

Core implementation for interval_unique_root tactic.

Proves ∃! x ∈ I, f(x) = 0 by:

1. Checking Newton contraction (derivative bounded away from 0)
2. Applying verify_unique_root_computable theorem

Uses the fully computable verify_unique_root_computable theorem which only requires checkNewtonContractsCore. This allows native_decide to work without noncomputable Real functions.

Equations

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

def LeanCert.Tactic.Discovery.intervalUniqueRootTac : Lean.ParserDescr

The interval_unique_root tactic.

Proves goals of the form ∃! x ∈ I, f(x) = 0 by:

1. Using Newton contraction to verify uniqueness (derivative bounded away from 0)
2. Applying the Intermediate Value Theorem for existence

Usage:

example : ∃! x ∈ I_1_2, Expr.eval (fun _ => x) (x² - 2) = 0 := by
  interval_unique_root

Requirements:

• Function must be in ExprSupported (const, var, add, mul, neg, sin, cos, exp only)
• Newton step must contract (derivative doesn't contain 0)

Equations

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

unsafe def LeanCert.Tactic.Discovery.elabIntervalUniqueRoot : Lean.Elab.Tactic.Tactic

Equations

• LeanCert.Tactic.Discovery.elabIntervalUniqueRoot stx = LeanCert.Tactic.Discovery.intervalUniqueRootCore (match stx[1].getOptional? with | some n => n.toNat | none => 10)

Integration Tactic

def LeanCert.Tactic.Discovery.parseIntegrationGoal (goalType : Lean.Expr) : Lean.MetaM (Option (Lean.Expr × Lean.Expr × Lean.Expr × Lean.Expr))

Extract components from integration goal: ∫ x in lo..hi, f(x) ∈ bound returns (lo, hi, integral, bound)

Equations

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

unsafe def LeanCert.Tactic.Discovery.intervalIntegrateCore (_taylorDepth : ℕ) : Lean.Elab.Tactic.TacticM Unit

Core implementation for interval_integrate tactic.

Proves goals of the form ∫ x in (I.lo)...(I.hi), f(x) ∈ bound by:

1. Computing the integral bound using interval arithmetic
2. Proving the computed bound contains the integral

The goal must be exactly of the form: ∫ x in (I.lo:ℝ)..(I.hi:ℝ), Expr.eval (fun _ => x) e ∈ integrateInterval1Core e I cfg

Equations

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

def LeanCert.Tactic.Discovery.intervalIntegrateTac : Lean.ParserDescr

The interval_integrate tactic.

Proves goals of the form ∫ x in (I.lo)...(I.hi), f(x) ∈ bound by:

1. Computing the integral bound using interval arithmetic
2. Applying the integrateInterval1Core_correct theorem

Usage:

example : ∫ x in (0:ℝ)..1, x ∈ Validity.Integration.integrateInterval1Core (Expr.var 0) ⟨0, 1, by norm_num⟩ default := by
  interval_integrate

Limitations:

• The bound must exactly match integrateInterval1Core e I cfg
• The function must be in ExprSupportedCore (no log, inv)

Equations

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

unsafe def LeanCert.Tactic.Discovery.elabIntervalIntegrate : Lean.Elab.Tactic.Tactic

Equations

• LeanCert.Tactic.Discovery.elabIntervalIntegrate stx = LeanCert.Tactic.Discovery.intervalIntegrateCore (match stx[1].getOptional? with | some n => n.toNat | none => 10)

Discover Tactic

def LeanCert.Tactic.Discovery.discoverTac : Lean.ParserDescr

The discover tactic - generic discovery.

Analyzes the goal and applies the appropriate discovery tactic.

Equations

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

unsafe def LeanCert.Tactic.Discovery.elabDiscover : Lean.Elab.Tactic.Tactic

Equations

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

Exploration Command

def LeanCert.Tactic.Discovery.signedInt.quot : Lean.ParserDescr

Equations

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

def Lean.Parser.Category.signedInt : Category

Syntax for signed integer: either a nat or -nat

Equations

• Lean.Parser.Category.signedInt = { }

def LeanCert.Tactic.Discovery.signedInt_ : Lean.ParserDescr

Equations

• LeanCert.Tactic.Discovery.signedInt_ = Lean.ParserDescr.node `LeanCert.Tactic.Discovery.signedInt_ 1022 (Lean.ParserDescr.const `num)

def LeanCert.Tactic.Discovery.«signedInt-_» : Lean.ParserDescr

Equations

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

def LeanCert.Tactic.Discovery.parseSignedInt : Lean.Syntax → ℤ

Parse a signedInt syntax to Int

Equations

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

def LeanCert.Tactic.Discovery.«command#explore_On[_,_]» : Lean.ParserDescr

The #explore command analyzes a function on an interval.

Usage:

#explore (Expr.sin (Expr.var 0)) on [0, 7]
#explore (Expr.cos (Expr.var 0)) on [-1, 2]

Output includes:

• Range bounds
• Global minimum/maximum
• Root detection (sign changes)

Note: Bounds must be integer literals (positive or negative).

Equations

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