# Documentation

Mathlib.Tactic.Simps.Basic

# 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α)↦ @Mul.mul α (@Semigroup.toMul α hα) instead of @Semigroup.mul. [this is not correctly implemented in Lean 4 yet]

## Unimplemented Features #

• Correct interaction with heterogenous operations like HAdd and HMul
• Adding custom simp-attributes / other attributes

### Improvements #

• If multiple declarations are generated from a simps without explicit projection names, then only the first one is shown when mousing over simps.
• Double check output of simps (especially in combination with to_additive).

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

def updateName (nm : Lean.Name) (s : String) (isPrefix : Bool) :

updateName nm s isPrefix adds s to the last component of nm, either as prefix or as suffix (specified by isPrefix), separated by _. Used by simps_add_projections.

Equations
def Lean.Meta.mkSimpContextResult (cfg : optParam Lean.Meta.Simp.Config { maxSteps := Lean.Meta.Simp.defaultMaxSteps, maxDischargeDepth := 2, contextual := false, memoize := true, singlePass := false, zeta := true, beta := true, eta := true, etaStruct := Lean.Meta.EtaStructMode.all, iota := true, proj := true, decide := true, arith := false, autoUnfold := false, dsimp := true }) (simpOnly : ) (hasStar : ) :

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.
def Lean.Meta.mkSimpContext (cfg : optParam Lean.Meta.Simp.Config { maxSteps := Lean.Meta.Simp.defaultMaxSteps, maxDischargeDepth := 2, contextual := false, memoize := true, singlePass := false, zeta := true, beta := true, eta := true, etaStruct := Lean.Meta.EtaStructMode.all, iota := true, proj := true, decide := true, arith := false, autoUnfold := false, dsimp := true }) (simpOnly : ) (hasStar : ) :

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

Tests whether declName has the @[simp] attribute in env.

Equations

Declare notation classes.

arguments to @[simps] attribute.

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

The @[simps] attribute automatically derives lemmas specifying the projections of this declaration.

Example:

@[simps] def foo : ℕ × ℤ := (1, 2)
× ℤ := (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, then this notation is used instead of the corresponding projection. [TODO: not yet implemented for heterogenous operations like HMul and HAdd]

• 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⟩
≃ β) : β → α := e.symm
@[simps] def Equiv.trans (e₁ : α ≃ β) (e₂ : β ≃ γ) : α ≃ γ :=
⟨e₂ ∘ e₁, e₁.symm ∘ e₂.symm⟩
→ α := e.symm
@[simps] def Equiv.trans (e₁ : α ≃ β) (e₂ : β ≃ γ) : α ≃ γ :=
⟨e₂ ∘ e₁, e₁.symm ∘ e₂.symm⟩
≃ β) (e₂ : β ≃ γ) : α ≃ γ :=
⟨e₂ ∘ e₁, e₁.symm ∘ e₂.symm⟩
≃ γ) : α ≃ γ :=
⟨e₂ ∘ e₁, e₁.symm ∘ e₂.symm⟩
≃ γ :=
⟨e₂ ∘ e₁, e₁.symm ∘ e₂.symm⟩
∘ e₁, e₁.symm ∘ 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
∀ {α β γ} (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
⇑(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
⇑e₂ ∘ ⇑e₁) a
@[simp] lemma Equiv.trans_invFun : ∀ {α β γ} (e₁ e₂) (a : γ),
⇑((e₁.trans e₂).symm) a = (⇑(e₁.symm) ∘ ⇑(e₂.symm)) a
∘ ⇑e₁) a
@[simp] lemma Equiv.trans_invFun : ∀ {α β γ} (e₁ e₂) (a : γ),
⇑((e₁.trans e₂).symm) a = (⇑(e₁.symm) ∘ ⇑(e₂.symm)) a
⇑e₁) a
@[simp] lemma Equiv.trans_invFun : ∀ {α β γ} (e₁ e₂) (a : γ),
⇑((e₁.trans e₂).symm) a = (⇑(e₁.symm) ∘ ⇑(e₂.symm)) a
∀ {α β γ} (e₁ e₂) (a : γ),
⇑((e₁.trans e₂).symm) a = (⇑(e₁.symm) ∘ ⇑(e₂.symm)) a
⇑((e₁.trans e₂).symm) a = (⇑(e₁.symm) ∘ ⇑(e₂.symm)) a
⇑(e₁.symm) ∘ ⇑(e₂.symm)) a
∘ ⇑(e₂.symm)) a
⇑(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)→ apply, invFun → symm_apply)→ 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 and PProd. 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⟩
× 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⟩
× 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}

