-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/BitVec/Lemmas.lean
theorem toInt_abs_eq_natAbs {x : BitVec w} : x.abs.toInt =
    if x = intMin w then (intMin w).toInt else x.toInt.natAbs

Proof state:
case pos
w : Nat
x : BitVec w
hx : ¬x = intMin w
h : x.msb = true
⊢ (if x.msb = true then -x.toInt else x.toInt) = ↑x.toInt.natAbs

Tactic:
simp only [h, ↓reduceIte]

Result:
case pos
w : Nat
x : BitVec w
hx : ¬x = intMin w
h : x.msb = true
⊢ -x.toInt = ↑x.toInt.natAbs

Proof state:
case pos
w : Nat
x : BitVec w
hx : x = intMin w
⊢ (if x = intMin w then (intMin w).toInt else if x.msb = true then -x.toInt else x.toInt) =
    if x = intMin w then (intMin w).toInt else ↑x.toInt.natAbs

Tactic:
simp [hx]

Result:
no goals

Proof state:
case neg
w : Nat
x : BitVec w
hx : ¬x = intMin w
h : ¬x.msb = true
⊢ (if x.msb = true then -x.toInt else x.toInt) = ↑x.toInt.natAbs

Tactic:
simp only [h, Bool.false_eq_true, ↓reduceIte]

Result:
case neg
w : Nat
x : BitVec w
hx : ¬x = intMin w
h : ¬x.msb = true
⊢ x.toInt = ↑x.toInt.natAbs

Proof state:
w : Nat
x : BitVec w
hx : ¬x = intMin w
h : ¬x.msb = true
⊢ 2 * x.toNat < 2 ^ w

Tactic:
exact msb_eq_false_iff_two_mul_lt.mp (by simp [h])

Result:
no goals

Proof state:
w : Nat
x : BitVec w
hx : ¬x = intMin w
h : x.msb = true
⊢ x.toInt < 0

Tactic:
rw [toInt_neg_iff]

Result:
w : Nat
x : BitVec w
hx : ¬x = intMin w
h : x.msb = true
⊢ 2 ^ w ≤ 2 * x.toNat

Proof state:
case pos
w : Nat
x : BitVec w
hx : ¬x = intMin w
h : x.msb = true
⊢ -x.toInt = ↑x.toInt.natAbs

Tactic:
have : x.toInt < 0 := by
  rw [toInt_neg_iff]
  have := msb_eq_true_iff_two_mul_ge.mp h
  omega

Result:
case pos
w : Nat
x : BitVec w
hx : ¬x = intMin w
h : x.msb = true
this : x.toInt < 0
⊢ -x.toInt = ↑x.toInt.natAbs

Proof state:
w : Nat
x : BitVec w
hx : ¬x = intMin w
h : ¬x.msb = true
⊢ 0 ≤ x.toInt

Tactic:
rw [toInt_pos_iff]

Result:
w : Nat
x : BitVec w
hx : ¬x = intMin w
h : ¬x.msb = true
⊢ 2 * x.toNat < 2 ^ w

Proof state:
case neg
w : Nat
x : BitVec w
hx : ¬x = intMin w
⊢ (if x = intMin w then (intMin w).toInt else if x.msb = true then -x.toInt else x.toInt) =
    if x = intMin w then (intMin w).toInt else ↑x.toInt.natAbs

Tactic:
simp [hx]

Result:
case neg
w : Nat
x : BitVec w
hx : ¬x = intMin w
⊢ (if x.msb = true then -x.toInt else x.toInt) = ↑x.toInt.natAbs

Proof state:
case pos
w : Nat
x : BitVec w
hx : ¬x = intMin w
h : x.msb = true
this : x.toInt < 0
⊢ -x.toInt = ↑x.toInt.natAbs

Tactic:
omega

Result:
no goals

Proof state:
case neg
w : Nat
x : BitVec w
hx : ¬x = intMin w
⊢ (if x.msb = true then -x.toInt else x.toInt) = ↑x.toInt.natAbs

Tactic:
by_cases h : x.msb

Result:
case pos
w : Nat
x : BitVec w
hx : ¬x = intMin w
h : x.msb = true
⊢ (if x.msb = true then -x.toInt else x.toInt) = ↑x.toInt.natAbs

case neg
w : Nat
x : BitVec w
hx : ¬x = intMin w
h : ¬x.msb = true
⊢ (if x.msb = true then -x.toInt else x.toInt) = ↑x.toInt.natAbs

Proof state:
case neg
w : Nat
x : BitVec w
hx : ¬x = intMin w
h : ¬x.msb = true
⊢ x.toInt = ↑x.toInt.natAbs

Tactic:
have : 0 ≤ x.toInt := by
  rw [toInt_pos_iff]
  exact msb_eq_false_iff_two_mul_lt.mp (by simp [h])

Result:
case neg
w : Nat
x : BitVec w
hx : ¬x = intMin w
h : ¬x.msb = true
this : 0 ≤ x.toInt
⊢ x.toInt = ↑x.toInt.natAbs

Proof state:
w : Nat
x : BitVec w
hx : ¬x = intMin w
h : x.msb = true
this : 2 * x.toNat ≥ 2 ^ w
⊢ 2 ^ w ≤ 2 * x.toNat

Tactic:
omega

Result:
no goals

Proof state:
w : Nat
x : BitVec w
hx : ¬x = intMin w
h : ¬x.msb = true
⊢ x.msb = false

Tactic:
simp [h]

Result:
no goals

Proof state:
case neg
w : Nat
x : BitVec w
hx : ¬x = intMin w
h : ¬x.msb = true
this : 0 ≤ x.toInt
⊢ x.toInt = ↑x.toInt.natAbs

Tactic:
omega

Result:
no goals

Proof state:
w : Nat
x : BitVec w
⊢ x.abs.toInt = if x = intMin w then (intMin w).toInt else ↑x.toInt.natAbs

Tactic:
rw [toInt_abs_eq_ite]

Result:
w : Nat
x : BitVec w
⊢ (if x = intMin w then (intMin w).toInt else if x.msb = true then -x.toInt else x.toInt) =
    if x = intMin w then (intMin w).toInt else ↑x.toInt.natAbs

Proof state:
w : Nat
x : BitVec w
⊢ (if x = intMin w then (intMin w).toInt else if x.msb = true then -x.toInt else x.toInt) =
    if x = intMin w then (intMin w).toInt else ↑x.toInt.natAbs

Tactic:
by_cases hx : x = intMin w

Result:
case pos
w : Nat
x : BitVec w
hx : x = intMin w
⊢ (if x = intMin w then (intMin w).toInt else if x.msb = true then -x.toInt else x.toInt) =
    if x = intMin w then (intMin w).toInt else ↑x.toInt.natAbs

case neg
w : Nat
x : BitVec w
hx : ¬x = intMin w
⊢ (if x = intMin w then (intMin w).toInt else if x.msb = true then -x.toInt else x.toInt) =
    if x = intMin w then (intMin w).toInt else ↑x.toInt.natAbs

Proof state:
w : Nat
x : BitVec w
hx : ¬x = intMin w
h : x.msb = true
⊢ 2 ^ w ≤ 2 * x.toNat

Tactic:
have := msb_eq_true_iff_two_mul_ge.mp h

Result:
w : Nat
x : BitVec w
hx : ¬x = intMin w
h : x.msb = true
this : 2 * x.toNat ≥ 2 ^ w
⊢ 2 ^ w ≤ 2 * x.toNat