Zulip Chat Archive

Stream: mathlib4

Topic: Finite set over infinite type


Sebastian Zivota (Jan 31 2023 at 21:13):

Is there a theorem asserting that for infinite α, ∀ (s : Finset α), ∃ (x : α), x ∉ s? If not, how would one go about proving that?

Mario Carneiro (Jan 31 2023 at 21:15):

if not then the set is finite by definition

Sebastian Zivota (Jan 31 2023 at 21:16):

For the sake of a concrete example, can I prove ∀ (s : Finset String), ∃ (x : α), x ∉ s?

Mario Carneiro (Jan 31 2023 at 21:16):

Oh I was assuming you have an actual assumption of the form Infinite A

Mario Carneiro (Jan 31 2023 at 21:17):

which probably exists for string, not sure

Sebastian Zivota (Jan 31 2023 at 21:18):

Thanks, that helps a lot already

Mario Carneiro (Jan 31 2023 at 21:20):

hm, docs4#Set.Infinite.exists_not_mem_finset looks close to what you want

Mario Carneiro (Jan 31 2023 at 21:23):

there is a proof that Nat and List A are infinite, but not String. It shouldn't be hard by applying the isomorphism from List Char

Mario Carneiro (Jan 31 2023 at 21:25):

oh, docs4#Infinite.exists_not_mem_finset is exactly the theorem you want

Sebastian Zivota (Jan 31 2023 at 21:27):

Excellent, thank you very much

Sebastian Zivota (Jan 31 2023 at 21:33):

Although there does indeed not seem to be an instance of Infinite String

Kevin Buzzard (Jan 31 2023 at 21:33):

I wouldn't get your hopes up regarding the existence of too many theorems about strings in mathlib4 :-)

Mario Carneiro (Jan 31 2023 at 21:35):

yeah, the people who care about strings don't talk to the people who care about infinitude :grinning_face_with_smiling_eyes:

Johan Commelin (Jan 31 2023 at 21:42):

[string theorists leave the room]

Sebastian Zivota (Jan 31 2023 at 21:45):

Fortunately it's easy to prove, should I open a PR?

Mario Carneiro (Jan 31 2023 at 21:47):

sure

Kevin Buzzard (Jan 31 2023 at 21:47):

to which repo? I'm not sure mathlib4 wants new material which isn't in mathlib3 right now

Mario Carneiro (Jan 31 2023 at 21:48):

yes, mathlib4 wants new material

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

This was not my understanding of what was going on right now. I thought the idea was to keep mathlib3 and mathlib4 in exact sync.

Eric Wieser (Jan 31 2023 at 21:50):

Why not put it in both?

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

Right -- that was the answer I was expecting.

Eric Wieser (Jan 31 2023 at 21:51):

If people want to not have to worry about mathlib3 any more, they should help with the port!

Mario Carneiro (Jan 31 2023 at 21:51):

I really do not want to encourage backports for everything, this is a lot more work and counterproductive besides

Johan Commelin (Jan 31 2023 at 21:51):

If you are starting a new file, I don't see any reason why it should be backported to ml3.

Mario Carneiro (Jan 31 2023 at 21:52):

if nothing in mathlib3 depends on it there is no need for a backport

Kevin Buzzard (Jan 31 2023 at 21:58):

I'm not sure we're starting a new file just containing the result that String is an infinite type!

Ruben Van de Velde (Jan 31 2023 at 22:00):

Well, why not? It's easy enough to merge it into some other file after the port is done

Mario Carneiro (Jan 31 2023 at 22:02):

mathlib4 is already not exactly 1-1 with align statements. The whole discussion seems silly to me, of course we should allow new material - there is already quite a bit of new material, in addition to tons of upstream new material

Ruben Van de Velde (Jan 31 2023 at 22:03):

Would std4 take the definition of Infinite? :innocent:

Mario Carneiro (Jan 31 2023 at 22:03):

and not allowing new material will set us back more than necessary

Mario Carneiro (Jan 31 2023 at 22:03):

Ruben Van de Velde said:

Would std4 take the definition of Infinite? :innocent:

the real question is whether it would be able to disentangle all the dependencies

Mario Carneiro (Jan 31 2023 at 22:04):

the definition of infinite itself isn't so bad but it depends on all the finiteness stuff

Mario Carneiro (Jan 31 2023 at 22:04):

James Gallicchio 's List.Perm PR is just one small part of this, it will take a while to work through all of it

Sebastian Zivota (Jan 31 2023 at 22:12):

https://github.com/leanprover-community/mathlib4/pull/1973

I put the mathlib4 version into Data.Fintype.Card, where the Infinite ℤ instance also lives. The proof can't be backported one-to-one because, as far as I can tell, Lean3/Mathlib3 doesn't have the String.replicate function.

Ruben Van de Velde (Jan 31 2023 at 22:20):

Anything called replicate in 4 was probably called repeat in 3

Ruben Van de Velde (Jan 31 2023 at 22:23):

Mario Carneiro said:

the definition of infinite itself isn't so bad but it depends on all the finiteness stuff

I wasn't really serious, but it's not that bad. It doesn't depend on Fintype, just Finite, which needs only Nat/Fin n (which are in core, I think) and Equiv (including Function.Left/RightInverse)


Last updated: Dec 20 2023 at 11:08 UTC