Lean4
/-- The `@[simps]` attribute automatically derives lemmas specifying the projections of this
declaration.
Example:
```lean
@[simps] def foo : ℕ × ℤ := (1, 2)
```
derives two `simp` lemmas:
```lean
@[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 `Neg` or `Mul`,
then this notation is used instead of the corresponding projection.
* You can specify custom projections, by giving a declaration with name
`{StructureName}.Simps.{projectionName}`. See Note [custom simps projection].
Example:
```lean
def Equiv.Simps.invFun (e : α ≃ β) : β → α := e.symm
@[simps] def Equiv.trans (e₁ : α ≃ β) (e₂ : β ≃ γ) : α ≃ γ :=
⟨e₂ ∘ e₁, e₁.symm ∘ e₂.symm⟩
```
generates
```
@[simp] lemma Equiv.trans_toFun : ∀ {α β γ} (e₁ e₂) (a : α), ⇑(e₁.trans e₂) a = (⇑e₂ ∘ ⇑e₁) a
@[simp] lemma Equiv.trans_invFun : ∀ {α β γ} (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 (toFun → apply, invFun → symm_apply)`.
See `initialize_simps_projections` for more information.
* 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`, `PProd`, and `Opposite`. You can give explicit projection names or change the value of
`Simps.Config.notRecursive` to override this behavior.
Example:
```lean
structure MyProd (α β : Type*) := (fst : α) (snd : β)
@[simps] def foo : Prod ℕ ℕ × MyProd ℕ ℕ := ⟨⟨1, 2⟩, 3, 4⟩
```
generates
```lean
@[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
```
* 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 form `foo.proj1.proj2.proj3 = ...`.
Example:
```lean
structure MyProd (α β : Type*) := (fst : α) (snd : β)
@[simps fst fst_fst snd] def foo : Prod ℕ ℕ × MyProd ℕ ℕ := ⟨⟨1, 2⟩, 3, 4⟩
```
generates
```lean
@[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:
```lean
structure EquivPlusData (α β) extends α ≃ β where
data : Bool
@[simps] def EquivPlusData.rfl {α} : EquivPlusData α α := { Equiv.refl α with data := true }
```
generates the following:
```lean
@[simp] lemma bar_toEquiv : ∀ {α : Sort*}, bar.toEquiv = Equiv.refl α
@[simp] lemma bar_data : ∀ {α : Sort*}, bar.data = true
```
This is true, even though Lean inserts an eta-expanded version of `Equiv.refl α` in the
definition of `bar`.
* You can add additional attributes to all lemmas generated by `simps` using e.g.
`@[simps (attr := grind =)]`.
* For configuration options, see the doc string of `Simps.Config`.
* The precise syntax is `simps (attr := a) config ident*`, where `a` is a list of attributes,
`config` declares configuration options and `ident*` is a list of desired projection names.
* Configuration options can be given using `(config := e)` where `e : Simps.Config`,
or by specifying options directly, like `-fullyApplied` or `(notRecursive := [])`.
* `@[simps]` reduces let-expressions where necessary.
* When option `trace.simps.verbose` is true, `simps` will print the projections it finds and the
lemmas it generates. The same can be achieved by using `@[simps?]`.
* Use `@[to_additive (attr := simps)]` to apply both `to_additive` and `simps` to a definition
This will also generate the additive versions of all `simp` lemmas.
-/
/- If one of the fields is a partially applied constructor, we will eta-expand it
(this likely never happens, so is not included in the official doc). -/
@[attr_parser 1000]
public meta def simps : Lean.ParserDescr✝ :=
ParserDescr.node✝ `Lean.Parser.Attr.simps 1022
(ParserDescr.binary✝ `andthen
(ParserDescr.binary✝ `andthen
(ParserDescr.binary✝ `andthen (ParserDescr.nonReservedSymbol✝ "simps" false✝)
(ParserDescr.unary✝ `optional (ParserDescr.symbol✝ "!")))
(ParserDescr.unary✝ `optional (ParserDescr.symbol✝ "?")))
Lean.Parser.Attr.simpsArgsRest)
