Zulip Chat Archive

Stream: maths

Topic: to_additive


Yury G. Kudryashov (Jul 21 2019 at 07:52):

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 (Jul 21 2019 at 08:16):

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 (Jul 21 2019 at 09:12):

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 (Jul 21 2019 at 12:12):

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 (Jul 21 2019 at 12:50):

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

Kevin Buzzard (Jul 21 2019 at 13:08):

I'm hoping there's an algorithm

Kevin Buzzard (Jul 21 2019 at 13:09):

Of that nature yes

Kevin Buzzard (Jul 21 2019 at 13:45):

@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 (Jul 21 2019 at 14:47):

I started using Lean about two months ago.

Yury G. Kudryashov (Jul 21 2019 at 14:47):

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

Yury G. Kudryashov (Jul 21 2019 at 14:52):

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


Last updated: Dec 20 2023 at 11:08 UTC