Making Fin error on out-of-range number instead of wrapping

Stream: new members

[MrQubo]

Is it possible to have type like Fin, but without modular arithmetics?
E.g. I would expect that to not compile:

#eval (3 : Fin 2)
#eval ((1 : Fin 2) + (1 : Fin 2) : Fin 2)

In other words, I want Fin n to be a number i with a proof that 0 ≤ i < n.

Actually, I was mislead by the documentation of Fin. It does not mention it having modular arithmetic at all.

I could write {n : Nat // 0 ≤ n ∧ n < 4}, but I would prefer being able to construct the type directly from integer literals, and having implicit conversion to Nat.

[Aaron Liu]

Why? What's your use case? Usually we want functions to be total, which is why 1 / 0 gives 0.

[MrQubo]

In my case structure is well-defined only for numbers in the range. I also find it very weird that this works:

def x : Nat := 123
#eval @List.Vector.get Nat 3 ⟨[1, 2, 3], by simp⟩ x

i.e. the index wraps because it uses Fin. With List.Vector I expected to have compile-time checks of index, not wrapping behaviour.

[Ruben Van de Velde]

So the issue here is with numeric literals. You can write your Fin values as Fin.mk 3 (proof that 3 < n)

[MrQubo]

Ah, I see it now. So e.g. this doesn't work

def vec_snd {α n} (l : List.Vector α n) (h : n ≥ 2) : α :=
  List.Vector.get l 1

and I need to use ⟨1, h⟩.
I still think that wrapping behaviour should be removed. But I guess in most cases n won't be a literal so doesn't matter that much.

[MrQubo]

Actually, not true. It applies not only to numeric literals. It also applies to arithmetics, and even .succ.
Example, this typechecks:

inductive Lam : ∀ (_ : Nat), Type
| bvar : ∀ {n}, (m : Nat) → (_ : m < n := by omega) → Lam n
| fvar : ∀ {n}, String → Lam n
| app : ∀ {n}, Lam n → Lam n → Lam n
| lam : ∀ {n}, Lam n.succ → Lam n
deriving Repr
open Lam

def renum_bvars {n} (t : Lam n) (i : Fin n.succ := 0) : Lam n.succ :=
  match t with
  | bvar m _ =>
    if m ≥ i
      then bvar m.succ
      else bvar m
  | fvar name => fvar name
  | app f arg => app (renum_bvars f i) (renum_bvars arg i)
  | lam body => lam (@renum_bvars n.succ body i.succ.succ)

I can write this to avoid modular arithmetic:

def renum_bvars {n} (t : Lam n) (i : Fin n.succ := 0) : Lam n.succ :=
  match t with
  | bvar m _ =>
    if m ≥ i
      then bvar m.succ
      else bvar m
  | fvar name => fvar name
  | app f arg => app (renum_bvars f i) (renum_bvars arg i)
  | lam body => lam (@renum_bvars n.succ body ⟨i.val.succ, by simp⟩)

[Aaron Liu]

docs#Fin.succ takes a Fin n and returns a Fin (n + 1).

[Aaron Liu]

MrQubo said:

Example, this typechecks:

inductive Lam : ∀ (_ : Nat), Type
| bvar : ∀ {n}, (m : Nat) → (_ : m < n := by omega) → Lam n
| fvar : ∀ {n}, String → Lam n
| app : ∀ {n}, Lam n → Lam n → Lam n
| lam : ∀ {n}, Lam n.succ → Lam n
deriving Repr
open Lam

def renum_bvars {n} (t : Lam n) (i : Fin n.succ := 0) : Lam n.succ :=
  match t with
  | bvar m _ =>
    if m ≥ i
      then bvar m.succ
      else bvar m
  | fvar name => fvar name
  | app f arg => app (renum_bvars f i) (renum_bvars arg i)
  | lam body => lam (@renum_bvars n.succ body i.succ.succ)

Not for me! Am I doing something wrong or did you just not notice the

application type mismatch
  renum_bvars body (Fin.succ i).succ
argument
  (Fin.succ i).succ
has type
  Fin (n.succ + 1 + 1) : Type
but is expected to have type
  optParam (Fin n.succ.succ) 0 : Type

[Edward van de Meent]

the "no modular arithmetic" code uses only one succ, that fixes it

[MrQubo]

@Aaron Liu Indeed, doesn't typechecks on nightly. Thanks!
I'm on

Lean 4.16.0-rc2
Target: x86_64-unknown-linux-gnu

and it does typecheck.

[MrQubo]

Edward van de Meent said:

the "no modular arithmetic" code uses only one succ, that fixes it

But the point was, that the code with .succ.succ also "worked" (in a sense that it was typechecking).

[Edward van de Meent]

that's weird, it doesn't typecheck on the playground with

Lean 4.16.0-rc2
Target: x86_64-unknown-linux-gnu

[Edward van de Meent]

maybe you need to refresh your editor?

[Mitchell Lee]

If you don't want addition on Fin 2 to wrap around, then the solution is to not add two elements of Fin 2 if the result would be big enough to wrap around.

It is impossible to redesign the addition on Fin 2 in such a way that the line of code ((1 : Fin 2) + (1 : Fin 2) : Fin 2) is a type error. This is because Lean's type checking system has no way of knowing whether the numbers you are adding are big enough to wrap around or not.

[Mitchell Lee]

The documentation of Fin does not mention modular arithmetic because the definition of Fin, by itself, does not include any arithmetic operations. The arithmetic operations are defined separately. For example, see docs#Fin.add, whose documentation does mention modular arithmetic.

[MrQubo]

This is because Lean's type checking system has no way of knowing whether the numbers you are adding are big enough to wrap around or not.

That's not true, or I don't understand what you mean.
Currently I'm using {i : Nat // i < n} instead of Fin n, and it does work like I want. It's a bit more cumbersome to use though. So yes, I can check during compilation whether addition will wrap over n or not. Or, in this particular case, verify that it never won't, as that's what I need.

My main concern is that, the name Fin is not suitable for what that type does. Mod would be much better IMO.

And my question is that, is there a type in lean or mathlib for {i : Nat // i < n}?

[Yakov Pechersky]

What is the Add instance you've defined on your type?

[Kevin Buzzard]

MrQubo said:

And my question is that, is there a type in lean or mathlib for {i : Nat // i < n}?

Yes, that type is Fin n. It just has an addition on it that you don't like.

The prevailing philosophy in library design here is that it's more convenient in practice to output junk values given junk inputs rather than to complain that things aren't possible (or equivalently to demand proofs from the user). This is the same reason that we have 1 / 0 = 0 as opposed to demanding a proof that you're not dividing by 0 or complaining that the division isn't possible.

[Mitchell Lee]

It is worth noting that if Fin were changed to not use modular arithmetic, a sizable part of Lean's core library would have to be reworked. So, no, it is not really possible to change it at this point. Just use Fin n. You do not have to use the addition operation if you do not want to.

Also, it is worth noting that many programming languages, including C++ which Lean relies on, use modular arithmetic (specifically, arithmetic modulo $2^8$, $2^{16}$, $2^{32}$, and $2^{64}$) for their bounded integer types, because CPUs are especially good at it.

[MrQubo]

Kevin Buzzard said:

MrQubo said:

And my question is that, is there a type in lean or mathlib for {i : Nat // i < n}?

Yes, that type is Fin n. It just has an addition on it that you don't like.

The prevailing philosophy in library design here is that it's more convenient in practice to output junk values given junk inputs rather than to complain that things aren't possible (or equivalently to demand proofs from the user). This is the same reason that we have 1 / 0 = 0 as opposed to demanding a proof that you're not dividing by 0 or complaining that the division isn't possible.

That makes sense. I guess it makes you worry less about proofs while programming, and only while writing a proof you might end up having to consider a case of 1 / 0 e.g.

[MrQubo]

Yakov Pechersky said:

What is the Add instance you've defined on your type?

I've tried defining addition for it, but no luck. I'm just doing addition on Nat, and constructing the proof separately. Thanks to autoProps, as mentioned earlier in this thread, most proofs are constructed automatically.