3 incorrectly accepted as Fin 1?

Stream: new members

[aron]

I've got a type that contains type indices n : Nat and a Fin n:

inductive Ctx (α : Type u) : (n : Nat) → Type u
  | nil : Ctx α 0
  | add {n} (body : Ctx α n) (tip : α) : Ctx α (n+1)

inductive HasType {α : Type u} : (n : Nat) → (index : Fin n) → Ctx α n → α → Type u where
  | stop : HasType 1 3 (Ctx.add Ctx.nil ty) ty -- <-- 3 works here?
  | pop : HasType n fin ctx ty → HasType (n+1) fin.succ (Ctx.add ctx otherTy) ty

In the stop constructor it looks like lean has no problem with me setting the Fin n to a value of 3, even though obviously 3 < 1 is false.

This also works when I do ⟨ 3, _ ⟩. Although when I do ⟨ 3, by sorry ⟩ it clearly shows that the goal is 3 < 1. So why does this work? Is this a bug?

[Jz Pan]

It wraps around.

[aron]

Sorry what does that mean?

[Etienne Marion]

It comes from this: Fin.ofNat'. It uses 3 % n.

[Yaël Dillies]

3 : Fin 1 means ⟨3 % 1, (some_proof : 3 % 1 < 1)⟩ : Fin 1

[Yaël Dillies]

In particular, (3 : Fin 1) = (0 : Fin 1)

[aron]

oh. that seems.. unexpected.

[aron]

:neutral:

[Robin Arnez]

Well it's because Fin n is meant to model a modular ring with addition, subtraction and multiplication and in particular it is also the basis for UInt8 etc. which have similar behavior.

[aron]

:neutral:
:expressionless:
:neutral:

[Kevin Buzzard]

Someone should be making a list of everyone who is caught out by this clearly unexpected behaviour

[Matt Diamond]

I thought ZMod was meant to model a modular ring... maybe Fin should be more strict while ZMod continues with the existing behavior

[Jireh Loreaux]

This OfNat is in core, as are the arithmetic instances. I don't think they're changing. Moreover, I've never seen another suggestion for behavior that makes more sense / is better.

If you want a Fin with different arithmetic, create a type synonym.

[Yaël Dillies]

Here's a concrete suggestion: If you want to verify that index i : ℕ isn't out of bounds, do ⟨i, some_proof⟩ : Fin n, rather than i : Fin n.

[Yaël Dillies]

For anyone coming here from the future, the ℕ → Fin n coercion was removed from Lean core in lean#8620, and in mathlib docs#Fin.instCommRing isn't an instance either anymore.