• [TODO] 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 }
≃ β 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
∀ {α : Sort*}, bar.toEquiv = Equiv.refl α
@[simp] lemma bar_data : ∀ {α : Sort*}, bar.data = true
∀ {α : Sort*}, bar.data = true


This is true, even though Lean inserts an eta-expanded version of Equiv.refl α in the definition of bar.

• For configuration options, see the doc string of Simps.Config.

• The precise syntax is simps (config := e)? ident*, where e : Expr is an expression of type Simps.Config and ident* is a list of desired projection names.

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

The @[simps] attribute automatically derives lemmas specifying the projections of this declaration.

Example:

@[simps] def foo : ℕ × ℤ := (1, 2)
× ℤ := (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, then this notation is used instead of the corresponding projection. [TODO: not yet implemented for heterogenous operations like HMul and HAdd]

• 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⟩
≃ β) : β → α := e.symm
@[simps] def Equiv.trans (e₁ : α ≃ β) (e₂ : β ≃ γ) : α ≃ γ :=
⟨e₂ ∘ e₁, e₁.symm ∘ e₂.symm⟩
→ α := e.symm
@[simps] def Equiv.trans (e₁ : α ≃ β) (e₂ : β ≃ γ) : α ≃ γ :=
⟨e₂ ∘ e₁, e₁.symm ∘ e₂.symm⟩
≃ β) (e₂ : β ≃ γ) : α ≃ γ :=
⟨e₂ ∘ e₁, e₁.symm ∘ e₂.symm⟩
≃ γ) : α ≃ γ :=
⟨e₂ ∘ e₁, e₁.symm ∘ e₂.symm⟩
≃ γ :=
⟨e₂ ∘ e₁, e₁.symm ∘ e₂.symm⟩
∘ e₁, e₁.symm ∘ 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
∀ {α β γ} (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
⇑(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
⇑e₂ ∘ ⇑e₁) a
@[simp] lemma Equiv.trans_invFun : ∀ {α β γ} (e₁ e₂) (a : γ),
⇑((e₁.trans e₂).symm) a = (⇑(e₁.symm) ∘ ⇑(e₂.symm)) a
∘ ⇑e₁) a
@[simp] lemma Equiv.trans_invFun : ∀ {α β γ} (e₁ e₂) (a : γ),
⇑((e₁.trans e₂).symm) a = (⇑(e₁.symm) ∘ ⇑(e₂.symm)) a
⇑e₁) a
@[simp] lemma Equiv.trans_invFun : ∀ {α β γ} (e₁ e₂) (a : γ),
⇑((e₁.trans e₂).symm) a = (⇑(e₁.symm) ∘ ⇑(e₂.symm)) a
∀ {α β γ} (e₁ e₂) (a : γ),
⇑((e₁.trans e₂).symm) a = (⇑(e₁.symm) ∘ ⇑(e₂.symm)) a
⇑((e₁.trans e₂).symm) a = (⇑(e₁.symm) ∘ ⇑(e₂.symm)) a
⇑(e₁.symm) ∘ ⇑(e₂.symm)) a
∘ ⇑(e₂.symm)) a
⇑(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)→ apply, invFun → symm_apply)→ 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 and PProd. 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⟩
× 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⟩
× 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}

• [TODO] 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 }
≃ β 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
∀ {α : Sort*}, bar.toEquiv = Equiv.refl α
@[simp] lemma bar_data : ∀ {α : Sort*}, bar.data = true
∀ {α : Sort*}, bar.data = true


This is true, even though Lean inserts an eta-expanded version of Equiv.refl α in the definition of bar.

• For configuration options, see the doc string of Simps.Config.

• The precise syntax is simps (config := e)? ident*, where e : Expr is an expression of type Simps.Config and ident* is a list of desired projection names.

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

