Fin.instOfNat vs Fin.instOfNatFin

Stream: mathlib4

[Yury G. Kudryashov]

I'm trying to write a version of List.get_mk_zero from std4#758 that will work with (0 : Fin (length l)) instead of Fin.mk 0 _. I fail to make a version that works both with docs#Fin.instOfNat and docs#Fin.instOfNatFin. The issue is that usually Lean fails to generate NeZero instance (but can get it by unfolding some definitions and matching a list with .cons _ _, thus matching its length with _ + 1; or it can get it as an output of some rw/simp).

[Yury G. Kudryashov]

Moreover, this fails:

example (a : ℕ) : @instOfNat n a = @instOfNatFin (n + 1) a _ := by
  with_reducible_and_instances rfl

[Yury G. Kudryashov]

Can we change the instance in core to use some version of docs#NeZero (e.g., a Nat-only version or a version that takes [OfNat α 0] instead of [Zero α]), or it goes against some deliberate design choices?

[Yury G. Kudryashov]

@Kim Morrison , who's the right person to answer this :up: question?

[Kim Morrison]

Which instance is it that you want to change? I'm not following yet.

[Kim Morrison]

Separately, docs#Fin.instOfNatFin seems to crash my browser (chrome on macos). Anyone else? (EDIT: restarting has fixed it; other things were crashing too.)

[Mario Carneiro]

works fine on FF / ubuntu, redirecting to https://leanprover-community.github.io/mathlib4_docs/Mathlib/Data/Fin/Basic.html#Fin.instOfNatFin

[Yury G. Kudryashov]

In Mathlib, we define the following instance:

instance {a : ℕ} [NeZero n] : OfNat (Fin n) a where
  ofNat := Fin.ofNat' a (NeZero.pos n)

[Yury G. Kudryashov]

This way we can argue about, e.g., (0 : Fin (2 ^ n)) for a variable n.

[Yury G. Kudryashov]

(BTW, this may be useful to prove some lemmas about this type, then apply to UInt*)

[Yury G. Kudryashov]

But this instance conflicts with the instance (n a : Nat) : OfNat (Fin (n + 1)) a in core.

[Kim Morrison]

I see, and you'd like that to not have a +1, but instead some other typeclass playing the role of NeZero.

[Yury G. Kudryashov]

Exactly. Either backport a generic NeZero, or create a Nat-specific version.