10.6. Configuring Simplification🔗

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

structure

Lean.Meta.Simp.Config : Type

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

See also Lean.Meta.Simp.neutralConfig and Lean.Meta.DSimp.Config.

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 expressions. That is, `let x := v; e[x]` reduces to `e[v]`. 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 entry `x : t := e`, the free variable `x` reduces to `e`.
`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.

def

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

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`
		When `true` (default: `true`), performs zeta reduction of let expressions. That is, `let x := v; e[x]` reduces to `e[v]`. 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.
`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`
		When `true` (default: `false`), local definitions are unfolded. That is, given a local context containing entry `x : t := e`, the free variable `x` reduces to `e`.
`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.

10.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