The @[simps] attribute automatically derives lemmas specifying the projections of this declaration.

Example:

@[simps] def foo : ℕ × ℤ := (1, 2)
× ℤ := (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, then this notation is used instead of the corresponding projection. [TODO: not yet implemented for heterogenous operations like HMul and HAdd]

• 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⟩
≃ β) : β → α := e.symm
@[simps] def Equiv.trans (e₁ : α ≃ β) (e₂ : β ≃ γ) : α ≃ γ :=
⟨e₂ ∘ e₁, e₁.symm ∘ e₂.symm⟩
→ α := e.symm
@[simps] def Equiv.trans (e₁ : α ≃ β) (e₂ : β ≃ γ) : α ≃ γ :=
⟨e₂ ∘ e₁, e₁.symm ∘ e₂.symm⟩
≃ β) (e₂ : β ≃ γ) : α ≃ γ :=
⟨e₂ ∘ e₁, e₁.symm ∘ e₂.symm⟩
≃ γ) : α ≃ γ :=
⟨e₂ ∘ e₁, e₁.symm ∘ e₂.symm⟩
≃ γ :=
⟨e₂ ∘ e₁, e₁.symm ∘ e₂.symm⟩
∘ e₁, e₁.symm ∘ 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
∀ {α β γ} (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
⇑(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
⇑e₂ ∘ ⇑e₁) a
@[simp] lemma Equiv.trans_invFun : ∀ {α β γ} (e₁ e₂) (a : γ),
⇑((e₁.trans e₂).symm) a = (⇑(e₁.symm) ∘ ⇑(e₂.symm)) a
∘ ⇑e₁) a
@[simp] lemma Equiv.trans_invFun : ∀ {α β γ} (e₁ e₂) (a : γ),
⇑((e₁.trans e₂).symm) a = (⇑(e₁.symm) ∘ ⇑(e₂.symm)) a
⇑e₁) a
@[simp] lemma Equiv.trans_invFun : ∀ {α β γ} (e₁ e₂) (a : γ),
⇑((e₁.trans e₂).symm) a = (⇑(e₁.symm) ∘ ⇑(e₂.symm)) a
∀ {α β γ} (e₁ e₂) (a : γ),
⇑((e₁.trans e₂).symm) a = (⇑(e₁.symm) ∘ ⇑(e₂.symm)) a
⇑((e₁.trans e₂).symm) a = (⇑(e₁.symm) ∘ ⇑(e₂.symm)) a
⇑(e₁.symm) ∘ ⇑(e₂.symm)) a
∘ ⇑(e₂.symm)) a
⇑(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)→ apply, invFun → symm_apply)→ 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 and PProd. 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⟩
× 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⟩
× 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}

• [TODO] 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 }
≃ β 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
∀ {α : Sort*}, bar.toEquiv = Equiv.refl α
@[simp] lemma bar_data : ∀ {α : Sort*}, bar.data = true
∀ {α : Sort*}, bar.data = true


This is true, even though Lean inserts an eta-expanded version of Equiv.refl α in the definition of bar.

• For configuration options, see the doc string of Simps.Config.

• The precise syntax is simps (config := e)? ident*, where e : Expr is an expression of type Simps.Config and ident* is a list of desired projection names.

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

The @[simps] attribute automatically derives lemmas specifying the projections of this declaration.

Example:

