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

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.

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: May 15 2021 at 23:13 UTC