Repository navigation
grind often fails on goals containing (...#usize : Nat) #1035
Description
I've noticed that grind often fails on goals containing (...#usize : Nat). Here is a small example demonstrating this:
example (x : Nat) : (5 : Nat) ∣ (5 : Nat) * x := by grind --works
example (x : Nat) : (5#usize : Nat) ∣ (5#usize : Nat) * x := by grind -- failsA solution could be to add grind norm attributes to the following lemmas:
attribute [grind norm] UScalar.ofNatCore_val_eq
attribute [grind norm] IScalar.ofInt_val_eqI don't fully understand the issue, but I believe grind is attempting to use its linear arithmetic solver on these kinds of goals and fails when numbers are wrapped in (...#usize : Nat).
Activity
sonmarcho commentedon May 18, 2026
I think the treatment of coercions to Nat is hardcoded in grind. But I'm surprised by
grind norm: isn'tnormthe simpset used internally bygrindto normalize expressions fed into the egraph (shouldn't we never touch it)? If yes to both it's probably worth creating an MWE and opening an issue for Lean.abentkamp commentedon May 19, 2026
You're right, we shouldn't use
grind normfor this.But I just remembered this:
grindhomomorphism demo leanprover/lean4#13497I'd guess that this would probably solve the issue.
sonmarcho commentedon May 20, 2026
I'm not sure that's the best solution? It looks more like we need some preprocessing step like what I'm doing here (I discussed the fact we need proper support for this in grind with Leo during the hackathon):
aeneas/backends/lean/Aeneas/Tactic/Step/GrindState.lean
Line 209 in 3fb1cd4
Also, I really think it's worth minimizing the issue and opening an issue on the Lean github: it looks very much like a bug with grind.