@[simps] def foo : ℕ × ℤ := (1, 2)
× ℤ := (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, then this notation is used instead of the corresponding projection. [TODO: not yet implemented for heterogenous operations like HMul and HAdd]

• 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⟩
≃ β) : β → α := e.symm
@[simps] def Equiv.trans (e₁ : α ≃ β) (e₂ : β ≃ γ) : α ≃ γ :=
⟨e₂ ∘ e₁, e₁.symm ∘ e₂.symm⟩
→ α := e.symm
@[simps] def Equiv.trans (e₁ : α ≃ β) (e₂ : β ≃ γ) : α ≃ γ :=
⟨e₂ ∘ e₁, e₁.symm ∘ e₂.symm⟩
≃ β) (e₂ : β ≃ γ) : α ≃ γ :=
⟨e₂ ∘ e₁, e₁.symm ∘ e₂.symm⟩
≃ γ) : α ≃ γ :=
⟨e₂ ∘ e₁, e₁.symm ∘ e₂.symm⟩
≃ γ :=
⟨e₂ ∘ e₁, e₁.symm ∘ e₂.symm⟩
∘ e₁, e₁.symm ∘ 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
∀ {α β γ} (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
⇑(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
⇑e₂ ∘ ⇑e₁) a
@[simp] lemma Equiv.trans_invFun : ∀ {α β γ} (e₁ e₂) (a : γ),
⇑((e₁.trans e₂).symm) a = (⇑(e₁.symm) ∘ ⇑(e₂.symm)) a
∘ ⇑e₁) a
@[simp] lemma Equiv.trans_invFun : ∀ {α β γ} (e₁ e₂) (a : γ),
⇑((e₁.trans e₂).symm) a = (⇑(e₁.symm) ∘ ⇑(e₂.symm)) a
⇑e₁) a
@[simp] lemma Equiv.trans_invFun : ∀ {α β γ} (e₁ e₂) (a : γ),
⇑((e₁.trans e₂).symm) a = (⇑(e₁.symm) ∘ ⇑(e₂.symm)) a
∀ {α β γ} (e₁ e₂) (a : γ),
⇑((e₁.trans e₂).symm) a = (⇑(e₁.symm) ∘ ⇑(e₂.symm)) a
⇑((e₁.trans e₂).symm) a = (⇑(e₁.symm) ∘ ⇑(e₂.symm)) a
⇑(e₁.symm) ∘ ⇑(e₂.symm)) a
∘ ⇑(e₂.symm)) a
⇑(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)→ apply, invFun → symm_apply)→ 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 and PProd. 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⟩
× 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⟩
× 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}

• [TODO] 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 }
≃ β 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
∀ {α : Sort*}, bar.toEquiv = Equiv.refl α
@[simp] lemma bar_data : ∀ {α : Sort*}, bar.data = true
∀ {α : Sort*}, bar.data = true


This is true, even though Lean inserts an eta-expanded version of Equiv.refl α in the definition of bar.

• For configuration options, see the doc string of Simps.Config.

• The precise syntax is simps (config := e)? ident*, where e : Expr is an expression of type Simps.Config and ident* is a list of desired projection names.

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

The @[simps] attribute automatically derives lemmas specifying the projections of this declaration.

Example:

@[simps] def foo : ℕ × ℤ := (1, 2)
× ℤ := (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, then this notation is used instead of the corresponding projection. [TODO: not yet implemented for heterogenous operations like HMul and HAdd]

• 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⟩
≃ β) : β → α := e.symm
@[simps] def Equiv.trans (e₁ : α ≃ β) (e₂ : β ≃ γ) : α ≃ γ :=
⟨e₂ ∘ e₁, e₁.symm ∘ e₂.symm⟩
→ α := e.symm
@[simps] def Equiv.trans (e₁ : α ≃ β) (e₂ : β ≃ γ) : α ≃ γ :=
⟨e₂ ∘ e₁, e₁.symm ∘ e₂.symm⟩
≃ β) (e₂ : β ≃ γ) : α ≃ γ :=
⟨e₂ ∘ e₁, e₁.symm ∘ e₂.symm⟩
≃ γ) : α ≃ γ :=
⟨e₂ ∘ e₁, e₁.symm ∘ e₂.symm⟩
≃ γ :=
⟨e₂ ∘ e₁, e₁.symm ∘ e₂.symm⟩
∘ e₁, e₁.symm ∘ 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
∀ {α β γ} (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
⇑(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
⇑e₂ ∘ ⇑e₁) a
@[simp] lemma Equiv.trans_invFun : ∀ {α β γ} (e₁ e₂) (a : γ),
⇑((e₁.trans e₂).symm) a = (⇑(e₁.symm) ∘ ⇑(e₂.symm)) a
∘ ⇑e₁) a
@[simp] lemma Equiv.trans_invFun : ∀ {α β γ} (e₁ e₂) (a : γ),
⇑((e₁.trans e₂).symm) a = (⇑(e₁.symm) ∘ ⇑(e₂.symm)) a
⇑e₁) a
@[simp] lemma Equiv.trans_invFun : ∀ {α β γ} (e₁ e₂) (a : γ),
⇑((e₁.trans e₂).symm) a = (⇑(e₁.symm) ∘ ⇑(e₂.symm)) a
∀ {α β γ} (e₁ e₂) (a : γ),
⇑((e₁.trans e₂).symm) a = (⇑(e₁.symm) ∘ ⇑(e₂.symm)) a
⇑((e₁.trans e₂).symm) a = (⇑(e₁.symm) ∘ ⇑(e₂.symm)) a
⇑(e₁.symm) ∘ ⇑(e₂.symm)) a
∘ ⇑(e₂.symm)) a
⇑(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)→ apply, invFun → symm_apply)→ 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 and PProd. 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⟩
× 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⟩
× 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}

