Zulip Chat Archive

Stream: mathlib4

Topic: data.set.basic


Yaël Dillies (Dec 03 2022 at 01:05):

Please can people not port data.set.basic? I am working on splitting it up (part of the motivation is previous discussions here and the other part is in #17801).

Kevin Buzzard (Dec 03 2022 at 01:07):

It's very much on the porting radar so I would recommend prioritising it, doing nothing in the PR other than splitting it, and asking for a speedy merge when you're ready.

Yaël Dillies (Dec 03 2022 at 01:08):

Yeah, I know and I will try, but I need some :zzz: first

Scott Morrison (Dec 03 2022 at 01:08):

@Yaël Dillies, how soon do you think you can have your PR in by?

Scott Morrison (Dec 03 2022 at 01:09):

Sleep first. :-)

Yaël Dillies (Dec 03 2022 at 01:09):

In 24±ε hours

Yaël Dillies (Dec 03 2022 at 21:50):

Update: I'm waiting for #17805 (some cleanup that's easier to do once than twice) before performing the actual split. I already tried a prototype split in local and it seems to go down well.

Ruben Van de Velde (Dec 03 2022 at 22:07):

@Yaël Dillies build seems to be failing in 17805

Yaël Dillies (Dec 03 2022 at 22:12):

Feel free to fix. I'm off for the next couple of hours

Yaël Dillies (Dec 05 2022 at 10:26):

/me is starting the actual split

Yaël Dillies (Dec 05 2022 at 14:04):

Here's the PR: #17825. Beware it's a complete mess still. I'm gonna do something else for the next few hours because I exhausted my productivity.

Yaël Dillies (Dec 05 2022 at 14:05):

I'm happy to take comments but please don't touch it yet. I have enough to wrangle with myself.

Shreyas Srinivas (Dec 05 2022 at 16:42):

I am working on data.set.basic. What would you suggest?

Shreyas Srinivas (Dec 05 2022 at 16:42):

I am actually waiting for data.order.symm_diff

Sky Wilshaw (Dec 05 2022 at 16:43):

This file probably can't be ported just yet, we need to wait for #17825 to land.

Shreyas Srinivas (Dec 05 2022 at 16:44):

but symm_diff only depends on boolean_algebra

Shreyas Srinivas (Dec 05 2022 at 16:44):

and that has been ported as of two or three days ago.

Yaël Dillies (Dec 05 2022 at 16:46):

If you want to contribute to the port, may I suggest you first try porting a file that's less critical?

Sky Wilshaw (Dec 05 2022 at 16:46):

mathlib4#842 has been approved to merge data.order.symm_diff, but bors is a bit broken so it hasn't been merged yet.

Yaël Dillies (Dec 05 2022 at 16:47):

At any rate, please nobody port data.set.basic yet.

Shreyas Srinivas (Dec 05 2022 at 16:52):

Yaël Dillies said:

If you want to contribute to the port, may I suggest you first try porting a file that's less critical?

Okay. Could you suggest where I might begin? I am a CS theorist in training (i.e. doing my PhD). My interests go towards combinatorics, graphs theory, computability etc, and at least some of the relevant files rely on data.set

Yaël Dillies (Dec 05 2022 at 16:53):

Have you looked at what files are currently available?

Shreyas Srinivas (Dec 05 2022 at 16:54):

I checked https://math.commelin.net/files/port_status.html
Of the files that have had their immediate dependencies ported, it appears all are taken. Before reading this conversation, I was waiting for order.symm_diff to go through before porting data.set.basic

Sky Wilshaw (Dec 05 2022 at 16:55):

Here's a more up to date one:

