grind on a new UInt type

Stream: general

[Alexander Bentkamp]

I would like to create a copy of UInt64, which I call USize64. How can I set grind up to work on it just as well as on UInt64? Here is an example of what I would like to achieve:

set_option trace.grind.debug true

/- This works: -/
example {i} :
UInt64.toNat i < UInt64.toNat 3 →
 UInt64.toNat 4 + UInt64.toNat i < 100 :=
   by grind only => done

/- A copy of UInt64 -/
structure USize64 where ofUInt64 :: toUInt64 : UInt64

instance {n} : OfNat USize64 n := ⟨⟨OfNat.ofNat n⟩⟩
def USize64.toNat (n : USize64) : Nat := UInt64.toNat n.toUInt64

/- The same example fails on my new type: -/
example {i} :
USize64.toNat i < USize64.toNat 3 →
 USize64.toNat 4 + USize64.toNat i < 100 :=
   by grind only => done

I have tried to instantiate the Lean.Grind.ToInt type classes, but without success.

[Robin Arnez]

I think the relevant stuff is in Init.GrindInstances.Ring.UInt lines 281-318 and lines 45-73
and Init.GrindInstances.ToInt lines 248-280

[Alexander Bentkamp]

I think I tried to add all of these before. Is there a way to get debug output from grind that would tell me exactly which of these instances is used?

[Robin Arnez]

Oh right in this case this is grind using the seval simproc UInt64.reduceToNat from here

[Alexander Bentkamp]

Oh. That's great to know! How did you find out?

[Alexander Bentkamp]

And, more importantly, can I add custom simprocs to grind? I saw an older thread that you cannot. Is this still the case?

[Robin Arnez]

You can, kinda, but I'd not recommend doing this for anything other than evaluation simprocs:

import Lean

/-- A copy of UInt64 -/
structure USize64 where ofUInt64 :: toUInt64 : UInt64

instance {n} : OfNat USize64 n := ⟨⟨OfNat.ofNat n⟩⟩
def USize64.toNat (n : USize64) : Nat := UInt64.toNat n.toUInt64

open Lean Meta in
simproc [seval] USize64.reduceToNat (USize64.toNat _) := fun e => do
  let_expr USize64.toNat n := e | return .continue
  let some (n, _) ← getOfNatValue? n ``USize64 | return .continue
  return .done { expr := toExpr n.toUInt64.toNat }

/-- Works -/
example {i} : USize64.toNat i < USize64.toNat 3 → USize64.toNat 4 + USize64.toNat i < 100 := by
  grind only => done

[Alexander Bentkamp]

Wow, that's great! Thank you!