Large numeric computations and `fin_cases`

Stream: mathlib4

[Gareth Ma]

TLDR: how to prove this in Lean 4? Currently even creating those 576 goals via fin_cases causes maximum recursion depth error.

import Mathlib.Tactic

def E : Matrix (Fin 24) (Fin 24) ℤ := !![
4,3,3,5,5,-2,0,-1,-5,-4,-5,-3,-5,4,3,0,-4,4,2,-4,1,2,1,0;
4,-3,-4,-3,5,-1,4,1,-3,-1,3,1,4,2,-5,-1,-5,1,-1,3,-4,-4,-2,3;
-2,-2,5,-1,-5,-1,3,-3,4,-4,3,-2,-4,0,2,-4,-3,1,0,-3,-3,-3,-4,4;
5,-6,0,0,-1,-2,-1,1,3,3,-4,0,3,-3,2,2,-1,0,-6,4,-4,0,-4,3;
-6,4,2,5,-6,-2,-2,-4,3,2,-2,-6,-6,-2,1,0,-5,3,5,2,-4,-3,3,-2;
2,4,5,-2,1,-3,1,-2,-4,-6,1,0,-4,5,-4,-4,0,-6,4,-6,-3,-2,-4,3;
-6,0,3,2,2,-2,-6,2,-2,-6,-4,2,-3,-1,-4,1,-4,0,-5,4,-6,1,4,-4;
-5,2,-5,-4,-3,-6,-1,2,-1,-3,1,-5,-1,0,-3,-2,2,-1,-5,2,4,5,-5,-6;
1,3,-4,1,-2,-1,2,5,2,-1,-3,-2,5,-6,-3,-1,-5,2,-2,4,3,-2,5,1;
-6,0,-2,-4,-4,-1,-4,-1,-4,5,-2,4,-3,0,1,3,0,0,4,-4,2,4,5,-3;
-6,-5,-3,-3,-4,1,-5,-2,0,-5,-3,-6,-3,1,-6,-5,0,-3,-3,-4,-3,-5,4,4;
4,3,-5,-6,-3,1,0,0,-1,-2,-5,5,-2,5,5,0,-4,5,-5,-2,-2,3,-1,-5;
-6,-1,-5,2,1,1,1,5,3,5,-5,-2,-2,5,1,-5,1,0,3,4,-3,-4,-6,-5;
5,3,5,2,-4,0,1,-5,0,0,-2,0,-1,3,1,5,4,0,2,1,-2,0,-1,-1;
-3,-5,4,1,2,-3,-4,0,1,1,1,4,5,4,-6,2,3,-2,-2,-2,1,-1,4,-5;
-2,3,-4,4,1,2,-6,3,-4,5,-5,3,-3,-2,4,3,-3,2,-1,0,-5,5,-3,-5;
-5,-2,-3,-3,3,-3,-5,-1,-3,-3,-2,-6,-6,3,5,5,0,-6,3,-6,-2,-2,2,3;
5,2,5,-2,0,-4,2,4,-1,-6,0,-5,-4,5,-3,3,5,4,2,5,-2,-3,2,-4;
-1,-4,-6,5,-6,-5,5,-1,5,4,5,3,4,-3,0,1,3,-6,-2,2,-6,-2,3,-2;
5,-2,3,-3,2,-1,-1,-3,2,1,-3,1,-1,-1,0,-3,2,-4,-1,-4,-5,1,5,4;
-6,3,5,1,1,1,0,3,5,5,-2,-2,1,-3,1,-3,3,3,-3,-3,5,5,1,5;
1,5,3,-2,3,-6,-4,2,5,3,0,-5,2,4,4,2,3,-3,4,-2,1,5,4,-5;
-1,-5,4,0,5,0,4,3,4,-3,-6,5,3,-5,-5,2,-3,-5,-5,2,1,5,-5,-3;
1,-1,-6,-1,-3,3,-4,2,-6,-3,-1,2,0,1,-5,-6,5,-6,2,5,1,1,0,-3;
]

example (i j : Fin 24) : Even (∑ k, E i k * E j k) := by
  fin_cases i <;> fin_cases j <;> sorry

[Kim Morrison]

#time
set_option maxHeartbeats 0 in
set_option maxRecDepth 100000 in
example : ∀ (i j : Fin 24), Even (∑ k, E i k * E j k) := by decide

takes about 20 seconds.

[Kim Morrison]

But ... presumably there is a reason why this is true?

[Gareth Ma]

Oh what :O maybe I minimised my example wrong, I’ll have a look tomorrow

[Gareth Ma]

.

[Gareth Ma]

I expected it to take longer

[Gareth Ma]

The matrix is specially generated

[Kim Morrison]

So use how you specially generated it to give a proof?

[Gareth Ma]

No I meant the matrix is even (each dot product is even) because I generated it in Sage to have that property, otherwise it’s not true

[Kim Morrison]

Surely you don't mean you randomly generated matrices and then filtered for this property until you found one.

[Gareth Ma]

Okay I think I understand what you mean. I'll have to try it tomorrow since I'm doing something else right now