Discovery Mode: Elaboration Commands

This module provides interactive commands for exploring mathematical functions:

• #find_min - Find the global minimum of an expression on a domain
• #find_max - Find the global maximum of an expression on a domain
• #bounds - Find both min and max bounds
• #eval_interval - Quick interval evaluation

Usage Examples

-- Find minimum of x² + sin(x) on [-2, 2]
#find_min (fun x => x^2 + Real.sin x) on [-2, 2]

-- Find maximum with higher precision
#find_max (fun x => Real.exp x - x^2) on [0, 1] precision 20

-- Find bounds for a 2D function
#bounds (fun x y => x*y + x^2) on [-1, 1] × [-1, 1]

Note: #minimize and #maximize are aliases for backward compatibility.

Implementation

The commands work by:

1. Elaborating the user's expression
2. Reifying it to a LeanCert.Core.Expr AST
3. Running the optimization algorithm
4. Pretty-printing the result

@[reducible, inline]

abbrev LeanCert.Discovery.Commands.LExpr : Type

Equations

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

Interval Parsing Helpers

unsafe def LeanCert.Discovery.Commands.parseRatUnsafe (e : Lean.Expr) : Lean.MetaM ℚ

Parse a rational number from a Lean expression using native evaluation

Equations

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

@[implemented_by LeanCert.Discovery.Commands.parseRatUnsafe]

partial def LeanCert.Discovery.Commands.parseRat (e : Lean.Expr) : Lean.MetaM ℚ

Safe wrapper for parseRatUnsafe

partial def LeanCert.Discovery.Commands.parseIntFromExpr (e : Lean.Expr) : Lean.MetaM ℤ

Parse an integer from a reduced Lean expression

partial def LeanCert.Discovery.Commands.parseIntFromSyntax (stx : Lean.Syntax) : Lean.Elab.TermElabM ℤ

Parse an integer directly from term syntax

def LeanCert.Discovery.Commands.parseInterval (stx : Lean.Syntax) : Lean.Elab.TermElabM Core.IntervalRat

Parse an interval from syntax like [a, b]

Equations

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

partial def LeanCert.Discovery.Commands.parseBox (stx : Lean.Syntax) : Lean.Elab.TermElabM Engine.Optimization.Box

Parse a box (product of intervals)

Result Formatting

def LeanCert.Discovery.Commands.formatRat (q : ℚ) (_precision : ℕ := 6) : String

Format a rational for display as a decimal string

Equations

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

def LeanCert.Discovery.Commands.formatInterval (I : Core.IntervalRat) : String

Format an interval for display

Equations

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

#find_min Command

def LeanCert.Discovery.Commands.findMinCmd : Lean.ParserDescr

Syntax for #find_min command

Equations

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

unsafe def LeanCert.Discovery.Commands.elabFindMin : Lean.Elab.Command.CommandElab

Elaborator for #find_min

Equations

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

def LeanCert.Discovery.Commands.minimizeCmd : Lean.ParserDescr

Backward-compatible alias for #find_min

Equations

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

#find_max Command

def LeanCert.Discovery.Commands.findMaxCmd : Lean.ParserDescr

Syntax for #find_max command

Equations

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

unsafe def LeanCert.Discovery.Commands.elabFindMax : Lean.Elab.Command.CommandElab

Elaborator for #find_max

Equations

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

def LeanCert.Discovery.Commands.maximizeCmd : Lean.ParserDescr

Backward-compatible alias for #find_max

Equations

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

#bounds Command

def LeanCert.Discovery.Commands.boundsCmd : Lean.ParserDescr

Syntax for #bounds command

Equations

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

unsafe def LeanCert.Discovery.Commands.elabBounds : Lean.Elab.Command.CommandElab

Elaborator for #bounds

Equations

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

#eval_interval Command

def LeanCert.Discovery.Commands.evalIntervalCmd : Lean.ParserDescr

Syntax for quick interval evaluation

Equations

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

unsafe def LeanCert.Discovery.Commands.elabEvalInterval : Lean.Elab.Command.CommandElab

Elaborator for #eval_interval

Equations

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