Zulip Chat Archive

Stream: general

Topic: Finite Set Questions


Jack Thorns (Jan 16 2023 at 21:44):

Hello, I've recently been trying to get into using Lean with mathlib for a few weeks now, and I have many confusions over what's going on with finsets that I've been unable to figure out myself.

In particular I'm trying to take a standard set I've defined on the naturals, and show that it is finite (and the way mathlib seems to be doing this is showing it's equivalent to some kind of finset?) if and only if another condition holds. In the forward implication, I have that it's finite, and to show the "other condition".

I could easily do so by using the well ordering theorem and the knowledge it has an upper bound on paper, but I'm not sure how to do this with lean. Equivalently, I've seen that finsets have a max defined for them, but I am unsure how to extract this as an object as I can abuse it's properties.

I'd appreciate some direction towards more detailed resources on how finsets work, and how they interact with sets, or alternatively some simple examples of them being used. In particular, the symbol is confusing.

I can provide details on the exact thing I'm trying to do / show if need be, but I'm still looking for more general help / resources on finsets.

Thank you!

Kevin Buzzard (Jan 16 2023 at 21:49):

You don't _have_ to use finset; there are two implementations of finite sets -- set.finite and finset. Without any context about what you're trying to do it's difficult to suggest which one would be best to work with.

For your specific questions, what you should do is abstract out a lemma (e.g. write a lemma in your file saying something like \forall s : set \N, s.finite <-> \exists B, \forall x \in s, x \le B or whatever the precise statement that you need is, and then sorry the proof, check that the lemma is what you need to finish what you're actually doing, and then copy the lemma into a new file, add imports to make it work, and then post the minimised file as a #mwe and ask for advice on how to fill in the sorry. In general, questions of the form "how do I fill in the sorry in this code which will compile on your machine" are far more effectively answered on this site than questions of the form you've just asked.

Kevin Buzzard (Jan 16 2023 at 21:50):

The symbol is the way to promote a term to a type. Lean uses type theory, so everything is a universe, a type or a term. A term s of type finset \N is a term, and it's not a type. But ↥s will be a type.

Jack Thorns (Jan 16 2023 at 22:02):

Sorry, I should've specified what I'm trying to do from the start.

I'm trying to prove that def prime_pow_dvd_n (n p: ℕ) (h: nat.prime p) : set ℕ := { k | p^k ∣ n } is finite if and only if n is not zero, purely as an exercise in writing proofs using lean.

What I don't quite understand is how to provide a proof that a particular set is indeed finite, which would both be needed in this proof, or in the lemma you suggested (which I agree does seem to be a useful), which is why I would appreciate an example.

There seem to be built-in theorems for equivalences with being nonempty and a fintype (I also can't figure out what that is), which I can't figure out how to use either.

Yaël Dillies (Jan 16 2023 at 22:04):

The way you can prove this set is finite is by showing that it's smaller than some obviously finite set. Here you could take ↑(finset.range n) as the obviously finite set

Jack Thorns (Jan 16 2023 at 22:14):

That is something I've tried but have been unable to do, there's so many different types and terms going on that it's quite confusing, since it's mixing finsets and standard sets. Is there some way to force the finset into being a "normal " set type, keeping the proof that it's finite?

Mario Carneiro (Jan 16 2023 at 22:15):

yes, that's what the arrow is doing in yael's quote

Yaël Dillies (Jan 16 2023 at 22:15):

Yes, if s : finset α, then ↑s : set α with the proof being docs#finset.finite_to_set

Jack Thorns (Jan 16 2023 at 22:17):

Aha! Thank you, I will give this a try.

Jack Thorns (Jan 16 2023 at 22:42):

The (unproven) lemma has indeed let me make progress, but I'm getting some strange things happening unrelated now?

I have the goal k + 1 ∈ prime_pow_dvd_n n p h, (this set is just the exact same set for a natural n and prime p as the one above, and h is a proof that p is prime), but when I told lean to split, why exactly did it create two goals, one with n = p ^ (k + 1) * ?m_1 and the other just ?

Patrick Stevens (Jan 16 2023 at 23:12):

If that was a "I don't understand what happened here", it's that Lean couldn't figure out what number m would make n = p^(k+1) * m, so it has created a goal for you to supply it with m, and a goal for you to prove that your choice of m works. (If instead that was a "why was Lean unable to figure out m", or "why did Lean want to know m in the first place", I pass.)

Jack Thorns (Jan 16 2023 at 23:40):

It was the first one, thank you.

Jack Thorns (Jan 17 2023 at 00:12):

Is it possible to extract the maximum of a finite set as a term?

Eric Wieser (Jan 17 2023 at 01:25):

Not if the set is empty

Eric Wieser (Jan 17 2023 at 01:25):

docs#finset.max / docs#finset.max' / docs#finset.inf are all good options

Jack Thorns (Jan 17 2023 at 04:15):

I've been trying to prove the lemma suggested by Kevin, and I have the set converted to a finset using the proof that the set is finite.

However, now I'm trying to extract the maximum of the set as a term like in the docs, and as you'd expect it requires a proof that the set is nonempty.

example {s : set } (h: s.nonempty) : s.finite   k,  x  s, x  k
begin
    split,
    {
        intro h',
        let s₀ := (set.finite.to_finset h'),
    }
end

However, when I try and extract the max using something like let m := h₁.max', it requires the proof h₁.nonempty, but I only have s.nonempty. I can't seem to find a theorem (if it exists) that can give me what I need, so is there something I'm missing or is this just a flawed approach?

Kevin Buzzard (Jan 17 2023 at 07:57):

It would be nicer (for me, because I'm lazy and don't know the entire library) if you were to post your question as a #mwe with all imports, rather than just a code snippet which doesn't work out of the box.

Yaël Dillies (Jan 17 2023 at 08:09):

There's no h₁ in your code snippet, so I can't really help either.

Filippo A. E. Nuccio (Jan 17 2023 at 08:38):

When you say "it requires the proof h₁.nonempty", who is "it" exactly? Is it some lemma you found in the library, so that we can have a look at it?

Riccardo Brasca (Jan 17 2023 at 08:50):

The standard answer here is #mwe :)

Kyle Miller (Jan 17 2023 at 09:40):

This ends up being true even without the s.nonempty hypothesis. You can also prove it without talking about finset at all; you can use docs#set.exists_max_image for getting the maximum of a finite set.

Eric Wieser (Jan 17 2023 at 11:38):

Eric Wieser said:

Not if the set is empty

Ah, but you didn't say "a set of ℕ", in which case you can do it if the set is empty (you get 0)

Yaël Dillies (Jan 17 2023 at 15:20):

Note that you should never use by_cases : s.nonempty but instead do obtain rfl | hs := s.eq_empty_or_nonempty (docs#set.eq_empty_or_nonempty, docs#finset.eq_empty_or_nonempty)

Jack Thorns (Jan 17 2023 at 21:33):

I apologise for not giving information properly, but I am new here so I can only ask that you try and be patient with me.

I appreciate the extra information presented above, but I'm going to write this as an amendment to my original message.

It was correctly pointed out that the assumption of the set being nonempty is not really needed, and whilst that will be considered when I attempt to finish this proof, for now this is still a useful learning point for me.

In my message, I meant s₀ and not h₁, I had confused my term names. Here should be a satisfactory #mwe (I think?):

import data.nat.prime

section
open nat

variables {k : }

example {s : set } (h: s.nonempty) : s.finite   k,  x  s, x  k :=
begin
    split,
    {
        intro h',
        let s₀ := (set.finite.to_finset h'),
        let m := s₀.max',
    },
end

end

The thing I was referring to, is that in the widget screen in vscode, it displays s₀.nonempty → ℕ := s₀.max', so we need a proof that s₀ is nonempty to get the maximum value (right?).

But I was unable to find a way to get such a proof from h.

Eric Wieser (Jan 17 2023 at 21:45):

The thing I was referring to, is that in the widget screen in vscode, it displays s₀.nonempty → ℕ := s₀.max', so we need a proof that s₀ is nonempty to get the maximum value (right?). But I was unable to find a way to get such a proof from h.

Correct! I would expect there to be a lemma somewhere that can get this from h. (edit: it's docs#set.finite.to_finset_nonempty)

Alternatively, you could ditch the nonempty assumption by using .sup instead of .max'.

Damiano Testa (Jan 17 2023 at 21:46):

... or, you could use

        let m := s₀.max' _,

informing Lean that you want the actual max' and also will supply a proof of non-emptiness.

Damiano Testa (Jan 17 2023 at 21:47):

(this allows you to separate further your goal in two: you can use m on one of the two goals, and you can provide the proof that Eric mentions in the other.)

Damiano Testa (Jan 17 2023 at 21:48):

Also, you are missing an import, I think.

Jack Thorns (Jan 17 2023 at 21:53):

When I try and use set.finite.to_finset_nonempty, the infoview says that it doesn't know what it is

Damiano Testa (Jan 17 2023 at 21:54):

import data.set.finite?

Jack Thorns (Jan 17 2023 at 21:55):

I already added that import as I thought that might be the problem, but it still says unknown identifier. (I'm just using #check set.finite.to_finset_nonempty)

Damiano Testa (Jan 17 2023 at 21:58):

If I copy-paste your check, I get

set.finite.to_finset_nonempty :  (h : ?M_2.finite), h.to_finset.nonempty  ?M_2.nonempty

Jack Thorns (Jan 17 2023 at 22:03):

How strange, just

import data.set.finite

section

#check set.finite.to_finset_nonempty

end

gives me the error unknown identifier 'set.finite.to_finset_nonempty'.

Could I somehow have an outdated version of mathlib? I did recently update it so that would be odd (or at least, I thought I did).

Eric Wieser (Jan 17 2023 at 22:05):

What does your leanproject.toml say?

Damiano Testa (Jan 17 2023 at 22:05):

It could be that section is expecting a name.

Damiano Testa (Jan 17 2023 at 22:07):

Your latest code works as is in the community playground.

Jack Thorns (Jan 17 2023 at 22:13):

Okay so now I seem to be getting technical issues, I'm attempting to create a new project to test it there, and now the lean server is crashing with the error binary package was not provided for 'windows'? I just ran leanproject new in a fresh empty directory.

Eric Wieser (Jan 17 2023 at 22:15):

You need to reinstall elan, its update mechanism broke

Jack Thorns (Jan 17 2023 at 22:21):

It is complaining that it cannot verify the legitimacy of the server, and I can't remember how I got around this last time. (When I try and use curl to install elan)

Edit:
Ah, figured it out and it had no problems creating a project this time, checking the code now.

Rejoice! It seems to be working now.

Jack Thorns (Jan 18 2023 at 00:07):

A further question, how can I define a function which, given some constraints, is defined as the maximum of a finite set, or even without constraints, I'm just not familiar with defining functions in this way.

Kevin Buzzard (Jan 18 2023 at 00:12):

What will you do if your finite set is empty?

Jack Thorns (Jan 18 2023 at 00:12):

I'd assume there was a way to provide a proof of nonemptiness to the function?

Bolton Bailey (Jan 18 2023 at 00:14):

You could look at how docs#finset.sup' is defined

Kevin Buzzard (Jan 18 2023 at 00:14):

Jack Thorns said:

I'd assume there was a way to provide a proof of nonemptiness to the function?

Yes sure! But with formalisation you need to say exactly what you mean (e.g. by giving a #mwe with the precise statement of what you want, or something as near as possible). What hypotheses do you want on your set, for example? It need some kind of ordering. What kind? Would you allow two incomparable maxima? etc etc. You say "the maximum" and that's already making implicit assumptions. What is the actual exact question?

Jack Thorns (Jan 18 2023 at 00:16):

Ah so, it is the same prime power set as before, being

import data.nat.prime

section
def prime_pow_dvd_n (n p: ) (h: nat.prime p) : set  := { k | p^k  n }

end

and I have a lemma stating that this set is always nonempty, but of course it only makes sense to talk about this set when n is nonzero, so n ≠ 0 is a constraint, and nat.prime p is a constraint.

What I've attempted so far is essentially

def max_prime_pow {n p: } {h: nat.prime p} {h': n  0} :      :=

but I'm not sure how to continue. My apologies for being vague once again.

Kevin Buzzard (Jan 18 2023 at 00:24):

Oh I see, it's a set of naturals. Sorry, I'd not put two and two together. We already have what you're trying to define in mathlib; it's docs#padic_val_nat . I know that doesn't answer your question of how to define it, but hopefully it gets the job done. Every definition in lean comes with a cost, and the cost is that you have to write the API for the definition. The advantage of using a definition which is already there is that there will be lemmas about the definition already, saving you the bother.

Yakov Pechersky (Jan 18 2023 at 00:27):

To just put together what others had already messaged:

import data.nat.prime

section

def prime_pow_dvd_n (n p : ) : set  := { k | p^k  n }

lemma prime_pow_dvd_n_finite {n p : } (h : nat.prime p) (h' : n  0) : (prime_pow_dvd_n n p).finite :=
sorry

noncomputable
def max_prime_pow {n p: } (h: nat.prime p) (h': n  0) :  :=
(prime_pow_dvd_n_finite h h').to_finset.sup id

end

Jack Thorns (Jan 18 2023 at 00:28):

That's alright, even if I'm not necessarily using what I wrote up to now, it was at least a good exercise and I can use the source of that function to learn more about how to write it.

Jack Thorns (Jan 18 2023 at 00:29):

Yakov Pechersky said:

To just put together what others had already messaged:

import data.nat.prime

section

def prime_pow_dvd_n (n p : ) : set  := { k | p^k  n }

lemma prime_pow_dvd_n_finite {n p : } (h : nat.prime p) (h' : n  0) : (prime_pow_dvd_n n p).finite :=
sorry

noncomputable
def max_prime_pow {n p: } (h: nat.prime p) (h': n  0) :  :=
(prime_pow_dvd_n_finite h h').to_finset.sup id

end

Ah! Thank you very much!

Yakov Pechersky (Jan 18 2023 at 00:29):

Note, I defined the set without requiring nat.prime p or n \ne 0, since the set exists regardless of those. It's only the finiteness that requires the preconditions. I also switched some arguments from implicit to explicit.

Bhavik Mehta (Jan 18 2023 at 20:49):

I didn't follow all of this discussion, but this last function should be just n.factorization p, and in the cases where n is nonzero and p is prime, you can prove it's the largest natural k for which p^k divides n


Last updated: Dec 20 2023 at 11:08 UTC