to_additive

Stream: maths

[Yury G. Kudryashov]

Hi, I think it would be nice to have the following features in to_additive:
1. Automatically add constructors, rec_on etc. to the dictionary.
2. Automatically add attribute [to_additive name._proof_{{n}}] name._proof_{{n}} before trying to transport name.
Is it hard?

[Scott Morrison]

Those sound like good ideas. I don't think they should be too hard. There are a few tactics that crawl the environment looking for declarations. The only example I know well (because I wrote it) is library_search.

[Yury G. Kudryashov]

If I have a structure, I see how I can ask Lean for its constructor and members, so it shouldn't be too hard to do (1). What should I do for (2)? Go over the proof and look for names starting with name._proof_?

[Kevin Buzzard]

I think that to_additive should just be some sort of other thing, which takes a valid Lean file mul_stuff.lean and changes all the muls to adds etc and bungs the resulting new API on the bottom of the mul file.

[Yury G. Kudryashov]

@Kevin Buzzard What should it do with names? s/mul/add/, s/sum/prod/, s/inv/neg/?

[Kevin Buzzard]

I'm hoping there's an algorithm

[Kevin Buzzard]

Of that nature yes

[Kevin Buzzard]

@Yury G. Kudryashov do you know about Lean's canonical structures? Could they be used here? I guess Assia and Cyril both gave talks about this at Lean together 2019

[Yury G. Kudryashov]

I started using Lean about two months ago.

[Yury G. Kudryashov]

@Kevin Buzzard So no, I know nothing about Lean's canonical structures.

[Yury G. Kudryashov]

Actually, I wonder is it more useful to have is_group α (*), is_group α (+), is_monoid (α → α) (∘), then use rw [assoc (*)] instead of rw [mul_assoc].