Commit 2020-07-24 21:19 6f9da356

feat(tactic/simps): improvements (#3477) Features:

• @[simps] will look for has_coe_to_sort and has_coe_to_fun instances, and use those instead of direct projections. This should make it way more applicable for equiv, local_equiv and all other structures that coerce to a function (and for the few structures that coerce to a type). This works out-of-the-box without special configuration.
• Use has_mul.mul, has_zero.zero and all the other "notation projections" instead of the projections directly. This should make it more useful in category theory and the algebraic hierarchy (note: the [notation_class] attribute still needs to be added to all notation classes not defined in init.core)
• Add an easy way to specify custom projections of structures (like using ⇑e.symm instead of e.inv_fun). They have to be definitionally equal to the projection. Minor changes:
• Change the syntax to specify options.
• prod (and pprod) are treated as a special case: we do not recursively apply projections of these structure. This was the most common reason that we had to write the desired projections manually. You can still override this behavior by writing out the projections manually.
• A flag to apply simp to the rhs of the generated lemma, so that they are in simp-normal-form.
• Added an options to add more attributes to the generated lemmas
• Added an option which definitions to unfold to determine whether a type is a function type. By default it will unfold reducible definitions and instances (but e.g. not set α)
• Added an option to unfold definitions in the declaration to determine whether it is a constructor. (default: none)
• Added an option to not fully-apply the terms in the generated lemmas. Design decisions:
• For every field in a structure there is a specified "projection expression" that acts as the projection for that field. For most fields this is just the projection of the structure, but this will be automatically overridden under certain conditions, like a coercion to functions/sorts existing, or a notation typeclass existing for a certain field.
• The first time you call simps for a specific structure, these projection expressions are cached using an attribute for that structure, and it is assumed you want to use the same projection expressions every time.
• You can also manually specify the projection. See Note [custom simps projection].