• [TODO] 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 }
≃ β 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
∀ {α : Sort*}, bar.toEquiv = Equiv.refl α
@[simp] lemma bar_data : ∀ {α : Sort*}, bar.data = true
∀ {α : Sort*}, bar.data = true


This is true, even though Lean inserts an eta-expanded version of Equiv.refl α in the definition of bar.

• For configuration options, see the doc string of Simps.Config.

• The precise syntax is simps (config := e)? ident*, where e : Expr is an expression of type Simps.Config and ident* is a list of desired projection names.

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

Linter to check that simps! is used when needed

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

Syntax for renaming a projection in initialize_simps_projections.

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

Syntax for making a projection non-default in initialize_simps_projections.

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

Syntax for making a projection default in initialize_simps_projections.

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

Syntax for making a projection prefix.

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

Syntax for a single rule in initialize_simps_projections.

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

Syntax for initialize_simps_projections.

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

This command specifies custom names and custom projections for the simp attribute simpsAttr.

• You can specify custom names by writing e.g. initialize_simps_projections Equiv (toFun → apply, invFun → symm_apply)→ apply, invFun → symm_apply)→ symm_apply).
• See Note [custom simps projection] and the examples below for information how to declare custom projections.
• TODO in Lean 4: 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).
• You can disable a projection by default by running initialize_simps_projections Equiv (-invFun) This will ensure that no simp lemmas are generated for this projection, unless this projection is explicitly specified by the user.
• Conversely, you can enable a projection by default by running initialize_simps_projections Equiv (+toEquiv).
• If you want the projection name added as a prefix in the generated lemma name, you can use as_prefix fieldName: initialize_simps_projections Equiv (toFun → coe, as_prefix coe)→ 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.
• Run initialize_simps_projections? (or set_option trace.simps.verbose true) to see the generated projections.
• Running initialize_simps_projections MyStruc 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 FunLike instance (or instance that implies a FunLike instance).
  instance {mM : Mul M} {mN : Mul N} : FunLike (MulHom M N) M N := ...
initialize_simps_projections MulHom (toFun → apply)
→ 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)→ coe, as_prefix coe) In this case you have to use @[simps (config := {fullyApplied := false})] or equivalently @[simps (config := .asFn)] 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)
→ apply, toFun → coe, as_prefix coe, -coe)
initialize_simps_projections MulHom (toFun → apply, toFun → coe, as_prefix coe, -apply)
→ coe, as_prefix coe, -coe)
initialize_simps_projections MulHom (toFun → apply, toFun → coe, as_prefix coe, -apply)
→ apply, toFun → coe, as_prefix coe, -apply)
→ coe, as_prefix coe, -apply)

In the first case, you can get both lemmas using @[simps, simps (config := .asFn) coe] and in the second case you can get both lemmas using @[simps (config := .asFn), simps apply].
• If you declare a new homomorphism-like structure (like RelEmbedding), then initialize_simps_projections will automatically find any FunLike coercions that will be used as the default projection for the toFun field.
  initialize_simps_projections relEmbedding (toFun → apply)
→ 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)
≃ β) : β → α := e.symm
initialize_simps_projections Equiv (toFun → apply, invFun → symm_apply)
→ α := e.symm
initialize_simps_projections Equiv (toFun → apply, invFun → symm_apply)
→ apply, invFun → symm_apply)
→ symm_apply)

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

This command specifies custom names and custom projections for the simp attribute simpsAttr.

