Zulip Chat Archive

Stream: general

Topic: multiple ext lemmas per structure


Gabriel Ebner (May 13 2020 at 16:54):

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 (May 13 2020 at 16:55):

how does that even work?

Gabriel Ebner (May 13 2020 at 16:57):

:shrug:

Gabriel Ebner (May 13 2020 at 16:58):

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

Johan Commelin (May 13 2020 at 16:58):

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

Gabriel Ebner (May 13 2020 at 16:58):

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

Mario Carneiro (May 13 2020 at 16:59):

There are examples in the doc comment on extensional_attribute

Mario Carneiro (May 13 2020 at 17:00):

you can mark one lemma as the extensionality for two types

Mario Carneiro (May 13 2020 at 17:00):

that are presumably defeq

Reid Barton (May 13 2020 at 17:11):

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

Mario Carneiro (May 13 2020 at 17:18):

oh wow that looks pretty terrible

Mario Carneiro (May 13 2020 at 17:19):

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

Gabriel Ebner (May 13 2020 at 17:20):

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 (May 13 2020 at 17:20):

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

Mario Carneiro (May 13 2020 at 17:21):

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

Yury G. Kudryashov (May 13 2020 at 17:45):

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

Yury G. Kudryashov (May 13 2020 at 17:46):

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

Yury G. Kudryashov (May 13 2020 at 17:52):

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

Yury G. Kudryashov (May 13 2020 at 17:53):

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

Johan Commelin (May 13 2020 at 17:56):

Yup, that's a good example

Gabriel Ebner (May 13 2020 at 17:56):

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

Mario Carneiro (May 13 2020 at 17:57):

This needs some kind of discrimination tree lookup

Yury G. Kudryashov (May 13 2020 at 18:31):

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

Yury G. Kudryashov (May 13 2020 at 18:32):

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

Gabriel Ebner (May 13 2020 at 18:43):

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


Last updated: Dec 20 2023 at 11:08 UTC