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 simplication lemmas for each projection of the object/instance that contains data. See the doc strings for simps_attr and simps_cfg for more details and configuration options
@[_simps_str] is automatically added to structures that have been used in @[simps] at least once. They contain 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 has_mul and has_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 has_mul is tagged with @[notation_class] then the projection used for semigroup will be λ α hα, @has_mul.mul α (@semigroup.to_has_mul α hα) instead of @semigroup.mul.

Tags

structures, projections, simp, simplifier, generates declarations

source

meta def simps_str_attr :

user_attribute unit (list name × list expr)

The @[_simps_str] attribute specifies the preferred projections of the given structure, used by the @[simps] attribute.

This will usually be tagged by the @[simps] tactic.
You can also generate this with the command initialize_simps_projections.
To change the default value, see Note [custom simps projection].
You are strongly discouraged to add this attribute manually.
The first argument is the list of names of the universe variables used in the structure
The second argument is the expressions that correspond to the projections of the structure (these can contain the universe parameters specified in the first argument).

source

meta def notation_class_attr :

user_attribute unit (bool × option name)

The @[notation_class] attribute specifies that this is a notation class, and this notation should be used instead of projections by @[simps].

The first argument tt for notation classes and ff for classes applied to the structure, like has_coe_to_sort and has_coe_to_fun
The second argument is the name of the projection (by default it is the first projection of the structure)

source

meta def simps_get_raw_projections :

environment → name → tactic (list name × list expr)

Get the projections used by simps associated to a given structure str. The second component is the list of projections, and the first component the (shared) list of universe levels used by the projections. The returned universe levels are the universe levels of the structure. For the projections there are three cases

If the declaration {structure_name}.simps.{projection_name} has been declared, then the value of this declaration is used (after checking that it is definitionally equal to the actual projection
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 has_mul and has_zero those projections are used instead of the corresponding projection
Otherwise, the projection of the structure is chosen. For example: simps_get_raw_projections env `prod gives the default projections lean ([u, v], [prod.fst.{u v}, prod.snd.{u v}]) while simps_get_raw_projections env `equiv gives lean ([u_1, u_2], [λ α β, coe_fn, λ {α β} (e : α ≃ β), ⇑(e.symm), left_inv, right_inv]) after declaring the coercion from equiv to function and adding the declaration lean def equiv.simps.inv_fun {α β} (e : α ≃ β) : β → α := e.symm

source

meta def initialize_simps_projections_cmd :

interactive.parse (lean.parser.tk "initialize_simps_projections") → lean.parser unit

Specify simps projections, see Note [custom simps projection]. Set trace.simps.verbose to true to see the generated projections.

source

meta def simps_get_projection_exprs :

environment → expr → expr → tactic (list (expr × name × expr))

Get the projections of a structure used by @[simps] applied to the appropriate arguments. Returns a list of triples (projection expression, projection name, corresponding right-hand-side), one for each projection.

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

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

source

structure simps_cfg :

Type

attrs : list name
short_name : bool
simp_rhs : bool
type_md : tactic.transparency
rhs_md : tactic.transparency
fully_applied : bool

Configuration options for the @[simps] attribute.

attrs specifies the list of attributes given to the generated lemmas. Default: [`simp]. If [`simp] is in the list, then [`_refl_lemma] is added automatically if appropriate. The attributes can be either basic attributes, or user attributes without parameters.
short_name gives the generated lemmas a shorter name. This only has an effect when multiple projections are applied in a lemma. When this is ff (default) all projection names will be appended to the definition name to form the lemma name, and when this is tt, only the last projection name will be appended.
if simp_rhs is tt then the right-hand-side of the generated lemmas will be put simp-normal form
type_md specifies how aggressively definitions are unfolded in the type of expressions for the purposes of finding out whether the type is a function type. Default: instances. This will unfold coercion instances (so that a coercion to a function type is recognized as a function type), but not declarations like set.
rhs_md specifies how aggressively definition in the declaration are unfolded for the purposes of finding out whether it is a constructor. Default: none
If fully_applied is ff then the generated simp-lemmas will be between non-fully applied terms, i.e. equalities between functions. This does not restrict the recursive behavior of @[simps], so only the "final" projection will be non-fully applied. However, it can be used in combination with explicit field names, to get a partially applied intermediate projection.

source

@[instance]

meta def simps_cfg.has_reflect :

has_reflect simps_cfg

source

@[instance]

def simps_cfg.inhabited :

inhabited simps_cfg

source

meta def simps_add_projection :

name → expr → expr → expr → list expr → list name → simps_cfg → tactic 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. If add_simp then we make the resulting lemma a simp-lemma.

source

meta def simps_add_projections :

environment → name → string → expr → expr → expr → list expr → list name → bool → simps_cfg → list string → tactic unit

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

source

meta def simps_tac :

name → (simps_cfg := {attrs := [name.mk_string "simp" name.anonymous], short_name := ff, simp_rhs := ff, type_md := tactic.transparency.instances, rhs_md := tactic.transparency.none, fully_applied := tt}) → (list string := list.nil) → tactic unit

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.

source

meta def simps_parser :

lean.parser (list string × simps_cfg)

The parser for the @[simps] attribute.

source

meta def simps_attr :

user_attribute unit (list string × simps_cfg)

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.