grind confused by `UInt.toNat`?

Stream: general

[Alexander Bentkamp]

Here is a simple where grind surprisingly fails:

example (b : UInt16) (h : b = 0) : UInt16.toNat b = 0 := by grind [UInt16.toNat_zero]

What's going on here?

[Robin Arnez]

Oh this is because grind normalizes UInt16.toNat 0 to 0 so the lemma UInt16.toNat_zero becomes 0 = 0 and is thus useless to grind. If you want grind to be able to apply this, you'll need to provide a lemma

@[grind gen]
theorem UInt16.toNat_of_eq_zero (h : b = 0) : UInt16.toNat b = 0 := by subst h; rfl

[Robin Arnez]

This might still be worth making an issue for, though

[Alexander Bentkamp]

https://github.com/leanprover/lean4/issues/11990