• You can specify custom names by writing e.g. initialize_simps_projections Equiv (toFun → apply, invFun → symm_apply)→ apply, invFun → symm_apply)→ symm_apply).
• See Note [custom simps projection] and the examples below for information how to declare custom projections.
• TODO in Lean 4: 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).
• You can disable a projection by default by running initialize_simps_projections Equiv (-invFun) This will ensure that no simp lemmas are generated for this projection, unless this projection is explicitly specified by the user.
• Conversely, you can enable a projection by default by running initialize_simps_projections Equiv (+toEquiv).
• If you want the projection name added as a prefix in the generated lemma name, you can use as_prefix fieldName: initialize_simps_projections Equiv (toFun → coe, as_prefix coe)→ 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.
• Run initialize_simps_projections? (or set_option trace.simps.verbose true) to see the generated projections.
• Running initialize_simps_projections MyStruc 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 FunLike instance (or instance that implies a FunLike instance).
  instance {mM : Mul M} {mN : Mul N} : FunLike (MulHom M N) M N := ...
initialize_simps_projections MulHom (toFun → apply)
→ 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)→ coe, as_prefix coe) In this case you have to use @[simps (config := {fullyApplied := false})] or equivalently @[simps (config := .asFn)] 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)
→ apply, toFun → coe, as_prefix coe, -coe)
initialize_simps_projections MulHom (toFun → apply, toFun → coe, as_prefix coe, -apply)
→ coe, as_prefix coe, -coe)
initialize_simps_projections MulHom (toFun → apply, toFun → coe, as_prefix coe, -apply)
→ apply, toFun → coe, as_prefix coe, -apply)
→ coe, as_prefix coe, -apply)

In the first case, you can get both lemmas using @[simps, simps (config := .asFn) coe] and in the second case you can get both lemmas using @[simps (config := .asFn), simps apply].
• If you declare a new homomorphism-like structure (like RelEmbedding), then initialize_simps_projections will automatically find any FunLike coercions that will be used as the default projection for the toFun field.
  initialize_simps_projections relEmbedding (toFun → apply)
→ 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)
≃ β) : β → α := e.symm
initialize_simps_projections Equiv (toFun → apply, invFun → symm_apply)
→ α := e.symm
initialize_simps_projections Equiv (toFun → apply, invFun → symm_apply)
→ apply, invFun → symm_apply)
→ symm_apply)

Equations
• One or more equations did not get rendered due to their size.
• The name used in the generated simp lemmas

name : Lean.Name
• 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.

expr : Lean.Expr
• 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.

projNrs :
• A boolean specifying whether simp lemmas are generated for this projection by default.

isDefault : Bool
• A boolean specifying whether this projection is written as prefix.

isPrefix : Bool

Projection data for a single projection of a structure

Instances For
Equations
Equations
• One or more equations did not get rendered due to their size.

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.
• name for this projection used in the structure definition

strName : Lean.Name
• syntax that might have provided strName

strStx : Lean.Syntax
• name for this projection used in the generated simp lemmas

newName : Lean.Name
• syntax that provided newName

newStx : Lean.Syntax
• will simp lemmas be generated for with (without specifically naming this?)

isDefault : Bool
• is the projection name a prefix?

isPrefix : Bool
• projection expression

expr? :
• the list of projection numbers this expression corresponds to

projNrs :
• is this a projection that is changed by the user?

isCustom : Bool

Projection data used internally in getRawProjections.

Instances For

Turn ParsedProjectionData into ProjectionData.

Equations
• = { name := p.newName, expr := Option.getD p.expr? default, projNrs := Array.toList p.projNrs, isDefault := p.isDefault, isPrefix := p.isPrefix }
Equations
• One or more equations did not get rendered due to their size.
• A renaming rule before→after→after or Each name comes with the syntax used to write the rule, which is used to declare hover information.

rename:
• A adding rule +fieldName

• A hiding rule -fieldName

erase:
• A prefix rule prefix fieldName

prefix:

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

Instances For
Equations
• One or more equations did not get rendered due to their size.

Returns the projection information of a structure.

Equations
• One or more equations did not get rendered due to their size.
def Simps.findProjectionIndices (strName : Lean.Name) (projName : Lean.Name) :

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.
partial def Simps.getCompositeOfProjectionsAux (stx : Lean.Syntax) (proj : String) (e : Lean.Expr) (pos : ) (args : ) :

