Zulip Chat Archive
Stream: general
Topic: zorn
Kenny Lau (Oct 30 2018 at 08:14):
The current implementation of zorn is not exactly the most convenient, and require some casing to use (see: all the use cases). The more convenient statement would be "a nonempty type such that every nonempty chain has an upper bound has a maximal element. Also, zorn.chain is for strict orders, which wouldn't be the best thing to use for partial orders (zorn.zorn_partial_order) and subsets (zorn.zorn_subset).
Kenny Lau (Oct 30 2018 at 08:14):
@Mario Carneiro I'll create a PR if you approve
Mario Carneiro (Oct 30 2018 at 08:15):
I think I have done this already
Kenny Lau (Oct 30 2018 at 08:15):
ok the latter problem is solved by zorn.chain.total
Kenny Lau (Oct 30 2018 at 08:16):
but where can I find your work?
Mario Carneiro (Oct 30 2018 at 08:19):
https://github.com/leanprover-community/mathlib/blob/module/order/zorn.lean#L244-L258
Mario Carneiro (Oct 30 2018 at 08:20):
I can merge that early if you want, or you can just copy it into your branch and it will get merged with mine eventually
Mario Carneiro (Oct 30 2018 at 08:20):
Alternatively you might want a different interface; I played with a few alternatives but that's the only version I actually ended up using
Kenny Lau (Oct 30 2018 at 08:21):
oh
Mario Carneiro (Oct 30 2018 at 08:23):
also zorn.chain is for strict or non-strict orders
Kenny Lau (Oct 30 2018 at 08:31):
yes but it's not convenient to use
Mario Carneiro (Oct 30 2018 at 08:32):
?
Kenny Lau (Oct 30 2018 at 08:33):
that's why zorn.chain.total exists right
Kenny Lau (Oct 30 2018 at 08:33):
it's a wrapper for if you use zorn.chain on a non-strict order
Kenny Lau (Oct 30 2018 at 08:33):
(that's "for if" as in "por si")
Kenny Lau (Oct 30 2018 at 08:34):
(that I just googled to translate to "just in case")
Kenny Lau (Oct 30 2018 at 08:35):
s/googled to translate/googled which tells me that it translates/
Kenny Lau (Oct 30 2018 at 08:35):
I can't English
Mario Carneiro (Oct 30 2018 at 08:38):
I'm not following. The definition makes sense for both strict and non-strict orders and there are lemmas to give you equivalent forms when you know one or the other
Kenny Lau (Oct 30 2018 at 08:39):
yes, so I say that zorn.chain.total solves the problem
Mario Carneiro (Oct 30 2018 at 08:40):
do you mean total_of_refl by the way? I can't find zorn.chain.total
Kenny Lau (Oct 30 2018 at 08:41):
maybe you opened zorn
Kenny Lau (Oct 30 2018 at 08:41):
in which case it's chain.total
Mario Carneiro (Oct 30 2018 at 08:41):
_of_refl
Mario Carneiro (Oct 30 2018 at 08:41):
actually I find chain.directed to be the most useful one; it is rare to actually need a chain as opposed to a directed set in zorn constructions
Kenny Lau (Oct 30 2018 at 08:42):
Mario Carneiro (Oct 30 2018 at 08:43):
oh, I guess that's just specializing to le
Mario Carneiro (Oct 30 2018 at 08:44):
That shouldn't be necessary (now?) since the <le_refl> part should be derivable by tc inference
Kenny Lau (Oct 30 2018 at 08:44):
it's shorter
Kenny Lau (Oct 30 2018 at 08:44):
also that's the first one I noticed
Mario Carneiro (Oct 30 2018 at 08:44):
well if I deleted it the other one would lose the of_refl part
Patrick Massot (Oct 30 2018 at 09:01):
https://github.com/leanprover-community/mathlib/blob/module/order/zorn.lean#L244-L258
Oh! Mario resumed work on modules! Is there hope to have modules before the Freiburg meeting next week? I see lots of underscores in that latest commit though :sad:
Johan Commelin (Oct 30 2018 at 20:04):
Hurray! We are cheering for you Mario!
Last updated: Dec 20 2023 at 11:08 UTC