-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/BitVec/Lemmas.lean
theorem toNat_signExtend_of_le (x : BitVec w) {v : Nat} (hv : w ≤ v) :
    (x.signExtend v).toNat = x.toNat + if x.msb then 2^v - 2^w else 0

Proof state:
case pos
w : Nat
x : BitVec w
v : Nat
hv : w ≤ v
i k : Nat
hk : v = w + k
hx : x.msb = true
⊢ (decide (i < w + k) && (!decide (i < w) || x.getLsbD i)) = if i < w then x.getLsbD i else decide (i - w < k)

Tactic:
have hi : i < w ∨ (w ≤ i ∧ i < w + k) ∨ w + k ≤ i := by omega

Result:
case pos
w : Nat
x : BitVec w
v : Nat
hv : w ≤ v
i k : Nat
hk : v = w + k
hx : x.msb = true
hi : i < w ∨ w ≤ i ∧ i < w + k ∨ w + k ≤ i
⊢ (decide (i < w + k) && (!decide (i < w) || x.getLsbD i)) = if i < w then x.getLsbD i else decide (i - w < k)

Proof state:
w : Nat
x : BitVec w
v : Nat
hv : w ≤ v
i k : Nat
hk : v = w + k
hx : ¬x.msb = true
⊢ i < w ∨ w ≤ i ∧ i < w + k ∨ w + k ≤ i

Tactic:
omega

Result:
no goals

Proof state:
w : Nat
x : BitVec w
v : Nat
hv : w ≤ v
i k : Nat
hk : v = w + k
hx : x.msb = true
hi : w + k ≤ i
⊢ ¬i < w

Tactic:
omega

Result:
no goals

Proof state:
case pred
w : Nat
x : BitVec w
v : Nat
hv : w ≤ v
i k : Nat
hk : v = w + k
⊢ (signExtend v x).toNat.testBit i = (x.toNat + if x.msb = true then 2 ^ v - 2 ^ w else 0).testBit i

Tactic:
rw [hk, testBit_toNat, getLsbD_signExtend, Nat.pow_add, ← Nat.mul_sub_one, Nat.add_comm (x.toNat)]

Result:
case pred
w : Nat
x : BitVec w
v : Nat
hv : w ≤ v
i k : Nat
hk : v = w + k
⊢ (decide (i < w + k) && if i < w then x.getLsbD i else x.msb) =
    ((if x.msb = true then 2 ^ w * (2 ^ k - 1) else 0) + x.toNat).testBit i

Proof state:
case pos
w : Nat
x : BitVec w
v : Nat
hv : w ≤ v
i k : Nat
hk : v = w + k
hx : x.msb = true
⊢ (decide (i < w + k) && if i < w then x.getLsbD i else x.msb) =
    ((if x.msb = true then 2 ^ w * (2 ^ k - 1) else 0) + x.toNat).testBit i

Tactic:
simp only [hx, Bool.if_true_right, ↓reduceIte,
  Nat.testBit_mul_pow_two_add _ x.isLt,
  testBit_toNat, Nat.testBit_two_pow_sub_one]

Result:
case pos
w : Nat
x : BitVec w
v : Nat
hv : w ≤ v
i k : Nat
hk : v = w + k
hx : x.msb = true
⊢ (decide (i < w + k) && (!decide (i < w) || x.getLsbD i)) = if i < w then x.getLsbD i else decide (i - w < k)

Proof state:
case pred
w : Nat
x : BitVec w
v : Nat
hv : w ≤ v
i k : Nat
hk : v = w + k
⊢ (decide (i < w + k) && if i < w then x.getLsbD i else x.msb) =
    ((if x.msb = true then 2 ^ w * (2 ^ k - 1) else 0) + x.toNat).testBit i

Tactic:
by_cases hx : x.msb

Result:
case pos
w : Nat
x : BitVec w
v : Nat
hv : w ≤ v
i k : Nat
hk : v = w + k
hx : x.msb = true
⊢ (decide (i < w + k) && if i < w then x.getLsbD i else x.msb) =
    ((if x.msb = true then 2 ^ w * (2 ^ k - 1) else 0) + x.toNat).testBit i