# The following files have all dependencies ported already, and should be ready to port:
# Earlier items in the list are required in more places in mathlib.
control.traversable.basic    -- mathlib4#788 @kbuzzard 1fc36cc9c8264e6e81253f88be7fb2cb6c92d76a
algebra.divisibility.basic    -- mathlib4#833 70d50ecfd4900dd6d328da39ab7ebd516abe4025
lean_core.data.vector    -- mathlib4#834 e574b1a4e891376b0ef974b926da39e05da12a06
data.string.basic    -- WIP @javra
data.nat.bits
control.bifunctor    -- mathlib4#809 62a5626868683c104774de8d85b9855234ac807c
category_theory.functor.fully_faithful    -- WIP mathlib4#846 70d50ecfd4900dd6d328da39ab7ebd516abe4025
category_theory.bicategory.basic    -- Depending on slice tactic
algebra.group.ext    -- mathlib4#850 e574b1a4e891376b0ef974b926da39e05da12a06
data.stream.init    -- mathlib4#849 e574b1a4e891376b0ef974b926da39e05da12a06
data.rbtree.init    -- WIP @digama
data.typevec    -- WIP j-loreaux
control.monad.writer
data.rbtree.default_lt    -- WIP @digama
category_theory.category.Kleisli    -- WIP mathlib4#843 70d50ecfd4900dd6d328da39ab7ebd516abe4025
lean_core.data.buffer.parser
data.two_pointing    -- WIP Yaël
data.vector3    -- WIP Thomas mathlib4#633 fd47bdf09e90f553519c712378e651975fe8c829
lean_core.data.dlist
data.erased
data.json
data.mllist    -- probably not needed
data.nat.even_odd_rec
data.sigma.default    -- do not port default files
algebra.group_with_zero.default    -- do not port default files
algebra.ring.default    -- do not port default files
combinatorics.quiver.push
lean_core.algebraic_geometry.EllipticCurve

# The following files have their immediate dependencies ported already, and may be ready to port:
order.hom.basic    -- please adopt mathlib4#804 62a5626868683c104774de8d85b9855234ac807c
order.symm_diff    -- mathlib4#842 6eb334bd8f3433d5b08ba156b8ec3e6af47e1904
algebra.group.type_tags    -- mathlib4#832 6eb334bd8f3433d5b08ba156b8ec3e6af47e1904
algebra.order.monoid.with_zero.defs    -- mathlib4#851 dad7ecf9a1feae63e6e49f07619b7087403fb8d4
algebra.hom.equiv.basic    -- mathlib4#835 76171581280d5b5d1e2d1f4f37e5420357bdc636
data.sigma.order    -- WIP j-loreaux
order.heyting.boundary    -- mathlib4#844 70d50ecfd4900dd6d328da39ab7ebd516abe4025

Ruben Van de Velde (Dec 05 2022 at 16:55):

Yaël, I'm not seeing the mathlib4 companion pr to #17825 yet, when do you think you'll have it ready?

Sky Wilshaw (Dec 05 2022 at 16:55):

Given you have a CS background, maybe the things in data or control might be more accessible to you.

Yaël Dillies (Dec 05 2022 at 16:56):

I will open it once I got #17825 to compile. I'm not a great fan of work duplication!

Yaël Dillies (Dec 05 2022 at 16:58):

... also because I will need to port some of data.set.basic while doing so.

Ruben Van de Velde (Dec 05 2022 at 17:02):

Just to be clear: are you going to expand the scope of your block further after this?

Yaël Dillies (Dec 05 2022 at 17:02):

I am not planning to, no.

Shreyas Srinivas (Dec 05 2022 at 17:04):

If data.set.basic is t
Sky Wilshaw said:

Given you have a CS background, maybe the things in data or control might be more accessible to you.

I think I will take up data.nat.bits then. I'd be happy to help with files under data.set too because from a theorist's point of view, these appear to be the most important for graph theory and combinatorics.

Yaël Dillies (Dec 05 2022 at 17:04):

I can tell you that the most important files for combinatorics are rather the ones involving docs#finset, but we're far from it still!

Sky Wilshaw (Dec 05 2022 at 17:06):

As far as I'm aware, there are some changes from Lean 3 to Lean 4 involving bit0 and bit1 - I'd ask some others for advice on this.

Shreyas Srinivas (Dec 05 2022 at 17:14):

okay, in that case I'd like to remove the WIP for data.set.basic in the port status file. But I don't seem to have the permission to edit the wiki. What's the process to get this?

Shreyas Srinivas (Dec 05 2022 at 17:14):

Sky Wilshaw said:

As far as I'm aware, there are some changes from Lean 3 to Lean 4 involving bit0 and bit1 - I'd ask some others for advice on this.

Thanks, I will open a separate thread for this.

Kevin Buzzard (Dec 05 2022 at 20:02):

