simps

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

Example:

@[simps] def foo : ℕ × ℤ := (1, 2)

derives two simp-lemmas:

@[simp] lemma foo_fst : foo.fst = 1
@[simp] lemma foo_snd : foo.snd = 2

• It does not derive simp-lemmas for the prop-valued projections.
• It will automatically reduce newly created beta-redexes, but will not unfold any definitions.
• If the structure has a coercion to either sorts or functions, and this is defined to be one of the projections, then this coercion will be used instead of the projection.
• If the structure is a class that has an instance to a notation class, like has_mul, then this notation is used instead of the corresponding projection.

• You can specify custom projections, by giving a declaration with name {structure_name}.simps.{projection_name}. See Note [custom simps projection].

  Example:

  def equiv.simps.inv_fun (e : α ≃ β) : β → α := e.symm
  @[simps] def equiv.trans (e₁ : α ≃ β) (e₂ : β ≃ γ) : α ≃ γ :=
  ⟨e₂ ∘ e₁, e₁.symm ∘ e₂.symm⟩
  

  generates

  @[simp] lemma equiv.trans_to_fun : ∀ {α β γ} (e₁ e₂) (a : α), ⇑(e₁.trans e₂) a = (⇑e₂ ∘ ⇑e₁) a
  @[simp] lemma equiv.trans_inv_fun : ∀ {α β γ} (e₁ e₂) (a : γ),
  ⇑((e₁.trans e₂).symm) a = (⇑(e₁.symm) ∘ ⇑(e₂.symm)) a
  

• 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. Give explicit projection names to override this.

  Example:

  structure my_prod (α β : Type*) := (fst : α) (snd : β)
  @[simps] def foo : prod ℕ ℕ × my_prod ℕ ℕ := ⟨⟨1, 2⟩, 3, 4⟩
  

  generates

  @[simp] lemma  foo_fst : foo.fst = (1, 2)
  @[simp] lemma foo_snd_fst : foo.snd.fst = 3
  @[simp] lemma foo_snd_snd : foo.snd.snd = 4
  

• 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 my_prod (α β : Type*) := (fst : α) (snd : β)
  @[simps fst fst_fst snd] def foo : prod ℕ ℕ × my_prod ℕ ℕ := ⟨⟨1, 2⟩, 3, 4⟩
  

  generates

  @[simp] lemma foo_fst : foo.fst = (1, 2)
  @[simp] lemma foo_fst_fst : foo.fst.fst = 1
  @[simp] lemma foo_snd : foo.snd = {fst := 3, snd := 4}
  

• If one of the values is an eta-expanded structure, we will eta-reduce this structure.

  Example:

  structure equiv_plus_data (α β) extends α ≃ β := (data : bool)
  @[simps] def bar {α} : equiv_plus_data α α := { data := tt, ..equiv.refl α }
  

  generates the following, even though Lean inserts an eta-expanded version of equiv.refl α in the definition of bar:

  @[simp] lemma bar_to_equiv : ∀ {α : Sort u_1}, bar.to_equiv = equiv.refl α
  @[simp] lemma bar_data : ∀ {α : Sort u_1}, bar.data = tt
  

• For configuration options, see the doc string of simps_cfg.
• The precise syntax is ('simps' ident* e), where e is an expression of type simps_cfg.
• If one of the projections is marked as a coercion, the generated lemmas do not use this coercion.
• @[simps] reduces let-expressions where necessary.
• If one of the fields is a partially applied constructor, we will eta-expand it (this likely never happens).
• When option trace.simps.verbose is true, simps will print the projections it finds and the lemmas it generates.