Auxiliary function of getCompositeOfProjections.

def Simps.getCompositeOfProjections (structName : Lean.Name) (proj : String) (stx : Lean.Syntax) :

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)
→ Type _) where
toFun := ∀ i j, A i →+ A j →+ A (i + j)
initialize_simps_projections (toFun_toFun_toFun → myMul)
∀ i j, A i →+ A j →+ A (i + j)
initialize_simps_projections (toFun_toFun_toFun → myMul)
→+ A j →+ A (i + j)
initialize_simps_projections (toFun_toFun_toFun → myMul)
→+ A (i + j)
initialize_simps_projections (toFun_toFun_toFun → myMul)
→ myMul)


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

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

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.

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.
def Simps.findProjection (str : Lean.Name) (proj : Simps.ParsedProjectionData) (rawUnivs : ) :

Auxilliary 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.
def Simps.checkForUnusedCustomProjs (stx : Lean.Syntax) (str : Lean.Name) (projs : ) :

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.

Data about default coercions. An entry consists of (projName, (className, functionName, arity)), where

• projName is the name of a projection in a structure that must be used to trigger the search for a coercion as projection.
• className is the name of the class we are looking for
• functionName is the function that we are using for a coercion as projection (this is typically the first field of className).
• arity is the number of arguments of className.
Equations

Auxilliary function for getRawProjections. Find custom projections, automatically found by simps. These come from FunLike and SetLike instances. Todo: also support algebraic operations and notation classes, like +.

Equations
• One or more equations did not get rendered due to their size.
def Simps.getRawProjections (stx : Lean.Syntax) (str : Lean.Name) (traceIfExists : ) (rules : ) (trc : ) :

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.

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.

Function elaborating initialize_simps_projections.

Equations
• One or more equations did not get rendered due to their size.
structure Simps.Config :
• Make generated lemmas simp lemmas

isSimp : Bool
• Other simp-attributes to apply to generated lemmas. Attributes that are currently not simp-attributes are not supported.

attrs :
• simplify the right-hand side of generated simp-lemmas using dsimp, simp.

simpRhs : Bool
• TransparencyMode used to reduce the type in order to detect whether it is a structure.

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

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

fullyApplied : Bool
• 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.

notRecursive :
• Output debug messages. Not used much, use set_option simps.debug true instead.

debug : Bool

Configuration options for @[simps]

Instances For
Equations
• One or more equations did not get rendered due to their size.

Function elaborating Config

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

A common configuration for @[simps]: generate equalities between functions instead equalities between fully applied Expressions. Use this using @[simps (config := .asFn)].

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

A common configuration for @[simps]: don't tag the generated lemmas with @[simp]. Use this using @[simps (config := .lemmasOnly)].

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

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

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⟩)× β) (⟨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⟩)≃ α) (⟨id, id, fun _ ↦ rfl, fun _ ↦ rfl⟩)↦ rfl, fun _ ↦ rfl⟩)↦ rfl⟩) will give the output

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

Equations
• One or more equations did not get rendered due to their size.
def Simps.addProjection (ref : Lean.Syntax) (univs : ) (declName : Lean.Name) (type : Lean.Expr) (lhs : Lean.Expr) (rhs : Lean.Expr) (args : ) (cfg : Simps.Config) :

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.

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.

partial def Simps.addProjections (ref : Lean.Syntax) (univs : ) (nm : Lean.Name) (type : Lean.Expr) (lhs : Lean.Expr) (rhs : Lean.Expr) (args : ) (mustBeStr : Bool) (cfg : Simps.Config) (todo : ) (toApply : ) :

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)

def simpsTac (ref : Lean.Syntax) (nm : Lean.Name) (cfg : optParam Simps.Config { isSimp := true, attrs := [], simpRhs := false, typeMd := Lean.Meta.TransparencyMode.instances, rhsMd := Lean.Meta.TransparencyMode.reducible, fullyApplied := true, notRecursive := [Prod, PProd], debug := false }) (todo : optParam () []) (trc : ) :

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.

elaborate the syntax and run simpsTac.

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

The simps attribute.