-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/BitVec/Bitblast.lean
theorem msb_abs {w : Nat} {x : BitVec w} :
    x.abs.msb = (decide (x = intMin w) && decide (0 < w))

Proof state:
case neg
w : Nat
x : BitVec w
h₀ : 0 < w
h₁ : ¬x = intMin w
h₂ : x.msb = true
h₃ : ¬x = 0#w
⊢ ¬x = 0#w

Tactic:
simp [h₃]

Result:
no goals

Proof state:
case pos
w : Nat
x : BitVec w
h₀ : 0 < w
h₁ : ¬x = intMin w
h₂ : x.msb = true
h₃ : x = 0#w
⊢ ¬x = 0#w

Tactic:
simp [h₃] at h₂

Result:
no goals

Proof state:
case pos
w : Nat
x : BitVec w
h₀ : 0 < w
h₁ : ¬x = intMin w
h₂ : x.msb = true
⊢ ¬x = 0#w ∧ ¬x = intMin w

Tactic:
and_intros

Result:
case pos.refine_1
w : Nat
x : BitVec w
h₀ : 0 < w
h₁ : ¬x = intMin w
h₂ : x.msb = true
⊢ ¬x = 0#w

case pos.refine_2
w : Nat
x : BitVec w
h₀ : 0 < w
h₁ : ¬x = intMin w
h₂ : x.msb = true
⊢ ¬x = intMin w

Proof state:
case pos
w : Nat
x : BitVec w
h₀ : 0 < w
h₁ : ¬x = intMin w
h₂ : x.msb = true
⊢ (if x.msb = true then -x else x).msb = (false && decide (0 < w))

Tactic:
simp [h₂, msb_neg]

Result:
case pos
w : Nat
x : BitVec w
h₀ : 0 < w
h₁ : ¬x = intMin w
h₂ : x.msb = true
⊢ ¬x = 0#w ∧ ¬x = intMin w

Proof state:
case pos
w : Nat
x : BitVec w
h₀ : 0 < w
⊢ (if x.msb = true then x.neg else x).msb = (decide (x = intMin w) && decide (0 < w))

Tactic:
by_cases h₁ : x = intMin w

Result:
case pos
w : Nat
x : BitVec w
h₀ : 0 < w
h₁ : x = intMin w
⊢ (if x.msb = true then x.neg else x).msb = (decide (x = intMin w) && decide (0 < w))

case neg
w : Nat
x : BitVec w
h₀ : 0 < w
h₁ : ¬x = intMin w
⊢ (if x.msb = true then x.neg else x).msb = (decide (x = intMin w) && decide (0 < w))

Proof state:
case pos.refine_1
w : Nat
x : BitVec w
h₀ : 0 < w
h₁ : ¬x = intMin w
h₂ : x.msb = true
⊢ ¬x = 0#w

Tactic:
by_cases h₃ : x = 0#w

Result:
case pos
w : Nat
x : BitVec w
h₀ : 0 < w
h₁ : ¬x = intMin w
h₂ : x.msb = true
h₃ : x = 0#w
⊢ ¬x = 0#w

case neg
w : Nat
x : BitVec w
h₀ : 0 < w
h₁ : ¬x = intMin w
h₂ : x.msb = true
h₃ : ¬x = 0#w
⊢ ¬x = 0#w

Proof state:
w : Nat
x : BitVec w
⊢ (if x.msb = true then x.neg else x).msb = (decide (x = intMin w) && decide (0 < w))

Tactic:
by_cases h₀ : 0 < w

Result:
case pos
w : Nat
x : BitVec w
h₀ : 0 < w
⊢ (if x.msb = true then x.neg else x).msb = (decide (x = intMin w) && decide (0 < w))

case neg
w : Nat
x : BitVec w
h₀ : ¬0 < w
⊢ (if x.msb = true then x.neg else x).msb = (decide (x = intMin w) && decide (0 < w))

Proof state:
case neg
w : Nat
x : BitVec w
h₀ : 0 < w
h₁ : ¬x = intMin w
⊢ (if x.msb = true then -x else x).msb = (false && decide (0 < w))

Tactic:
by_cases h₂ : x.msb

Result:
case pos
w : Nat
x : BitVec w
h₀ : 0 < w
h₁ : ¬x = intMin w
h₂ : x.msb = true
⊢ (if x.msb = true then -x else x).msb = (false && decide (0 < w))

case neg
w : Nat
x : BitVec w
h₀ : 0 < w
h₁ : ¬x = intMin w
h₂ : ¬x.msb = true
⊢ (if x.msb = true then -x else x).msb = (false && decide (0 < w))

Proof state:
case pos.refine_2
w : Nat
x : BitVec w
h₀ : 0 < w
h₁ : ¬x = intMin w
h₂ : x.msb = true
⊢ ¬x = intMin w

Tactic:
simp [h₁]

Result:
no goals

Proof state:
w : Nat
x : BitVec w
⊢ x.abs.msb = (decide (x = intMin w) && decide (0 < w))

Tactic:
simp only [BitVec.abs, getMsbD_neg, ne_eq, decide_not, Bool.not_bne]

Result:
w : Nat
x : BitVec w
⊢ (if x.msb = true then x.neg else x).msb = (decide (x = intMin w) && decide (0 < w))

Proof state:
case pos
w : Nat
x : BitVec w
h₀ : 0 < w
h₁ : x = intMin w
⊢ (if x.msb = true then x.neg else x).msb = (decide (x = intMin w) && decide (0 < w))

Tactic:
simp [h₁, msb_intMin]

Result:
no goals

Proof state:
case neg
w : Nat
x : BitVec w
h₀ : 0 < w
h₁ : ¬x = intMin w
⊢ (if x.msb = true then x.neg else x).msb = (decide (x = intMin w) && decide (0 < w))

Tactic:
simp only [neg_eq, h₁, decide_false]

Result:
case neg
w : Nat
x : BitVec w
h₀ : 0 < w
h₁ : ¬x = intMin w
⊢ (if x.msb = true then -x else x).msb = (false && decide (0 < w))

Proof state:
w : Nat
x : BitVec w
h₀ : ¬0 < w
⊢ w = 0

Tactic:
omega

Result:
no goals

Proof state:
case neg
w : Nat
x : BitVec w
h₀ : ¬0 < w
⊢ (if x.msb = true then x.neg else x).msb = (decide (x = intMin w) && decide (0 < w))

Tactic:
simp [BitVec.msb, show w = 0 by omega]

Result:
no goals

Proof state:
case neg
w : Nat
x : BitVec w
h₀ : 0 < w
h₁ : ¬x = intMin w
h₂ : ¬x.msb = true
⊢ (if x.msb = true then -x else x).msb = (false && decide (0 < w))

Tactic:
simp [h₂]

Result:
no goals