Zulip Chat Archive

Stream: general

Topic: Turning `Fin` into a structure again

Gabriel Ebner (Aug 29 2022 at 12:09):

As some of you might have noticed, in Lean 4 Fin is a structure. Just like it was in Lean 3 before Johan PRd lean#452. However there are now good reasons to make Fin a structure. For example, Leo plans implement some compiler optimizations for Fins that would not be possible with the subtype definition.

In my opinion, the structure definition has lots of other advantages. For example, the unifier won't reduce Fin n to Subtype (· < n) and then try to unify the less-than function (and its type class instance). The difference between Fin.mk and Subtype.mk disappears. And the cases tactic produces Fin.mk instead of Subtype.mk (as it does now).

A big reason behind Johan's change was that we could reuse API for subtypes. From what I can tell, we have since added lots of API around function.injective and function.embedding which works for general subobjects and not just literal subtypes. This seems to significantly reduce the pain points mentioned by Johan.

I have tried out changing fin into a structure again in mathlib, and it requires only very little change. The biggest one is the locally_finite_order instance which unfortunately doesn't generalize to function.injective (as it requires a computable inverse). Are there any objections to change fin to a structure?

Johan Commelin (Aug 29 2022 at 12:12):

No objections for me. You've made a strong case for the change.

Yaël Dillies (Aug 29 2022 at 12:34):

The fix you introduced for the locally_finite_order instance looks good to me, so no objection.

Wrenna Robson (Sep 05 2022 at 02:09):

That link doesn't seem to work for me.

Junyan Xu (Sep 05 2022 at 02:56):

The branch was deleted after merged in #16292.

Wrenna Robson (Sep 05 2022 at 13:15):

It looks like the documentation still says : fin n is the subtype of ℕ consisting of natural numbers strictly smaller than n. Even though that isn't how it is defined.

Gabriel Ebner (Sep 05 2022 at 13:19):

Maybe we should just copy the Lean 4 docstring (authored by Mario):

`Fin n` is a natural number `i` with the constraint that `0 ≤ i < n`.
It is the "canonical type with `n` elements".

Although the 0 ≤ i is a bit redundant for a natural number..

Junyan Xu (Sep 05 2022 at 19:08):

Shouldn't it say "a term of type Fin n ..."?

Last updated: Aug 03 2023 at 10:10 UTC