chore: fix bv_omega regression since v4.9.0 (#4579)

This example, reported from LNSym, started failing when we changed the
definition of `Fin.sub` in
#4421.

When we use the new definition, `omega` produces a proof term that the
kernel is very slow on.

To work around this for now, I've removed `BitVec.toNat_sub` from the
`bv_toNat` simp set,
and replaced it with `BitVec.toNat_sub'` which uses the old definition
for subtraction.

This is only a workaround, and I would like to understand why the term
chokes the kernel.

```
example
    (n : Nat)
    (addr2 addr1 : BitVec 64)
    (h0 : n ≤ 18446744073709551616)
    (h1 : addr2 + 18446744073709551615#64 - addr1 ≤ BitVec.ofNat 64 (n - 1))
    (h2 : addr2 - addr1 ≤ addr2 + 18446744073709551615#64 - addr1) :
    n = 18446744073709551616 := by
  bv_omega
```

Author: kim-em

src/Init/Data/BitVec/Lemmas.lean

@@ -1043,8 +1043,16 @@ theorem ofInt_add {n} (x y : Int) : BitVec.ofInt n (x + y) =
 
 theorem sub_def {n} (x y : BitVec n) : x - y = .ofNat n ((2^n - y.toNat) + x.toNat) := by rfl
 
-@[simp, bv_toNat] theorem toNat_sub {n} (x y : BitVec n) :
-  (x - y).toNat = (((2^n - y.toNat) + x.toNat) % 2^n) := rfl
+@[simp] theorem toNat_sub {n} (x y : BitVec n) :
+    (x - y).toNat = (((2^n - y.toNat) + x.toNat) % 2^n) := rfl
+
+-- We prefer this lemma to `toNat_sub` for the `bv_toNat` simp set.
+-- For reasons we don't yet understand, unfolding via `toNat_sub` sometimes
+-- results in `omega` generating proof terms that are very slow in the kernel.
+@[bv_toNat] theorem toNat_sub' {n} (x y : BitVec n) :
+    (x - y).toNat = ((x.toNat + (2^n - y.toNat)) % 2^n) := by
+  rw [toNat_sub, Nat.add_comm]
+
 @[simp] theorem toFin_sub (x y : BitVec n) : (x - y).toFin = toFin x - toFin y := rfl
 
 @[simp] theorem ofFin_sub (x : Fin (2^n)) (y : BitVec n) : .ofFin x - y = .ofFin (x - y.toFin) :=

tests/lean/run/omega.lean

@@ -466,6 +466,31 @@ example (x y : BitVec 64) (_ : x < (y.truncate 32).zeroExtend 64) :
     ~~~x > (1#64 <<< 63) := by
   bv_omega
 
+-- This example, reported from LNSym,
+-- started failing when we changed the definition of `Fin.sub` in https://github.com/leanprover/lean4/pull/4421.
+-- When we use the new definition, `omega` produces a proof term that the kernel is very slow on.
+-- To work around this for now, I've removed `BitVec.toNat_sub` from the `bv_toNat` simp set,
+-- and replaced it with `BitVec.toNat_sub'` which uses the old definition for subtraction.
+-- This is only a workaround, and I would like to understand why the term chokes the kernel.
+example
+    (n : Nat)
+    (addr2 addr1 : BitVec 64)
+    (h0 : n ≤ 18446744073709551616)
+    (h1 : addr2 + 18446744073709551615#64 - addr1 ≤ BitVec.ofNat 64 (n - 1))
+    (h2 : addr2 - addr1 ≤ addr2 + 18446744073709551615#64 - addr1) :
+    n = 18446744073709551616 := by
+  bv_omega
+
+-- This smaller example exhibits the same problem.
+example
+    (n : Nat)
+    (addr2 addr1 : BitVec 16)
+    (h0 : n ≤ 65536)
+    (h1 : addr2 + 65535#16 - addr1 ≤ BitVec.ofNat 16 (n - 1))
+    (h2 : addr2 - addr1 ≤ addr2 + 65535#16 - addr1) :
+    n = 65536 := by
+  bv_omega
+
 /-! ### Error messages -/
 
 /--