Zulip Chat Archive

Stream: maths

Topic: to_additive


view this post on Zulip 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?

view this post on Zulip 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.

view this post on Zulip 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_?

view this post on Zulip 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.

view this post on Zulip 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/?

view this post on Zulip Kevin Buzzard (Jul 21 2019 at 13:08):

I'm hoping there's an algorithm

view this post on Zulip Kevin Buzzard (Jul 21 2019 at 13:09):

Of that nature yes

view this post on Zulip 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

view this post on Zulip Yury G. Kudryashov (Jul 21 2019 at 14:47):

I started using Lean about two months ago.

view this post on Zulip Yury G. Kudryashov (Jul 21 2019 at 14:47):

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

view this post on Zulip 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: May 09 2021 at 10:11 UTC