-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/BitVec/Lemmas.lean
theorem toInt_neg_of_ne_intMin {x : BitVec w} (rs : x ≠ intMin w) :
    (-x).toInt = -(x.toInt)

Proof state:
case neg
w : Nat
x : BitVec w
rs : ¬x.toNat = 2 ^ (w - 1) % 2 ^ w
x_zero : ¬x = 0
w_0 : ¬w = 0
⊢ (-x).toInt = -x.toInt

Tactic:
have : 0 < w := by omega

Result:
case neg
w : Nat
x : BitVec w
rs : ¬x.toNat = 2 ^ (w - 1) % 2 ^ w
x_zero : ¬x = 0
w_0 : ¬w = 0
this : 0 < w
⊢ (-x).toInt = -x.toInt

Proof state:
w : Nat
x : BitVec w
rs : x ≠ intMin w
⊢ (-x).toInt = -x.toInt

Tactic:
simp only [ne_eq, toNat_eq, toNat_intMin] at rs

Result:
w : Nat
x : BitVec w
rs : ¬x.toNat = 2 ^ (w - 1) % 2 ^ w
⊢ (-x).toInt = -x.toInt

Proof state:
w : Nat
x : BitVec w
rs : ¬x.toNat = 2 ^ (w - 1) % 2 ^ w
x_zero : ¬x = 0
w_0 : ¬w = 0
this : 0 < w
⊢ 0 < w

Tactic:
omega

Result:
no goals

Proof state:
w : Nat
x : BitVec w
rs : ¬x.toNat = 2 ^ (w - 1)
x_zero : ¬x = 0
w_0 : ¬w = 0
this : 0 < w
⊢ 0 < w

Tactic:
omega

Result:
no goals

Proof state:
w : Nat
x : BitVec w
rs : ¬x.toNat = 2 ^ (w - 1) % 2 ^ w
x_zero : ¬x = 0
w_0 : ¬w = 0
⊢ 0 < w

Tactic:
omega

Result:
no goals

Proof state:
case neg
w : Nat
x : BitVec w
rs : ¬x.toNat = 2 ^ (w - 1) % 2 ^ w
x_zero : ¬x = 0
w_0 : ¬w = 0
this : 0 < w
⊢ (-x).toInt = -x.toInt

Tactic:
rw [Nat.two_pow_pred_mod_two_pow (by omega)] at rs

Result:
case neg
w : Nat
x : BitVec w
rs : ¬x.toNat = 2 ^ (w - 1)
x_zero : ¬x = 0
w_0 : ¬w = 0
this : 0 < w
⊢ (-x).toInt = -x.toInt

Proof state:
case pos
x : BitVec 0
rs : ¬x.toNat = 2 ^ (0 - 1) % 2 ^ 0
x_zero : ¬x = 0
⊢ (-x).toInt = -x.toInt

Tactic:
simp [BitVec.eq_nil x]

Result:
no goals

Proof state:
case neg
w : Nat
x : BitVec w
rs : ¬x.toNat = 2 ^ (w - 1)
x_zero : ¬x = 0
w_0 : ¬w = 0
this : 0 < w
⊢ (-x).toInt = -x.toInt

Tactic:
simp only [BitVec.toInt, BitVec.toNat_neg, BitVec.sub_toNat_mod_cancel x_zero]

Result:
case neg
w : Nat
x : BitVec w
rs : ¬x.toNat = 2 ^ (w - 1)
x_zero : ¬x = 0
w_0 : ¬w = 0
this : 0 < w
⊢ (if 2 * (2 ^ w - x.toNat) < 2 ^ w then ↑(2 ^ w - x.toNat) else ↑(2 ^ w - x.toNat) - ↑(2 ^ w)) =
    -if 2 * x.toNat < 2 ^ w then ↑x.toNat else ↑x.toNat - ↑(2 ^ w)

Proof state:
case pos
w : Nat
x : BitVec w
rs : ¬x.toNat = 2 ^ (w - 1) % 2 ^ w
x_zero : ¬x = 0
w_0 : w = 0
⊢ (-x).toInt = -x.toInt

Tactic:
subst w_0

Result:
case pos
x : BitVec 0
rs : ¬x.toNat = 2 ^ (0 - 1) % 2 ^ 0
x_zero : ¬x = 0
⊢ (-x).toInt = -x.toInt

Proof state:
case neg
w : Nat
x : BitVec w
rs : ¬x.toNat = 2 ^ (w - 1) % 2 ^ w
x_zero : ¬x = 0
⊢ (-x).toInt = -x.toInt

