multiple ext lemmas per structure

Stream: general

[Gabriel Ebner]

I'm currently fixing some horrible performance problems in the ext tactic. (It takes a few seconds after import all.) Some parts of the code support more than one extensionality lemma per structure. Does anybody use this / want this / have any idea what this is about?

[Mario Carneiro]

how does that even work?

[Gabriel Ebner]

:shrug:

[Gabriel Ebner]

I just noticed that the ext attribute stores a list of names.

[Johan Commelin]

I guess we don't want/need this. Do you have examples?

[Gabriel Ebner]

I'm pretty sure we don't because every lemma but the last is discarded.

[Mario Carneiro]

There are examples in the doc comment on extensional_attribute

[Mario Carneiro]

you can mark one lemma as the extensionality for two types

[Mario Carneiro]

that are presumably defeq

[Reid Barton]

Is this related to the several lines of bit1 (bit0 (bit0 ...)) I get when #printing an extensionality lemma?

[Mario Carneiro]

oh wow that looks pretty terrible

[Mario Carneiro]

@[ext] stores an expr, and #print apparently doesn't use the proper pp settings to show that expr

[Gabriel Ebner]

The whole user_attribute param story is pretty bad. NEVER USE user_attribute.get_param. This will call eval_expr. Calling eval_expr coincidentally also disables the attribute cache IIRC.

[Gabriel Ebner]

The parameters are stored as expressions using has_reflect in case it wasn't clear.

[Mario Carneiro]

how are you supposed to get the parameter without get_param? It's not passed to after_set

[Yury G. Kudryashov]

Multiple ext lemmas per structure can be useful, e.g., here

[Yury G. Kudryashov]

free_monoid.hom_eq is an ext lemma for free_monoid α →* M.

[Yury G. Kudryashov]

And it makes sense to have similar lemmas for other structures with relatively small generating sets.

[Yury G. Kudryashov]

E.g., two nat →+ M are equal if they agree at 1.

[Johan Commelin]

Yup, that's a good example

[Gabriel Ebner]

But it doesn't work at the moment, right? We can do that as a follow-up PR.

[Mario Carneiro]

This needs some kind of discrimination tree lookup

[Yury G. Kudryashov]

I added @[ext] to free_monoid.hom_eq, and mathlib still builds.

[Yury G. Kudryashov]

Probably it tries this lemma first for each monoid_hom, then falls back to monoid_hom.ext.

[Gabriel Ebner]

Even better, it first tries the named extensionality lemma, and if that fails, it tries all of them..