fix: don't use modulo for UInt upcasting

[digama0]

This makes (v : UInt8).toUInt16.toNat = (v : UInt8).toNat a defeq, which simplifies proofs.

[leanprover-community-mathlib4-bot]

Mathlib CI status (docs):

• 💥 Mathlib branch lean-pr-testing-3960 build failed against this PR. (2024-04-20 16:02:42) View Log
• 💥 Mathlib branch lean-pr-testing-3960 build failed against this PR. (2024-04-20 16:23:33) View Log

[nomeata]

(Removed from queue due to mathlib failures; were they expected?)

[digama0]

Yes, they are expected. Should I make a bump PR? The breakage should be minimal, because mathlib doesn't do much with fixed size integers.

[digama0]

Just checked, it is from theorems in Std like this:

@[simp] theorem UInt8.toUInt16_toNat (x : UInt8) : x.toUInt16.toNat = x.toNat :=
  Nat.mod_eq_of_lt (Nat.lt_of_lt_of_le x.toNat_lt (by decide))

@[simp] theorem UInt8.toUInt32_toNat (x : UInt8) : x.toUInt32.toNat = x.toNat :=
  Nat.mod_eq_of_lt (Nat.lt_of_lt_of_le x.toNat_lt (by decide))

@[simp] theorem UInt8.toUInt64_toNat (x : UInt8) : x.toUInt64.toNat = x.toNat :=
  Nat.mod_eq_of_lt (Nat.lt_of_lt_of_le x.toNat_lt (by decide))

which are exactly the ones that are rfl after this PR. So it should be easily fixable.

[nomeata]

If you say it's fine I can merge, although it doesn't hurt to have the fixes ready ahead of time, by pushing to the lean-pr-testing branches. Then whoever updates nightly-testing has less to think about, don't they?

[kim-em]

I did encounter the errors on Std's nightly-testing before reading this thread, but found it pretty quickly.

I think a good option, when not having a lean-pr-testing-NNNN branch ready (or even when!) is to post on zulip's nightly-testing stream saying that a breakage is expected (and, if available, a quick description of the fix).