case neg
w : Nat
x : BitVec w
v : Nat
hv : w ≤ v
i k : Nat
hk : v = w + k
hx : ¬x.msb = true
⊢ (decide (i < w + k) && if i < w then x.getLsbD i else x.msb) =
    ((if x.msb = true then 2 ^ w * (2 ^ k - 1) else 0) + x.toNat).testBit i

Proof state:
case pos.inr.inr
w : Nat
x : BitVec w
v : Nat
hv : w ≤ v
i k : Nat
hk : v = w + k
hx : x.msb = true
hi : w + k ≤ i
⊢ k ≤ i - w

Tactic:
omega

Result:
no goals

Proof state:
w : Nat
x : BitVec w
v : Nat
hv : w ≤ v
i k : Nat
hk : v = w + k
hx : ¬x.msb = true
hi : w + k ≤ i
⊢ w ≤ i

Tactic:
omega

Result:
no goals

Proof state:
case neg.inl
w : Nat
x : BitVec w
v : Nat
hv : w ≤ v
i k : Nat
hk : v = w + k
hx : ¬x.msb = true
hi : i < w
⊢ (decide (i < w + k) && (decide (i < w) && x.getLsbD i)) = x.getLsbD i

Tactic:
simp [hi]

Result:
case neg.inl
w : Nat
x : BitVec w
v : Nat
hv : w ≤ v
i k : Nat
hk : v = w + k
hx : ¬x.msb = true
hi : i < w
⊢ x.getLsbD i = true → i < w + k

Proof state:
case neg
w : Nat
x : BitVec w
v : Nat
hv : w ≤ v
i k : Nat
hk : v = w + k
hx : ¬x.msb = true
⊢ (decide (i < w + k) && (decide (i < w) && x.getLsbD i)) = x.getLsbD i

Tactic:
have hi : i < w ∨ (w ≤ i ∧ i < w + k) ∨ w + k ≤ i := by omega

Result:
case neg
w : Nat
x : BitVec w
v : Nat
hv : w ≤ v
i k : Nat
hk : v = w + k
hx : ¬x.msb = true
hi : i < w ∨ w ≤ i ∧ i < w + k ∨ w + k ≤ i
⊢ (decide (i < w + k) && (decide (i < w) && x.getLsbD i)) = x.getLsbD i

Proof state:
case neg.inl
w : Nat
x : BitVec w
v : Nat
hv : w ≤ v
i k : Nat
hk : v = w + k
hx : ¬x.msb = true
hi : i < w
⊢ x.getLsbD i = true → i < w + k

Tactic:
omega

Result:
no goals

Proof state:
w : Nat
x : BitVec w
v : Nat
hv : w ≤ v
i k : Nat
hk : v = w + k
hx : ¬x.msb = true
hi : w + k ≤ i
⊢ ¬i < w

Tactic:
omega

Result:
no goals

Proof state:
w : Nat
x : BitVec w
v : Nat
hv : w ≤ v
i k : Nat
hk : v = w + k
hx : x.msb = true
⊢ i < w ∨ w ≤ i ∧ i < w + k ∨ w + k ≤ i

Tactic:
omega

Result:
no goals

Proof state:
case pos.inl
w : Nat
x : BitVec w
v : Nat
hv : w ≤ v
i k : Nat
hk : v = w + k
hx : x.msb = true
hi : i < w
⊢ (decide (i < w + k) && (!decide (i < w) || x.getLsbD i)) = if i < w then x.getLsbD i else decide (i - w < k)

Tactic:
simp [hi]

Result:
case pos.inl
w : Nat
x : BitVec w
v : Nat
hv : w ≤ v
i k : Nat
hk : v = w + k
hx : x.msb = true
hi : i < w
⊢ x.getLsbD i = true → i < w + k

Proof state:
case pos.inr.inr
w : Nat
x : BitVec w
v : Nat
hv : w ≤ v
i k : Nat
hk : v = w + k
hx : x.msb = true
hi : w + k ≤ i
⊢ (decide (i < w + k) && (!decide (i < w) || x.getLsbD i)) = if i < w then x.getLsbD i else decide (i - w < k)

