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
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.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". -/
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