# 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 for `Lean.Parser.Attr.simps` and `Simps.Config` for more details and configuration options.
- `structureExt` (just an environment extension, not actually an attribute) 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, like `Mul` and `Zero`. This specifies that the projections that `@[simps]` used are the projections from these notation classes instead of the projections of the superclasses. Example: if `Mul` is tagged with `@[notation_class]` then the projection used for `Semigroup` will be `fun α hα ↦ @Mul.mul α (@Semigroup.toMul α hα)` instead of `@Semigroup.mul`. [this is not correctly implemented in Lean 4 yet]

### Possible Future Improvements #

- If multiple declarations are generated from a `simps` without explicit projection names, then only the first one is shown when mousing over `simps`.

## Changes w.r.t. Lean 3 #

There are some small changes in the attribute. None of them should have great effects

- The attribute will now raise an error if it tries to generate a lemma when there already exists a lemma with that name (in Lean 3 it would generate a different unique name)
- `transparency.none` has been replaced by `TransparencyMode.reducible`
- The `attr` configuration option has been split into `isSimp` and `attrs` (for extra attributes)
- Because Lean 4 uses bundled structures, this means that `simps` applied to anything that implements a notation class will almost certainly require a user-provided custom simps projection.

## Tags #

structures, projections, simp, simplifier, generates declarations

source
instance instCoeNameStructName :
Coe NameStruct✝ Lean.Name
Equations

- instCoeNameStructName = { coe := NameStruct.toName✝ }

source
def Lean.Meta.mkSimpContextResult (cfg : Simp.Config := { }) (simpOnly : Bool := false) (kind : Elab.Tactic.SimpKind := Elab.Tactic.SimpKind.simp) (dischargeWrapper : Elab.Tactic.Simp.DischargeWrapper := Elab.Tactic.Simp.DischargeWrapper.default) (hasStar : Bool := false) :
MetaM Elab.Tactic.MkSimpContextResult

Make `MkSimpContextResult` giving data instead of Syntax. Doesn't support arguments. Intended to be very similar to `Lean.Elab.Tactic.mkSimpContext` Todo: support arguments.

Equations

- One or more equations did not get rendered due to their size.

Instances For

source
def Lean.Meta.mkSimpContext (cfg : Simp.Config := { }) (simpOnly : Bool := false) (kind : Elab.Tactic.SimpKind := Elab.Tactic.SimpKind.simp) (dischargeWrapper : Elab.Tactic.Simp.DischargeWrapper := Elab.Tactic.Simp.DischargeWrapper.default) (hasStar : Bool := false) :
MetaM Simp.Context

Make `Simp.Context` giving data instead of Syntax. Doesn't support arguments. Intended to be very similar to `Lean.Elab.Tactic.mkSimpContext` Todo: support arguments.

Equations

- Lean.Meta.mkSimpContext cfg simpOnly kind dischargeWrapper hasStar = do let data ← Lean.Meta.mkSimpContextResult cfg simpOnly kind dischargeWrapper hasStar pure data.ctx

Instances For

Declare notation classes.

source
def Lean.Parser.Attr.simpsOptAttrOption :
ParserDescr

An `(attr := ...)` option for `simps`.

Equations

- One or more equations did not get rendered due to their size.

Instances For

source
def Lean.Parser.Attr.simpsArgsRest :
ParserDescr

Arguments to `@[simps]` attribute. Currently, a potential `(attr := ...)` argument has to come before other configuration options.

Equations

- One or more equations did not get rendered due to their size.

Instances For

source
def Lean.Parser.Attr.simps :
ParserDescr

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 `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:

      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:

      structure MyProd (α β : Type*) := (fst : α) (snd : β)
      @[simps] def foo : Prod ℕ ℕ × MyProd ℕ ℕ := ⟨⟨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

- 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:

      structure MyProd (α β : Type*) := (fst : α) (snd : β)
      @[simps fst fst_fst snd] def foo : Prod ℕ ℕ × MyProd ℕ ℕ := ⟨⟨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 EquivPlusData (α β) extends α ≃ β where
        data : Bool
      @[simps] def EquivPlusData.rfl {α} : EquivPlusData α α := { Equiv.refl α with data := true }

  generates the following:

      @[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.

Equations

- One or more equations did not get rendered due to their size.

Instances For

source
def Lean.Parser.Attr.attrSimps?_ :
ParserDescr

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 `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:

      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:

      structure MyProd (α β : Type*) := (fst : α) (snd : β)
      @[simps] def foo : Prod ℕ ℕ × MyProd ℕ ℕ := ⟨⟨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

