Making norm_num work for UInt64

Stream: metaprogramming / tactics

[Geoffrey Irving]

How would one make norm_num work for UInt64? In particular, I'd like it to be able to do things like this:

import Mathlib

lemma simple : (64 : UInt64).toNat = 64 := by norm_num

In this case of course rfl works, but often I have things like (64 : UInt64).toNat in the middle of larger expressions.

[Mario Carneiro]

you can do rw [show (64 : UInt64).toNat = 64 by rfl]

[Geoffrey Irving]

Yes, I know how to do it laboriously. The question is whether I can make a nice tactic do it.

[Geoffrey Irving]

Often I have expressions with a few different numbers like this (127.toNat, etc.).

[Eric Wieser]

Maybe we should have a simp lemma that says (OfNat.ofNat n : UInt64).toNat = OfNat.ofNat n &&& (1 << 64 - 1)?

[Mario Carneiro]

I'm a little worried about rules like that since it seems like norm_num would happily simplify that to ofNat n &&& 18446744073709551615

[Eric Wieser]

But n will be a numeral so that will simplify all the way?

[Mario Carneiro]

it still seems like a wasteful approach, I dislike proofs about N bit integers where the proof work gets larger for larger N

[Mario Carneiro]

A norm_num extension that works directly on terms of the form (OfNat.ofNat n : UInt64).toNat seems better (without the detour through &&&)