-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/BitVec/Lemmas.lean
theorem toInt_ushiftRight_of_lt {x : BitVec w} {n : Nat} (hn : 0 < n) :
    (x >>> n).toInt = x.toNat >>> n

Proof state:
case pos
w : Nat
x : BitVec w
n : Nat
hn✝ : 0 < n
h : 2 ^ w ≤ 2 * x.toNat >>> n
hn : n ≤ w
h1 : x.toNat >>> n < 2 ^ (w - n)
⊢ ↑(x.toNat >>> n) - ↑(2 ^ w) = ↑(x.toNat >>> n)

Tactic:
have : 2 ^ (w - n).succ ≤ 2^ w := Nat.pow_le_pow_of_le (by decide) (by omega)

Result:
case pos
w : Nat
x : BitVec w
n : Nat
hn✝ : 0 < n
h : 2 ^ w ≤ 2 * x.toNat >>> n
hn : n ≤ w
h1 : x.toNat >>> n < 2 ^ (w - n)
this : 2 ^ (w - n).succ ≤ 2 ^ w
⊢ ↑(x.toNat >>> n) - ↑(2 ^ w) = ↑(x.toNat >>> n)

Proof state:
case neg
w : Nat
x : BitVec w
n : Nat
hn✝ : 0 < n
hn : ¬n ≤ w
this : x.toNat >>> n = 0
h : 2 ^ w = 0
⊢ ↑(x.toNat >>> n) - ↑(2 ^ w) = ↑(x.toNat >>> n)

Tactic:
omega

Result:
no goals

Proof state:
case pos
w : Nat
x : BitVec w
n : Nat
hn✝ : 0 < n
h : 2 ^ w ≤ 2 * x.toNat >>> n
hn : n ≤ w
h1 : x.toNat >>> n < 2 ^ (w - n)
this✝ : 2 ^ (w - n).succ ≤ 2 ^ w
this : 2 * x.toNat >>> n < 2 ^ w
⊢ ↑(x.toNat >>> n) - ↑(2 ^ w) = ↑(x.toNat >>> n)

Tactic:
omega

Result:
no goals

Proof state:
w : Nat
x : BitVec w
n : Nat
hn : 0 < n
h : 2 ^ w ≤ 2 * x.toNat >>> n
⊢ ↑(x.toNat >>> n) - ↑(2 ^ w) = ↑(x.toNat >>> n)

Tactic:
by_cases hn : n ≤ w

Result:
case pos
w : Nat
x : BitVec w
n : Nat
hn✝ : 0 < n
h : 2 ^ w ≤ 2 * x.toNat >>> n
hn : n ≤ w
⊢ ↑(x.toNat >>> n) - ↑(2 ^ w) = ↑(x.toNat >>> n)

case neg
w : Nat
x : BitVec w
n : Nat
hn✝ : 0 < n
h : 2 ^ w ≤ 2 * x.toNat >>> n
hn : ¬n ≤ w
⊢ ↑(x.toNat >>> n) - ↑(2 ^ w) = ↑(x.toNat >>> n)

Proof state:
w : Nat
x : BitVec w
n : Nat
hn✝ : 0 < n
h : 2 ^ w ≤ 2 * x.toNat >>> n
hn : n ≤ w
h1 : x.toNat >>> n < 2 ^ (w - n)
⊢ (w - n).succ ≤ w

Tactic:
omega

Result:
no goals

Proof state:
w : Nat
x : BitVec w
n : Nat
hn : 0 < n
⊢ 2 ^ w ≤ 2 * x.toNat >>> n → ↑(x.toNat >>> n) - ↑(2 ^ w) = ↑(x.toNat >>> n)

Tactic:
intros h

Result:
w : Nat
x : BitVec w
n : Nat
hn : 0 < n
h : 2 ^ w ≤ 2 * x.toNat >>> n
⊢ ↑(x.toNat >>> n) - ↑(2 ^ w) = ↑(x.toNat >>> n)