Tactic:
simp [hi, show ¬ (i < w + k) by omega, show ¬ (i < w) by omega]

Result:
case pos.inr.inr
w : Nat
x : BitVec w
v : Nat
hv : w ≤ v
i k : Nat
hk : v = w + k
hx : x.msb = true
hi : w + k ≤ i
⊢ k ≤ i - w

Proof state:
case pos
w : Nat
x : BitVec w
v : Nat
hv : w ≤ v
i k : Nat
hk : v = w + k
hx : x.msb = true
hi : i < w ∨ w ≤ i ∧ i < w + k ∨ w + k ≤ i
⊢ (decide (i < w + k) && (!decide (i < w) || x.getLsbD i)) = if i < w then x.getLsbD i else decide (i - w < k)

Tactic:
rcases hi with hi | hi | hi

Result:
case pos.inl
w : Nat
x : BitVec w
v : Nat
hv : w ≤ v
i k : Nat
hk : v = w + k
hx : x.msb = true
hi : i < w
⊢ (decide (i < w + k) && (!decide (i < w) || x.getLsbD i)) = if i < w then x.getLsbD i else decide (i - w < k)

case pos.inr.inl
w : Nat
x : BitVec w
v : Nat
hv : w ≤ v
i k : Nat
hk : v = w + k
hx : x.msb = true
hi : w ≤ i ∧ i < w + k
⊢ (decide (i < w + k) && (!decide (i < w) || x.getLsbD i)) = if i < w then x.getLsbD i else decide (i - w < k)

case pos.inr.inr
w : Nat
x : BitVec w
v : Nat
hv : w ≤ v
i k : Nat
hk : v = w + k
hx : x.msb = true
hi : w + k ≤ i
⊢ (decide (i < w + k) && (!decide (i < w) || x.getLsbD i)) = if i < w then x.getLsbD i else decide (i - w < k)

Proof state:
case neg.inr.inr
w : Nat
x : BitVec w
v : Nat
hv : w ≤ v
i k : Nat
hk : v = w + k
hx : ¬x.msb = true
hi : w + k ≤ i
⊢ (decide (i < w + k) && (decide (i < w) && x.getLsbD i)) = x.getLsbD i

Tactic:
simp [hi, show ¬ (i < w + k) by omega, show ¬ (i < w) by omega, getLsbD_ge x i (by omega)]

Result:
no goals

Proof state:
case neg.inr.inl
w : Nat
x : BitVec w
v : Nat
hv : w ≤ v
i k : Nat
hk : v = w + k
hx : ¬x.msb = true
hi : w ≤ i ∧ i < w + k
⊢ (decide (i < w + k) && (decide (i < w) && x.getLsbD i)) = x.getLsbD i

Tactic:
simp [hi]

Result:
no goals

Proof state:
case neg
w : Nat
x : BitVec w
v : Nat
hv : w ≤ v
i k : Nat
hk : v = w + k
hx : ¬x.msb = true
⊢ (decide (i < w + k) && if i < w then x.getLsbD i else x.msb) =
    ((if x.msb = true then 2 ^ w * (2 ^ k - 1) else 0) + x.toNat).testBit i

Tactic:
simp only [hx, Bool.if_false_right,
  Bool.false_eq_true, ↓reduceIte, Nat.zero_add, testBit_toNat]

Result:
case neg
w : Nat
x : BitVec w
v : Nat
hv : w ≤ v
i k : Nat
hk : v = w + k
hx : ¬x.msb = true
⊢ (decide (i < w + k) && (decide (i < w) && x.getLsbD i)) = x.getLsbD i

Proof state:
case pos.inr.inl
w : Nat
x : BitVec w
v : Nat
hv : w ≤ v
i k : Nat
hk : v = w + k
hx : x.msb = true
hi : w ≤ i ∧ i < w + k
⊢ i - w < k

Tactic:
omega

Result:
no goals