Proving equalities for `UInt` types

Stream: new members

[Eduard Vintilă]

Greetings, everyone!

Lately, I've been working on a Lean project which makes use of fixed-length unsigned integer types such as UInt32, but I've been having some issues in proving some trivial equalities using these types.

For example, proving an equality on natural numbers such as the one below is fairly straightforward :

import Mathlib

example (α β: ℕ) (hneq : α ≠ β + 1) :
    α + 1 ≠ β + 2 := by
    simp [hneq]

The same example on UInt32 seems to fail, however:

import Mathlib

example (α β: UInt32) (hneq : α ≠ β + 1) :
    α + 1 ≠ β + 2 := by
    simp [hneq]

unsolved goals
αβ: UInt32
hneq: α ≠ β + 1
⊢ ¬α + 1 = β + 2

By tracing which simp rules are applied by using set_option trace.Meta.Tactic.simp true, I observed that unification fails at this step for UInt32 numbers:

[Meta.Tactic.simp.unify] @add_left_inj:1000, failed to unify
      ?b + ?a = ?c + ?a
    with
      α + 1 = β + 2

Meanwhile, for natural numbers, it succedes just as expected:

[Meta.Tactic.simp.rewrite] @add_left_inj:1000, α + 1 = β + 2 ==> α = β + 1

Interestingly enough, if I add theorems for associativity and 2 = 1 + 1 for UInt32 numbers, along with mentioning which rules simp should use, the example works:

import Mathlib

@[simp] theorem test_two : (2 : UInt32) = (1 : UInt32) + (1 : UInt32)  := by ac_rfl
@[simp] theorem test_assoc (a b c : UInt32) : a + (b + c) = (a + b) + c  := by ac_rfl


example (α β: UInt32) (hneq : α ≠ β + 1) :
    α + 1 ≠ β + 2 := by
    simp only [ne_eq, add_left_inj, not_false_eq_true, hneq, test_two, test_assoc]

Tactic state
No goals

However, these kind of theorems are already included in mathlib. Furthermore, UInt32 types are defined as Fin 2^32, for which there is already an abelian group instantiation in mathlib and should already cover properties such as associativity.
Why do I need to state them explicitly in order to prove trivial equalities like the one I've shown?

I'm not sure whether I'm not importing the right library files, or even that I may need to use different tactics/proof techniques to prove equalities like this. Any insights would be greatly appreciated! Thank you!