- 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:

      structure MyProd (α β : Type*) := (fst : α) (snd : β)
      @[simps fst fst_fst snd] def foo : Prod ℕ ℕ × MyProd ℕ ℕ := ⟨⟨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 EquivPlusData (α β) extends α ≃ β where
        data : Bool
      @[simps] def EquivPlusData.rfl {α} : EquivPlusData α α := { Equiv.refl α with data := true }

  generates the following:

      @[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.

Equations

- One or more equations did not get rendered due to their size.

Instances For

source
def Lean.Parser.Attr.attrSimps!_ :
ParserDescr

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 `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:

      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:

      structure MyProd (α β : Type*) := (fst : α) (snd : β)
      @[simps] def foo : Prod ℕ ℕ × MyProd ℕ ℕ := ⟨⟨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

- 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:

      structure MyProd (α β : Type*) := (fst : α) (snd : β)
      @[simps fst fst_fst snd] def foo : Prod ℕ ℕ × MyProd ℕ ℕ := ⟨⟨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 EquivPlusData (α β) extends α ≃ β where
        data : Bool
      @[simps] def EquivPlusData.rfl {α} : EquivPlusData α α := { Equiv.refl α with data := true }

  generates the following:

      @[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.

Equations

- One or more equations did not get rendered due to their size.

Instances For

source
def Lean.Parser.Attr.attrSimps!?_ :
ParserDescr

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 `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:

      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:

      structure MyProd (α β : Type*) := (fst : α) (snd : β)
      @[simps] def foo : Prod ℕ ℕ × MyProd ℕ ℕ := ⟨⟨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

- 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:

      structure MyProd (α β : Type*) := (fst : α) (snd : β)
      @[simps fst fst_fst snd] def foo : Prod ℕ ℕ × MyProd ℕ ℕ := ⟨⟨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 EquivPlusData (α β) extends α ≃ β where
        data : Bool
      @[simps] def EquivPlusData.rfl {α} : EquivPlusData α α := { Equiv.refl α with data := true }

  generates the following:

      @[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.

Equations

- One or more equations did not get rendered due to their size.

Instances For

source
def Lean.Parser.Attr.attrSimps?!_ :
ParserDescr

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 `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:

      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:

      structure MyProd (α β : Type*) := (fst : α) (snd : β)
      @[simps] def foo : Prod ℕ ℕ × MyProd ℕ ℕ := ⟨⟨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

- 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:

      structure MyProd (α β : Type*) := (fst : α) (snd : β)
      @[simps fst fst_fst snd] def foo : Prod ℕ ℕ × MyProd ℕ ℕ := ⟨⟨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 EquivPlusData (α β) extends α ≃ β where
        data : Bool
      @[simps] def EquivPlusData.rfl {α} : EquivPlusData α α := { Equiv.refl α with data := true }

  generates the following:

      @[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.

Equations

- One or more equations did not get rendered due to their size.

Instances For

source
opaque Lean.Parser.linter.simpsNoConstructor :
Lean.Option Bool

Linter to check that `simps!` is used when needed

source
opaque Lean.Parser.linter.simpsUnusedCustomDeclarations :
Lean.Option Bool

Linter to check that no unused custom declarations are declared for simps.

source
def Lean.Parser.Command.simpsRule.rename :
ParserDescr

Syntax for renaming a projection in `initialize_simps_projections`.

Equations

- One or more equations did not get rendered due to their size.

Instances For

source
def Lean.Parser.Command.simpsRule.erase :
ParserDescr

Syntax for making a projection non-default in `initialize_simps_projections`.

Equations

- One or more equations did not get rendered due to their size.

Instances For

source
def Lean.Parser.Command.simpsRule.add :
ParserDescr

Syntax for making a projection default in `initialize_simps_projections`.

Equations

- One or more equations did not get rendered due to their size.

Instances For

source
def Lean.Parser.Command.simpsRule.prefix :
ParserDescr

Syntax for making a projection prefix.

Equations

- One or more equations did not get rendered due to their size.

Instances For

source
def Lean.Parser.Command.simpsRule :
ParserDescr

Syntax for a single rule in `initialize_simps_projections`.

Equations

- One or more equations did not get rendered due to their size.

Instances For

source
def Lean.Parser.Command.simpsProj :
ParserDescr

Syntax for `initialize_simps_projections`.

Equations

- One or more equations did not get rendered due to their size.

Instances For

source
def Lean.Parser.Command.initialize_simps_projections :
ParserDescr

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)

Equations

- One or more equations did not get rendered due to their size.

Instances For

source
def Lean.Parser.Command.commandInitialize_simps_projections?_ :
ParserDescr

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)

Equations

- One or more equations did not get rendered due to their size.

Instances For

source
structure Simps.ProjectionData :
Type

Projection data for a single projection of a structure

- name : Lean.Name

  The name used in the generated `simp` lemmas

- expr : Lean.Expr

  An Expression used by simps for the projection. It must be definitionally equal to an original projection (or a composition of multiple projections). These Expressions can contain the universe parameters specified in the first argument of `structureExt`.

- projNrs : List Nat

  A list of natural numbers, which is the projection number(s) that have to be applied to the Expression. For example the list `[0, 1]` corresponds to applying the first projection of the structure, and then the second projection of the resulting structure (this assumes that the target of the first projection is a structure with at least two projections). The composition of these projections is required to be definitionally equal to the provided Expression.

- isDefault : Bool

  A Boolean specifying whether `simp` lemmas are generated for this projection by default.

- isPrefix : Bool

  A Boolean specifying whether this projection is written as prefix.

Instances For

source
instance Simps.instInhabitedProjectionData :
Inhabited ProjectionData
Equations

- Simps.instInhabitedProjectionData = { default := Simps.instInhabitedProjectionData.default }

source
def Simps.instInhabitedProjectionData.default :
ProjectionData
Equations

- Simps.instInhabitedProjectionData.default = { name := default, expr := default, projNrs := default, isDefault := default, isPrefix := default }

Instances For

source
instance Simps.instToMessageDataProjectionData :
Lean.ToMessageData ProjectionData
Equations

- One or more equations did not get rendered due to their size.

source
opaque Simps.structureExt :
Lean.NameMapExtension (List Lean.Name × Array ProjectionData)

The `Simps.structureExt` environment extension specifies the preferred projections of the given structure, used by the `@[simps]` attribute.

- You can generate this with the command `initialize_simps_projections`.
- If not generated, the `@[simps]` attribute will generate this automatically.
- To change the default value, see Note [custom simps projection].
- The first argument is the list of names of the universe variables used in the structure
- The second argument is an array that consists of the projection data for each projection.

source
structure Simps.ParsedProjectionData :
Type

Projection data used internally in `getRawProjections`.

- strName : Lean.Name

  name for this projection used in the structure definition

- strStx : Lean.Syntax

  syntax that might have provided `strName`

- newName : Lean.Name

  name for this projection used in the generated `simp` lemmas

- newStx : Lean.Syntax

  syntax that provided `newName`

- isDefault : Bool

  will simp lemmas be generated for with (without specifically naming this?)

- isPrefix : Bool

  is the projection name a prefix?

- expr? : Option Lean.Expr

  projection expression

- projNrs : Array Nat

  the list of projection numbers this expression corresponds to

- isCustom : Bool

  is this a projection that is changed by the user?

Instances For

source
def Simps.ParsedProjectionData.toProjectionData (p : ParsedProjectionData) :
ProjectionData

Turn `ParsedProjectionData` into `ProjectionData`.

Equations

- p.toProjectionData = { name := p.newName, expr := p.expr?.getD default, projNrs := p.projNrs.toList, isDefault := p.isDefault, isPrefix := p.isPrefix }

Instances For

source
instance Simps.instToMessageDataParsedProjectionData :
Lean.ToMessageData ParsedProjectionData
Equations

- One or more equations did not get rendered due to their size.

source
inductive Simps.ProjectionRule :
Type

The type of rules that specify how metadata for projections in changes. See `initialize_simps_projections`.

- rename (oldName : Lean.Name) (oldStx : Lean.Syntax) (newName : Lean.Name) (newStx : Lean.Syntax) : ProjectionRule

  A renaming rule `before→after` or Each name comes with the syntax used to write the rule, which is used to declare hover information.

- add : Lean.Name → Lean.Syntax → ProjectionRule

  An adding rule `+fieldName`

- erase : Lean.Name → Lean.Syntax → ProjectionRule

  A hiding rule `-fieldName`

- prefix : Lean.Name → Lean.Syntax → ProjectionRule

  A prefix rule `prefix fieldName`

Instances For

source
instance Simps.instToMessageDataProjectionRule :
Lean.ToMessageData ProjectionRule
Equations

- One or more equations did not get rendered due to their size.

source
def Simps.projectionsInfo (l : List ProjectionData) (pref : String) (str : Lean.Name) :
Lean.MessageData

Returns the projection information of a structure.

Equations

- One or more equations did not get rendered due to their size.

Instances For

source
def Simps.findProjectionIndices (strName projName : Lean.Name) :
Lean.MetaM (List Nat)

Find the indices of the projections that need to be applied to elaborate `$e.$projName`. Example: If `e : α ≃+ β` and `projName = `invFun` then this returns `[0, 1]`, because the first projection of `MulEquiv` is `toEquiv` and the second projection of `Equiv` is `invFun`.

Equations

- One or more equations did not get rendered due to their size.

Instances For

source
partial def Simps.getCompositeOfProjectionsAux (proj : String) (e : Lean.Expr) (pos : Array Nat) (args : Array Lean.Expr) :
Lean.MetaM (Lean.Expr × Array Nat)

Auxiliary function of `getCompositeOfProjections`.

source
def Simps.getCompositeOfProjections (structName : Lean.Name) (proj : String) :
Lean.MetaM (Lean.Expr × Array Nat)

Suppose we are given a structure `str` and a projection `proj`, that could be multiple nested projections (separated by `_`), where each projection could be a projection of a parent structure. This function returns an expression that is the composition of these projections and a list of natural numbers, that are the projection numbers of the applied projections. Note that this function is similar to elaborating dot notation, but it can do a little more.

Example: if we do

    structure gradedFun (A : ℕ → Type*) where
      toFun := ∀ i j, A i →+ A j →+ A (i + j)
    initialize_simps_projections (toFun_toFun_toFun → myMul)

we will be able to generate the "projection" `fun {A} (f : gradedFun A) (x : A i) (y : A j) ↦ ↑(↑(f.toFun i j) x) y`, which projection notation cannot do.

Equations

- One or more equations did not get rendered due to their size.

Instances For

source
def Simps.mkParsedProjectionData (structName : Lean.Name) :
Lean.CoreM (Array ParsedProjectionData)

Get the default `ParsedProjectionData` for structure `str`. It first returns the direct fields of the structure in the right order, and then all (non-subobject fields) of all parent structures. The subobject fields are precisely the non-default fields.

Equations

- One or more equations did not get rendered due to their size.

Instances For

source
def Simps.applyProjectionRules (projs : Array ParsedProjectionData) (rules : Array ProjectionRule) :
Lean.CoreM (Array ParsedProjectionData)

Execute the projection renamings (and turning off projections) as specified by `rules`.

Equations

- One or more equations did not get rendered due to their size.

Instances For

source
def Simps.findProjection (str : Lean.Name) (proj : ParsedProjectionData) (rawUnivs : List Lean.Level) :
Lean.CoreM ParsedProjectionData

Auxiliary function for `getRawProjections`. Generates the default projection, and looks for a custom projection declared by the user, and replaces the default projection with the custom one, if it can find it.

Equations

- One or more equations did not get rendered due to their size.

Instances For

source
def Simps.checkForUnusedCustomProjs (stx : Lean.Syntax) (str : Lean.Name) (projs : Array ParsedProjectionData) :
Lean.CoreM Unit

Checks if there are declarations in the current file in the namespace `{str}.Simps` that are not used.

Equations

- One or more equations did not get rendered due to their size.

Instances For

source
def Simps.findAutomaticProjectionsAux (str : Lean.Name) (proj : ParsedProjectionData) (args : Array Lean.Expr) :
Lean.Elab.TermElabM (Option (Lean.Expr × Lean.Name))

If a structure has a field that corresponds to a coercion to functions or sets, or corresponds to notation, find the custom projection that uses this coercion or notation. Returns the custom projection and the name of the projection used.

We catch most errors this function causes, so that we don't fail if an unrelated projection has an applicable name. (e.g. `Iso.inv`)

Implementation note: getting rid of TermElabM is tricky, since `Expr.mkAppOptM` doesn't allow to keep metavariables around, which are necessary for `OutParam`.

Equations

- One or more equations did not get rendered due to their size.

Instances For

source
def Simps.findAutomaticProjections (str : Lean.Name) (projs : Array ParsedProjectionData) :
Lean.CoreM (Array ParsedProjectionData)

Auxiliary function for `getRawProjections`. Find custom projections, automatically found by simps. These come from `DFunLike` and `SetLike` instances.

Equations

- One or more equations did not get rendered due to their size.

Instances For

source
def Simps.getRawProjections (stx : Lean.Syntax) (str : Lean.Name) (traceIfExists : Bool := false) (rules : Array ProjectionRule := #[]) (trc : Bool := false) :
Lean.CoreM (List Lean.Name × Array ProjectionData)

Get the projections used by `simps` associated to a given structure `str`.

The returned information is also stored in the environment extension `Simps.structureExt`, which is given to `str`. If `str` already has this attribute, the information is read from this extension instead. See the documentation for this extension for the data this tactic returns.

The returned universe levels are the universe levels of the structure. For the projections there are three cases

- If the declaration `{StructureName}.Simps.{projectionName}` has been declared, then the value of this declaration is used (after checking that it is definitionally equal to the actual projection. If you rename the projection name, the declaration should have the new projection name.
- You can also declare a custom projection that is a composite of multiple projections.
- 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 like `Mul` and `Zero` those projections are used instead of the corresponding projection. Projections for coercions and notation classes are not automatically generated if they are composites of multiple projections (for example when you use `extend` without the `oldStructureCmd` (does this exist?)).
- Otherwise, the projection of the structure is chosen. For example: `getRawProjections env `Prod` gives the default projections.

      ([u, v], [(`fst, `(Prod.fst.{u v}), [0], true, false),
         (`snd, `(@Prod.snd.{u v}), [1], true, false)])

Optionally, this command accepts three optional arguments:

- If `traceIfExists` the command will always generate a trace message when the structure already has an entry in `structureExt`.
- The `rules` argument specifies whether projections should be added, renamed, used as prefix, and not used by default.
- if `trc` is true, this tactic will trace information just as if `set_option trace.simps.verbose true` was set.

Equations

- One or more equations did not get rendered due to their size.

Instances For

source
def Simps.Mathlib.LibraryNote.«custom simps projection» :
LibraryNote

You can specify custom projections for the `@[simps]` attribute. To do this for the projection `MyStructure.originalProjection` by adding a declaration `MyStructure.Simps.myProjection` that is definitionally equal to `MyStructure.originalProjection` but has the projection in the desired (simp-normal) form. Then you can call

    initialize_simps_projections (originalProjection → myProjection, ...)

to register this projection. See `elabInitializeSimpsProjections` for more information.

You can also specify custom projections that are definitionally equal to a composite of multiple projections. This is often desirable when extending structures (without `oldStructureCmd`).

`CoeFun` and notation class (like `Mul`) instances will be automatically used, if they are definitionally equal to a projection of the structure (but not when they are equal to the composite of multiple projections).

Equations

- Simps.Mathlib.LibraryNote.«custom simps projection» = ()

Instances For

source
def Simps.elabSimpsRule :
Lean.Syntax → Lean.Elab.Command.CommandElabM ProjectionRule

Parse a rule for `initialize_simps_projections`. It is `<name>→<name>`, `-<name>`, `+<name>` or `as_prefix <name>`.

Equations

- One or more equations did not get rendered due to their size.

Instances For

source
def Simps.elabInitializeSimpsProjections :
Lean.Elab.Command.CommandElab

Function elaborating `initialize_simps_projections`.

Equations

- One or more equations did not get rendered due to their size.

Instances For

source
structure Simps.Config :
Type

Configuration options for `@[simps]`

- isSimp : Bool

  Make generated lemmas simp lemmas

- attrs : Array Lean.Syntax

  Other attributes to apply to generated lemmas.

- simpRhs : Bool

  simplify the right-hand side of generated simp-lemmas using `dsimp, simp`.

- typeMd : Lean.Meta.TransparencyMode

  TransparencyMode used to reduce the type in order to detect whether it is a structure.

- rhsMd : Lean.Meta.TransparencyMode

  TransparencyMode used to reduce the right-hand side in order to detect whether it is a constructor. Note: was `none` in Lean 3

- fullyApplied : Bool

  Generated lemmas that are fully applied, i.e. generates equalities between applied functions. Set this to `false` to generate equalities between functions.

- notRecursive : List Lean.Name

  List of types in which we are not recursing to generate simplification lemmas. E.g. if we write `@[simps] def e : α × β ≃ β × α := ...` we will generate `e_apply` and not `e_apply_fst`.

- debug : Bool

  Output debug messages. Not used much, use `set_option simps.debug true` instead.

- nameStem : Option String

  The stem to use for the projection names. If `none`, the default, use the suffix of the current declaration name, or the empty string if the declaration is an instance and the instance is named according to the `inst` convention.

Instances For

source
instance Simps.instInhabitedConfig :
Inhabited Config
Equations

- Simps.instInhabitedConfig = { default := Simps.instInhabitedConfig.default }

source
def Simps.instInhabitedConfig.default :
Config
Equations

- One or more equations did not get rendered due to their size.

Instances For

source
def Simps.elabSimpsConfig :
Lean.Syntax → Lean.Elab.Command.CommandElabM Config

Function elaborating `Config`

Equations

- One or more equations did not get rendered due to their size.

Instances For

source
def Lean.Expr.instantiateLambdasOrApps (es : Array Expr) (e : Expr) :
Expr

`instantiateLambdasOrApps es e` instantiates lambdas in `e` by expressions from `es`. If the length of `es` is larger than the number of lambdas in `e`, then the term is applied to the remaining terms. Also reduces head let-expressions in `e`, including those after instantiating all lambdas.

This is very similar to `expr.substs`, but this also reduces head let-expressions.

Equations

- Lean.Expr.instantiateLambdasOrApps es e = e.betaRev es.reverse true

Instances For

source
def Simps.getProjectionExprs (stx : Lean.Syntax) (tgt rhs : Lean.Expr) (cfg : Config) :
Lean.MetaM (Array (Lean.Expr × ProjectionData))

Get the projections of a structure used by `@[simps]` applied to the appropriate arguments. Returns a list of tuples

    (corresponding right-hand-side, given projection name, projection Expression,
      future projection numbers, used by default, is prefix)

(where all fields except the first are packed in a `ProjectionData` structure) 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. For example, in the structure

Example 1: `getProjectionExprs env `(α × β) `(⟨x, y⟩)` will give the output

      [(`(x), `fst, `(@Prod.fst.{u v} α β), [], true, false),
       (`(y), `snd, `(@Prod.snd.{u v} α β), [], true, false)]

Example 2: `getProjectionExprs env `(α ≃ α) `(⟨id, id, fun _ ↦ rfl, fun _ ↦ rfl⟩)` will give the output

      [(`(id), `apply, (Equiv.toFun), [], true, false),
       (`(id), `symm_apply, (fun e ↦ e.symm.toFun), [], true, false),
       ...,
       ...]

Equations

- One or more equations did not get rendered due to their size.

Instances For

source
def Simps.addProjection (ref : Lean.Syntax) (univs : List Lean.Name) (declName : Lean.Name) (type lhs rhs : Lean.Expr) (args : Array Lean.Expr) (cfg : Config) :
Lean.MetaM Unit

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.

Equations

- One or more equations did not get rendered due to their size.

Instances For

source
partial def Simps.headStructureEtaReduce (e : Lean.Expr) :
Lean.MetaM Lean.Expr

Perform head-structure-eta-reduction on expression `e`. That is, if `e` is of the form `⟨f.1, f.2, ..., f.n⟩` with `f` definitionally equal to `e`, then `headStructureEtaReduce e = headStructureEtaReduce f` and `headStructureEtaReduce e = e` otherwise.

source
partial def Simps.addProjections (ref : Lean.Syntax) (univs : List Lean.Name) (nm : NameStruct✝) (type lhs rhs : Lean.Expr) (args : Array Lean.Expr) (mustBeStr : Bool) (cfg : Config) (todo : List (String × Lean.Syntax)) (toApply : List Nat) :
Lean.MetaM (Array Lean.Name)

Derive lemmas specifying the projections of the declaration. `nm`: name of the lemma If `todo` is non-empty, it will generate exactly the names in `todo`. `toApply` is non-empty after a custom projection that is a composition of multiple projections was just used. In that case we need to apply these projections before we continue changing `lhs`. `simpLemmas`: names of the simp lemmas added so far.(simpLemmas : Array Name)

source
def simpsTac (ref : Lean.Syntax) (nm : Lean.Name) (cfg : Simps.Config := { }) (todo : List (String × Lean.Syntax) := []) (trc : Bool := false) :
Lean.AttrM (Array Lean.Name)

`simpsTac` 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 `shortNm` is true, the generated names will only use the last projection name. If `trc` is true, trace as if `trace.simps.verbose` is true.

Equations

- One or more equations did not get rendered due to their size.

Instances For

source
def simpsTacFromSyntax (nm : Lean.Name) (stx : Lean.Syntax) :
Lean.AttrM (Array Lean.Name)

elaborate the syntax and run `simpsTac`.

Equations

- One or more equations did not get rendered due to their size.

Instances For

source
opaque simpsAttr :
Lean.ParametricAttribute (Array Lean.Name)

The `simps` attribute.