Proof state:
case pos
w : Nat
x : BitVec w
n : Nat
hn✝ : 0 < n
h : 2 ^ w ≤ 2 * x.toNat >>> n
hn : n ≤ w
h1 : x.toNat >>> n < 2 ^ (w - n)
this : 2 ^ (w - n).succ ≤ 2 ^ w
⊢ ↑(x.toNat >>> n) - ↑(2 ^ w) = ↑(x.toNat >>> n)

Tactic:
have := show 2 * x.toNat >>> n < 2 ^ w by
  omega

Result:
case pos
w : Nat
x : BitVec w
n : Nat
hn✝ : 0 < n
h : 2 ^ w ≤ 2 * x.toNat >>> n
hn : n ≤ w
h1 : x.toNat >>> n < 2 ^ (w - n)
this✝ : 2 ^ (w - n).succ ≤ 2 ^ w
this : 2 * x.toNat >>> n < 2 ^ w
⊢ ↑(x.toNat >>> n) - ↑(2 ^ w) = ↑(x.toNat >>> n)

Proof state:
case hn
w : Nat
x : BitVec w
n : Nat
hn✝ : 0 < n
h : 2 ^ w ≤ 2 * x.toNat >>> n
hn : ¬n ≤ w
⊢ x.toNat < 2 ^ n

Tactic:
have : 2^w ≤ 2^n := Nat.pow_le_pow_of_le (by decide) (by omega)

Result:
case hn
w : Nat
x : BitVec w
n : Nat
hn✝ : 0 < n
h : 2 ^ w ≤ 2 * x.toNat >>> n
hn : ¬n ≤ w
this : 2 ^ w ≤ 2 ^ n
⊢ x.toNat < 2 ^ n

Proof state:
w : Nat
x : BitVec w
n : Nat
hn : 0 < n
⊢ (x >>> n).toInt = ↑(x.toNat >>> n)

Tactic:
rw [toInt_eq_toNat_cond]

Result:
w : Nat
x : BitVec w
n : Nat
hn : 0 < n
⊢ (if 2 * (x >>> n).toNat < 2 ^ w then ↑(x >>> n).toNat else ↑(x >>> n).toNat - ↑(2 ^ w)) = ↑(x.toNat >>> n)

Proof state:
case neg
w : Nat
x : BitVec w
n : Nat
hn✝ : 0 < n
h : 2 ^ w ≤ 2 * x.toNat >>> n
hn : ¬n ≤ w
this : x.toNat >>> n = 0
⊢ ↑(x.toNat >>> n) - ↑(2 ^ w) = ↑(x.toNat >>> n)

Tactic:
simp [this] at h

Result:
case neg
w : Nat
x : BitVec w
n : Nat
hn✝ : 0 < n
hn : ¬n ≤ w
this : x.toNat >>> n = 0
h : 2 ^ w = 0
⊢ ↑(x.toNat >>> n) - ↑(2 ^ w) = ↑(x.toNat >>> n)

Proof state:
case neg
w : Nat
x : BitVec w
n : Nat
hn✝ : 0 < n
h : 2 ^ w ≤ 2 * x.toNat >>> n
hn : ¬n ≤ w
⊢ ↑(x.toNat >>> n) - ↑(2 ^ w) = ↑(x.toNat >>> n)

Tactic:
have : x.toNat >>> n = 0 := by
  apply Nat.shiftRight_eq_zero
  have : 2^w ≤ 2^n := Nat.pow_le_pow_of_le (by decide) (by omega)
  omega

Result:
case neg
w : Nat
x : BitVec w
n : Nat
hn✝ : 0 < n
h : 2 ^ w ≤ 2 * x.toNat >>> n
hn : ¬n ≤ w
this : x.toNat >>> n = 0
⊢ ↑(x.toNat >>> n) - ↑(2 ^ w) = ↑(x.toNat >>> n)

Proof state:
w : Nat
x : BitVec w
n : Nat
hn✝ : 0 < n
h : 2 ^ w ≤ 2 * x.toNat >>> n
hn : ¬n ≤ w
⊢ w ≤ n

Tactic:
omega

Result:
no goals

Proof state:
w : Nat
x : BitVec w
n : Nat
hn✝ : 0 < n
h : 2 ^ w ≤ 2 * x.toNat >>> n
hn : ¬n ≤ w
⊢ x.toNat >>> n = 0

