attributes, name_map with non-def keys

Stream: general

[Yury G. Kudryashov]

Hi,
Is there any way to store a name_map name other than user_attr?
For my rewrite of to_additive, I want to store a name_map name of prefixes used to automatically map names from multiplicative to additive. Sometimes (e.g., for quotient_group), the key is not a def but a namespace. I see two ways of dealing with this:

1. Define a dummy @[to_additive quotient_add_group] def quotient_group : bool := tt.
2. Store all (src, tgt) pairs as a list (name × name) attribute on a single def.
3. Explicitly specify @[to_additive quotient_add_group.lemma_name] def lemma_name := sorry every time.
4. Something else?
The second approach fails with “error: deep recursion was detected at 'live variable analysis'” once we have sufficiently many items in the list. Any suggestions?

[Mario Carneiro]

I can't think of any way which isn't a horrible hack

[Mario Carneiro]

You could do something similar to the replacer tactic. You store the data, reflected as an expr, as the content of a definition, and smuggle the data around via tactics triggered by an attribute

[Mario Carneiro]

Or maybe just use IO to open up a program with actual memory access

[Yury G. Kudryashov]

@Mario Carneiro I think, I'll define a dummy def quotient_group. This is a hack but other options require too much work to deal with one or two exceptions.

[Mario Carneiro]

A variation on (1) is to call the dummy quotient_group._namespace to avoid using the real name

[Mario Carneiro]

assuming of course you know you are looking for a namespace, not a def, and so know to adjust the lookup

[Yury G. Kudryashov]

I use attr.get_cache : tactic (name_map name) as a set of prefix mappings, and quotient_group._namespace is not a prefix of quotient_group.my_lemma.

[Mario Carneiro]

I mean that given quotient_group._namespace, you should first strip off the _namespace suffix and then do a prefix match with the target name

[Simon Hudon]

What are you using the prefix map for?

[Yury G. Kudryashov]

@Simon Hudon See #1345. I use it to avoid attribute [to_additive add_group.cases_on] group.cases_on and friends.

[Yury G. Kudryashov]

I assume that if I want to map my.long.name to additive, and I have attribute [to_additive add_my] my, then most probably add_my.long.name will work.

[Yury G. Kudryashov]

This heuristic works in most cases.

[Simon Hudon]

I have a PR where I started something similar. It was mostly for the auxiliary equations. You might what to take a look. There were a couple of details I couldn't work out though and I haven't pushed it across the finish line

[Yury G. Kudryashov]

Could you please send me a link?

[Simon Hudon]

Of course! Sorry I forgot! #431

[Yury G. Kudryashov]

@Simon Hudon Thanks! It turns out that I missed the presense of get_eqn_lemmas_for!

[Simon Hudon]

:+1:

[Yury G. Kudryashov]

Do you know what is better: transport eqn lemmas, or ask smt_tactic.interactive.add_eqn_lemmas to generate them? Is there any difference?

[Yury G. Kudryashov]

If add_eqn_lemmas is better, then how do I convert smt_tactic α to tactic α?

[Simon Hudon]

I don't think add_eqn_lemmas has an effect outside the scope of the current tactic

[Yury G. Kudryashov]

Thank you

[Simon Hudon]

This is the annoying thing though. With Lean 3.4.2, you can't mimic eqn lemmas too well. I added a feature to 3.5 but mathlib has not migrated to 3.5 yet

[Simon Hudon]

In short: transport the equations but they are not going to be as nice to use as those for the multiplicative structures