Lean4
/-- This command allows customisation of the lemmas generated by `simps`.
By default, tagging a definition of an element `myObj` of a structure `MyStruct` with `@[simps]`
generates one `@[simp]` lemma `myObj_myProj` for each projection `myProj` of `MyStruct`. There are a
few exceptions to this general rule:
* For algebraic structures, we will automatically use the notation (like `Mul`)
for the projections if such an instance is available.
* By default, the projections to parent structures are not default projections,
but all the data-carrying fields are (including those in parent structures).
This default behavior is customisable as such:
* You can disable a projection by default by running
`initialize_simps_projections MulEquiv (-invFun)`
This will ensure that no simp lemmas are generated for this projection,
unless this projection is explicitly specified by the user (as in
`@[simps invFun] def myEquiv : MulEquiv _ _ := _`).
* Conversely, you can enable a projection by default by running
`initialize_simps_projections MulEquiv (+toEquiv)`.
* You can specify custom names by writing e.g.
`initialize_simps_projections MulEquiv (toFun → apply, invFun → symm_apply)`.
* If you want the projection name added as a prefix in the generated lemma name, you can use
`as_prefix fieldName`:
`initialize_simps_projections MulEquiv (toFun → coe, as_prefix coe)`
Note that this does not influence the parsing of projection names: if you have a declaration
`foo` and you want to apply the projections `snd`, `coe` (which is a prefix) and `fst`, in that
order you can run `@[simps snd_coe_fst] def foo ...` and this will generate a lemma with the
name `coe_foo_snd_fst`.
Here are a few extra pieces of information:
* Run `initialize_simps_projections?` (or `set_option trace.simps.verbose true`)
to see the generated projections.
* Running `initialize_simps_projections MyStruct` without arguments is not necessary, it has the
same effect if you just add `@[simps]` to a declaration.
* It is recommended to call `@[simps]` or `initialize_simps_projections` in the same file as the
structure declaration. Otherwise, the projections could be generated multiple times in different
files.
Some common uses:
* If you define a new homomorphism-like structure (like `MulHom`) you can just run
`initialize_simps_projections` after defining the `DFunLike` instance (or instance that implies
a `DFunLike` instance).
```
instance {mM : Mul M} {mN : Mul N} : FunLike (MulHom M N) M N := ...
initialize_simps_projections MulHom (toFun → apply)
```
This will generate `foo_apply` lemmas for each declaration `foo`.
* If you prefer `coe_foo` lemmas that state equalities between functions, use
`initialize_simps_projections MulHom (toFun → coe, as_prefix coe)`
In this case you have to use `@[simps -fullyApplied]` whenever you call `@[simps]`.
* You can also initialize to use both, in which case you have to choose which one to use by default,
by using either of the following
```
initialize_simps_projections MulHom (toFun → apply, toFun → coe, as_prefix coe, -coe)
initialize_simps_projections MulHom (toFun → apply, toFun → coe, as_prefix coe, -apply)
```
In the first case, you can get both lemmas using `@[simps, simps -fullyApplied coe]` and in
the second case you can get both lemmas using `@[simps -fullyApplied, simps apply]`.
* If you declare a new homomorphism-like structure (like `RelEmbedding`),
then `initialize_simps_projections` will automatically find any `DFunLike` coercions
that will be used as the default projection for the `toFun` field.
```
initialize_simps_projections relEmbedding (toFun → apply)
```
* If you have an isomorphism-like structure (like `Equiv`) you often want to define a custom
projection for the inverse:
```
def Equiv.Simps.symm_apply (e : α ≃ β) : β → α := e.symm
initialize_simps_projections Equiv (toFun → apply, invFun → symm_apply)
```
-/
@[command_parser 1000]
public meta def initialize_simps_projections : Lean.ParserDescr✝ :=
ParserDescr.node✝ `Lean.Parser.Command.initialize_simps_projections 1022
(ParserDescr.binary✝ `andthen
(ParserDescr.binary✝ `andthen (ParserDescr.symbol✝ "initialize_simps_projections")
(ParserDescr.unary✝ `optional (ParserDescr.symbol✝ "?")))
Lean.Parser.Command.simpsProj)