Tactic:
apply Nat.shiftRight_eq_zero

Result:
case hn
w : Nat
x : BitVec w
n : Nat
hn✝ : 0 < n
h : 2 ^ w ≤ 2 * x.toNat >>> n
hn : ¬n ≤ w
⊢ x.toNat < 2 ^ n

Proof state:
w : Nat
x : BitVec w
n : Nat
hn✝ : 0 < n
h : 2 ^ w ≤ 2 * x.toNat >>> n
hn : n ≤ w
h1 : x.toNat >>> n < 2 ^ (w - n)
this : 2 ^ (w - n).succ ≤ 2 ^ w
⊢ 2 * x.toNat >>> n < 2 ^ w

Tactic:
omega

Result:
no goals

Proof state:
case pos
w : Nat
x : BitVec w
n : Nat
hn✝ : 0 < n
h : 2 ^ w ≤ 2 * x.toNat >>> n
hn : n ≤ w
⊢ ↑(x.toNat >>> n) - ↑(2 ^ w) = ↑(x.toNat >>> n)

Tactic:
have h1 := Nat.mul_lt_mul_of_pos_left (toNat_ushiftRight_lt x n hn) Nat.two_pos

Result:
case pos
w : Nat
x : BitVec w
n : Nat
hn✝ : 0 < n
h : 2 ^ w ≤ 2 * x.toNat >>> n
hn : n ≤ w
h1 : 2 * (x >>> n).toNat < 2 * 2 ^ (w - n)
⊢ ↑(x.toNat >>> n) - ↑(2 ^ w) = ↑(x.toNat >>> n)

Proof state:
case hn
w : Nat
x : BitVec w
n : Nat
hn✝ : 0 < n
h : 2 ^ w ≤ 2 * x.toNat >>> n
hn : ¬n ≤ w
this : 2 ^ w ≤ 2 ^ n
⊢ x.toNat < 2 ^ n

Tactic:
omega

Result:
no goals

Proof state:
w : Nat
x : BitVec w
n : Nat
hn✝ : 0 < n
h : 2 ^ w ≤ 2 * x.toNat >>> n
hn : n ≤ w
h1 : x.toNat >>> n < 2 ^ (w - n)
⊢ 1 < 2

Tactic:
decide

Result:
no goals

Proof state:
case pos
w : Nat
x : BitVec w
n : Nat
hn✝ : 0 < n
h : 2 ^ w ≤ 2 * x.toNat >>> n
hn : n ≤ w
h1 : 2 * (x >>> n).toNat < 2 * 2 ^ (w - n)
⊢ ↑(x.toNat >>> n) - ↑(2 ^ w) = ↑(x.toNat >>> n)

Tactic:
simp only [toNat_ushiftRight, Nat.zero_lt_succ, Nat.mul_lt_mul_left] at h1

Result:
case pos
w : Nat
x : BitVec w
n : Nat
hn✝ : 0 < n
h : 2 ^ w ≤ 2 * x.toNat >>> n
hn : n ≤ w
h1 : x.toNat >>> n < 2 ^ (w - n)
⊢ ↑(x.toNat >>> n) - ↑(2 ^ w) = ↑(x.toNat >>> n)

Proof state:
w : Nat
x : BitVec w
n : Nat
hn : 0 < n
⊢ (if 2 * (x >>> n).toNat < 2 ^ w then ↑(x >>> n).toNat else ↑(x >>> n).toNat - ↑(2 ^ w)) = ↑(x.toNat >>> n)

Tactic:
simp only [toNat_ushiftRight, ite_eq_left_iff, Nat.not_lt]

Result:
w : Nat
x : BitVec w
n : Nat
hn : 0 < n
⊢ 2 ^ w ≤ 2 * x.toNat >>> n → ↑(x.toNat >>> n) - ↑(2 ^ w) = ↑(x.toNat >>> n)

Proof state:
w : Nat
x : BitVec w
n : Nat
hn✝ : 0 < n
h : 2 ^ w ≤ 2 * x.toNat >>> n
hn : ¬n ≤ w
⊢ 1 < 2

Tactic:
decide

Result:
no goals