Zulip Chat Archive

Stream: general

Topic: Definition of `fin.of_nat`

FR (May 07 2022 at 18:46):

docs#fin.of_nat is not convenient to use. Maybe def of_nat {n : ℕ} [nonempty (fin n)] (a : nat) : fin n is better?

instance : nonempty (fin (succ n)) := ⟨⟨0, succ_pos n⟩⟩

def of_nat [h : nonempty (fin n)] (a : nat) : fin n :=
a % n, h.elim $ λ i, nat.mod_lt _ (lt_of_le_of_lt (nat.zero_le _) i.2)⟩

variable [nonempty (fin n)]

instance : has_zero (fin n) := of_nat 0
instance : has_one (fin n)  := of_nat 1

FR (May 07 2022 at 18:54):

If it is preferred, I will make a PR to the core library. My Github username is negiizhao.

Eric Wieser (May 07 2022 at 19:26):

I think those instance create a typeclass loop, doesn't has_zero imply non_empty?

Eric Wieser (May 07 2022 at 19:26):


Eric Wieser (May 07 2022 at 19:27):

Yeah, so we can't have the instances you suggest

Eric Wieser (May 07 2022 at 19:27):

If you wanted to go down that route we could use [fact (n \ne 0)] instead, but I think that would be more annoying

FR (May 08 2022 at 07:17):

docs#fact is in mathlib, we can't use it in core library.
How about make a new typeclass like nonempty_fin? I just can't figure out a better solution...

Yaël Dillies (May 08 2022 at 07:24):

Why can't you just use the current fin.of_nat?

FR (May 08 2022 at 07:27):

We can use the current fin.of_nat only for fin (succ n).

FR (May 08 2022 at 07:29):

The same goes for 0 and 1.

Yaël Dillies (May 08 2022 at 07:31):

Sure. And there's no way you can use it for fin 0, so what's the problem?

FR (May 08 2022 at 07:52):

For example, we can't say

example {n : } (x : fin n) : x + 0 = x := sorry

even though we know that fin n is nonempty and therefore has 0.

In APIs, this is often written as x : fin n.succ. But it would become annoying when using these APIs.

Yaël Dillies (May 08 2022 at 07:54):

I've been using these APIs lots and it is not. Can you give an example?

FR (May 08 2022 at 08:22):

Sorry, I tried, but it's not easy to make a mwe.

In the case like docs#fin_add_flip, it's not easy to change the expression in fin to the form n.succ.

I also tried to use docs#fin.of_nat', but there are only a few related APIs.

Eric Wieser (May 08 2022 at 08:25):

Note that I suggested the fact version of has_zero before, here: https://leanprover.zulipchat.com/#narrow/stream/113489-new-members/topic/Permutation.20groups.20-.20coercions.20from.20nat.20to.20.28fin.20n.29

Eric Wieser (May 08 2022 at 08:26):

It sounds like we just need to copy across the of_nat API for of_nat

FR (May 14 2022 at 08:32):

Is there any plan for refactoring?

Last updated: Aug 03 2023 at 10:10 UTC