-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/BitVec/Bitblast.lean
theorem msb_neg {w : Nat} {x : BitVec w} :
    (-x).msb = ((x != 0#w && x != intMin w) ^^ x.msb)

Proof state:
w : Nat
x : BitVec w
⊢ (x.getMsbD 0 ^^ decide (∃ j, j < w ∧ 0 < j ∧ x.getMsbD j = true)) = (x != 0#w && x != intMin w ^^ x.getMsbD 0)

Tactic:
by_cases hmin : x = intMin _

Result:
case pos
w : Nat
x : BitVec w
hmin : x = intMin w
⊢ (x.getMsbD 0 ^^ decide (∃ j, j < w ∧ 0 < j ∧ x.getMsbD j = true)) = (x != 0#w && x != intMin w ^^ x.getMsbD 0)

case neg
w : Nat
x : BitVec w
hmin : ¬x = intMin w
⊢ (x.getMsbD 0 ^^ decide (∃ j, j < w ∧ 0 < j ∧ x.getMsbD j = true)) = (x != 0#w && x != intMin w ^^ x.getMsbD 0)

Proof state:
w : Nat
x : BitVec w
hmin : ¬x = intMin w
hzero : x = 0#w
⊢ (x.getMsbD 0 ^^ decide (∃ j, j < w ∧ 0 < j ∧ x.getMsbD j = true)) = (x != 0#w && x != intMin w ^^ x.getMsbD 0)

Tactic:
simp [hzero]

Result:
no goals

Proof state:
w : Nat
x : BitVec w
hmin : x = intMin w
this : (∃ j, j < w ∧ 0 < j ∧ 0 < w ∧ j = 0) ↔ False
⊢ (x.getMsbD 0 ^^ decide (∃ j, j < w ∧ 0 < j ∧ x.getMsbD j = true)) = (x != 0#w && x != intMin w ^^ x.getMsbD 0)

Tactic:
simp [hmin, getMsbD_intMin, this]

Result:
no goals

Proof state:
case pred
w : Nat
x : BitVec w
hmin : ¬x = intMin w
hzero : ¬x = 0#w
w_pos : 0 < w
getMsbD_x : ∀ (x_1 : Nat), x_1 < w → 0 < x_1 → x.getMsbD x_1 = false
hmsb : x.msb = false
i : Nat
hi : i < w
⊢ x.getMsbD i = false

Tactic:
cases i

Result:
case pred.zero
w : Nat
x : BitVec w
hmin : ¬x = intMin w
hzero : ¬x = 0#w
w_pos : 0 < w
getMsbD_x : ∀ (x_1 : Nat), x_1 < w → 0 < x_1 → x.getMsbD x_1 = false
hmsb : x.msb = false
hi : 0 < w
⊢ x.getMsbD 0 = false

case pred.succ
w : Nat
x : BitVec w
hmin : ¬x = intMin w
hzero : ¬x = 0#w
w_pos : 0 < w
getMsbD_x : ∀ (x_1 : Nat), x_1 < w → 0 < x_1 → x.getMsbD x_1 = false
hmsb : x.msb = false
n✝ : Nat
hi : n✝ + 1 < w
⊢ x.getMsbD (n✝ + 1) = false

Proof state:
w : Nat
x : BitVec w
hmin : x = intMin w
⊢ ∀ (x : Nat), x < w → 0 < x → 0 < w → ¬x = 0

Tactic:
omega

Result:
no goals

Proof state:
w : Nat
x : BitVec w
hmin : ¬x = intMin w
hzero : ¬x = 0#w
w_pos : 0 < w
getMsbD_x : ∀ (x_1 : Nat), x_1 < w → 0 < x_1 → x.getMsbD x_1 = false
hmsb : x.msb = true
hi : 0 < w
⊢ x.getMsbD 0 = decide (0 = 0)

Tactic:
exact hmsb

Result:
no goals

Proof state:
w : Nat
x : BitVec w
hmin : ¬x = intMin w
hzero : ¬x = 0#w
w_pos : 0 < w
getMsbD_x : ∀ (x_1 : Nat), x_1 < w → 0 < x_1 → x.getMsbD x_1 = false
hmsb : x.msb = false
⊢ False

Tactic:
apply hzero

Result:
w : Nat
x : BitVec w
hmin : ¬x = intMin w
hzero : ¬x = 0#w
w_pos : 0 < w
getMsbD_x : ∀ (x_1 : Nat), x_1 < w → 0 < x_1 → x.getMsbD x_1 = false
hmsb : x.msb = false
⊢ x = 0#w

Proof state:
w : Nat
x : BitVec w
hmin : ¬x = intMin w
hzero : ¬x = 0#w
w_pos : 0 < w
getMsbD_x : ∀ (x_1 : Nat), x_1 < w → 0 < x_1 → x.getMsbD x_1 = false
hmsb : x.msb = true
⊢ x = intMin w

Tactic:
apply eq_of_getMsbD_eq

Result:
case pred
w : Nat
x : BitVec w
hmin : ¬x = intMin w
hzero : ¬x = 0#w
w_pos : 0 < w
getMsbD_x : ∀ (x_1 : Nat), x_1 < w → 0 < x_1 → x.getMsbD x_1 = false
hmsb : x.msb = true
⊢ ∀ (i : Nat), i < w → x.getMsbD i = (intMin w).getMsbD i

Proof state:
case zero
x : BitVec 0
hmin : ¬x = intMin 0
hzero : ¬0#0 = 0#0
⊢ 0 < 0

Tactic:
contradiction

Result:
no goals

Proof state:
w : Nat
x : BitVec w
hmin : ¬x = intMin w
hzero : ¬x = 0#w
w_pos : 0 < w
getMsbD_x : ∀ (x_1 : Nat), x_1 < w → 0 < x_1 → x.getMsbD x_1 = false
hmsb : x.msb = true
n✝ : Nat
hi : n✝ + 1 < w
⊢ x.getMsbD (n✝ + 1) = decide (n✝ + 1 = 0)

Tactic:
exact getMsbD_x _ hi (by omega)

Result:
no goals

Proof state:
case succ
n✝ : Nat
x : BitVec (n✝ + 1)
hmin : ¬x = intMin (n✝ + 1)
hzero : ¬x = 0#(n✝ + 1)
⊢ 0 < n✝ + 1

Tactic:
omega

Result:
no goals

Proof state:
w : Nat
x : BitVec w
hmin : ¬x = intMin w
hzero : ¬x = 0#w
w_pos : 0 < w
getMsbD_x : ∀ (x_1 : Nat), x_1 < w → 0 < x_1 → x.getMsbD x_1 = false
hmsb : x.msb = true
⊢ False

Tactic:
apply hmin

Result:
w : Nat
x : BitVec w
hmin : ¬x = intMin w
hzero : ¬x = 0#w
w_pos : 0 < w
getMsbD_x : ∀ (x_1 : Nat), x_1 < w → 0 < x_1 → x.getMsbD x_1 = false
hmsb : x.msb = true
⊢ x = intMin w

Proof state:
case pred
w : Nat
x : BitVec w
hmin : ¬x = intMin w
hzero : ¬x = 0#w
w_pos : 0 < w
getMsbD_x : ∀ (x_1 : Nat), x_1 < w → 0 < x_1 → x.getMsbD x_1 = false
hmsb : x.msb = true
i : Nat
hi : i < w
⊢ x.getMsbD i = (intMin w).getMsbD i

Tactic:
simp only [getMsbD_intMin, w_pos, decide_true, Bool.true_and]

Result:
case pred
w : Nat
x : BitVec w
hmin : ¬x = intMin w
hzero : ¬x = 0#w
w_pos : 0 < w
getMsbD_x : ∀ (x_1 : Nat), x_1 < w → 0 < x_1 → x.getMsbD x_1 = false
hmsb : x.msb = true
i : Nat
hi : i < w
⊢ x.getMsbD i = decide (i = 0)

Proof state:
case pred.zero
w : Nat
x : BitVec w
hmin : ¬x = intMin w
hzero : ¬x = 0#w
w_pos : 0 < w
getMsbD_x : ∀ (x_1 : Nat), x_1 < w → 0 < x_1 → x.getMsbD x_1 = false
hmsb : x.msb = false
hi : 0 < w
⊢ x.getMsbD 0 = false

case pred.succ
w : Nat
x : BitVec w
hmin : ¬x = intMin w
hzero : ¬x = 0#w
w_pos : 0 < w
getMsbD_x : ∀ (x_1 : Nat), x_1 < w → 0 < x_1 → x.getMsbD x_1 = false
hmsb : x.msb = false
n✝ : Nat
hi : n✝ + 1 < w
⊢ x.getMsbD (n✝ + 1) = false

Tactic:
case zero => exact hmsb

Result:
case pred.succ
w : Nat
x : BitVec w
hmin : ¬x = intMin w
hzero : ¬x = 0#w
w_pos : 0 < w
getMsbD_x : ∀ (x_1 : Nat), x_1 < w → 0 < x_1 → x.getMsbD x_1 = false
hmsb : x.msb = false
n✝ : Nat
hi : n✝ + 1 < w
⊢ x.getMsbD (n✝ + 1) = false

Proof state:
case h
w : Nat
x : BitVec w
hmin : ¬x = intMin w
hzero : ¬x = 0#w
w_pos : 0 < w
a✝ : ¬∃ j, j < w ∧ 0 < j ∧ x.getMsbD j = true
⊢ False

Tactic:
rename_i getMsbD_x

Result:
case h
w : Nat
x : BitVec w
hmin : ¬x = intMin w
hzero : ¬x = 0#w
w_pos : 0 < w
getMsbD_x : ¬∃ j, j < w ∧ 0 < j ∧ x.getMsbD j = true
⊢ False

Proof state:
w : Nat
x : BitVec w
hmin : ¬x = intMin w
hzero : ¬x = 0#w
w_pos : 0 < w
this : ∃ j, j < w ∧ 0 < j ∧ x.getMsbD j = true
⊢ (x != intMin w) = true

Tactic:
simpa

Result:
no goals

Proof state:
case h
w : Nat
x : BitVec w
hmin : ¬x = intMin w
hzero : ¬x = 0#w
w_pos : 0 < w
getMsbD_x : ¬∃ j, j < w ∧ 0 < j ∧ x.getMsbD j = true
⊢ False

Tactic:
simp only [not_exists, _root_.not_and, not_eq_true] at getMsbD_x

Result:
case h
w : Nat
x : BitVec w
hmin : ¬x = intMin w
hzero : ¬x = 0#w
w_pos : 0 < w
getMsbD_x : ∀ (x_1 : Nat), x_1 < w → 0 < x_1 → x.getMsbD x_1 = false
⊢ False

Proof state:
case pred.succ
w : Nat
x : BitVec w
hmin : ¬x = intMin w
hzero : ¬x = 0#w
w_pos : 0 < w
getMsbD_x : ∀ (x_1 : Nat), x_1 < w → 0 < x_1 → x.getMsbD x_1 = false
hmsb : x.msb = false
n✝ : Nat
hi : n✝ + 1 < w
⊢ x.getMsbD (n✝ + 1) = false

Tactic:
case succ => exact getMsbD_x _ hi (by omega)

Result:
no goals

Proof state:
case h
w : Nat
x : BitVec w
hmin : ¬x = intMin w
hzero : ¬x = 0#w
w_pos : 0 < w
getMsbD_x : ∀ (x_1 : Nat), x_1 < w → 0 < x_1 → x.getMsbD x_1 = false
⊢ False

Tactic:
cases hmsb : x.msb

Result:
case h.false
w : Nat
x : BitVec w
hmin : ¬x = intMin w
hzero : ¬x = 0#w
w_pos : 0 < w
getMsbD_x : ∀ (x_1 : Nat), x_1 < w → 0 < x_1 → x.getMsbD x_1 = false
hmsb : x.msb = false
⊢ False

case h.true
w : Nat
x : BitVec w
hmin : ¬x = intMin w
hzero : ¬x = 0#w
w_pos : 0 < w
getMsbD_x : ∀ (x_1 : Nat), x_1 < w → 0 < x_1 → x.getMsbD x_1 = false
hmsb : x.msb = true
⊢ False

Proof state:
w : Nat
x : BitVec w
hmin : ¬x = intMin w
hzero : ¬x = 0#w
w_pos : 0 < w
this : ∃ j, j < w ∧ 0 < j ∧ x.getMsbD j = true
⊢ (x != 0#w) = true

Tactic:
simpa

Result:
no goals