Finite Set Questions

Stream: general

[Jack Thorns]

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]

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]

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]

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]

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]

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]

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

[Yaël Dillies]

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

[Jack Thorns]

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

[Jack Thorns]

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]

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]

It was the first one, thank you.

[Jack Thorns]

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

[Eric Wieser]

Not if the set is empty

[Eric Wieser]

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

[Jack Thorns]

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]

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]

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

[Filippo A. E. Nuccio]

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]

The standard answer here is #mwe :)

[Kyle Miller]

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.

import tactic

example {s : set ℕ} : s.finite ↔ ∃ (k : ℕ), ∀ x ∈ s, x ≤ k :=
begin
  split,
  { intro hf,
    by_cases hn : s.nonempty,
    { obtain ⟨k, hk, h⟩ := set.exists_max_image s id hf hn,
      exact ⟨k, h⟩, },
    { rw set.not_nonempty_iff_eq_empty at hn,
      subst hn,
      simp } },
  { rintro ⟨k, h⟩,
    apply (set.to_finite (set.Icc 0 k)).subset,
    intros x hx,
    simpa using h x hx }
end

[Eric Wieser]

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]

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]

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]

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]

... 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]

(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]

Also, you are missing an import, I think.

[Jack Thorns]

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

[Damiano Testa]

import data.set.finite?

[Jack Thorns]

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]

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]

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]

What does your leanproject.toml say?

[Damiano Testa]

It could be that section is expecting a name.

[Damiano Testa]

Your latest code works as is in the community playground.

[Jack Thorns]

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]

You need to reinstall elan, its update mechanism broke

[Jack Thorns]

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]

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]

What will you do if your finite set is empty?

[Jack Thorns]

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

[Bolton Bailey]

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

[Kevin Buzzard]

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]

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]

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]

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]

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]

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]

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]

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