simps attribute

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. If add_simp then we make the resulting lemma a simp-lemma.

Derive lemmas specifying the projections of the declaration. If todo is non-empty, it will generate exactly the names in todo.

simps_tac 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 short_nm is true, the generated names will only use the last projection name.

The parser for simps. Pattern: 'lemmas_only'? ident*

• Automatically derive lemmas specifying the projections of this declaration.
• Example: (note that the forward and reverse functions are specified differently!)

  @[simps] def refl (α) : α ≃ α := ⟨id, λ x, x, λ x, rfl, λ x, rfl⟩
  
  

  derives two simp-lemmas:

  @[simp] lemma refl_to_fun (α) (x : α) : (refl α).to_fun x = id x
  
  @[simp] lemma refl_inv_fun (α) (x : α) : (refl α).inv_fun x = x
  
  

• It does not derive simp-lemmas for the prop-valued projections.
• It will automatically reduce newly created beta-redexes, but not unfold any definitions.
• If one of the fields itself is a structure, this command will recursively create simp-lemmas for all fields in that structure.
• You can use @[simps proj1 proj2 ...] to only generate the projection lemmas for the specified projections. For example:

  attribute [simps to_fun] refl
  
  

• If one of the values is an eta-expanded structure, we will eta-reduce this structure.
• You can use @[simps lemmas_only] to derive the lemmas, but not mark them as simp-lemmas.
• You can use @[simps short_name] to only use the name of the last projection for the name of the generated lemmas.
• The precise syntax is ('simps' 'lemmas_only'? 'short_name'? ident*).
• 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).