Zulip Chat Archive

Stream: Is there code for X?

Topic: smallest element of a set?


view this post on Zulip Kevin Lacker (Oct 05 2020 at 16:11):

Is there a way to express specifically, "the smallest element of s" where s is a set of natural numbers

view this post on Zulip Markus Himmel (Oct 05 2020 at 16:17):

There are docs#well_founded.min (see also docs#nat.lt_wf) and docs#nat.find.

view this post on Zulip Kevin Lacker (Oct 05 2020 at 16:20):

so I have to import something for .min to work on set \N, right? how do I figure out what to import

view this post on Zulip Markus Himmel (Oct 05 2020 at 16:21):

I might be wrong, but I don't think you can make it work with dot notation. I think you have to write well_founded.min nat.lt_wf S S_nonempty

view this post on Zulip Johan Commelin (Oct 05 2020 at 16:25):

Kevin Lacker said:

how do I figure out what to import

by asking here... and after a while you'll know the library well enough that you start answering these questions yourself (-;

also grep helps me to find stuff quite often.

view this post on Zulip Kevin Lacker (Oct 05 2020 at 16:31):

ok. why does some stuff work with dot notation and some stuff not work with dot notation?

view this post on Zulip Markus Himmel (Oct 05 2020 at 16:36):

Roughly speaking: if X is of type foo (possibly with some arguments), then dot notation allows us to write X.bar as a shorthand for foo.bar X. So in order to write S.min, where S is a set, the declaration would have to be named set.min

view this post on Zulip Kevin Lacker (Oct 05 2020 at 16:39):

hmm. why isn't a set of natural numbers a well-founded set? i guess because it is only relative to a particular relation

view this post on Zulip Bryan Gin-ge Chen (Oct 05 2020 at 16:40):

For more on dot notation see the end of 3.3.1 and 9.1 in TPiL. I think it finally clicked for me though after I read this thread.

view this post on Zulip Kevin Lacker (Oct 05 2020 at 16:40):

well, i'm used to it in the context of programming languages

view this post on Zulip Kevin Lacker (Oct 05 2020 at 16:40):

the real question in my head is, why isn't .min a function on sets of integers, like it would be in a "normal" programming language

view this post on Zulip Kevin Lacker (Oct 05 2020 at 16:42):

for some reason, i'm sure it's a good one, it doesn't just use the sane default of < for the less-than relation

view this post on Zulip Kevin Lacker (Oct 05 2020 at 16:44):

i read that thread but there's too many references to other concepts i don't get for me to really get it. which is ok... compared to a normal programming language there's just far more methods and far fewer classes, so their organization is kind of necessarily harder to get through

view this post on Zulip Yakov Pechersky (Oct 05 2020 at 16:48):

Do you mean .min a function on finsets of integers?

view this post on Zulip Yakov Pechersky (Oct 05 2020 at 16:49):

Because your_min {x : Z | x < 0} is ...?

view this post on Zulip Kevin Lacker (Oct 05 2020 at 16:49):

sorry, natural numbers, not integers

view this post on Zulip Yakov Pechersky (Oct 05 2020 at 16:50):

Well, I think docs#finset.min' would work for what you want.

view this post on Zulip Johan Commelin (Oct 05 2020 at 16:51):

@Kevin Lacker You can use S.min once you define set.min. But if you define set.min only for S : set nat then mathlib will not like it, because that definition is too restrictive. So you will have to come up with a definition of set.min that is sufficiently general that it covers all cases that one possibly would want to call set.min.

view this post on Zulip Kevin Lacker (Oct 05 2020 at 16:57):

i see. so it kind of tracks back to, there is no way to define a function that sometimes throws an error, or that is only defined on some subset of its input.

view this post on Zulip Yakov Pechersky (Oct 05 2020 at 16:58):

There is, using option or subtype.

view this post on Zulip Yakov Pechersky (Oct 05 2020 at 16:59):

Depends on what you want to do. Compare the docs#finset.min and docs#finset.min'

view this post on Zulip Kevin Lacker (Oct 05 2020 at 17:00):

ok i have to read up more to discuss this sufficiently intelligently

view this post on Zulip Paul van Wamelen (Oct 05 2020 at 18:46):

There is a nice example of getting the smallest nat in a set of nats around line 127 of C:\Projects\lean\mathlib_ufm2\archive\imo\imo1988_q6.lean.

view this post on Zulip Kevin Lacker (Oct 05 2020 at 19:13):

well_founded.not_lt_min nat.lt_wf S S_nonempty hk it is

view this post on Zulip Kevin Lacker (Oct 05 2020 at 22:26):

and after all that, reviewer complains that the simplest way to write this is to use the is_least predicate :rolling_eyes: ( but thank you for pointing that out @Yury G. Kudryashov )

view this post on Zulip Yury G. Kudryashov (Oct 05 2020 at 22:28):

I'm sorry for not telling this earlier. When I read the original question, I thought you were asking about a function that takes a set and returns its minimal element.

view this post on Zulip Yury G. Kudryashov (Oct 05 2020 at 22:28):

Probably we should ask for #xy every time.

view this post on Zulip Kevin Lacker (Oct 05 2020 at 22:29):

sigh... yeah, i should have realized that the answer to these two questions would live in totally different sublibraries


Last updated: May 17 2021 at 16:26 UTC