mathlib3 documentation

tactic.mk_simp_attribute

User command to register simp attributes #

In this file we define a command mk_simp_attribute that can be used to register simp sets. We also define all simp attributes that are used in the library and tag lemmas from Lean core with these attributes.

User command #

source
meta def tactic.mk_simp_attribute_cmd (_x : interactive.parse (lean.parser.tk "mk_simp_attribute")) :
lean.parser unit

The command mk_simp_attribute simp_name "description" creates a simp set with name simp_name. Lemmas tagged with @[simp_name] will be included when simp with simp_name is called. mk_simp_attribute simp_name none will use a default description.

Appending the command with with attr1 attr2 ... will include all declarations tagged with attr1, attr2, ... in the new simp set.

This command is preferred to using run_cmd mk_simp_attr `simp_name since it adds a doc string to the attribute that is defined. If you need to create a simp set in a file where this command is not available, you should use

run_cmd mk_simp_attr `simp_name
run_cmd add_doc_string `simp_attr.simp_name "Description of the simp set here"
source
def tactic_doc.command.mk_simp_attribute  :
tactic_doc_entry

The command mk_simp_attribute simp_name "description" creates a simp set with name simp_name. Lemmas tagged with @[simp_name] will be included when simp with simp_name is called. mk_simp_attribute simp_name none will use a default description.

Appending the command with with attr1 attr2 ... will include all declarations tagged with attr1, attr2, ... in the new simp set.

This command is preferred to using run_cmd mk_simp_attr `simp_name since it adds a doc string to the attribute that is defined. If you need to create a simp set in a file where this command is not available, you should use

run_cmd mk_simp_attr `simp_name
run_cmd add_doc_string `simp_attr.simp_name "Description of the simp set here"

Attributes #

source
meta def simp_attr.equiv_rw_simp  :
(user_attribute simp_lemmas)

The simpset equiv_rw_simp is used by the tactic equiv_rw to simplify applications of equivalences and their inverses.

source
meta def simp_attr.field_simps  :
(user_attribute simp_lemmas)

The simpset field_simps is used by the tactic field_simp to reduce an expression in a field to an expression of the form n / d where n and d are division-free.

source
meta def simp_attr.functor_norm  :
(user_attribute simp_lemmas)

Simp set for functor_norm

source
meta def simp_attr.ghost_simps  :
(user_attribute simp_lemmas)

Simplification rules for ghost equations

source
meta def simp_attr.integral_simps  :
(user_attribute simp_lemmas)

Simp set for integral rules.

source
meta def simp_attr.is_R_or_C_simps  :
(user_attribute simp_lemmas)

Simp attribute for lemmas about is_R_or_C

source
meta def simp_attr.mfld_simps  :
(user_attribute simp_lemmas)

The simpset mfld_simps records several simp lemmas that are especially useful in manifolds. It is a subset of the whole set of simp lemmas, but it makes it possible to have quicker proofs (when used with squeeze_simp or simp only) while retaining readability.

The typical use case is the following, in a file on manifolds: If simp [foo, bar] is slow, replace it with squeeze_simp [foo, bar] with mfld_simps and paste its output. The list of lemmas should be reasonable (contrary to the output of squeeze_simp [foo, bar] which might contain tens of lemmas), and the outcome should be quick enough.

source
meta def simp_attr.monad_norm  :
(user_attribute simp_lemmas)

simp set for monad_norm

source
meta def simp_attr.nontriviality  :
(user_attribute simp_lemmas)

Simp lemmas for nontriviality tactic

source
meta def simp_attr.parity_simps  :
(user_attribute simp_lemmas)

Simp attribute for lemmas about even

source
meta def simp_attr.push_cast  :
(user_attribute simp_lemmas)

The push_cast simp attribute uses norm_cast lemmas to move casts toward the leaf nodes of the expression.

source
meta def simp_attr.split_if_reduction  :
(user_attribute simp_lemmas)

Simp set for if-then-else statements, used in the split_ifs tactic

source
meta def simp_attr.transport_simps  :
(user_attribute simp_lemmas)

The simpset transport_simps is used by the tactic transport to simplify certain expressions involving application of equivalences, and trivial eq.rec or ep.mpr conversions. It's probably best not to adjust it without understanding the algorithm used by transport.

source
meta def simp_attr.typevec  :
(user_attribute simp_lemmas)

simp set for the manipulation of typevec and arrow expressions