Error in matching against `Fin n` for large `n`

Stream: mathlib4

[Anand Rao Tadipatri]

A friend and I were writing a bit of code that required matching against Fin 17, and surprisingly, we hit an error in doing this:

/--
error: Missing cases:
(Fin.mk (Nat.succ (Nat.succ (Nat.succ (Nat.succ (Nat.succ (Nat.succ (Nat.succ (Nat.succ (Nat.succ (Nat.succ (Nat.succ (Nat.succ (Nat.succ (Nat.succ (Nat.succ (Nat.succ (Nat.succ _))))))))))))))))) _)
-/
def test : Fin 17 → Bool
| 0 => false
| 1 => false
| 2 => true
| 3 => true
| 4 => true
| 5 => true
| 6 => true
| 7 => true
| 8 => true
| 9 => true
| 10 => true
| 11 => true
| 12 => true
| 13 => true
| 14 => true
| 15 => false
| 16 => true

However, matching against Fin 15 seems to work perfectly fine:

def test : Fin 15 → Bool
| 0 => false
| 1 => false
| 2 => true
| 3 => true
| 4 => true
| 5 => true
| 6 => true
| 7 => true
| 8 => true
| 9 => true
| 10 => true
| 11 => true
| 12 => true
| 13 => true
| 14 => true

Does anyone know why this might be happening? Is it because of an issue in the equation compiler?

[Robin Arnez]

It's the depth limit in contradiction (here)

[Robin Arnez]

The problem is that disproving x + 17 < 17 by cases takes 18 invocations but 16 is the limit:

import Lean

def test : Fin 17 → Bool
  | 0 => false | 1 => false | 2 => true  | 3 => true  | 4 => true  | 5 => true   | 6 => true  | 7 => true | 8 => true | 9 => true
  | 10 => true | 11 => true | 12 => true | 13 => true | 14 => true | 15 => false | 16 => true
  | ⟨k + 17, h⟩ => by
    exfalso
    iterate 18 cases ‹_›

[Edward van de Meent]

tbh it sounds like you just shouldn't be matching against Fin 17, but do some if ... else ... stuff instead...

[Anand Rao Tadipatri]

Thank you!

[Eric Wieser]

You could also consider

import Mathlib

def test : Fin 15 → Bool :=
  ![false, false, true, true, true, true, true, true, true, true, true, true, true, true, true]

[Anand Rao Tadipatri]

Ah, that's really neat! Thank you!