## Stream: general

### Topic: Generalizing fin away from (n + 1)

#### Yakov Pechersky (Aug 07 2022 at 21:28):

A lot of the structures and lemmas we have on fin only operate on fin (n + 1) or fin (n + 2). That means when one wants to talk about {0, 1, ..., b - 1}, you really need to think about {0, 1, ...., b, b + 1} : finset (fin (b + 2)). I have a branch#pechersky/fin-nontrivial that, for example, defined bounded_order (fin n'), not fin (n + 1), but requires [nonempty (fin n')]. Of course, I also provide nonempty (fin (n + 1)) to the TC. This is inspired by the fintype/finite split going on recently. This approach also gives 0 : fin n' and 1 : fin n'. We also get a last' _ : fin n'.

I wanted to bring this up here for thoughts, and for help. Right now, I am hitting some TC loop according to the TC linter -- I am not sure how to diagnose and fix that.

#### Mario Carneiro (Aug 07 2022 at 21:46):

A lot of zmod.basic is written like that already, using fact (0 < n) in place of nonempty (fin n)

#### Yakov Pechersky (Aug 07 2022 at 21:59):

Is that a "vote" for TC-based fin API or against it? Or just a comment? To me, nonempty (fin n) and nontrivial (fin n) look "cleaner" than fact based hypotheses.

#### Yakov Pechersky (Aug 07 2022 at 22:00):

Additionally, fact (0 < n) for zmod n is mainly to separate out int = zmod 0 from zmod (n + 1) = fin (n + 1)

#### Mario Carneiro (Aug 07 2022 at 22:02):

that's a recommendation to use fact (0 < n) instead of another equivalent formulation of it

#### Mario Carneiro (Aug 07 2022 at 22:02):

nonempty (fin n) is not great because it's not obviously related to zmod facts

#### Mario Carneiro (Aug 07 2022 at 22:03):

a zmod theorem predicated on nonempty (fin n) would be weird

#### Mario Carneiro (Aug 07 2022 at 22:03):

and we don't want two ways to assert the same thing

#### Mario Carneiro (Aug 07 2022 at 22:03):

and nonempty (fin n) and nontrivial (fin n) doesn't generalize very well

#### FR (Aug 07 2022 at 22:31):

It was discussed a few times, but then no more progress was made. https://leanprover.zulipchat.com/#narrow/stream/113488-general/topic/Definition.20of.20.20.60fin.2Eof_nat.60

#### Eric Wieser (Aug 07 2022 at 22:36):

It's not immediately clear whether this would be an overall improvement, or just shift the pain around

#### Yakov Pechersky (Aug 07 2022 at 23:04):

nonempty (fin n) has the benefit of being more "canonical" than fact (0 < b) or fact (1 <= b).

#### Eric Wieser (Aug 07 2022 at 23:33):

It's the sole inhabitant of what feels like a non-canonical island, while the other spellings are non-canonical inhabitants of what feels like the canonical island of spellings...

#### Yakov Pechersky (Aug 07 2022 at 23:42):

You know what they say, "every typeclass hypothesis is an island"... or are you thinking more of the island of stability

Last updated: Aug 03 2023 at 10:10 UTC