Conversion from ℤ → UInt64 → ℤ

Stream: mathlib4

[Geoffrey Irving]

It feels like this should be very easy to prove, but I am stuck. Not sure how to unpack the various definitions. The conversion is happening via the fact that Fin n is a commutative ring, so one conceptual proof is induction on the presentation of ℤ, but I don't know how to express that.

import Mathlib.Data.UInt

@[simp] lemma UInt64.toInt_intCast (n : ℤ) : ((n : UInt64).toNat : ℤ) = n % 2^64 := by
  sorry

[Eric Rodriguez]

the Nat version is easy:

@[simp] lemma UInt64.toInt_intCast (n : ℕ) : ((n : UInt64).toNat) = n % 2^64 := Fin.coe_ofNat_eq_mod _ _

and I assume you need it for this. Some way of doing this is just saying that $n + N * 2^64$ is positive for some large enough $N$ and then use the natural number result I guess? but not sure how much API is there

[Geoffrey Irving]

I already have the Nat version. Now I need the Int version.

[Geoffrey Irving]

(I need to do a bit of signed 128-bit arithmetic, and this is a necessary lemma for proving things about that.)

[Geoffrey Irving]

True, adding a big multiple should do it. Thanks!

[Geoffrey Irving]

Though the APIs are super different: the Nat one is more native since Fin wraps Nat, and doesn’t use general rings.

[Geoffrey Irving]

Resolved: rewriting as Nat or -Nat makes it straightforward, via

theorem Int.induction_overlap {p : ℤ → Prop} (hi : ∀ n : ℕ, p n) (lo : ∀ n : ℕ, p (-n)) :
    ∀ n : ℤ, p n := by intro n; induction' n with n; exact hi n; exact lo (_ + 1)

[Eric Wieser]

Arguably that should replace docs#Int.eq_nat_or_neg (swapping obtain ⟨n, rfl, rfl⟩ := z.eq_nat_or_neg for induction x using that_lemma)