Pattern matching on Fin isn't exhaustive for large matches

Stream: lean4

[David Garland]

For a quick example of what I mean, here's a small code snippet:

def foo2 : Fin 2 → Bool
  | 0 => true
  | 1 => true

def foo4 : Fin 4 → Bool
  | 0 => true
  | 1 => true
  | 2 => true
  | 3 => true

def foo8 : Fin 8 → Bool
  | 0 => true
  | 1 => true
  | 2 => true
  | 3 => true
  | 4 => true
  | 5 => true
  | 6 => true
  | 7 => true

def foo16 : Fin 16 → Bool
  | 0 => true
  | 1 => true
  | 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 => true

Intuitively, all of these should compile-- in reality, all of them except for foo16 do.

When I brought this up to some others who were more familiar with the internals of the compiler they pointed out that this is likely due to this Contradiction.Config.searchFuel value being locked to 16: https://github.com/leanprover/lean4/blob/4391bc2977d3bf16f6780bb830c5fcd51f426d7d/src/Lean/Meta/Tactic/Contradiction.lean#L19

The solution they proposed would be to maybe allow some way to configure this setting, however I also wonder if for this specific sort of case you couldn't also just have it look at the number of match arms and have it set the fuel to max(Contradiction.Config.searchFuel, numberOfMatchArms)automatically-- maybe this is asking too much for what must be a niche use case if this bug hasn't been discussed before, though.

They also suggested that I might post an RFC for this, but I see that the RFC proposal template on the GitHub suggests that I should ask here first just to be sure the issue has been talked about by the community.

Are the two potential proposed solutions enough for a proposal, or are there maybe some other options (or maybe even workarounds) that I've missed? Thank you for reading ^^

[Mario Carneiro]

If you want to construct large Fin functions, you should use Fin.cons or the mathlib ![...] notation. This does not entail expensive match analysis

[David Garland]

Mario Carneiro said:

If you want to construct large Fin functions, you should use Fin.cons or the mathlib ![...] notation. This does not entail expensive match analysis

I see, thank you-- though I don't know how exactly to find documentation for the latter as it doesn't exactly seem google-able, and I'm also not entirely sure how I might use the former to rewrite my example, if it is intended to be able to do that
In the actual code I was writing, I wanted actually varying outputs for each case-- I used Bool only for simplicity, so that the issue at hand was the focus

[Mario Carneiro]

re: not google-able, one trick you can do for weird notation is to grep for it in mathlib and ctrl-click to go to definition

[Mario Carneiro]

in this case, the relevant function is docs#Matrix.vecCons

[David Garland]

Grep for it as in cloning it and using that command locally? Or is this a feature of GitHub nowadays that I need to get to learning?
In any case thank you for the link! ^^

[Kim Morrison]

"grep for it in mathlib" really means "open mathlib in VSCode and use VSCode search with the regular expression button clicked"

[David Garland]

Gotcha, thank you

[Mario Carneiro]

Also, docs#Fin.cases exists as a dependent version of docs#Fin.cons if you are defining a dependent Fin function

[Mario Carneiro]

Here's another version of the proof which uses a 'manual' proof of exhaustiveness:

def foo16 : Fin 16 → Bool
  | 0 => true
  | 1 => true
  | 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 => true
  | ⟨_+16, _⟩ => by omega

[David Garland]

Interesting! I appreciate you being thorough in your explanation, I'm learning some things now-- first time I had seen this style of using Fin n -> a to represent Vec n a, I see now how that vecCons thing makes sense to use here, and actually makes the thing I was trying to do shorter to write as well