16.6. Configuring Simplification🔗

simp is primarily configured via a configuration parameter, passed as a named argument called config.

structure

Lean.Meta.Simp.Config : Type
Lean.Meta.Simp.Config : Type

The configuration for simp. Passed to simp using, for example, the simp (config := {contextual := true}) syntax.

Constructor

Lean.Meta.Simp.Config.mk

Fields

maxSteps : Nat

The maximum number of subexpressions to visit when performing simplification. The default is 100000.

maxDischargeDepth : Nat

When simp discharges side conditions for conditional lemmas, it can recursively apply simplification. The maxDischargeDepth (default: 2) is the maximum recursion depth when recursively applying simplification to side conditions.

contextual : Bool

When contextual is true (default: false) and simplification encounters an implication p → q it includes p as an additional simp lemma when simplifying q.

memoize : Bool

When true (default: true) then the simplifier caches the result of simplifying each subexpression, if possible.

singlePass : Bool

When singlePass is true (default: false), the simplifier runs through a single round of simplification, which consists of running pre-methods, recursing using congruence lemmas, and then running post-methods. Otherwise, when it is false, it iteratively applies this simplification procedure.

zeta : Bool

When true (default: true), performs zeta reduction of let and have expressions. That is, let x := v; e[x] reduces to e[v]. If zetaHave is false then have expressions are not zeta reduced. See also zetaDelta.

beta : Bool

When true (default: true), performs beta reduction of applications of fun expressions. That is, (fun x => e[x]) v reduces to e[v].

eta : Bool

TODO (currently unimplemented). When true (default: true), performs eta reduction for fun expressions. That is, (fun x => f x) reduces to f.

etaStruct : Lean.Meta.EtaStructMode

Configures how to determine definitional equality between two structure instances. See documentation for Lean.Meta.EtaStructMode.

iota : Bool

When true (default: true), reduces match expressions applied to constructors.

proj : Bool

When true (default: true), reduces projections of structure constructors.

decide : Bool

When true (default: false), rewrites a proposition p to True or False by inferring a Decidable p instance and reducing it.

arith : Bool

When true (default: false), simplifies simple arithmetic expressions.

autoUnfold : Bool

When true (default: false), unfolds definitions. This can be enabled using the simp! syntax.

dsimp : Bool

When true (default: true) then switches to dsimp on dependent arguments if there is no congruence theorem that would allow simp to visit them. When dsimp is false, then the argument is not visited.

failIfUnchanged : Bool

If failIfUnchanged is true (default: true), then calls to simp, dsimp, or simp_all will fail if they do not make progress.

ground : Bool

If ground is true (default: false), then ground terms are reduced. A term is ground when it does not contain free or meta variables. Reduction is interrupted at a function application f ... if f is marked to not be unfolded. Ground term reduction applies @[seval] lemmas.

unfoldPartialApp : Bool

If unfoldPartialApp is true (default: false), then calls to simp, dsimp, or simp_all will unfold even partial applications of f when we request f to be unfolded.

zetaDelta : Bool

When true (default: false), local definitions are unfolded. That is, given a local context containing x : t := e, then the free variable x reduces to e. Otherwise, x must be provided as a simp argument.

index : Bool

When index (default : true) is false, simp will only use the root symbol to find candidate simp theorems. It approximates Lean 3 simp behavior.

implicitDefEqProofs : Bool

If implicitDefEqProofs := true, simp does not create proof terms when the input and output terms are definitionally equal.

zetaUnused : Bool

When true (default : true), then simp will remove unused let and have expressions: let x := v; e simplifies to e when x does not occur in e. This option takes precedence over zeta and zetaHave.

catchRuntime : Bool

When true (default : true), then simps will catch runtime exceptions and convert them into simp exceptions.

zetaHave : Bool

When false (default: true), then disables zeta reduction of have expressions. If zeta is false, then this option has no effect. Unused haves are still removed if zeta or zetaUnused are true.

letToHave : Bool

When true (default : true), then simp will attempt to transform lets into haves if they are non-dependent. This only applies when zeta := false.

def

Lean.Meta.Simp.neutralConfig : Lean.Meta.Simp.Config
Lean.Meta.Simp.neutralConfig :
  Lean.Meta.Simp.Config

A neutral configuration for simp, turning off all reductions and other built-in simplifications.

structure

Lean.Meta.DSimp.Config : Type
Lean.Meta.DSimp.Config : Type

The configuration for dsimp. Passed to dsimp using, for example, the dsimp (config := {zeta := false}) syntax.

Implementation note: this structure is only used for processing the (config := ...) syntax, and it is not used internally. It is immediately converted to Lean.Meta.Simp.Config by Lean.Elab.Tactic.elabSimpConfig.

Constructor

Lean.Meta.DSimp.Config.mk

Fields

zeta : Bool

beta : Bool

When true (default: true), performs beta reduction of applications of fun expressions. That is, (fun x => e[x]) v reduces to e[v].

eta : Bool

TODO (currently unimplemented). When true (default: true), performs eta reduction for fun expressions. That is, (fun x => f x) reduces to f.

etaStruct : Lean.Meta.EtaStructMode

Configures how to determine definitional equality between two structure instances. See documentation for Lean.Meta.EtaStructMode.

iota : Bool

When true (default: true), reduces match expressions applied to constructors.

proj : Bool

When true (default: true), reduces projections of structure constructors.

decide : Bool

When true (default: false), rewrites a proposition p to True or False by inferring a Decidable p instance and reducing it.

autoUnfold : Bool

When true (default: false), unfolds definitions. This can be enabled using the simp! syntax.

failIfUnchanged : Bool

If failIfUnchanged is true (default: true), then calls to simp, dsimp, or simp_all will fail if they do not make progress.

unfoldPartialApp : Bool

If unfoldPartialApp is true (default: false), then calls to simp, dsimp, or simp_all will unfold even partial applications of f when we request f to be unfolded.

zetaDelta : Bool

index : Bool

When index (default : true) is false, simp will only use the root symbol to find candidate simp theorems. It approximates Lean 3 simp behavior.

zetaUnused : Bool

When true (default : true), then simp will remove unused let and have expressions: let x := v; e simplifies to e when x does not occur in e.

zetaHave : Bool

16.6.1. Options🔗

Some global options affect simp:

option

simprocs

Default value: true

Enable/disable simprocs (simplification procedures).

option

tactic.simp.trace

Default value: false

When tracing is enabled, calls to simp or dsimp will print an equivalent simp only call.

option

linter.unnecessarySimpa

Default value: true

enable the 'unnecessary simpa' linter

option

trace.Meta.Tactic.simp.rewrite

Default value: false

enable/disable tracing for the given module and submodules

option

trace.Meta.Tactic.simp.discharge

Default value: false

enable/disable tracing for the given module and submodules