-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/BitVec/Bitblast.lean
theorem sshiftRightRec_eq (x : BitVec w₁) (y : BitVec w₂) (n : Nat) :
    sshiftRightRec x y n = x.sshiftRight' ((y.setWidth (n + 1)).setWidth w₂)

Proof state:
w₁ w₂ n : Nat
ih : ∀ (x : BitVec w₁) (y : BitVec w₂), x.sshiftRightRec y n = x.sshiftRight' (setWidth w₂ (setWidth (n + 1) y))
x : BitVec w₁
y : BitVec w₂
h : ¬y.getLsbD (n + 1) = true
⊢ y.getLsbD (n + 1) = false

Tactic:
simp [h]

Result:
no goals

Proof state:
w₁ w₂ : Nat
x : BitVec w₁
y : BitVec w₂
⊢ x.sshiftRightRec y 0 = x.sshiftRight' (setWidth w₂ (setWidth (0 + 1) y))

Tactic:
ext i

Result:
case pred
w₁ w₂ : Nat
x : BitVec w₁
y : BitVec w₂
i : Nat
a✝ : i < w₁
⊢ (x.sshiftRightRec y 0).getLsbD i = (x.sshiftRight' (setWidth w₂ (setWidth (0 + 1) y))).getLsbD i

Proof state:
case zero
w₁ w₂ : Nat
x : BitVec w₁
y : BitVec w₂
⊢ x.sshiftRightRec y 0 = x.sshiftRight' (setWidth w₂ (setWidth (0 + 1) y))

case succ
w₁ w₂ n✝ : Nat
a✝ : ∀ (x : BitVec w₁) (y : BitVec w₂), x.sshiftRightRec y n✝ = x.sshiftRight' (setWidth w₂ (setWidth (n✝ + 1) y))
x : BitVec w₁
y : BitVec w₂
⊢ x.sshiftRightRec y (n✝ + 1) = x.sshiftRight' (setWidth w₂ (setWidth (n✝ + 1 + 1) y))

Tactic:
case zero =>
  ext i
  simp [twoPow_zero, Nat.reduceAdd, and_one_eq_setWidth_ofBool_getLsbD, setWidth_one]

Result:
case succ
w₁ w₂ n✝ : Nat
a✝ : ∀ (x : BitVec w₁) (y : BitVec w₂), x.sshiftRightRec y n✝ = x.sshiftRight' (setWidth w₂ (setWidth (n✝ + 1) y))
x : BitVec w₁
y : BitVec w₂
⊢ x.sshiftRightRec y (n✝ + 1) = x.sshiftRight' (setWidth w₂ (setWidth (n✝ + 1 + 1) y))

Proof state:
w₁ w₂ n : Nat
ih : ∀ (x : BitVec w₁) (y : BitVec w₂), x.sshiftRightRec y n = x.sshiftRight' (setWidth w₂ (setWidth (n + 1) y))
x : BitVec w₁
y : BitVec w₂
⊢ x.sshiftRightRec y (n + 1) = x.sshiftRight' (setWidth w₂ (setWidth (n + 1 + 1) y))

Tactic:
simp only [sshiftRightRec_succ_eq, and_twoPow, ih]

Result:
w₁ w₂ n : Nat
ih : ∀ (x : BitVec w₁) (y : BitVec w₂), x.sshiftRightRec y n = x.sshiftRight' (setWidth w₂ (setWidth (n + 1) y))
x : BitVec w₁
y : BitVec w₂
⊢ (x.sshiftRight' (setWidth w₂ (setWidth (n + 1) y))).sshiftRight'
      (if y.getLsbD (n + 1) = true then twoPow w₂ (n + 1) else 0#w₂) =
    x.sshiftRight' (setWidth w₂ (setWidth (n + 1 + 1) y))

Proof state:
w₁ w₂ : Nat
x : BitVec w₁
y : BitVec w₂
n : Nat
⊢ x.sshiftRightRec y n = x.sshiftRight' (setWidth w₂ (setWidth (n + 1) y))

Tactic:
induction n generalizing x y

Result:
case zero
w₁ w₂ : Nat
x : BitVec w₁
y : BitVec w₂
⊢ x.sshiftRightRec y 0 = x.sshiftRight' (setWidth w₂ (setWidth (0 + 1) y))

case succ
w₁ w₂ n✝ : Nat
a✝ : ∀ (x : BitVec w₁) (y : BitVec w₂), x.sshiftRightRec y n✝ = x.sshiftRight' (setWidth w₂ (setWidth (n✝ + 1) y))
x : BitVec w₁
y : BitVec w₂
⊢ x.sshiftRightRec y (n✝ + 1) = x.sshiftRight' (setWidth w₂ (setWidth (n✝ + 1 + 1) y))

Proof state:
case pos
w₁ w₂ n : Nat
ih : ∀ (x : BitVec w₁) (y : BitVec w₂), x.sshiftRightRec y n = x.sshiftRight' (setWidth w₂ (setWidth (n + 1) y))
x : BitVec w₁
y : BitVec w₂
h : y.getLsbD (n + 1) = true
⊢ (x.sshiftRight' (setWidth w₂ (setWidth (n + 1) y))).sshiftRight' (if true = true then twoPow w₂ (n + 1) else 0#w₂) =
    (x.sshiftRight' (setWidth w₂ (setWidth (n + 1) y))).sshiftRight' (twoPow w₂ (n + 1))

Tactic:
simp

Result:
no goals

Proof state:
case pred
w₁ w₂ : Nat
x : BitVec w₁
y : BitVec w₂
i : Nat
a✝ : i < w₁
⊢ (x.sshiftRightRec y 0).getLsbD i = (x.sshiftRight' (setWidth w₂ (setWidth (0 + 1) y))).getLsbD i

Tactic:
simp [twoPow_zero, Nat.reduceAdd, and_one_eq_setWidth_ofBool_getLsbD, setWidth_one]

Result:
no goals

Proof state:
w₁ w₂ n : Nat
ih : ∀ (x : BitVec w₁) (y : BitVec w₂), x.sshiftRightRec y n = x.sshiftRight' (setWidth w₂ (setWidth (n + 1) y))
x : BitVec w₁
y : BitVec w₂
⊢ (x.sshiftRight' (setWidth w₂ (setWidth (n + 1) y))).sshiftRight'
      (if y.getLsbD (n + 1) = true then twoPow w₂ (n + 1) else 0#w₂) =
    x.sshiftRight' (setWidth w₂ (setWidth (n + 1 + 1) y))

Tactic:
by_cases h : y.getLsbD (n + 1)

Result:
case pos
w₁ w₂ n : Nat
ih : ∀ (x : BitVec w₁) (y : BitVec w₂), x.sshiftRightRec y n = x.sshiftRight' (setWidth w₂ (setWidth (n + 1) y))
x : BitVec w₁
y : BitVec w₂
h : y.getLsbD (n + 1) = true
⊢ (x.sshiftRight' (setWidth w₂ (setWidth (n + 1) y))).sshiftRight'
      (if y.getLsbD (n + 1) = true then twoPow w₂ (n + 1) else 0#w₂) =
    x.sshiftRight' (setWidth w₂ (setWidth (n + 1 + 1) y))

case neg
w₁ w₂ n : Nat
ih : ∀ (x : BitVec w₁) (y : BitVec w₂), x.sshiftRightRec y n = x.sshiftRight' (setWidth w₂ (setWidth (n + 1) y))
x : BitVec w₁
y : BitVec w₂
h : ¬y.getLsbD (n + 1) = true
⊢ (x.sshiftRight' (setWidth w₂ (setWidth (n + 1) y))).sshiftRight'
      (if y.getLsbD (n + 1) = true then twoPow w₂ (n + 1) else 0#w₂) =
    x.sshiftRight' (setWidth w₂ (setWidth (n + 1 + 1) y))

Proof state:
w₁ w₂ n : Nat
ih : ∀ (x : BitVec w₁) (y : BitVec w₂), x.sshiftRightRec y n = x.sshiftRight' (setWidth w₂ (setWidth (n + 1) y))
x : BitVec w₁
y : BitVec w₂
h : y.getLsbD (n + 1) = true
⊢ setWidth w₂ (setWidth (n + 1) y) &&& twoPow w₂ (n + 1) = 0#w₂

Tactic:
simp [and_twoPow]

Result:
no goals

Proof state:
case neg
w₁ w₂ n : Nat
ih : ∀ (x : BitVec w₁) (y : BitVec w₂), x.sshiftRightRec y n = x.sshiftRight' (setWidth w₂ (setWidth (n + 1) y))
x : BitVec w₁
y : BitVec w₂
h : ¬y.getLsbD (n + 1) = true
⊢ (x.sshiftRight' (setWidth w₂ (setWidth (n + 1) y))).sshiftRight'
      (if y.getLsbD (n + 1) = true then twoPow w₂ (n + 1) else 0#w₂) =
    x.sshiftRight' (setWidth w₂ (setWidth (n + 1) y))

Tactic:
simp [h]

Result:
no goals

Proof state:
case pos
w₁ w₂ n : Nat
ih : ∀ (x : BitVec w₁) (y : BitVec w₂), x.sshiftRightRec y n = x.sshiftRight' (setWidth w₂ (setWidth (n + 1) y))
x : BitVec w₁
y : BitVec w₂
h : y.getLsbD (n + 1) = true
⊢ (x.sshiftRight' (setWidth w₂ (setWidth (n + 1) y))).sshiftRight'
      (if y.getLsbD (n + 1) = true then twoPow w₂ (n + 1) else 0#w₂) =
    x.sshiftRight' (setWidth w₂ (setWidth (n + 1 + 1) y))

Tactic:
rw [setWidth_setWidth_succ_eq_setWidth_setWidth_or_twoPow_of_getLsbD_true h,
  sshiftRight'_or_of_and_eq_zero (by simp [and_twoPow]), h]

Result:
case pos
w₁ w₂ n : Nat
ih : ∀ (x : BitVec w₁) (y : BitVec w₂), x.sshiftRightRec y n = x.sshiftRight' (setWidth w₂ (setWidth (n + 1) y))
x : BitVec w₁
y : BitVec w₂
h : y.getLsbD (n + 1) = true
⊢ (x.sshiftRight' (setWidth w₂ (setWidth (n + 1) y))).sshiftRight' (if true = true then twoPow w₂ (n + 1) else 0#w₂) =
    (x.sshiftRight' (setWidth w₂ (setWidth (n + 1) y))).sshiftRight' (twoPow w₂ (n + 1))

Proof state:
case neg
w₁ w₂ n : Nat
ih : ∀ (x : BitVec w₁) (y : BitVec w₂), x.sshiftRightRec y n = x.sshiftRight' (setWidth w₂ (setWidth (n + 1) y))
x : BitVec w₁
y : BitVec w₂
h : ¬y.getLsbD (n + 1) = true
⊢ (x.sshiftRight' (setWidth w₂ (setWidth (n + 1) y))).sshiftRight'
      (if y.getLsbD (n + 1) = true then twoPow w₂ (n + 1) else 0#w₂) =
    x.sshiftRight' (setWidth w₂ (setWidth (n + 1 + 1) y))

Tactic:
rw [setWidth_setWidth_succ_eq_setWidth_setWidth_of_getLsbD_false (i := n + 1)
  (by simp [h])]

Result:
case neg
w₁ w₂ n : Nat
ih : ∀ (x : BitVec w₁) (y : BitVec w₂), x.sshiftRightRec y n = x.sshiftRight' (setWidth w₂ (setWidth (n + 1) y))
x : BitVec w₁
y : BitVec w₂
h : ¬y.getLsbD (n + 1) = true
⊢ (x.sshiftRight' (setWidth w₂ (setWidth (n + 1) y))).sshiftRight'
      (if y.getLsbD (n + 1) = true then twoPow w₂ (n + 1) else 0#w₂) =
    x.sshiftRight' (setWidth w₂ (setWidth (n + 1) y))