Turning `Fin` into a structure again

Stream: general

[Gabriel Ebner]

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]

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

[Yaël Dillies]

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

[Wrenna Robson]

That link doesn't seem to work for me.

[Junyan Xu]

The branch was deleted after merged in #16292.

[Wrenna Robson]

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]

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]

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