Zulip Chat Archive

Stream: mathlib4

Topic: data.set.finite


Patrick Massot (Nov 15 2022 at 21:40):

I think an interesting graph to took at in order to measure how far we are from porting anything interesting is the import graph of data.set.finite:
data_set_finite.pdf

Patrick Massot (Nov 15 2022 at 21:42):

This is rather depressing but I suspect that a lot of this comes from the fact that data.finite.basic both defines finiteness and tries to provide all possible instances.

Patrick Massot (Nov 15 2022 at 21:42):

In any case, there is certainly no reason why data.set.finite needs all this algebra.

Patrick Massot (Nov 15 2022 at 21:44):

Maybe we should simply port everything and stop worrying, but it's hard to think there is nothing to fix here.

Heather Macbeth (Nov 15 2022 at 21:44):

Since the very first filter files import finiteness, we should definitely fix this! There is no reason for basic topology to import basic algebra.

Patrick Massot (Nov 15 2022 at 21:45):

This is creepy. Heather seems to be spying on my computer and knows how I found about that horrible graph.

Patrick Massot (Nov 15 2022 at 21:45):

Of course I first generated filter.pdf

Jireh Loreaux (Nov 15 2022 at 21:50):

Perhaps a stupid question: why do the very first filter files import finiteness?

Heather Macbeth (Nov 15 2022 at 21:50):

Among other reasons, because the cofinite filter is defined in them. This could be avoided.

Yaël Dillies (Nov 15 2022 at 21:51):

I have plans to split up finiteness. I will update you in the next two days.

Heather Macbeth (Nov 15 2022 at 21:53):

Also, because there are lemmas about Sups of finsets in order.conditionally_complete_lattice (this could be avoided), and order.copy imports conditionally_complete_lattice (this could be avoided), and order.filter.basic imports order.copy (this could be avoided).

Patrick Massot (Nov 15 2022 at 21:55):

Perhaps a stupid question: why do the very first filter files import finiteness?

By definition, the set of members of a filter is stable under (binary) intersection. One of the very first consequences you want to state is stability under finite intersections.

Patrick Massot (Nov 15 2022 at 21:57):

And really this isn't only about filters. Stating that a set is finite is a really really basic thing in mathematics.

Kyle Miller (Nov 15 2022 at 21:58):

I remember @Yury G. Kudryashov had plans to make docs#set.finite be defined in terms of docs#finite, so that we could remove the data.fintype.basic dependency of data.set.finite and try to lower these things.

When I reorganized this module back in May, my goal was to get things thematically in order and to figure out dependencies. An obvious thing to split out now are all the fintype instances for sets -- data.set.finite has long been a mismash of set.finite and things about finite sets.

Kyle Miller (Nov 15 2022 at 21:59):

Organizationally, many of the set.finite constructors come from these finite or fintype instances, but these don't have to be in the module that defines set.finite

Yaël Dillies (Nov 15 2022 at 21:59):

Yes, that's exactly my thought.

Jireh Loreaux (Nov 15 2022 at 21:59):

Patrick, sure, finiteness is very basic, but I often consider filters as similarly basic, but your finite intersection argument definitely convinced me.

Adam Topaz (Nov 15 2022 at 22:01):

Of course, everyone's favorite definition of a finite set is that every ultrafilter is principal ;)

Adam Topaz (Nov 15 2022 at 22:03):

(Maybe I've been thinking about condensed mathematics too much)

Kevin Buzzard (Nov 16 2022 at 01:35):

I think that in ZF it's consistent that every ultrafilter on the naturals is principal :-)

Junyan Xu (Nov 16 2022 at 04:08):

https://en.wikipedia.org/wiki/Ultrafilter_(set_theory)#Weaker_statements says

ZF alone does not even imply that there exists a non-principal ultrafilter on some set.

Jireh Loreaux (Nov 16 2022 at 04:35):

yeah, the ultrafilter lemma is equivalent to the Boolean prime ideal theorem

Junyan Xu (Nov 16 2022 at 04:54):

The Wikipedia page says this is strictly weaker than the ultrafilter lemma, but ZF still doesn't imply it.

Jireh Loreaux (Nov 16 2022 at 06:20):

oooo, interesting!

Yaël Dillies (Nov 16 2022 at 22:49):

#17574 for the list part of the monster.

Heather Macbeth (Nov 17 2022 at 19:16):

Beyond #17574, it looks like half of data.list.basic doesn't depend on any algebra at all, just

import data.option.basic
import logic.nontrivial
import order.basic

See branch#hrmacbeth-minimal-list. I have never looked at this file and can't tell whether the algebra-independent half has any coherence or content. Could someone who has comment on whether this split is worthwhile?

Heather Macbeth (Nov 17 2022 at 19:17):

(The "algebra" in the other half, with imports

import algebra.order.with_zero
import data.nat.order.lemmas
import data.set.function

seems to be mostly addition and subtraction of natural numbers.)

Mario Carneiro (Nov 17 2022 at 19:20):

I'm inclined to say that you should have data.nat.basic lemmas available (assuming that doesn't pull in the algebraic hierarchy). That should give you a much bigger fraction of the file

Heather Macbeth (Nov 17 2022 at 19:20):

Currently data.nat.basic imports

import order.basic
import algebra.group_with_zero.basic
import algebra.ring.defs

Mario Carneiro (Nov 17 2022 at 19:21):

also note that most of data.nat.basic is in Std now, so it is "free" from a untangling-imports perspective (but this hasn't been reflected in lean 3)

Mario Carneiro (Nov 17 2022 at 19:21):

maybe data.nat.basic needs a split then?

Mario Carneiro (Nov 17 2022 at 19:23):

I'm pretty sure most of data.nat.basic is "stuff that should have been in core" (i.e. no dependencies), that's the stuff that is in Std now and which should be split off

Heather Macbeth (Nov 17 2022 at 19:23):

Indeed. But this is getting clearly into Scott's territory so let's wait til he wakes up.

Scott Morrison (Nov 17 2022 at 23:26):

Oh dear, I don't want my enthusiasm for splitting files to prevent other people splitting files!!!

Scott Morrison (Nov 17 2022 at 23:27):

So maybe I should just say: yes, obviously data.nat.basic and data.list.basic deserve splitting, and we should do it real-soon-now. :-)

Yaël Dillies (Nov 17 2022 at 23:52):

Well I had a split for data.fintype.basic but you got yours out first :sweat_smile:

Heather Macbeth (Nov 19 2022 at 05:34):

I started a branch aiming to remove

algebra.group_with_zero.divisibility
algebra.order.with_zero
algebra.ring.divisibility
data.set.basic

from the (indirect) imports of data.list.basic. Progress so far: branch#list-nat-order

Is this worth persevering with?

Heather Macbeth (Nov 19 2022 at 06:29):

So far so good, so I opened #17616.

Heather Macbeth (Nov 23 2022 at 18:07):

#17691 is another small PR towards untangling finiteness.

Heather Macbeth (Nov 24 2022 at 00:13):

Another PR working on the imports of data.list.*: #17702


Last updated: Dec 20 2023 at 11:08 UTC