8.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
    (maxSteps maxDischargeDepth : Nat)
    (contextual memoize singlePass zeta beta
     eta : Bool)
    (etaStruct : Lean.Meta.EtaStructMode)
    (iota proj decide arith autoUnfold dsimp
     failIfUnchanged ground unfoldPartialApp
     zetaDelta index implicitDefEqProofs : Bool)
    : Lean.Meta.Simp.Config

Fields

`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`.
`etaStruct`	:	`Lean.Meta.EtaStructMode`
		Configures how to determine definitional equality between two structure instances. See documentation for `Lean.Meta.EtaStructMode`.
`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`.
`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.
`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.
`eta`	:	`Bool`
		TODO (currently unimplemented). When `true` (default: `true`), performs eta reduction for `fun` expressions. That is, `(fun x => f x)` reduces to `f`.
`arith`	:	`Bool`
		When `true` (default: `false`), simplifies simple arithmetic expressions.
`maxSteps`	:	`Nat`
		The maximum number of subexpressions to visit when performing simplification. The default is 100000.
`failIfUnchanged`	:	`Bool`
		If `failIfUnchanged` is `true` (default: `true`), then calls to `simp`, `dsimp`, or `simp_all` will fail if they do not make progress.
`iota`	:	`Bool`
		When `true` (default: `true`), reduces `match` expressions applied to constructors.
`memoize`	:	`Bool`
		When true (default: `true`) then the simplifier caches the result of simplifying each subexpression, if possible.
`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`.
`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.
`decide`	:	`Bool`
		When `true` (default: `false`), rewrites a proposition `p` to `True` or `False` by inferring a `Decidable p` instance and reducing it.
`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.
`implicitDefEqProofs`	:	`Bool`
		When `true` (default: `true`), `simp` will not create a proof for a rewriting rule associated with an `rfl`-theorem. Rewriting rules are provided by users by annotating theorems with the attribute `@[simp]`. If the proof of the theorem is just `rfl` (reflexivity), and `implicitDefEqProofs := true`, `simp` will not create a proof term which is an application of the annotated theorem.
`autoUnfold`	:	`Bool`
		When `true` (default: `false`), unfolds definitions. This can be enabled using the `simp!` syntax.
`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]`.
`proj`	:	`Bool`
		When `true` (default: `true`), reduces projections of structure constructors.
`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.
`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.

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 (zeta beta eta : Bool)
    (etaStruct : Lean.Meta.EtaStructMode)
    (iota proj decide autoUnfold failIfUnchanged
     unfoldPartialApp zetaDelta index : Bool)
    : Lean.Meta.DSimp.Config

Fields

`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`.
`etaStruct`	:	`Lean.Meta.EtaStructMode`
		Configures how to determine definitional equality between two structure instances. See documentation for `Lean.Meta.EtaStructMode`.
`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.
`eta`	:	`Bool`
		TODO (currently unimplemented). When `true` (default: `true`), performs eta reduction for `fun` expressions. That is, `(fun x => f x)` reduces to `f`.
`failIfUnchanged`	:	`Bool`
		If `failIfUnchanged` is `true` (default: `true`), then calls to `simp`, `dsimp`, or `simp_all` will fail if they do not make progress.
`iota`	:	`Bool`
		When `true` (default: `true`), reduces `match` expressions applied to constructors.
`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`.
`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.
`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]`.
`proj`	:	`Bool`
		When `true` (default: `true`), reduces projections of structure constructors.
`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.

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