tactic.simps

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

@[protected, instance]
@[protected, instance]
meta structure projection_data  :
Type

Projection data for a single projection of a structure, consisting of the following fields:

• the name used in the generated simp lemmas
• 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 simps_str_attr.
• 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.
• A boolean specifying whether simp lemmas are generated for this projection by default.
• A boolean specifying whether this projection is written as prefix.
meta structure parsed_projection_data  :
Type

Temporary projection data parsed from initialize_simps_projections before the expression matching this projection has been found. Only used internally in simps_get_raw_projections.

@[protected, instance]
@[protected, instance]
def projection_rule  :
Type

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

meta def simps_str_attr  :

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 a list that consists of the projection data for each projection.
meta def notation_class_attr  :

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)
meta def projections_info (l : list projection_data) (pref : string) (str : name) :

Returns the projection information of a structure.

meta def get_composite_of_projections_aux (str : name) (proj : string) (x : expr) (pos : list ) (args : list expr) :

Auxiliary function of get_composite_of_projections.

meta def get_composite_of_projections (str : name) (proj : string) :

Given a structure str and a projection proj, that could be multiple nested projections (separated by _), 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.

meta def simps_get_raw_projections (e : environment) (str : name) (trace_if_exists : bool := ff) (rules : := list.nil) (trc : bool := ff) :

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

The returned information is also stored in a parameter of the attribute @[_simps_str], which is given to str. If str already has this attribute, the information is read from this attribute instead. See the documentation for this attribute 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 {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. 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 has_mul and has_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 old_structure_cmd).
• Otherwise, the projection of the structure is chosen. For example: simps_get_raw_projections env prod gives the default projections
  ([u, v], [prod.fst.{u v}, prod.snd.{u v}])