@Shreyas Srinivas I'm really sorry that it's difficult for you to find something to do. There is a lot of stuff going on which those "in the know" know about (e.g. the complications with data.set.basic and the fact that data.nat.bits is kind of being ignored because we don't know exactly what form we want it to be in in Lean 4). If you want some advice about where to find files to port, here's the algorithm I'm using.

1) Look at the pdfs being generated by a bot in the "port progress" thread in this #mathlib4 stream.
2) Choose a goal which we're making progress on, or a goal you're interested in.
3) Take a look at the linked pdf and see where the boundary is (green files are done, blue files are being worked on, white files are not done) and then check in the port-status wiki page and perhaps also glance through the open PRs in mathlib4 and also perhaps search this site for the name of the file just to check there are no problems with it.
4) Claim that file by editing the wiki page, making a branch in mathlib4, copying the autoported effort from mathlib3port, pushing to github and stating the mathlib3 commit (taken from the mathlib3port readme) in your first message on github about the file.
5) Get stuck in, and if you get stuck then create a new thread here in the mathlib4 stream with questions (questions are answered more quickly on Zulip than on github).

Good luck! You'll need push access to non-master branches in both mathlib3 and mathlib4; to do that you'll need to ask a maintainer for push rights to non-master branches of these repos and they'll need to know your github userid.

Sky Wilshaw (Dec 05 2022 at 21:26):

I think the biggest current difficulty (at least, from my limited perspective!) is the small number of available files. Because we're so early on in the port, I managed to port loads of files at the end of last week but since have found it really hard to make progress after I'd finished the easy ones.

Sky Wilshaw (Dec 05 2022 at 21:28):

My hope is that after we finish data.set.basic and algebra.order.field.defs, the amount of free files should start increasing.

Scott Morrison (Dec 05 2022 at 23:40):

I'm pretty concerned that this PR is going to hold everything up, at the worst possible time. (People are waiting to port this file, and it is on the critical path for the targets that we need to have done in the next two weeks so people preparing courses using Lean4 can do their course prep!)

Scott Morrison (Dec 05 2022 at 23:41):

I think we need to get this PR compiling and linting asap, and to prepare the mathlib4 port, which may require considerable work. I'll try to come back to this later today, but if anyone wants to fix the linting issues and downstream problems with missing imports, that would be great.

Yaël Dillies (Dec 06 2022 at 01:45):

Yeah I'm putting as much time as I can into it. Hopefully the split will be ready by this evening and compiling by the end of tomorrow.

Chris Hughes (Dec 06 2022 at 18:46):

Just to give @Yaël Dillies a sense of urgency. There are only six files in mathlib4 right now that are ready to be ported (i.e. all dependencies are ported) and aren't currently part of an open PR. There isn't really very much left to do that does not depend on data.set.basic.

Yaël Dillies (Dec 06 2022 at 18:47):

I've been trying for the past two hours to work on it from the Eurostar, but alas it just never loaded :sad:

Heather Macbeth (Dec 06 2022 at 18:50):

Kevin Buzzard said:

It's very much on the porting radar so I would recommend prioritising it, doing nothing in the PR other than splitting it, and asking for a speedy merge when you're ready.

Maybe you could switch to a more modest PR, along the lines of Kevin's advice. If I understand correctly you are currently doing a refactor (of order/monotone) as well as a split.

Yaël Dillies (Dec 06 2022 at 19:01):

Yes, this is needed to insert the coe to sort coercion before order.monotone

Yaël Dillies (Dec 06 2022 at 19:03):

There are already available subplits in the form of data.set.image, but they won't help with the port because those will be new files after data.set.basic

Yaël Dillies (Dec 06 2022 at 19:05):

If somebody wants to PR those subsplits independently, please do so! They are basically ready (just need module docs) and will fluidify the rest of the split (by having less downstream imports that need fixing).

Chris Hughes (Dec 06 2022 at 19:11):

Yaël Dillies said:

There are already available subplits in the form of data.set.image and data.set.n_ary, but they won't help with the port because those will be new files after data.set.basic

I imagine that it won't be long before data.set.image blocks something. There's not much that depends on sets but not images.

Chris Hughes (Dec 06 2022 at 19:11):

What needs to be done on the set file? Is it just fixing the build?

Chris Hughes (Dec 06 2022 at 19:21):

I think this PR will cause a bottleneck in Mathlib4 and prevent anyone from working on the port for a few days, particularly given that it changes already ported files. I'm leaning towards being much more firm about the idea of not changing already ported files in mathlib and generating much more work in the port and not merging this refactor unless it is done in Mathlib4.

Yaël Dillies (Dec 06 2022 at 21:45):

What is bothering you exactly? That there's no corresponding mathlib4 PR? Writing it will be much easier than writing the mathlib PR, so I've decided to do it once I managed to stabilise #17825.

