-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/BitVec/Lemmas.lean
theorem msb_udiv (x y : BitVec w) :
    (x / y).msb = (x.msb && y == 1#w)

Proof state:
w : Nat
x y✝ : BitVec (w + 1)
msb_x : x.msb = true
this : (y✝ == 1#(w + 1)) = decide (y✝.toNat = 1)
y : Nat
hy : y✝.toNat = y.succ.succ
⊢ 0 < 2

Tactic:
omega

Result:
no goals

Proof state:
w : Nat
x y✝ : BitVec (w + 1)
msb_x : x.msb = true
this✝ : (y✝ == 1#(w + 1)) = decide (y✝.toNat = 1)
y : Nat
hy : y✝.toNat = y.succ.succ
this : x.toNat / (y + 2) < 2 ^ w
⊢ (x / y✝).msb = decide (y + 2 = 1)

Tactic:
simp_all [msb_eq_decide, hy]

Result:
no goals

Proof state:
w : Nat
x y : BitVec w
msb_x : x.msb = false
this : x.toNat / y.toNat < 2 ^ (w - 1)
⊢ (x / y).msb = (false && y == 1#w)

Tactic:
simpa [msb_eq_decide]

Result:
no goals

Proof state:
w : Nat
x y : BitVec (w + 1)
msb_x : x.msb = true
this : (y == 1#(w + 1)) = decide (y.toNat = 1)
hy : y.toNat = 1
⊢ y.toNat = (1#(w + 1)).toNat

Tactic:
simp [hy]

Result:
no goals

Proof state:
w : Nat
x y : BitVec w
⊢ (x / y).msb = (x.msb && y == 1#w)

Tactic:
cases msb_x : x.msb

Result:
case false
w : Nat
x y : BitVec w
msb_x : x.msb = false
⊢ (x / y).msb = (false && y == 1#w)

case true
w : Nat
x y : BitVec w
msb_x : x.msb = true
⊢ (x / y).msb = (true && y == 1#w)

Proof state:
case true.zero
x y : BitVec 0
msb_x : x.msb = true
⊢ (x / y).msb = (true && y == 1#0)

Tactic:
contradiction

Result:
no goals

Proof state:
case true.succ
w : Nat
x y : BitVec (w + 1)
msb_x : x.msb = true
this : (y == 1#(w + 1)) = decide (y.toNat = 1)
⊢ (x / y).msb = (true && y == 1#(w + 1))

Tactic:
simp only [this, Bool.true_and]

Result:
case true.succ
w : Nat
x y : BitVec (w + 1)
msb_x : x.msb = true
this : (y == 1#(w + 1)) = decide (y.toNat = 1)
⊢ (x / y).msb = decide (y.toNat = 1)

Proof state:
w : Nat
x : BitVec (w + 1)
msb_x : x.msb = true
this : (1#(w + 1) == 1#(w + 1)) = decide ((1#(w + 1)).toNat = 1)
hy : (1#(w + 1)).toNat = 1
⊢ (x / 1#(w + 1)).msb = decide (1 = 1)

Tactic:
simpa using msb_x

Result:
no goals

Proof state:
w : Nat
x y✝ : BitVec (w + 1)
msb_x : x.msb = true
this : (y✝ == 1#(w + 1)) = decide (y✝.toNat = 1)
y : Nat
hy : y✝.toNat = y.succ.succ
⊢ x.toNat / 2 < 2 ^ w

Tactic:
omega

Result:
no goals

Proof state:
w : Nat
x y✝ : BitVec (w + 1)
msb_x : x.msb = true
this : (y✝ == 1#(w + 1)) = decide (y✝.toNat = 1)
y : Nat
hy : y✝.toNat = y.succ.succ
⊢ x.toNat / (y + 2) < 2 ^ w

Tactic:
calc
  x.toNat / (y + 2)
    ≤ x.toNat / 2 := by apply Nat.div_add_le_right (by omega)
  _ < 2 ^ w       := by omega

Result:
no goals

Proof state:
w : Nat
x y : BitVec w
msb_x : x.msb = false
⊢ x.toNat / y.toNat ≤ x.toNat

Tactic:
apply Nat.div_le_self

Result:
no goals

Proof state:
w : Nat
x y : BitVec (w + 1)
msb_x : x.msb = true
this : (y == 1#(w + 1)) = decide (y.toNat = 1)
hy : y.toNat = 1
⊢ (x / y).msb = decide (1 = 1)

Tactic:
obtain rfl : y = 1#_ := eq_of_toNat_eq (by simp [hy])

Result:
w : Nat
x : BitVec (w + 1)
msb_x : x.msb = true
this : (1#(w + 1) == 1#(w + 1)) = decide ((1#(w + 1)).toNat = 1)
hy : (1#(w + 1)).toNat = 1
⊢ (x / 1#(w + 1)).msb = decide (1 = 1)

Proof state:
w : Nat
x y✝ : BitVec (w + 1)
msb_x : x.msb = true
this : (y✝ == 1#(w + 1)) = decide (y✝.toNat = 1)
y : Nat
hy : y✝.toNat = y.succ.succ
⊢ (x / y✝).msb = decide (y + 2 = 1)

Tactic:
suffices x.toNat / (y + 2) < 2 ^ w by
  simp_all [msb_eq_decide, hy]

Result:
w : Nat
x y✝ : BitVec (w + 1)
msb_x : x.msb = true
this : (y✝ == 1#(w + 1)) = decide (y✝.toNat = 1)
y : Nat
hy : y✝.toNat = y.succ.succ
⊢ x.toNat / (y + 2) < 2 ^ w

Proof state:
case false
w : Nat
x y : BitVec w
msb_x : x.msb = false
⊢ (x / y).msb = (false && y == 1#w)

Tactic:
suffices x.toNat / y.toNat < 2 ^ (w - 1) by simpa [msb_eq_decide]

Result:
case false
w : Nat
x y : BitVec w
msb_x : x.msb = false
⊢ x.toNat / y.toNat < 2 ^ (w - 1)

Proof state:
case false
w : Nat
x y : BitVec w
msb_x : x.msb = false
⊢ x.toNat / y.toNat < 2 ^ (w - 1)

Tactic:
calc
  x.toNat / y.toNat ≤ x.toNat     := by apply Nat.div_le_self
                  _ < 2 ^ (w - 1) := by simpa [msb_eq_decide] using msb_x

Result:
no goals

Proof state:
w : Nat
x y : BitVec (w + 1)
msb_x : x.msb = true
this : (y == 1#(w + 1)) = decide (y.toNat = 1)
hy : y.toNat = 0
⊢ (x / y).msb = decide (0 = 1)

Tactic:
obtain rfl : y = 0#_ := eq_of_toNat_eq hy

Result:
w : Nat
x : BitVec (w + 1)
msb_x : x.msb = true
this : (0#(w + 1) == 1#(w + 1)) = decide ((0#(w + 1)).toNat = 1)
hy : (0#(w + 1)).toNat = 0
⊢ (x / 0#(w + 1)).msb = decide (0 = 1)

Proof state:
w : Nat
x y✝ : BitVec (w + 1)
msb_x : x.msb = true
this : (y✝ == 1#(w + 1)) = decide (y✝.toNat = 1)
y : Nat
hy : y✝.toNat = y.succ.succ
⊢ x.toNat / (y + 2) ≤ x.toNat / 2

Tactic:
apply Nat.div_add_le_right (by omega)

Result:
no goals

Proof state:
w : Nat
x : BitVec (w + 1)
msb_x : x.msb = true
this : (0#(w + 1) == 1#(w + 1)) = decide ((0#(w + 1)).toNat = 1)
hy : (0#(w + 1)).toNat = 0
⊢ (x / 0#(w + 1)).msb = decide (0 = 1)

Tactic:
simp

Result:
no goals

Proof state:
w : Nat
x y : BitVec w
msb_x : x.msb = false
⊢ x.toNat < 2 ^ (w - 1)

Tactic:
simpa [msb_eq_decide] using msb_x

Result:
no goals

Proof state:
case true
w : Nat
x y : BitVec w
msb_x : x.msb = true
⊢ (x / y).msb = (true && y == 1#w)

Tactic:
rcases w with _|w

Result:
case true.zero
x y : BitVec 0
msb_x : x.msb = true
⊢ (x / y).msb = (true && y == 1#0)

case true.succ
w : Nat
x y : BitVec (w + 1)
msb_x : x.msb = true
⊢ (x / y).msb = (true && y == 1#(w + 1))

Proof state:
case true.succ
w : Nat
x y : BitVec (w + 1)
msb_x : x.msb = true
this : (y == 1#(w + 1)) = decide (y.toNat = 1)
⊢ (x / y).msb = decide (y.toNat = 1)

Tactic:
match hy : y.toNat with
| 0 =>
  obtain rfl : y = 0#_ := eq_of_toNat_eq hy
  simp
| 1 =>
  obtain rfl : y = 1#_ := eq_of_toNat_eq (by simp [hy])
  simpa using msb_x
| y + 2 =>
  suffices x.toNat / (y + 2) < 2 ^ w by
    simp_all [msb_eq_decide, hy]
  calc
    x.toNat / (y + 2)
      ≤ x.toNat / 2 := by apply Nat.div_add_le_right (by omega)
    _ < 2 ^ w       := by omega

Result:
no goals