simp (ZMod): failed to synthetize CharZero

Stream: general

[Mirek Olšák]

I have noticed that when I get a little complicated expressions into the argument of ZMod (even if hidden under a definition), simp, and related tools (push_cast, ...) become unusable due to a crash on failed to synthesize CharZero (ZMod ...). MWE:

import Mathlib

def complicated (c : ℕ) : ℕ :=
  ((Finset.univ.filter (fun x ↦ x = 0) : Finset (Fin (c*6+1))).map
    Fin.valEmbedding ∩ Finset.Ico 0 c).max.unbotD 0

example (c : ℕ) (x : ℕ) :
    (1 : ZMod (complicated (c+3))) = 1 + x := by -- note: replacing 3 -> 2 works
  simp -- crash

Any ideas how to deal with it? Could I convince simp not to try to infer this?
As a possible workaround, I also thought if I could replace the complicated (c+3) in the local context with some local variable in such a way that simp could not expand it... Would that be feasible?

[Ruben Van de Velde]

There is no crash, just

failed to synthesize
  CharZero (ZMod (complicated (c + 3)))
(deterministic) timeout at `typeclass`, maximum number of heartbeats (20000) has been reached

[Mirek Olšák]

Ok, sorry if calling it a "crash" is a oversimplification, I thought it is an appropriate name for an error message instead of any reasonable outcome of the tactic... But I would like to know what to do with that.

[Kenny Lau]

turn off that simp lemma

[Mirek Olšák]

Sounds good, how do I detect which one it is causing?

[Kenny Lau]

try Nat.cast_inj

[Mirek Olšák]

attribute [-simp] Nat.cast_inj in
set_option diagnostics true in
example {c : ℕ} (x : ℕ) :
    (1 : ZMod (complicated (c+3))) = 1 + x := by
  simp

still fails on the same

[Kenny Lau]

@Mirek Olšák set_option trace.Debug.Meta.Tactic.simp true successfully found the offending simp lemma Nat.cast_eq_zero

[Mirek Olšák]

debug_traces
Thanks, that is helpful. Could you just explain me how you navigated the debug trace? I can see 1101 lines, none of them mentioning Nat.cast_eq_zero

[Mirek Olšák]

Ok, it might be a version difference -- I can find the Nat.cast_eq_zero in the traces in live Lean.

[Kenny Lau]

I just looked at the last one

[Notification Bot]

This topic was moved here from #lean4 > simp (ZMod): failed to synthetize CharZero by Michael Rothgang.

[Aaron Liu]

didn't we have this problem before

[Jovan Gerbscheid]

I have an issue lean#10414 and a fix lean#8883 to fix the exponentially slow unification that causes your time-out. You can upvote the issue for it to get more attention :)

[Jovan Gerbscheid]

By the way, to investigate a time-out, the easiest way is to use set_option trace.profiler true in in front of the simp.