Trivial Fin equality not solved by simp or omega

Stream: general

[Francisco Giordano]

I found neither simp nor omega were able to solve a seemingly trivial Fin equality. Shouldn't omega be able to solve this? Is there a missing simp theorem?

example : UInt8.val 0 = 0 := by simp -- unsolved goal
example : UInt8.val 0 = 0 := by omega -- omega could not prove the goal
example : UInt8.val 0 = 0 := by decide -- ok

[Henrik Böving]

Uint8 is not yet included in the scope of omega. That could change in the future, I don't know about the exact plans here

[Eric Wieser]

Omega or not, I'm surprised there isn't a simp lemma for this

[Francisco Giordano]

After looking at this a bit more I can't come up with a reasonable simp lemma that would help here. I was trying something like this but it's too specific and I can't even get it to work with the [simp] attribute:

theorem UInt8.val_ofNat_eq_ofNat (n : Nat) : UInt8.val (OfNat.ofNat n) = OfNat.ofNat n := rfl

[Eric Wieser]

You need

@[simp]
theorem UInt8.val_ofNat_eq_ofNat (n : Nat) : UInt8.val (no_index (OfNat.ofNat n)) = OfNat.ofNat n := rfl

[Eric Wieser]

There is a library note in mathlib about this, search for "no_index around OfNat.ofNat"

[Eric Wieser]

Unfortunately these don't yet surface in the docs

[Francisco Giordano]

Wow, that does fix it! Thanks.

Link for others: https://github.com/leanprover-community/mathlib4/blob/af9a9c9ca2d15cc943a98510094e76a55cd8d988/Mathlib/Data/Nat/Cast/Defs.lean#L60-L66

[Kim Morrison]

@Henrik Böving, I don't want to PR this because you are about to change UInt, but could you arrange that UIntX.val_ofNat is available as appropriate?

[Henrik Böving]

Yes

[Henrik Böving]

Done in https://github.com/leanprover/lean4/pull/5735