Generalizing fin away from (n + 1)

Stream: general

[Yakov Pechersky]

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]

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

[Yakov Pechersky]

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]

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

[Mario Carneiro]

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

[Mario Carneiro]

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

[Mario Carneiro]

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

[Mario Carneiro]

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

[Mario Carneiro]

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

[FR]

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]

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

[Yakov Pechersky]

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

[Eric Wieser]

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]

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