Tactic:
by_cases w_0 : w = 0

Result:
case pos
w : Nat
x : BitVec w
rs : ¬x.toNat = 2 ^ (w - 1) % 2 ^ w
x_zero : ¬x = 0
w_0 : w = 0
⊢ (-x).toInt = -x.toInt

case neg
w : Nat
x : BitVec w
rs : ¬x.toNat = 2 ^ (w - 1) % 2 ^ w
x_zero : ¬x = 0
w_0 : ¬w = 0
⊢ (-x).toInt = -x.toInt

Proof state:
case neg
w : Nat
x : BitVec w
rs : ¬x.toNat = 2 ^ (w - 1)
x_zero : ¬x = 0
w_0 : ¬w = 0
this : 0 < w
⊢ (if 2 * (2 ^ w - x.toNat) < 2 ^ w then ↑(2 ^ w - x.toNat) else ↑(2 ^ w - x.toNat) - ↑(2 ^ w)) =
    -if 2 * x.toNat < 2 ^ w then ↑x.toNat else ↑x.toNat - ↑(2 ^ w)

Tactic:
have := @Nat.two_pow_pred_mul_two w (by omega)

Result:
case neg
w : Nat
x : BitVec w
rs : ¬x.toNat = 2 ^ (w - 1)
x_zero : ¬x = 0
w_0 : ¬w = 0
this✝ : 0 < w
this : 2 ^ (w - 1) * 2 = 2 ^ w
⊢ (if 2 * (2 ^ w - x.toNat) < 2 ^ w then ↑(2 ^ w - x.toNat) else ↑(2 ^ w - x.toNat) - ↑(2 ^ w)) =
    -if 2 * x.toNat < 2 ^ w then ↑x.toNat else ↑x.toNat - ↑(2 ^ w)

Proof state:
case pos
w : Nat
x : BitVec w
rs : ¬x.toNat = 2 ^ (w - 1) % 2 ^ w
x_zero : x = 0
⊢ (-x).toInt = -x.toInt

Tactic:
subst x_zero

Result:
case pos
w : Nat
rs : ¬BitVec.toNat 0 = 2 ^ (w - 1) % 2 ^ w
⊢ (-0).toInt = -BitVec.toInt 0

Proof state:
case pos
w : Nat
rs : ¬BitVec.toNat 0 = 2 ^ (w - 1) % 2 ^ w
⊢ (-0).toInt = -BitVec.toInt 0

Tactic:
simp [BitVec.toInt]

Result:
case pos
w : Nat
rs : ¬BitVec.toNat 0 = 2 ^ (w - 1) % 2 ^ w
⊢ (if 0 < 2 ^ w then 0 else -↑(2 ^ w)) = -if 0 < 2 ^ w then 0 else -↑(2 ^ w)

Proof state:
w : Nat
x : BitVec w
rs : ¬x.toNat = 2 ^ (w - 1) % 2 ^ w
⊢ (-x).toInt = -x.toInt

Tactic:
by_cases x_zero : x = 0

Result:
case pos
w : Nat
x : BitVec w
rs : ¬x.toNat = 2 ^ (w - 1) % 2 ^ w
x_zero : x = 0
⊢ (-x).toInt = -x.toInt

case neg
w : Nat
x : BitVec w
rs : ¬x.toNat = 2 ^ (w - 1) % 2 ^ w
x_zero : ¬x = 0
⊢ (-x).toInt = -x.toInt

Proof state:
case pos
w : Nat
rs : ¬BitVec.toNat 0 = 2 ^ (w - 1) % 2 ^ w
⊢ (if 0 < 2 ^ w then 0 else -↑(2 ^ w)) = -if 0 < 2 ^ w then 0 else -↑(2 ^ w)

Tactic:
omega

Result:
no goals

Proof state:
case neg
w : Nat
x : BitVec w
rs : ¬x.toNat = 2 ^ (w - 1)
x_zero : ¬x = 0
w_0 : ¬w = 0
this✝ : 0 < w
this : 2 ^ (w - 1) * 2 = 2 ^ w
⊢ (if 2 * (2 ^ w - x.toNat) < 2 ^ w then ↑(2 ^ w - x.toNat) else ↑(2 ^ w - x.toNat) - ↑(2 ^ w)) =
    -if 2 * x.toNat < 2 ^ w then ↑x.toNat else ↑x.toNat - ↑(2 ^ w)

Tactic:
split <;> split <;> omega

Result:
no goals