From 61645f967176a36b0b6dff6d1297a8e8285191e2 Mon Sep 17 00:00:00 2001 From: Kyle Miller Date: Wed, 10 Apr 2024 14:53:19 +0200 Subject: [PATCH 1/2] doc: describe all `simp` configuration options Co-authored by Marc Huisinga, with input from Leo. --- src/Init/MetaTypes.lean | 92 ++++++++++++++++++++++++++++++++++++----- 1 file changed, 81 insertions(+), 11 deletions(-) diff --git a/src/Init/MetaTypes.lean b/src/Init/MetaTypes.lean index 82a0ffa63a94..23fd1019d673 100644 --- a/src/Init/MetaTypes.lean +++ b/src/Init/MetaTypes.lean @@ -68,38 +68,105 @@ namespace Simp def defaultMaxSteps := 100000 +/-- +The configuration for `simp`. +Passed to `simp` using, for example, the `simp (config := {contextual := true})` syntax. + +See also `Lean.Meta.Simp.neutralConfig`. +-/ structure Config where + /-- + The maximum number of subexpressions to visit when performing simplification. + The default is large number, but not infinite. + -/ maxSteps : Nat := defaultMaxSteps + /-- + 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. + -/ maxDischargeDepth : Nat := 2 + /-- + When `contextual` is true (default: `false`) and simplification encounters an implication `p → q` + it includes `p` as an additional simp lemma when simplifying `q`. + -/ contextual : Bool := false + /-- + When true (default: `true`) then the simplifier caches the result of simplifying each subexpression, if possible. + -/ memoize : Bool := true + /-- + 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. + -/ singlePass : Bool := false - /-- `let x := v; e[x]` reduces to `e[v]`. -/ + /-- + When `true` (default: `true`), performs zeta reduction of let expressions. + That is, `let x := v; e[x]` reduces to `e[v]`. + See also `zetaDelta`. + -/ zeta : Bool := true + /-- + When `true` (default: `true`), performs beta reduction of applications of `fun` expressions. + That is, `(fun x => e[x]) v` reduces to `e[v]`. + -/ beta : Bool := true + /-- + TODO (currently unimplemented). When `true` (default: `true`), performs eta reduction for `fun` expressions. + That is, `(fun x => f x)` reduces to `f`. + -/ eta : Bool := true + /-- + Configures how to determine definitional equality between two structure instances. + See documentation for `Lean.Meta.EtaStructMode`. + -/ etaStruct : EtaStructMode := .all + /-- + When `true` (default: `true`), reduces `match` expressions applied to constructors. + -/ iota : Bool := true + /-- + When `true` (default: `true`), reduces projections of structure constructors. + -/ proj : Bool := true + /-- + When `true` (default: `true`), rewrites a proposition `p` to `True` or `False` by inferring + a `Decidable p` instance and reducing it. + -/ decide : Bool := false + /-- When `true` (default: `false`), simplifies simple arithmetic expressions. -/ arith : Bool := false + /-- + When `true` (default: `false`), unfolds definitions. + This can be enabled using the `simp!` syntax. + -/ autoUnfold : Bool := false /-- - If `dsimp := true`, then switches to `dsimp` on dependent arguments where there is no congruence theorem that allows - `simp` to visit them. If `dsimp := false`, then argument is not visited. + 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. -/ dsimp : Bool := true - /-- If `failIfUnchanged := true`, then calls to `simp`, `dsimp`, or `simp_all` - will fail if they do not make progress. -/ + /-- + If `failIfUnchanged` is `true` (default: `true`), then calls to `simp`, `dsimp`, or `simp_all` + will fail if they do not make progress. + -/ failIfUnchanged : Bool := true - /-- If `ground := true`, 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. -/ + /-- + 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 : Bool := false - /-- If `unfoldPartialApp := true`, then calls to `simp`, `dsimp`, or `simp_all` - will unfold even partial applications of `f` when we request `f` to be unfolded. -/ + /-- + 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. + -/ unfoldPartialApp : Bool := false - /-- Given a local context containing entry `x : t := e`, free variable `x` reduces to `e`. -/ + /-- + 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`. + -/ zetaDelta : Bool := false deriving Inhabited, BEq @@ -107,6 +174,9 @@ structure Config where structure ConfigCtx extends Config where contextual := true +/-- +A neutral configuration for `simp`, turning off all reductions and other built-in simplifications. +-/ def neutralConfig : Simp.Config := { zeta := false beta := false From 572adbcbee4149322db69a88d7352219e9a9891a Mon Sep 17 00:00:00 2001 From: Kyle Miller Date: Thu, 11 Apr 2024 14:03:12 +0200 Subject: [PATCH 2/2] update --- src/Init/MetaTypes.lean | 3 ++- 1 file changed, 2 insertions(+), 1 deletion(-) diff --git a/src/Init/MetaTypes.lean b/src/Init/MetaTypes.lean index 23fd1019d673..8ba1a2e21734 100644 --- a/src/Init/MetaTypes.lean +++ b/src/Init/MetaTypes.lean @@ -77,7 +77,7 @@ See also `Lean.Meta.Simp.neutralConfig`. structure Config where /-- The maximum number of subexpressions to visit when performing simplification. - The default is large number, but not infinite. + The default is 100000. -/ maxSteps : Nat := defaultMaxSteps /-- @@ -156,6 +156,7 @@ structure Config where 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. -/ ground : Bool := false /--