fin_cases slow?!

Stream: mathlib4

[Moritz Firsching]

Here is an example of some theorem, where I was expecting that docs#Lean.Elab.Tactic.finCases would just do it, but it times out. In this example we have 4 numbers in ZMod 12 and I try to solve the theorem by trying out all 12^4=20736 combinations. However this didn't work and even when I increased the number of hearbeats and maxRecDepth is didn't work.

Is 20736 cases really too much? Can I do something to make it faster/use less memory.
(In this particular case, the proof can be adapted to look at it mod 3 and mod4 separately of course, and there is also docs#Nat.superFactorial_dvd_vandermonde_det, which solves this completely, but the point of this example is to have many fin_cases.

import Mathlib.Data.Nat.Factorial.SuperFactorial
import Mathlib.Tactic.FinCases
import Mathlib.Data.ZMod.Basic
/-
import Mathlib.NumberTheory.Wilson
import Mathlib.Data.Nat.Factorial.DoubleFactorial
-/
section Defs

open Finset BigOperators

theorem all_diff_mul_mod2 (a b c : ZMod 2) :
  (a - b) * (a - c) * (b - c)  = 0 := by
  change Fin 2 at a
  change Fin 2 at b
  change Fin 2 at c
  push_cast
  fin_cases a <;> fin_cases b <;> fin_cases c <;> rfl

theorem all_diff_mul_2 (a b c : ℤ) :
  ((2 : ℕ) : ℤ)  ∣ (a - b) * (a - c) * (b - c) := by
  rw [← ZMod.int_cast_zmod_eq_zero_iff_dvd]
  push_cast
  exact all_diff_mul_mod2 ↑a ↑b ↑c

/-
-- too slow for the 20736 cases ?!
set_option maxHeartbeats 2000000
set_option maxRecDepth 100000
theorem all_diff_mul_mod12 (a b c d : ZMod 12) :
  (a - b) * (a - c) * (a - d) * (b - c) * (b - d) * (c - d) = 0 := by
  change Fin 12 at a
  change Fin 12 at b
  change Fin 12 at c
  change Fin 12 at d
  push_cast
  fin_cases a <;> fin_cases b <;> fin_cases c <;> fin_cases d <;> rfl


theorem all_diff_mul_12 (a b c d : ℤ) :
  ((12 : ℕ) : ℤ)  ∣ (a - b) * (a - c) * (a - d) * (b - c) * (b - d) * (c - d) := by
  rw [← ZMod.int_cast_zmod_eq_zero_iff_dvd]
  push_cast
  exact all_diff_mul_mod12 _ _ _ _
-/

-- The same theorems using `Nat.superFactorial_dvd_vandermonde_det`...

-- just for fun, of course the fact that 1 divides the difference of two integers can be proved
-- with less effort...
theorem all_diff_mul_1' (a b : ℤ) :
  ((1 : ℕ) : ℤ)  ∣ (b - a) := by
  convert Nat.superFactorial_dvd_vandermonde_det [a, b].get
  rw [Matrix.det_vandermonde, Fin.prod_univ_succ]
  simp

theorem all_diff_mul_2' (a b c : ℤ) :
  ((2 : ℕ) : ℤ)  ∣ (a - b) * (a - c) * (b - c) := by
  have := Nat.superFactorial_dvd_vandermonde_det [c, b, a].get
  rw [Matrix.det_vandermonde] at this
  convert this
  rw [Fin.prod_univ_succ]
  have : Ioi (1 : Fin 2) = Finset.empty := by
    rfl
  simp [this, Finset.empty, Finset.prod_empty]
  ring

theorem all_diff_mul_12' (a b c d : ℤ) :
  ((12 : ℕ) : ℤ)  ∣ (a - b) * (a - c) * (a - d) * (b - c) * (b - d) * (c - d) := by
  have := Nat.superFactorial_dvd_vandermonde_det [a, b, c, d].get
  rw [Matrix.det_vandermonde] at this
  convert this
  repeat rw [Fin.prod_univ_succ]; simp
  ring

[Kevin Buzzard]

In Lean 3 my rule of thumb was that 20 cases was often too much :-)

