Zulip Chat Archive

Stream: general

Topic: fin as a subtype

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}?

Simon Hudon (Mar 02 2020 at 05:56):

Why?

Johan Commelin (Mar 02 2020 at 05:59):

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

Johan Commelin (Mar 02 2020 at 06:00):

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

Johan Commelin (Mar 02 2020 at 06:00):

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

Simon Hudon (Mar 02 2020 at 06:04):

For instance?

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

Simon Hudon (Mar 02 2020 at 06:09):

Right but how big is the duplication?

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

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

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

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

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

Mario Carneiro (Mar 02 2020 at 06:19):

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

Mario Carneiro (Mar 02 2020 at 06:19):

the defeq to subtype seems useful

Simon Hudon (Mar 02 2020 at 06:20):

What about using coercions from and to subtypes?

Mario Carneiro (Mar 02 2020 at 06:20):

cycles, can't do it

Mario Carneiro (Mar 02 2020 at 06:20):

lean 3 coercions kind of suck

Simon Hudon (Mar 02 2020 at 06:20):

I mean functions to convert

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

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

Mario Carneiro (Mar 02 2020 at 06:23):

missing defeqs at the type level are difficult to patch around

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

Yury G. Kudryashov (Mar 02 2020 at 06:27):

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

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

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

Mario Carneiro (Mar 02 2020 at 06:43):

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

Yury G. Kudryashov (Mar 02 2020 at 06:44):

In two different commits.

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: Dec 20 2023 at 11:08 UTC