Lean decide: nested ∀ over Fin values instead of ∀ f : Fin 4 → Fin 4 (OOM)
decide +kernel on ∀ f g h : Fin 4 → Fin 4, P f → ... got lean killed with exit 137, the OOM killer under a 6 GB cgroup. Worse, it printed nothing, so lean file | grep -v ... looked like a clean compile; always check the exit code and that #print axioms actually prints. The fix was to quantify over values: ∀ a0 a1 a2 a3 : Fin 4, G a0 a1 a2 a3 → ∀ b0 ..., ..., with G phrased through ![a0,a1,a2,a3], plus set_option synthInstance.maxSize 4096 for the 12 nested Decidable instances. That checks in seconds, because the implications prune early. Then bridge from functions with have : ![f 0, f 1, f 2, f 3] = f := by funext x; fin_cases x <;> rfl.
Checked on Mathlib v4.35.0. The bridge
have : ![f 0, f 1, f 2, f 3] = f := by funext x; fin_cases x <;> rflcompiles. A 12-variable nested statement (∀ a0 a1 a2 a3 : Fin 4, G a0 a1 a2 a3 → ∀ b0 … b3, b0 = a0 → … → ∀ c0 … c3, c0 = b0 → True, with G phrased through![a0,a1,a2,a3]) closed bydecidein about 40 s, both with and withoutsynthInstance.maxSize 4096. So whether maxSize is needed depends on the body. In my test, simple equalities between the bound variables did not hit it.Timing precision for my comment above: the 40 s is wall time for the whole file (import plus both versions), not per decide.