Scott Morrison (Dec 06 2022 at 22:07):

Yael, the problem is that most of the porting effort is now held up by this PR. Other people can't work on the port because of your PR.

Ruben Van de Velde (Dec 06 2022 at 22:36):

I feel like #17825 is trying to do so much at once that there's no way it's getting finished in a reasonable time - so many changes to argument order, proofs, ...

As an alternative, I pushed #17835, which should be easily reviewable commit-by-commit and highly unlikely to contain unintended changes. It doesn't do everything #17825 wants to do, but it creates a data.set.defs which doesn't import order.monotone, so should be a lot easier to build on top if if we decide to go forward.

I'd also be fine just not making any sweeping changes in mathlib3, of course

Eric Wieser (Dec 06 2022 at 22:37):

Yaël Dillies said:

If somebody wants to PR those subsplits independently, please do so! They are basically ready (just need module docs) and will fluidify the rest of the split (by having less downstream imports that need fixing).

I did set.n_ary in #17836

Ruben Van de Velde (Dec 06 2022 at 22:37):

That's it for me today - feel free to pick it up from here

Yaël Dillies (Dec 06 2022 at 22:59):

I have a family emergency. I won't be able to do anything today, maybe tomorrow as well. Please do whatever and sorry for the terrible timing.

Scott Morrison (Dec 06 2022 at 23:00):

No problem. I hope everything works out okay.

Scott Morrison (Dec 06 2022 at 23:00):

I think in this case we will just delay refactoring data.set.basic until after it has been ported.

Mauricio Collares (Dec 06 2022 at 23:09):

The PR builds, though (modulo linting failures)

Scott Morrison (Dec 06 2022 at 23:22):

Which PR?

Scott Morrison (Dec 06 2022 at 23:22):

Oh! #17825.

Scott Morrison (Dec 06 2022 at 23:23):

Okay, let's see if we can get it done, then.

Scott Morrison (Dec 06 2022 at 23:23):

I just had a look a porting data.set.basic as is. It's not too bad. There are a lot of broken proofs (and some that use tauto or cc, which we don't have for now.)

Scott Morrison (Dec 06 2022 at 23:25):

I'm not immediately sure how to fix the notation:

infixl:80 " '' " => image

theorem mem_image_iff_bex {f : α  β} {s : Set α} {y : β} :
    y  f '' s   (x : _)(_ : x  s), f x = y :=
  bex_def.symm

Fails at f '' s with missing end of character literal.

Scott Morrison (Dec 06 2022 at 23:25):

(If anyone wants to have a look, this is on the branch data_set_basic.)

Scott Morrison (Dec 06 2022 at 23:46):

I think I fixed the last linting errors on #17825.

Mario Carneiro (Dec 07 2022 at 00:05):

That sounds like a lexer issue, it should be fixable in core

Scott Morrison (Dec 07 2022 at 00:45):

Okay, we better #mwe it. I can hopefully do that later today, but if anyone is keen, please go ahead. :-)

Scott Morrison (Dec 07 2022 at 02:35):

Reported as https://github.com/leanprover/lean4/issues/1922

Mario Carneiro (Dec 07 2022 at 02:44):

