Simproc and Discharger DSLs for Sym.simp

Simproc DSL (sym_simproc)

A syntax category for specifying pre and post simproc chains in Sym.simp variants.

Primitives

• ground — evaluates ground (fully concrete) terms
• telescope — simplifies telescope binders (have-values, arrow hypotheses) but not the final body
• rewrite setName [with discharger] — rewrites using a named theorem set
• rewrite [thm₁, thm₂, ...] [with discharger] — rewrites using inline theorems
• arith [with discharger] — polynomial normal form for ring, semiring, and field terms
• self — recursive simplification (calls the full simplifier)
• none — identity (no simplification)

Combinators

• a >> b — apply a, then apply b to the result (andThen)
• a <|> b — try a, if no progress try b (orElse)

Discharger DSL (sym_discharger)

A syntax category for specifying dischargers used in the with clause of rewrite. Dischargers attempt to prove side conditions of conditional rewrite rules.

Primitives

• self — recursive simplifier discharge (dischargeSimpSelf)
• none — no discharge, only unconditional rewrites apply (dischargeNone)
• grind — discharge using grind (Grind.Goal.mkSymSimpDischarger)

def Lean.Parser.Category.sym_simproc : Category

def Lean.Parser.Sym.Simp.sym_simproc.quot : ParserDescr

def Lean.Parser.Category.sym_discharger : Category

def Lean.Parser.Sym.Simp.sym_discharger.quot : ParserDescr

def Lean.Parser.Sym.Simp.ground : ParserDescr

Evaluate ground (fully concrete) terms.

def Lean.Parser.Sym.Simp.telescope : ParserDescr

Simplify telescope binders but not the final body.

def Lean.Parser.Sym.Simp.control : ParserDescr

Simplify control-flow expressions (if-then-else, match, cond, dite). Visits only conditions and discriminants. Intended as a pre simproc.

def Lean.Parser.Sym.Simp.arrowTelescope : ParserDescr

Simplify arrow telescopes (p₁ → p₂ → ... → q) without entering binders. Simplifies each pᵢ and q individually. Intended as a pre simproc.

def Lean.Parser.Sym.Simp.rewriteSet : ParserDescr

Rewrite using a named theorem set. Optionally specify a discharger for conditional rewrites.

def Lean.Parser.Sym.Simp.rewriteInline : ParserDescr

Rewrite using inline theorems. Optionally specify a discharger for conditional rewrites.

def Lean.Parser.Sym.Simp.arith : ParserDescr

Normalize ring and semiring terms into polynomial normal form (Sym.Arith.normalize?). Simplifies the atoms recursively. Intended as a pre simproc. The optional discharger proves the side conditions x ≠ 0 under which x * x⁻¹ is cancelled in a field.

def Lean.Parser.Sym.Simp.self : ParserDescr

Recursive simplification (calls the full simplifier).

def Lean.Parser.Sym.Simp.none : ParserDescr

Identity simproc (no simplification).

def Lean.Parser.Sym.Simp.andThen : TrailingParserDescr

Apply a, then apply b to the result.

def Lean.Parser.Sym.Simp.orElse : TrailingParserDescr

Try a, if no progress try b.

def Lean.Parser.Sym.Simp.simprocParen : ParserDescr

Parenthesized simproc expression.

def Lean.Parser.Sym.Simp.dischSelf : ParserDescr

Recursive simplifier discharge. Calls the full simplifier to prove side conditions.

def Lean.Parser.Sym.Simp.dischNone : ParserDescr

No discharge. Only unconditional rewrites will apply.

def Lean.Parser.Sym.Simp.dischParen : ParserDescr

Parenthesized discharger expression.

def Lean.Parser.Sym.Simp.dischGrind : ParserDescr

Calls grind to prove side conditions. The goal's internalized hypotheses (hypotheses are internalized when the sym => block starts and by tactics such as intro and internalize) are shared across discharge attempts; the remaining local declarations (e.g., introduced by Sym.simp when entering binders) are internalized on each attempt.

register_sym_simp command

Declares a named Sym.simp variant with pre/post simproc chains, the discharger for the extra theorems provided at use time (simp myVariant [thm₁, thm₂, ...]), and optional config overrides.

register_sym_simp myVariant where
  pre  := telescope
  post := ground >> rewrite mySet with self
  discharger := grind

def Lean.Parser.Category.sym_simp_field : Category

def Lean.Parser.Command.sym_simp_field.quot : ParserDescr

def Lean.Parser.Command.symSimpFieldPre : ParserDescr

Pre-processing simproc chain.

def Lean.Parser.Command.symSimpFieldPost : ParserDescr

Post-processing simproc chain.

def Lean.Parser.Command.symSimpFieldDischarger : ParserDescr

Discharger for the side conditions of the extra theorems provided at use time (simp myVariant [thm₁, thm₂, ...]). Defaults to none.

def Lean.Parser.Command.symSimpFieldMaxSteps : ParserDescr

Maximum number of simplification steps.

def Lean.Parser.Command.symSimpFieldMaxDischargeDepth : ParserDescr

Maximum depth of recursive discharge attempts.

def Lean.Parser.Command.registerSymSimp : ParserDescr

Register a named Sym.simp variant.

register_sym_simp myVariant where
  pre  := telescope
  post := ground >> rewrite [thm1, thm2] with self
  discharger := grind
  maxSteps := 50000