simps attribute
This file defines the @[simps]
attribute, to automatically generate simp-lemmas
reducing a definition when projections are applied to it.
Implementation Notes
There are three attributes being defined here
@[simps]
is the attribute for objects of a structure or instances of a class. It will automatically generate simplification lemmas for each projection of the object/instance that contains data. See the doc strings forsimps_attr
andsimps_cfg
for more details and configuration options.@[_simps_str]
is automatically added to structures that have been used in@[simps]
at least once. This attribute contains the data of the projections used for this structure by all following invocations of@[simps]
.@[notation_class]
should be added to all classes that define notation, likehas_mul
andhas_zero
. This specifies that the projections that@[simps]
used are the projections from these notation classes instead of the projections of the superclasses. Example: ifhas_mul
is tagged with@[notation_class]
then the projection used forsemigroup
will beλ α hα, @has_mul.mul α (@semigroup.to_has_mul α hα)
instead of@semigroup.mul
.
Tags
structures, projections, simp, simplifier, generates declarations
The @[_simps_str]
attribute specifies the preferred projections of the given structure,
used by the @[simps]
attribute.
- This will usually be tagged by the
@[simps]
tactic. - You can also generate this with the command
initialize_simps_projections
. - To change the default value, see Note [custom simps projection].
- You are strongly discouraged to add this attribute manually.
- The first argument is the list of names of the universe variables used in the structure
- The second argument is a list that consists of
- a custom name for each projection of the structure
- an expressions for each projections of the structure (definitionally equal to the corresponding projection). These expressions can contain the universe parameters specified in the first argument).
The @[notation_class]
attribute specifies that this is a notation class,
and this notation should be used instead of projections by @[simps].
- The first argument
tt
for notation classes andff
for classes applied to the structure, likehas_coe_to_sort
andhas_coe_to_fun
- The second argument is the name of the projection (by default it is the first projection of the structure)
Get the projections used by simps
associated to a given structure str
. The second component is
the list of projections, and the first component the (shared) list of universe levels used by the
projections.
The returned information is also stored in a parameter of the attribute @[_simps_str]
, which
is given to str
. If str
already has this attribute, the information is read from this
attribute instead.
The returned universe levels are the universe levels of the structure. For the projections there are three cases
- If the declaration
{structure_name}.simps.{projection_name}
has been declared, then the value of this declaration is used (after checking that it is definitionally equal to the actual projection - Otherwise, for every class with the
notation_class
attribute, and the structure has an instance of that notation class, then the projection of that notation class is used for the projection that is definitionally equal to it (if there is such a projection). This means in practice that coercions to function types and sorts will be used instead of a projection, if this coercion is definitionally equal to a projection. Furthermore, for notation classes likehas_mul
andhas_zero
those projections are used instead of the corresponding projection - Otherwise, the projection of the structure is chosen.
For example:
simps_get_raw_projections env `prod
gives the default projections
([u, v], [prod.fst.{u v}, prod.snd.{u v}])
while ``simps_get_raw_projections env `equiv`` gives
([u_1, u_2], [λ α β, coe_fn, λ {α β} (e : α ≃ β), ⇑(e.symm), left_inv, right_inv])
after declaring the coercion from `equiv` to function and adding the declaration
def equiv.simps.inv_fun {α β} (e : α ≃ β) : β → α := e.symm
Optionally, this command accepts two optional arguments
- If
trace_if_exists
the command will always generate a trace message when the structure already has the attribute@[_simps_str]
. - The
name_changes
argument accepts a list of pairs(old_name, new_name)
. This is used to change the projection nameold_name
to the custom projection namenew_name
. Example: for the structureequiv
the projectionto_fun
could be renamedapply
. This name will be used for parsing and generating projection names. This argument is ignored if the structure already has an existing attribute.
Specify simps projections, see Note [custom simps projection].
You can specify custom names by writing e.g.
initialize_simps_projections equiv (to_fun → apply, inv_fun → symm_apply)
.
Set trace.simps.verbose
to true to see the generated projections.
If the projections were already specified before, you can call initialize_simps_projections
again to see the generated projections.
Get the projections of a structure used by @[simps]
applied to the appropriate arguments.
Returns a list of quadruples
(projection expression, given projection name, original (full) projection name,
corresponding right-hand-side),
one for each projection. The given projection name is the name for the projection used by the user
used to generate (and parse) projection names. The original projection name is the actual
projection name in the structure, which is only used to check whether the expression is an
eta-expansion of some other expression. For example, in the structure
Example 1: simps_get_projection_exprs env `(α × β) `(⟨x, y⟩)
will give the output
Example 2: simps_get_projection_exprs env `(α ≃ α) `(⟨id, id, λ _, rfl, λ _, rfl⟩)
will give the output
[(`(@equiv.to_fun.{u u} α α), `apply, `equiv.to_fun, `(id)),
(`(@equiv.inv_fun.{u u} α α), `symm_apply, `equiv.inv_fun, `(id)),
...,
...]
The last two fields of the list correspond to the propositional fields of the structure, and are rarely/never used.
- attrs : list name
- short_name : bool
- simp_rhs : bool
- type_md : tactic.transparency
- rhs_md : tactic.transparency
- fully_applied : bool
- not_recursive : list name
Configuration options for the @[simps]
attribute.
attrs
specifies the list of attributes given to the generated lemmas. Default:[`simp]
. The attributes can be either basic attributes, or user attributes without parameters. There are two attributes whichsimps
might add itself:- If
[`simp]
is in the list, then[`_refl_lemma]
is added automatically if appropriate. - If the definition is marked with
@[to_additive ...]
then all generated lemmas are marked with@[to_additive]
- If
short_name
gives the generated lemmas a shorter name. This only has an effect when multiple projections are applied in a lemma. When this isff
(default) all projection names will be appended to the definition name to form the lemma name, and when this istt
, only the last projection name will be appended.- if
simp_rhs
istt
then the right-hand-side of the generated lemmas will be put in simp-normal form. More precisely:dsimp, simp
will be called on all these expressions. See note [dsimp, simp]. type_md
specifies how aggressively definitions are unfolded in the type of expressions for the purposes of finding out whether the type is a function type. Default:instances
. This will unfold coercion instances (so that a coercion to a function type is recognized as a function type), but not declarations likeset
.rhs_md
specifies how aggressively definition in the declaration are unfolded for the purposes of finding out whether it is a constructor. Default:none
Exception:@[simps]
will automatically add the options{rhs_md := semireducible, simp_rhs := tt}
if the given definition is not a constructor with the given reducibility setting forrhs_md
.- If
fully_applied
isff
then the generated simp-lemmas will be between non-fully applied terms, i.e. equalities between functions. This does not restrict the recursive behavior of@[simps]
, so only the "final" projection will be non-fully applied. However, it can be used in combination with explicit field names, to get a partially applied intermediate projection. - The option
not_recursive
contains the list of names of types for which@[simps]
doesn't recursively apply projections. For example, given an equivalenceα × β ≃ β × α
one usually wants to only apply the projections forequiv
, and not also those for×
. This option is only relevant if no explicit projection names are given as argument to@[simps]
.
Add a lemma with nm
stating that lhs = rhs
. type
is the type of both lhs
and rhs
,
args
is the list of local constants occurring, and univs
is the list of universe variables.
If add_simp
then we make the resulting lemma a simp-lemma.
Derive lemmas specifying the projections of the declaration.
If todo
is non-empty, it will generate exactly the names in todo
.
simps_tac
derives simp-lemmas for all (nested) non-Prop projections of the declaration.
If todo
is non-empty, it will generate exactly the names in todo
.
If short_nm
is true, the generated names will only use the last projection name.
The parser for the @[simps]
attribute.
The @[simps]
attribute automatically derives lemmas specifying the projections of this
declaration.
Example:
@[simps] def foo : ℕ × ℤ := (1, 2)
derives two simp-lemmas:
@[simp] lemma foo_fst : foo.fst = 1
@[simp] lemma foo_snd : foo.snd = 2
- It does not derive simp-lemmas for the prop-valued projections.
- It will automatically reduce newly created beta-redexes, but will not unfold any definitions.
- If the structure has a coercion to either sorts or functions, and this is defined to be one of the projections, then this coercion will be used instead of the projection.
- If the structure is a class that has an instance to a notation class, like
has_mul
, then this notation is used instead of the corresponding projection. You can specify custom projections, by giving a declaration with name
{structure_name}.simps.{projection_name}
. See Note [custom simps projection].Example:
def equiv.simps.inv_fun (e : α ≃ β) : β → α := e.symm @[simps] def equiv.trans (e₁ : α ≃ β) (e₂ : β ≃ γ) : α ≃ γ := ⟨e₂ ∘ e₁, e₁.symm ∘ e₂.symm⟩
generates
@[simp] lemma equiv.trans_to_fun : ∀ {α β γ} (e₁ e₂) (a : α), ⇑(e₁.trans e₂) a = (⇑e₂ ∘ ⇑e₁) a @[simp] lemma equiv.trans_inv_fun : ∀ {α β γ} (e₁ e₂) (a : γ), ⇑((e₁.trans e₂).symm) a = (⇑(e₁.symm) ∘ ⇑(e₂.symm)) a
You can specify custom projection names, by specifying the new projection names using
initialize_simps_projections
. Example:initialize_simps_projections equiv (to_fun → apply, inv_fun → symm_apply)
.If one of the fields itself is a structure, this command will recursively create simp-lemmas for all fields in that structure.
- Exception: by default it will not recursively create simp-lemmas for fields in the structures
prod
andpprod
. Give explicit projection names to override this behavior.
Example:
structure my_prod (α β : Type*) := (fst : α) (snd : β) @[simps] def foo : prod ℕ ℕ × my_prod ℕ ℕ := ⟨⟨1, 2⟩, 3, 4⟩
generates
@[simp] lemma foo_fst : foo.fst = (1, 2) @[simp] lemma foo_snd_fst : foo.snd.fst = 3 @[simp] lemma foo_snd_snd : foo.snd.snd = 4
- Exception: by default it will not recursively create simp-lemmas for fields in the structures
You can use
@[simps proj1 proj2 ...]
to only generate the projection lemmas for the specified projections.Recursive projection names can be specified using
proj1_proj2_proj3
. This will create a lemma of the formfoo.proj1.proj2.proj3 = ...
.Example:
structure my_prod (α β : Type*) := (fst : α) (snd : β) @[simps fst fst_fst snd] def foo : prod ℕ ℕ × my_prod ℕ ℕ := ⟨⟨1, 2⟩, 3, 4⟩
generates
@[simp] lemma foo_fst : foo.fst = (1, 2) @[simp] lemma foo_fst_fst : foo.fst.fst = 1 @[simp] lemma foo_snd : foo.snd = {fst := 3, snd := 4}
If one of the values is an eta-expanded structure, we will eta-reduce this structure.
Example:
structure equiv_plus_data (α β) extends α ≃ β := (data : bool) @[simps] def bar {α} : equiv_plus_data α α := { data := tt, ..equiv.refl α }
generates the following, even though Lean inserts an eta-expanded version of
equiv.refl α
in the definition ofbar
:@[simp] lemma bar_to_equiv : ∀ {α : Sort u_1}, bar.to_equiv = equiv.refl α @[simp] lemma bar_data : ∀ {α : Sort u_1}, bar.data = tt
- For configuration options, see the doc string of
simps_cfg
. - The precise syntax is
('simps' ident* e)
, wheree
is an expression of typesimps_cfg
. @[simps]
reduces let-expressions where necessary.- If one of the fields is a partially applied constructor, we will eta-expand it (this likely never happens).
- When option
trace.simps.verbose
is true,simps
will print the projections it finds and the lemmas it generates. - Use
@[to_additive, simps]
to apply bothto_additive
andsimps
to a definition, making sure thatsimps
comes afterto_additive
. This will also generate the additive versions of all simp-lemmas. Note however, that the additive versions of the simp-lemmas always use the default name generated byto_additive
, even if a custom name is given for the additive version of the definition.