data.set.basic

Stream: mathlib4

[Yaël Dillies]

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]

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]

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

[Scott Morrison]

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

[Scott Morrison]

Sleep first. :-)

[Yaël Dillies]

In 24±ε hours

[Yaël Dillies]

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]

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

[Yaël Dillies]

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

[Yaël Dillies]

/me is starting the actual split

[Yaël Dillies]

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]

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

[Shreyas Srinivas]

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

[Shreyas Srinivas]

I am actually waiting for data.order.symm_diff

[Sky Wilshaw]

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

[Shreyas Srinivas]

but symm_diff only depends on boolean_algebra

[Shreyas Srinivas]

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

[Yaël Dillies]

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

[Sky Wilshaw]

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]

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

[Shreyas Srinivas]

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]

Have you looked at what files are currently available?

[Shreyas Srinivas]

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]

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]

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

[Sky Wilshaw]

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

[Yaël Dillies]

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

[Yaël Dillies]

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

[Ruben Van de Velde]

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

[Yaël Dillies]

I am not planning to, no.

[Shreyas Srinivas]

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]

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]

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]

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]

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]

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

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]

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]

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]

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]

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]

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]

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]

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]

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

[Yaël Dillies]

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]

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]

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]

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

[Chris Hughes]

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]

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]

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]

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]

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]

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

[Yaël Dillies]

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]

No problem. I hope everything works out okay.

[Scott Morrison]

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

[Mauricio Collares]

The PR builds, though (modulo linting failures)

[Scott Morrison]

Which PR?

[Scott Morrison]

Oh! #17825.

[Scott Morrison]

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

[Scott Morrison]

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]

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]

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

[Scott Morrison]

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

[Mario Carneiro]

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

[Scott Morrison]

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

[Scott Morrison]

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

[Mario Carneiro]

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

[Scott Morrison]

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

[Eric Wieser]

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]

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]

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]

'' is standard in the set theory literature afaiu.

[Eric Wieser]

If you could make standard maths notation $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]

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

[Eric Wieser]

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

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

[Thomas Murrills]

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]

f ❨ S ❩

[Thomas Murrills]

f ❪ S ❫

[Thomas Murrills]

f ⟮ S ⟯

[Eric Wieser]

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]

Personally I would prefer infix

[Eric Wieser]

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]

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]

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]

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

[Richard Osborn]

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

[Thomas Murrills]

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]

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

[Eric Wieser]

Symmetry with preimage is something else to consider

[Thomas Murrills]

Good point! What’s that syntax like?

[Eric Wieser]

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]

Is it just ⁻¹?

[Yaël Dillies]

f ⁻¹' s, rather

[Thomas Murrills]

ah, I see

[Pedro Sánchez Terraf]

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]

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

[Patrick Massot]

Can we get $f_*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]

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

[Eric Wieser]

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]

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

[Johan Commelin]

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

[Johan Commelin]

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]

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]

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]

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]

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

[Ruben Van de Velde]

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]

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

[Kevin Buzzard]

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

[Johan Commelin]

I'm not aware of any such reason

[Ruben Van de Velde]

Just docs/references.bib, maybe

[Johan Commelin]

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

[Scott Morrison]

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

[Scott Morrison]

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

[Scott Morrison]

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

[Scott Morrison]

Maybe we need a 1000 line linter. :-)

[Scott Morrison]

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]

I'll take a look

[Scott Morrison]

I better go make dinner here. :-)

[Johan Commelin]

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]

It's working now

[Scott Morrison]

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

[Johan Commelin]

Ok, let me try to fix the other one

[Scott Morrison]

oh, simp closes the goal

[Scott Morrison]

We're done!

[Johan Commelin]

Great!

[Scott Morrison]

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

[Scott Morrison]

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

[Scott Morrison]

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

[Scott Morrison]

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

[Ruben Van de Velde]

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

[Kevin Buzzard]

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]

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

[Eric Wieser]

And #17853 for algebra.algebra.basic

[Notification Bot]

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

[Scott Morrison]

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]

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

[Mario Carneiro]

What is the coe function from Set A to Type?

[Scott Morrison]

This is itself a hack:

[Scott Morrison]

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

why is it an abbrev?

[Mario Carneiro]

it should be a regular declaration

[Mario Carneiro]

I'm not sure I would call it a hack

[Mario Carneiro]

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

[Scott Morrison]

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

[Mario Carneiro]

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

[Mario Carneiro]

I'm not sure, should it be?

[Scott Morrison]

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

[Scott Morrison]

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

[Sebastian Ullrich]

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

[Mario Carneiro]

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

[Mario Carneiro]

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

[Yaël Dillies]

nonempty_subtype and nonempty_coe_sort are duplicates

[Scott Morrison]

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]

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

[Mario Carneiro]

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

[Mario Carneiro]

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

[Mario Carneiro]

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

[Johan Commelin]

Ok, let's get this merged

[Johan Commelin]

Ooh, Scott already did (-;