Zulip Chat Archive

Stream: maths

Topic: equivalent definitions


view this post on Zulip Johan Commelin (Sep 01 2020 at 08:20):

Continuing discussion from here:
https://leanprover.zulipchat.com/#narrow/stream/116395-maths/topic/.60prop_limits.60.20branch/near/208657290

@Damiano Testa would like to have a method to "jump" between equivalent definitions.
I wonder if we can do something to make this easier. We'll be getting more and more of those over time.

view this post on Zulip Johan Commelin (Sep 01 2020 at 08:20):

We already have this for local_ring, discrete_valuation_ring and there is a PR with three definitions of Dedekind domain.

view this post on Zulip Johan Commelin (Sep 01 2020 at 08:21):

Yury has proven some tfae lemmas in analysis. But I'm not sure that is the best way. (Maybe it is!)

view this post on Zulip Johan Commelin (Sep 01 2020 at 08:21):

Should we have an attribute @[alt_def name_of.main_def]

view this post on Zulip Patrick Massot (Sep 01 2020 at 08:47):

https://leanprover.zulipchat.com/#narrow/stream/239415-metaprogramming-.2F.20tactics/topic/reformulate

view this post on Zulip Johan Commelin (Sep 01 2020 at 08:51):

@Patrick Massot Yes, reformulate is a good idea. But maybe a "curated" approach could give even better results?

view this post on Zulip Johan Commelin (Sep 01 2020 at 08:52):

I do think that reformulate is "low-hanging" fruit for our community (not for me!). So we should probably try that first.

view this post on Zulip Patrick Massot (Sep 01 2020 at 09:10):

What do you mean by curated? You want a new attribute? I'd like to try the automated approach first. It seems very low hanging indeed, but you still need someone taking some time to do it.

view this post on Zulip Johan Commelin (Sep 01 2020 at 09:11):

With "curated" I indeed was thinking of a new attribute, as I suggested above.


Last updated: May 09 2021 at 09:11 UTC