Arithmetic issue when upgrading to v4.24

Stream: general

[Adrian Palacios]

I'm in the process of upgrading our Lean project from v4.23.0 to v4.24.0. The last error I need to solve is an omega case as follows:

      cases h₁ : decide ((Int.ofNat (18446744073709551616 - 9223372036854775808 / n₂ % 18446744073709551616)) % Int.ofNat (2 ^ 64) < (Int.ofNat (2 ^ 64) + 1) / 2) == true
      case false =>
        simp only [beq_eq_false_iff_ne, ne_eq] at h₁
        simp only [decide_eq_true_eq, Int.ofNat_eq_coe] at h₁
        omega

where the omega tactic yields:

omega could not prove the goal:
a possible counterexample may satisfy the constraints
  0 ≤ c - 18446744073709551616*d ≤ 18446744073709551615
  1 ≤ 18446744073709551616*b + c - 18446744073709551616*d ≤ 9223372036854775808
  2 ≤ a ≤ 9223372036854775807
where
 a := ↑n₂
 b := ↑(18446744073709551616 - 9223372036854775808 / n₂ % 18446744073709551616) / 18446744073709551616
 c := ↑9223372036854775808 / ↑n₂
 d := ↑(9223372036854775808 / n₂) / 18446744073709551616

The tactic state before omega looks like this:

bv₁ bv₂ : BitVec 64
n₂ : Nat
h₀ : 2 * n₂ < 2 ^ 64
h : 1 < n₂
h₁ : ¬↑(18446744073709551616 - 9223372036854775808 / n₂ % 18446744073709551616) % ↑(2 ^ 64) < (↑(2 ^ 64) + 1) / 2
⊢ (if
      ↑↑(Fin.Internal.ofNat 18446744073709551616 ⋯
                (18446744073709551616 - 9223372036854775808 / n₂ % 18446744073709551616)) %
          ↑18446744073709551616 <
        (↑18446744073709551616 + 1) / 2 then
    ↑↑(Fin.Internal.ofNat 18446744073709551616 ⋯
            (18446744073709551616 - 9223372036854775808 / n₂ % 18446744073709551616)) %
      ↑18446744073709551616
  else
    ↑↑(Fin.Internal.ofNat 18446744073709551616 ⋯
              (18446744073709551616 - 9223372036854775808 / n₂ % 18446744073709551616)) %
        ↑18446744073709551616 -
      ↑18446744073709551616) <
  9223372036854775807

I know that using simp only [Fin.Internal.ofNat] or simp solves the problem, but neither are acceptable to me (Fin.Internal.ofNat is internal, and we stick to simp only in our project). What's a clean way to solve this error? A few more things I've tried:

• using norm_cast but it's hitting a recursion error
• some combinations of conversions but I'm not familiar with Fin numbers so they don't simplify in most cases

[Eric Wieser]

Can you make a #mwe?

[Kevin Buzzard]

Does grind happen to do it?

[Robin Arnez]

I think the first problem is how Fin.Internal.ofNat even appeared in the first place; did you unfold BitVec.ofNat? In that case, try to instead use its API (e.g. BitVec.toFin_ofNat, BitVec.toNat_ofNat)

[Adrian Palacios]

@Eric Wieser I don't know how to make one. This is embedded in a long theorem proof and I assumed we were missing something obvious in this particular case.

@Kevin Buzzard grind doesn't work neither:

`grind` failed
case grind.1.1
bv₁ bv₂ : BitVec 64
n₂ : Nat
h₀ : 2 * n₂ ≤ 18446744073709551615
h : 2 ≤ n₂
h₁ : -1 * (↑(18446744073709551616 - 9223372036854775808 / n₂ % 18446744073709551616) % 18446744073709551616) +
    9223372036854775808 ≤
  0
h_1 : (-1 *
      if
          ↑↑(Fin.Internal.ofNat 18446744073709551616 ⋯
                      (18446744073709551616 - 9223372036854775808 / n₂ % 18446744073709551616)) %
                18446744073709551616 +
              -9223372036854775807 ≤
            0 then
        ↑↑(Fin.Internal.ofNat 18446744073709551616 ⋯
                (18446744073709551616 - 9223372036854775808 / n₂ % 18446744073709551616)) %
          18446744073709551616
      else
        ↑↑(Fin.Internal.ofNat 18446744073709551616 ⋯
                  (18446744073709551616 - 9223372036854775808 / n₂ % 18446744073709551616)) %
            18446744073709551616 +
          -18446744073709551616) +
    9223372036854775807 ≤
  0
h_2 : ↑↑(Fin.Internal.ofNat 18446744073709551616 ⋯ (18446744073709551616 - 9223372036854775808 / n₂ % 18446744073709551616)) %
      18446744073709551616 +
    -9223372036854775807 ≤
  0
h_3 : 9223372036854775808 / ↑n₂ % 18446744073709551616 + -18446744073709551616 ≤ 0
⊢ False

[Kevin Buzzard]

Try using extract_goal for a #mwe .

[Adrian Palacios]

@Kevin Buzzard my IDE says unknown tactic when using extract_goal.

@Robin Arnez we do use BitVec.ofNat earlier in the proof so I'm trying using BitVec APIs in a few places to see if it makes a difference (no luck so far). Here's this entire case before the omega:

    case inr h₁ =>
      subst h₁
      simp only [BitVec.neg, Int64.MAX, BitVec.udiv_eq, BitVec.udiv_def]
      simp only [Nat.reducePow, toNat_intMin, Nat.add_one_sub_one, Nat.reduceMod, toNat_ofNat,
        gt_iff_lt]
      simp only [BitVec.ofNat, Nat.reducePow, toInt_ofFin]
      simp only [BitVec.msb_eq_false_iff_two_mul_lt] at h₀
      replace h : 1 < bv₂.toNat := by
        simp only [BitVec.toInt, h₀, ↓reduceIte] at h
        simp only [← Int.ofNat_lt, Int.cast_ofNat_Int, h]
      generalize bv₂.toNat = n₂ at *
      simp only [Int.bmod_def]
      cases h₁ : decide ((Int.ofNat (18446744073709551616 - 9223372036854775808 / n₂ % 18446744073709551616)) % Int.ofNat (2 ^ 64) < (Int.ofNat (2 ^ 64) + 1) / 2) == true
      case false =>
        simp only [beq_eq_false_iff_ne, ne_eq] at h₁
        simp only [decide_eq_true_eq, Int.ofNat_eq_coe] at h₁

[Robin Arnez]

can you tell me the goal before the simp only [BitVec.ofNat, Nat.reducePow, toInt_ofFin]

[Kevin Buzzard]

extract_goal is a Mathlib tactic: import Mathlib or import Mathlib.Tactic.ExtractGoal. It can be very useful in situations like this; maybe it should be upstreamed?

[Adrian Palacios]

@Robin Arnez yes, it's this:

bv₁ bv₂ : BitVec 64
h : 1 < bv₂.toInt
h₀ : bv₂.msb = false
⊢ (BitVec.ofNat 64 (18446744073709551616 - 9223372036854775808 / bv₂.toNat % 18446744073709551616)).toInt <
  9223372036854775807

[Robin Arnez]

Try simp only [BitVec.toInt_ofNat', Nat.reducePow] instead of that one line

[Adrian Palacios]

@Robin Arnez that worked, thanks so much!

@Kevin Buzzard oh, that makes sense. We don't depend on Mathlib in our project (the Lean formalization of Cedar), but extract_goal sounds generic enough that could be upstreamed.