[Mario Carneiro]

lean 4 fin_cases is a lot better than lean 3, but 20000 is still a lot

[Mario Carneiro]

My guess is that the surrounding tactic infrastructure will start to get in the way at that point

[Mario Carneiro]

oh wait, this is the slow implementation, the fast one was only done for mod_cases I guess

[Michael Stoll]

set_option maxHeartbeats 400000 in
example : ∀ (a b c d : ZMod 12), (a - b) * (a - c) * (a - d) * (b - c) * (b - d) * (c - d) = 0 := by
  decide

works.

[Eric Wieser]

I was just about to write that!

[Michael Stoll]

(I used count_heartbeats in; without the heartbeats bump, it times out.)

[Moritz Firsching]

count_heartbeats in
theorem all_diff_mul_mod4 (a b c d : ZMod 4) :
  (a - b) * (a - c) * (a - d) * (b - c) * (b - d) * (c - d) = 0 := by
  change Fin 4 at a
  change Fin 4 at b
  change Fin 4 at c
  change Fin 4 at d
  push_cast
  fin_cases a <;> fin_cases b <;> fin_cases c <;> fin_cases d <;> rfl

Another datapoint: this gives
Used 30237 heartbeats, which is less than the current maximum of 200000.
for the 4^4=256 cases...

[Michael Stoll]

Generally, it seems that decide works reasonably well on statements quantified over elements of not-too-large residue class rings of the integers.

[Moritz Firsching]

ok, lesson learned decide is faster then fin_cases...

[Michael Stoll]

I learned that lesson in the same way quite some time ago! :smile:

[Mario Carneiro]

I'm not sure this is a general rule, it depends on the computation you want to do being efficiently kernel-computable

[Mario Carneiro]

for multiplying Fin values this is probably fine

[Michael Stoll]

(Back then with ∀ (a b c : ZMod 8) : a^2 + b^2 + c^2 ≠ 7.)

[Mario Carneiro]

but fin_cases has a really bad implementation right now, I intended to fix it a while ago but apparently that didn't happen

[Moritz Firsching]

what's bad about it?
(perhaps I can help in fixing it?!)

[Mario Carneiro]

it needs to be specialized for Fin instead of just kernel-computing a proof of Fintype (Fin n) to a literal

[Mario Carneiro]

Compare it with mod_cases

[Michael Stoll]

In the concrete example, it may be better to do it mod 3 and mod 4 (fast with decide) and then use the Chinese Remainder Theorem.

[Moritz Firsching]

yeah, as I said, I did this also and for that approach even fin_cases is fast enough. I guess the best approach is to use the theorem that states it for every n...

[Mario Carneiro]

yes please, don't brute force a theorem that you can prove for general n!

[Moritz Firsching]

Mario Carneiro said:

Compare it with mod_cases

I tried to write a fin_cases' tactic that specializes for Fin that copies pretty much what mod_cases does.
Here is the WIP:

https://github.com/leanprover-community/mathlib4/commit/0bc9d97a363beb3d3485f094793a37f41f27ddda

An example that uses this:

import Mathlib.Tactic.FinCases2

example (p : Fin 3 → Prop) (h0 : p 0) (h1 : p 1) (h2 : p 2) (x : Fin 3) : p x := by
  fin_cases' x inFin 3
  · convert h0
    exact Fin.ext h
  · convert h1
    exact Fin.ext h
  · convert h2
    exact Fin.ext h

There are (at least) two problems currently with this:

1. Right now one needs to provide n, so write fin_cases' x inFin 3', but 'x : Fin 3', so the tactic should be able to infer the 3 and we wouldn't need the silly inFin`.
2. Currenly fin_cases x inFin 3' produces hypothesis of the form ↑x = 0, ↑x = 1, and ↑x = 2, casting to ℕ, but of course it would be nicer just to have equalities in Fin 3: x = 0, x = 1, and x = 2`.

Any tips on how to best fix either of these problems?

Once this works as intented, I want so compare how it performs compared to the normal fin_cases tactic.