Definition of `fin.of_nat`

Stream: general

[FR]

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]

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

[Eric Wieser]

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

[Eric Wieser]

docs#has_zero.nonempty

[Eric Wieser]

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

[Eric Wieser]

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]

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]

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

[FR]

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

[FR]

The same goes for 0 and 1.

[Yaël Dillies]

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

[FR]

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]

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

[FR]

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]

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]

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

[FR]

Is there any plan for refactoring?