while simps_get_raw_projections env equiv gives

  ([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

  def equiv.simps.inv_fun {α β} (e : α ≃ β) : β → α := e.symm


Optionally, this command accepts three optional arguments:

• If trace_if_exists the command will always generate a trace message when the structure already has the attribute @[_simps_str].
• The rules argument accepts a list of pairs sum.inl (old_name, new_name). This is used to change the projection name old_name to the custom projection name new_name. Example: for the structure equiv the projection to_fun could be renamed apply. This name will be used for parsing and generating projection names. This argument is ignored if the structure already has an existing attribute. If an element of rules is of the form sum.inr name, this means that the projection name will not be applied by default.
• if trc is true, this tactic will trace information.

Parse a rule for initialize_simps_projections. It is either <name>→<name> or -<name>, possibly following by as_prefix.

meta def initialize_simps_projections_cmd (_x : interactive.parse (lean.parser.tk "initialize_simps_projections")) :

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

• You can specify custom names by writing e.g. initialize_simps_projections equiv (to_fun → apply, inv_fun → symm_apply).
• See Note [custom simps projection] and the examples below for information how to declare custom projections.
• If no custom projection is specified, the projection will be coe_fn/⇑ if a has_coe_to_fun instance has been declared, or the notation of a notation class (like has_mul) if such an instance is available. If none of these cases apply, the projection itself will be used.
• You can disable a projection by default by running initialize_simps_projections equiv (-inv_fun) This will ensure that no simp lemmas are generated for this projection, unless this projection is explicitly specified by the user.
• If you want the projection name added as a prefix in the generated lemma name, you can add the as_prefix modifier: initialize_simps_projections equiv (to_fun → coe as_prefix) 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.
• You can declare a new name for a projection that is the composite of multiple projections, e.g.
  structure A := (proj : ℕ)
structure B extends A
initialize_simps_projections? B (to_A_proj → proj, -to_A)

You can also make your custom projection that is definitionally equal to a composite of projections. In this case, coercions and notation classes are not automatically recognized, and should be manually given by giving a custom projection. This is especially useful when extending a structure (without old_structure_cmd). In the above example, it is desirable to add -to_A, so that @[simps] doesn't automatically apply the B.to_A projection and then recursively the A.proj projection in the lemmas it generates. If you want to get both the foo_proj and foo_to_A simp lemmas, you can use @[simps, simps to_A].
• Running initialize_simps_projections my_struc without arguments is not necessary, it has the same effect if you just add @[simps] to a declaration.
• If you do anything to change the default projections, make sure to call either @[simps] or initialize_simps_projections in the same file as the structure declaration. Otherwise, you might have a file that imports the structure, but not your custom projections.

Some common uses:

• If you define a new homomorphism-like structure (like mul_hom) you can just run initialize_simps_projections after defining the has_coe_to_fun instance
  instance {mM : has_mul M} {mN : has_mul N} : has_coe_to_fun (mul_hom M N) := ...
initialize_simps_projections mul_hom (to_fun → 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 mul_hom (to_fun → coe as_prefix) In this case you have to use @[simps {fully_applied := ff}] or equivalently @[simps as_fn] 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 mul_hom (to_fun → apply, to_fun → coe, -coe as_prefix)
initialize_simps_projections mul_hom (to_fun → apply, to_fun → coe as_prefix, -apply)

In the first case, you can get both lemmas using @[simps, simps coe as_fn] and in the second case you can get both lemmas using @[simps as_fn, simps apply].
• If your new homomorphism-like structure extends another structure (without old_structure_cmd) (like rel_embedding), then you have to specify explicitly that you want to use a coercion as a custom projection. For example
  def rel_embedding.simps.apply (h : r ↪r s) : α → β := h
initialize_simps_projections rel_embedding (to_embedding_to_fun → apply, -to_embedding)

• 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 (to_fun → apply, inv_fun → symm_apply)

structure simps_cfg  :
Type

Configuration options for the @[simps] attribute.

• attrs specifies the list of attributes given to the generated lemmas. Default: [simp]. The attributes can be either basic attributes, or user attributes without parameters. There are two attributes which simps might add itself:
• If [simp] is in the list, then [_refl_lemma] is added automatically if appropriate.
• If the definition is marked with @[to_additive ...] then all generated lemmas are marked with @[to_additive]. This is governed by the add_additive configuration option.
• if simp_rhs is tt then the right-hand-side of the generated lemmas will be put in simp-normal form. More precisely: dsimp, simp will be called on all these expressions. See note [dsimp, simp].
• 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 Exception: @[simps] will automatically add the options {rhs_md := semireducible, simp_rhs := tt} if the given definition is not a constructor with the given reducibility setting for rhs_md.
• 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.
• The option not_recursive contains the list of names of types for which @[simps] doesn't recursively apply projections. For example, given an equivalence α × β ≃ β × α one usually wants to only apply the projections for equiv, and not also those for ×. This option is only relevant if no explicit projection names are given as argument to @[simps].
• The option trace is set to tt when you write @[simps?]. In this case, the attribute will print all generated lemmas. It is almost the same as setting the option trace.simps.verbose, except that it doesn't print information about the found projections.
• if add_additive is some nm then @[to_additive] is added to the generated lemma. This option is automatically set to tt when the original declaration was tagged with @[to_additive, simps] (in that order), where nm is the additive name of the original declaration.
@[protected, instance]
@[protected, instance]
def as_fn  :

A common configuration for @[simps]: generate equalities between functions instead equalities between fully applied expressions.

Equations

A common configuration for @[simps]: don't tag the generated lemmas with @[simp].

Equations
meta def simps_get_projection_exprs (e : environment) (tgt rhs : expr) (cfg : simps_cfg) :

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, projection numbers,
used by default, is prefix)


(where all fields except the first are packed in a projection_data 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: simps_get_projection_exprs env (α × β) (⟨x, y⟩) will give the output

  [((x), fst, (@prod.fst.{u v} α β), [0], tt, ff),
((y), snd, (@prod.snd.{u v} α β), [1], tt, ff)]


Example 2: simps_get_projection_exprs env (α ≃ α) (⟨id, id, λ _, rfl, λ _, rfl⟩) will give the output

  [((id), apply, (coe), [0], tt, ff),
((id), symm_apply, (λ f, ⇑f.symm), [1], tt, ff),
...,
...]

meta def simps_add_projection (nm : name) (type lhs rhs : expr) (args : list expr) (univs : list name) (cfg : simps_cfg) :

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.

meta def simps_add_projections (e : environment) (nm : name) (type lhs rhs : expr) (args : list expr) (univs : list name) (must_be_str : bool) (cfg : simps_cfg) (todo : list string) (to_apply : list ) :

Derive lemmas specifying the projections of the declaration. If todo is non-empty, it will generate exactly the names in todo. to_apply 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.

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. If trc is true, trace as if trace.simps.verbose is true.

meta def simps_parser  :

The parser for the @[simps] attribute.

meta def simps_attr  :

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

• You can specify custom projection names, by specifying the new projection names using initialize_simps_projections. Example: initialize_simps_projections equiv (to_fun → apply, inv_fun → symm_apply). See initialize_simps_projections_cmd 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_cfg.not_recursive to override this behavior.

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:

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


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_cfg.

• The precise syntax is ('simps' ident* e), where e is an expression of type simps_cfg.

• @[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?], except that in this case it will not print projection information.

• Use @[to_additive, simps] to apply both to_additive and simps to a definition, making sure that simps comes after to_additive. This will also generate the additive versions of all simp` lemmas.