Zulip Chat Archive

Stream: general

Topic: fin as a subtype


view this post on Zulip Johan Commelin (Mar 02 2020 at 05:46):

Now that we are changing core, what do people think of redefining fin n as {k // k < n}?

view this post on Zulip Simon Hudon (Mar 02 2020 at 05:56):

Why?

view this post on Zulip Johan Commelin (Mar 02 2020 at 05:59):

Because it's a bit weird to me that this type would get special treating.

view this post on Zulip Johan Commelin (Mar 02 2020 at 06:00):

It's a subtype, but it isn't defined as such.

view this post on Zulip Johan Commelin (Mar 02 2020 at 06:00):

So the whole subtype machinery has to be reproven for fin.

view this post on Zulip Simon Hudon (Mar 02 2020 at 06:04):

For instance?

view this post on Zulip Mario Carneiro (Mar 02 2020 at 06:06):

Well, there are things like fin.eq_of_veq that are just copies of analogous subtype theorems

view this post on Zulip Simon Hudon (Mar 02 2020 at 06:09):

Right but how big is the duplication?

view this post on Zulip Mario Carneiro (Mar 02 2020 at 06:15):

Not that large but it has an effect on all later work. You have to use different functions and different theorems, something like the situation with nat.cast vs int.of_nat

view this post on Zulip Mario Carneiro (Mar 02 2020 at 06:16):

I think it doesn't add anything to write it as a structure like that. It might make sense to have a separate definition if fin was defined using the fancy inductive family construction, but right now it's literally just a subset

view this post on Zulip Simon Hudon (Mar 02 2020 at 06:17):

If someone feels like creating a branch of Lean with this change to see how much mathlib gets simplified, I'd be curious to see

view this post on Zulip Mario Carneiro (Mar 02 2020 at 06:18):

I don't think there will be any simplification, just changing constant names in a few places. It's just more regular

view this post on Zulip Simon Hudon (Mar 02 2020 at 06:18):

To me, it feels a bit like the difference between writing a structure with two fields vs using prod. Sometimes, the structure is a nicer solution

view this post on Zulip Mario Carneiro (Mar 02 2020 at 06:19):

it's not like the names of the fields are especially meaningful here

view this post on Zulip Mario Carneiro (Mar 02 2020 at 06:19):

the defeq to subtype seems useful

view this post on Zulip Simon Hudon (Mar 02 2020 at 06:20):

What about using coercions from and to subtypes?

view this post on Zulip Mario Carneiro (Mar 02 2020 at 06:20):

cycles, can't do it

view this post on Zulip Mario Carneiro (Mar 02 2020 at 06:20):

lean 3 coercions kind of suck

view this post on Zulip Simon Hudon (Mar 02 2020 at 06:20):

I mean functions to convert

view this post on Zulip Mario Carneiro (Mar 02 2020 at 06:22):

The sorts of places where you want the defeq is for higher order objects like a proof that a subtype is encodable implies that fin is encodable

view this post on Zulip Mario Carneiro (Mar 02 2020 at 06:22):

here you need the function to be an equiv and everything has to be transported along it

view this post on Zulip Mario Carneiro (Mar 02 2020 at 06:23):

missing defeqs at the type level are difficult to patch around

view this post on Zulip Simon Hudon (Mar 02 2020 at 06:26):

I don't think there will be any simplification, just changing constant names in a few places. It's just more regular

That sounds like a lot of hassle for very little payoff

view this post on Zulip Yury G. Kudryashov (Mar 02 2020 at 06:27):

BTW, is there any difference between fin.ext_iff and fin.eq_iff_veq?

view this post on Zulip Mario Carneiro (Mar 02 2020 at 06:39):

I prefer to think of changes in terms of how close to ideal they are, rather than how close to today's version they are. The latter mentality leads to cruft

view this post on Zulip Mario Carneiro (Mar 02 2020 at 06:41):

@Yury G. Kudryashov Apparently not, and they are literally neighbors in the file. Someone must have missed the first one and wrote the second

view this post on Zulip Mario Carneiro (Mar 02 2020 at 06:43):

...on the same day by the same person (ext_iff, eq_iff_veq)

view this post on Zulip Yury G. Kudryashov (Mar 02 2020 at 06:44):

In two different commits.

view this post on Zulip Mario Carneiro (Mar 02 2020 at 06:46):

This is actually another place where we could stand to be more regular in our naming. ext_iff is used for a bunch of structures now, so the names of extensionality for fin and subtype are now odd men out


Last updated: May 15 2021 at 23:13 UTC