Hm, since '' doesn't work maybe you should use ' to disambiguate it: f ''' s

Scott Morrison (Dec 07 2022 at 03:18):

I've temporarily gone with !!. Hopefully we won't forget to change it back. :-)

Eric Wieser (Dec 07 2022 at 22:06):

Yaël Dillies said:

If somebody wants to PR those subsplits independently, please do so! They are basically ready (just need module docs) and will fluidify the rest of the split (by having less downstream imports that need fixing).

set.image is in #17842

Kevin Buzzard (Dec 07 2022 at 22:23):

Re '': I think it's worth remarking that although '' is standard mathlib notation, it's not actually standard mathematical notation (despite Mario's claims that he saw it in a book once), so perhaps our instinct "please let us keep our nonstandard notation which we're used to" could be turned into "maybe we can fall in love with a new notation" if this issue is actually problematic. If you could make standard maths notation f(S) work (here f : X->Y and S : set Y) that would be even better ;-) Maybe even a weird unicode bracket? We use a weird unicode symbol for divides, after all, and nobody complains about that, because it was always there.

Thomas Murrills (Dec 07 2022 at 22:25):

All I can contribute to this is that from my perspective (a math person new to lean), '' does indeed look pretty strange and unfriendly!

Yaël Dillies (Dec 07 2022 at 22:26):

'' is standard in the set theory literature afaiu.

Eric Wieser (Dec 07 2022 at 22:28):

If you could make standard maths notation f(S)f(S) work

sometimes you can write f • s...

import group_theory.group_action.basic
open_locale pointwise
example {α} (f : function.End α) (s : set α) : f  s = f '' s := rfl

Scott Morrison (Dec 07 2022 at 22:29):

If anyone wants to propose some alternatives in case we can't keep '', we can use that in the interim instead of !!.

Eric Wieser (Dec 07 2022 at 22:30):

<$> also already works:

universes u  -- doesn't work over different universes
example {α : Type u} {β : Type u} (f : α  β) (s : set α) : f <$> s = f '' s := rfl

Eric Wieser (Dec 07 2022 at 22:35):

How about f ″ s? ( is "double prime")

Thomas Murrills (Dec 07 2022 at 22:35):

Here are some round Unicode brackets reminiscent of the standard (outside of actual set theory :) ) image notation—not sure if they’re visually distinct enough from ascii though.

Thomas Murrills (Dec 07 2022 at 22:35):

f ❨ S ❩

Thomas Murrills (Dec 07 2022 at 22:36):

f ❪ S ❫

Thomas Murrills (Dec 07 2022 at 22:37):

f ⟮ S ⟯

Eric Wieser (Dec 07 2022 at 22:37):

I think brackets would be a bad idea, especially while simultaneously trying to teach newcomers that in lean functions are written without brackets

Scott Morrison (Dec 07 2022 at 22:37):

Personally I would prefer infix

Eric Wieser (Dec 07 2022 at 22:38):

I'd really like if we could make <$> work (by rewriting the monad framework to be universe polymorphic), because then we could use the same notation for docs#finset.map, docs#subgroup.map, ... as well. But that's probably not a viable thing to try until after the port.

Thomas Murrills (Dec 07 2022 at 22:41):

I don’t think there’s a standard infix notation for the image recognizable by most mathematicians, so I suppose that opens it up to anything with the right vibes! (Other brackets I found included turtle shell, if not used for anything else: f ❲ S ❳)

Thomas Murrills (Dec 07 2022 at 22:47):

Though…I might gently caution against <$> if the goal is “make mathlib notation friendly to mathematicians”. That seems complicated and programmer-y to me, whereas at least '' is visually simple and has precedent in a niche area of math (well, they’re all niche, ultimately, but you know what I mean :) )

But on the other hand…maybe it would open up mathematicians to the joys of monads and unify the concept of image with other map operations in math…? Maybe programmer notation has something to add here? :) Just some thoughts.

Scott Morrison (Dec 07 2022 at 22:51):

I agree '' is much better than <$>, for the purpose of not making mathematicians' eyes glaze over.

Richard Osborn (Dec 07 2022 at 23:22):

Would a unicode double quote work? Not sure which one would best

Thomas Murrills (Dec 07 2022 at 23:44):

Eric Wieser has mentioned one such (presumably interim?) option—just for fun I wanted to see what others I could find on shapecatcher.
Two characters: Ꞌ Ꞌ ˈ ˈ
One character: (ʺ)
(Though I imagine !! is more convenient to use as a placeholder, so I’m guessing this would only be useful if the parsing issue is somehow insurmountable…)

Thomas Murrills (Dec 07 2022 at 23:47):

Though, actually, the one-character nature of f ᐦ S is kind of visually nice regardless, if it can be entered easily…!

Eric Wieser (Dec 07 2022 at 23:48):

Symmetry with preimage is something else to consider

Thomas Murrills (Dec 07 2022 at 23:48):

Good point! What’s that syntax like?

Eric Wieser (Dec 07 2022 at 23:48):

Note also that as of the commit to mathlib3 just now (which won't be in mathport yet), notation for '' is no longer a decision that needs to be made to port data.set.basic (it now lives in data.set.image)

Thomas Murrills (Dec 07 2022 at 23:49):

Is it just ⁻¹?

Yaël Dillies (Dec 07 2022 at 23:50):

f ⁻¹' s, rather

Thomas Murrills (Dec 07 2022 at 23:51):

ah, I see

Pedro Sánchez Terraf (Dec 07 2022 at 23:53):

Yaël Dillies said:

'' is standard in the set theory literature afaiu.

It's kind of f “ S. Sorry if too late for this comment.

Yaël Dillies (Dec 07 2022 at 23:55):

Yes, I know. I guess I meant "is the ascii equivalent of..."

Patrick Massot (Dec 08 2022 at 00:18):

Can we get fSf_*S to work with any map operation? I know it wasn't possible in Lean 3 for universe reasons, but maybe we can have a specific elaborator in Lean 4.

Eric Wieser (Dec 08 2022 at 00:23):

I think it was already possible in lean3, we'd just have to reinvent all the monad typeclasses in a polymorphic way

Eric Wieser (Dec 08 2022 at 00:24):

Maybe there's a universe elaboration issue I'm not aware of; I thought the limitation was just the way the typeclasses in core were designed.

Johan Commelin (Dec 08 2022 at 06:46):

Like Patrick suggests, having some version of _* as notation for map would be really nice.

Johan Commelin (Dec 08 2022 at 06:46):

I don't think we necessarily need to rewrite all the monad infrastructure.

Johan Commelin (Dec 08 2022 at 06:48):

Something like

class has_map (X Y Z : Type*) := -- probably `Z` should be out_param
(map := X -> Y -> Z)

which can have instances for X = A -> B, Y = set A, Z = set B. But also for X = A ->+* B, Y = ideal A, Z = ideal B, etc...

Scott Morrison (Dec 08 2022 at 08:19):

I've manually updated https://github.com/leanprover-community/mathlib4/pull/892 to remove the material that was moved out in https://github.com/leanprover-community/mathlib/pull/17842.

Kevin Buzzard (Dec 08 2022 at 08:25):

Are we going to go through this chaos several more times? This is not a good use of your time Scott. What other big files need a mathlib3 refactor before porting? If there are any then it would make sense to do them ASAP rather than just as the tide hits them. But maybe this is the last big example?

Johan Commelin (Dec 08 2022 at 08:29):

Top 50 long files (data/set/basic is now almost at the bottom):

    4194 src/data/list/basic.lean
    4012 src/measure_theory/measure/measure_space.lean
    3494 src/analysis/calculus/cont_diff.lean
    3193 src/group_theory/subgroup/basic.lean
    3132 src/analysis/calculus/fderiv.lean
    3086 src/topology/metric_space/basic.lean
    3061 src/data/finset/basic.lean
    3032 src/measure_theory/integral/lebesgue.lean
    2956 src/measure_theory/function/lp_space.lean
    2711 src/measure_theory/integral/interval_integral.lean
    2678 src/topology/algebra/order/basic.lean
    2676 src/data/buffer/parser/basic.lean
    2602 src/order/filter/basic.lean
    2489 src/tactic/core.lean
    2449 src/computability/turing_machine.lean
    2429 src/analysis/inner_product_space/basic.lean
    2378 src/set_theory/ordinal/arithmetic.lean
    2369 src/data/multiset/basic.lean
    2355 src/ring_theory/ideal/operations.lean
    2273 src/measure_theory/function/conditional_expectation/basic.lean
    2248 src/category_theory/limits/shapes/pullbacks.lean
    2229 src/analysis/special_functions/pow.lean
    2209 src/analysis/calculus/deriv.lean
    2176 src/linear_algebra/basic.lean
    2122 src/measure_theory/constructions/borel_space.lean
    2118 docs/references.bib
    2106 src/algebraic_geometry/open_immersion.lean
    2101 src/topology/algebra/module/basic.lean
    2079 src/data/matrix/basic.lean
    2049 src/ring_theory/power_series/basic.lean
    2014 src/data/real/ennreal.lean
    1988 src/data/dfinsupp/basic.lean
    1987 src/analysis/normed_space/operator_norm.lean
    1937 src/ring_theory/unique_factorization_domain.lean
    1932 src/topology/separation.lean
    1907 src/measure_theory/function/strongly_measurable/basic.lean
    1898 src/algebra/big_operators/basic.lean
    1896 src/topology/subset_properties.lean
    1886 src/measure_theory/integral/set_to_l1.lean
    1874 src/data/fin/basic.lean
    1872 src/algebra/algebra/basic.lean
    1851 src/data/set/lattice.lean
    1792 src/topology/uniform_space/basic.lean
    1763 src/combinatorics/simple_graph/connectivity.lean
    1750 src/geometry/manifold/mfderiv.lean
    1731 src/order/filter/at_top_bot.lean
    1728 src/data/set/basic.lean
    1728 src/analysis/normed/group/basic.lean
    1725 src/analysis/asymptotics/asymptotics.lean
    1691 src/measure_theory/integral/bochner.lean

Ruben Van de Velde (Dec 08 2022 at 08:30):

Okay, and which of those are closest to being available for porting? :)

Ruben Van de Velde (Dec 08 2022 at 08:33):

Seems like data.list.basic only depends on algebra.order.ring.canonical (unported) and data.nat.order.basic (ported in a pr), so we probably shouldn't touch it

Johan Commelin (Dec 08 2022 at 08:35):

Otoh, why would data.list.basic depend on algebra.order.ring.canonical...

Kevin Buzzard (Dec 08 2022 at 08:37):

Is there ever a good reason for letting files become more than 1000 lines long?

Johan Commelin (Dec 08 2022 at 08:38):

I'm not aware of any such reason

Ruben Van de Velde (Dec 08 2022 at 08:38):

Just docs/references.bib, maybe

Johan Commelin (Dec 08 2022 at 08:39):

There are currently 186 lean files that are > 1000 lines long

Scott Morrison (Dec 08 2022 at 08:47):

Okay, data.set.basic is almost ready to go.

Scott Morrison (Dec 08 2022 at 08:47):

One or two broken proofs, if someone wants to take over.

Scott Morrison (Dec 08 2022 at 08:48):

Yes, these refactors should have been done a while back, I guess. It's accumulated technical debt...

Scott Morrison (Dec 08 2022 at 08:50):

Maybe we need a 1000 line linter. :-)

Scott Morrison (Dec 08 2022 at 08:51):

All that is left on data.set.basic is a proof by itauto that has to be written out by hand, and a complicated simp that is failing, I don't quickly see how to reproduce it.

Johan Commelin (Dec 08 2022 at 08:52):

I'll take a look

Scott Morrison (Dec 08 2022 at 08:52):

I better go make dinner here. :-)

Johan Commelin (Dec 08 2022 at 09:31):

Hmmm, I'm struggling to get the newest Lean version working with VScode. I guess I need to go through a huge update fest.

Johan Commelin (Dec 08 2022 at 09:44):

It's working now

Scott Morrison (Dec 08 2022 at 09:55):

I replaced the itauto with the term mode proof from show_term {itauto} in mathlib3...

Johan Commelin (Dec 08 2022 at 09:56):

Ok, let me try to fix the other one

Scott Morrison (Dec 08 2022 at 09:56):

oh, simp closes the goal

Scott Morrison (Dec 08 2022 at 09:56):

We're done!

Johan Commelin (Dec 08 2022 at 09:57):

Great!

Scott Morrison (Dec 08 2022 at 09:57):

I'm never sure how much effort to put into working out why simp has changed.

Scott Morrison (Dec 08 2022 at 09:58):

Some fraction of the simp failures are worth diagnosing and fixing, as they'll make life easier later.

Scott Morrison (Dec 08 2022 at 09:58):

But it's very hard to guess how big that fraction is, or whether you're in it...

Scott Morrison (Dec 08 2022 at 09:59):

Oof, it definitely doesn't #lint...

Ruben Van de Velde (Dec 08 2022 at 10:44):

I'm taking a look at src/group_theory/subgroup/basic.lean, fwiw

Kevin Buzzard (Dec 08 2022 at 10:46):

That file was a personal goal for me in the porting process, because I felt that by the time we'd got to subgroups it would be possible to start marketing the port to young mathematicians. I got a bunch of people at Xena to write a lot of those files (bundled subgroups, subrings,.sub-other things) the first time around and it was a really good learning experience for them.

Eric Wieser (Dec 08 2022 at 11:04):

I made #17852 to push data.finset.basic a bit towards the bottom of that list

Eric Wieser (Dec 08 2022 at 11:40):

And #17853 for algebra.algebra.basic

Notification Bot (Dec 08 2022 at 12:55):

86 messages were moved from this topic to #mathlib4 > set image notation by Eric Wieser.

Scott Morrison (Dec 08 2022 at 22:34):

The remaining lint lemmas for data.set.basic warrant some discussion:

#check @nonempty_coe_sort /- Left-hand side simplifies from
  Nonempty ↑s
to
  Exists fun a ↦ a ∈ s
using
  simp only [nonempty_subtype]
Try to change the left-hand side to the simplified term!
 -/
#check @is_empty_coe_sort /- Left-hand side simplifies from
  IsEmpty ↑s
to
  ∀ (x : α), ¬x ∈ s
using
  simp only [isEmpty_subtype]
Try to change the left-hand side to the simplified term!
 -/
#check @sep_union /- Left-hand side simplifies from
  { x | x ∈ s ∪ t ∧ p x }
to
  { x | (x ∈ s ∨ x ∈ t) ∧ p x }
using
  simp only [Set.mem_union]
Try to change the left-hand side to the simplified term!
 -/
#check @sep_inter /- Left-hand side simplifies from
  { x | x ∈ s ∩ t ∧ p x }
to
  { x | (x ∈ s ∧ x ∈ t) ∧ p x }
using
  simp only [Set.mem_inter_iff]
Try to change the left-hand side to the simplified term!

Scott Morrison (Dec 08 2022 at 22:36):

They are all examples where simp having become a little bit stronger, we now have divergences in simp "normal form".

Mario Carneiro (Dec 08 2022 at 22:37):

What is the coe function from Set A to Type?

Scott Morrison (Dec 08 2022 at 22:37):

This is itself a hack:

Scott Morrison (Dec 08 2022 at 22:38):

-- Porting note: I've introduced this abbreviation, with the `@[coe]` attribute,
-- so that `norm_cast` has something to index on.
/-- Given the set `s`, `type_of_Set s` is the `Type` of element of `s`. -/
@[coe] abbrev type_of_Set (s : Set α) : Type u := { x // x  s }

/-- Coercion from a set to the corresponding subtype. -/
instance {α : Type u} : CoeSort (Set α) (Type u) :=
  type_of_Set

Mario Carneiro (Dec 08 2022 at 22:38):

why is it an abbrev?

Mario Carneiro (Dec 08 2022 at 22:38):

it should be a regular declaration

Mario Carneiro (Dec 08 2022 at 22:38):

I'm not sure I would call it a hack

Mario Carneiro (Dec 08 2022 at 22:38):

we already had such a function, it was called coe before

Scott Morrison (Dec 08 2022 at 22:38):

Okay, good. Making it regular caused a few more things to break, but they all look fixable.

Mario Carneiro (Dec 08 2022 at 22:40):

It looks like sep_union and friends are because sep is not a thing anymore

Mario Carneiro (Dec 08 2022 at 22:41):

I'm not sure, should it be?

Scott Morrison (Dec 08 2022 at 22:48):

Have to run. I've pushed making type_of_Set a def again, and fixed some of the probles.

Scott Morrison (Dec 08 2022 at 22:48):

There's one broken proof, and we're now missing the Preorder ↑s instance.

Sebastian Ullrich (Dec 09 2022 at 09:21):

Drive-by comment: this should be TypeOfSet, no? Or maybe Set.AsType?

Mario Carneiro (Dec 09 2022 at 09:47):

Yes on the casing convention. How about Set.Elems?

Mario Carneiro (Dec 09 2022 at 09:48):

or should it be Set.Elem since we don't pluralize types

Yaël Dillies (Dec 09 2022 at 10:40):

nonempty_subtype and nonempty_coe_sort are duplicates

Scott Morrison (Dec 12 2022 at 00:51):

data.set.basic is still waiting to be merged and holding lots up. The last problem had been the missing Preorder ↑s instance. Winston had committed a fix that just wrote the relevant instance from Subtype in by hand, but this isn't very satisfactory.

For now I've gone back to making Set.Elem reducible (no need to go so far as abbrev) so that the instances from Subtype come along for free. I'm dubious that this is really the right answer, but since so much is waiting on data.set.basic at the moment, I propose merging as is and then fixing later.

Johan Commelin (Dec 12 2022 at 06:46):

@Mario Carneiro Could you please chime in on this decision?

Mario Carneiro (Dec 12 2022 at 06:49):

Seems like we will want them to be distinct eventually if not already

Mario Carneiro (Dec 12 2022 at 06:49):

I thought that instances on \u s didn't apply to {x // x \in s} already in mathlib

Mario Carneiro (Dec 12 2022 at 06:50):

But I'm fine with doing whatever for now and refactoring later

Johan Commelin (Dec 12 2022 at 06:51):

Ok, let's get this merged

Johan Commelin (Dec 12 2022 at 06:51):

Ooh, Scott already did (-;


Last updated: Dec 20 2023 at 11:08 UTC