-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/BitVec/Lemmas.lean
theorem msb_umod {x y : BitVec w} :
    (x % y).msb = (x.msb && (x < y || y == 0#w))

Proof state:
w : Nat
x y : BitVec w
⊢ (x % y).msb = (x.msb && (decide (x < y) || y == 0#w))

Tactic:
rw [msb_eq_decide, toNat_umod]

Result:
w : Nat
x y : BitVec w
⊢ decide (2 ^ (w - 1) ≤ x.toNat % y.toNat) = (x.msb && (decide (x < y) || y == 0#w))

Proof state:
case neg
w : Nat
x y : BitVec w
msb_x : x.msb = true
x_lt_y : ¬x < y
y_le_x : y.toNat ≤ x.toNat
hy : y.toNat ≠ 0
⊢ x.toNat % y.toNat < 2 ^ (w - 1)

Tactic:
by_cases msb_y : y.toNat < 2 ^ (w - 1)

Result:
case pos
w : Nat
x y : BitVec w
msb_x : x.msb = true
x_lt_y : ¬x < y
y_le_x : y.toNat ≤ x.toNat
hy : y.toNat ≠ 0
msb_y : y.toNat < 2 ^ (w - 1)
⊢ x.toNat % y.toNat < 2 ^ (w - 1)

case neg
w : Nat
x y : BitVec w
msb_x : x.msb = true
x_lt_y : ¬x < y
y_le_x : y.toNat ≤ x.toNat
hy : y.toNat ≠ 0
msb_y : ¬y.toNat < 2 ^ (w - 1)
⊢ x.toNat % y.toNat < 2 ^ (w - 1)

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

Tactic:
simpa

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.mod_le

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:
w : Nat
x y : BitVec w
msb_x : x.msb = true
x_lt_y : ¬x < y
y_le_x : y.toNat ≤ x.toNat
hy : y.toNat ≠ 0
msb_y : y.toNat < 2 ^ (w - 1)
⊢ y.toNat > 0

Tactic:
omega

Result:
no goals

Proof state:
case true
w : Nat
x y : BitVec w
msb_x : x.msb = true
⊢ decide (2 ^ (w - 1) ≤ x.toNat % y.toNat) = (true && (decide (x < y) || y == 0#w))

Tactic:
by_cases hy : y = 0

Result:
case pos
w : Nat
x y : BitVec w
msb_x : x.msb = true
hy : y = 0
⊢ decide (2 ^ (w - 1) ≤ x.toNat % y.toNat) = (true && (decide (x < y) || y == 0#w))

case neg
w : Nat
x y : BitVec w
msb_x : x.msb = true
hy : ¬y = 0
⊢ decide (2 ^ (w - 1) ≤ x.toNat % y.toNat) = (true && (decide (x < y) || y == 0#w))

Proof state:
case neg
w : Nat
x y : BitVec w
msb_x : x.msb = true
hy : ¬y = 0
⊢ 2 ^ (w - 1) ≤ x.toNat % y.toNat ↔ x < y

Tactic:
by_cases x_lt_y : x < y

Result:
case pos
w : Nat
x y : BitVec w
msb_x : x.msb = true
hy : ¬y = 0
x_lt_y : x < y
⊢ 2 ^ (w - 1) ≤ x.toNat % y.toNat ↔ x < y

case neg
w : Nat
x y : BitVec w
msb_x : x.msb = true
hy : ¬y = 0
x_lt_y : ¬x < y
⊢ 2 ^ (w - 1) ≤ x.toNat % y.toNat ↔ x < y

Proof state:
case pos
w : Nat
x y : BitVec w
msb_x : x.msb = true
hy : y = 0
⊢ decide (2 ^ (w - 1) ≤ x.toNat % y.toNat) = (true && (decide (x < y) || y == 0#w))

Tactic:
simp_all [msb_eq_decide]

Result:
no goals

Proof state:
case neg
w : Nat
x y : BitVec w
msb_x : x.msb = true
hy : ¬y = 0
⊢ decide (2 ^ (w - 1) ≤ x.toNat % y.toNat) = (true && (decide (x < y) || y == 0#w))

Tactic:
suffices 2 ^ (w - 1) ≤ x.toNat % y.toNat ↔ x < y by simp_all

Result:
case neg
w : Nat
x y : BitVec w
msb_x : x.msb = true
hy : ¬y = 0
⊢ 2 ^ (w - 1) ≤ x.toNat % y.toNat ↔ x < y

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.mod_le
                  _ < 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
x_lt_y : ¬x < y
y_le_x : y.toNat ≤ x.toNat
hy : y.toNat ≠ 0
msb_y : 2 ^ w ≤ y.toNat
this : y.toNat ≤ y.toNat * (x.toNat / y.toNat)
⊢ x.toNat % y.toNat ≤ x.toNat - y.toNat

Tactic:
rw [Nat.mod_eq_sub]

Result:
w : Nat
x y : BitVec (w + 1)
msb_x : x.msb = true
x_lt_y : ¬x < y
y_le_x : y.toNat ≤ x.toNat
hy : y.toNat ≠ 0
msb_y : 2 ^ w ≤ y.toNat
this : y.toNat ≤ y.toNat * (x.toNat / y.toNat)
⊢ x.toNat - y.toNat * (x.toNat / y.toNat) ≤ x.toNat - y.toNat

Proof state:
w : Nat
x y : BitVec (w + 1)
msb_x : x.msb = true
x_lt_y : ¬x < y
y_le_x : y.toNat ≤ x.toNat
hy : y.toNat ≠ 0
msb_y : 2 ^ w ≤ y.toNat
⊢ y.toNat ≤ y.toNat * (x.toNat / y.toNat)

Tactic:
apply Nat.le_mul_of_pos_right

Result:
case h
w : Nat
x y : BitVec (w + 1)
msb_x : x.msb = true
x_lt_y : ¬x < y
y_le_x : y.toNat ≤ x.toNat
hy : y.toNat ≠ 0
msb_y : 2 ^ w ≤ y.toNat
⊢ 0 < x.toNat / y.toNat

Proof state:
case neg.succ
w : Nat
x y : BitVec (w + 1)
msb_x : x.msb = true
x_lt_y : ¬x < y
y_le_x : y.toNat ≤ x.toNat
hy : y.toNat ≠ 0
msb_y : 2 ^ w ≤ y.toNat
this : y.toNat ≤ y.toNat * (x.toNat / y.toNat)
⊢ x.toNat % y.toNat < 2 ^ w

Tactic:
have : x.toNat % y.toNat ≤ x.toNat - y.toNat := by
  rw [Nat.mod_eq_sub]; omega

Result:
case neg.succ
w : Nat
x y : BitVec (w + 1)
msb_x : x.msb = true
x_lt_y : ¬x < y
y_le_x : y.toNat ≤ x.toNat
hy : y.toNat ≠ 0
msb_y : 2 ^ w ≤ y.toNat
this✝ : y.toNat ≤ y.toNat * (x.toNat / y.toNat)
this : x.toNat % y.toNat ≤ x.toNat - y.toNat
⊢ x.toNat % y.toNat < 2 ^ w

Proof state:
case neg.succ
w : Nat
x y : BitVec (w + 1)
msb_x : x.msb = true
x_lt_y : ¬x < y
y_le_x : y.toNat ≤ x.toNat
hy : y.toNat ≠ 0
msb_y : 2 ^ w ≤ y.toNat
⊢ x.toNat % y.toNat < 2 ^ w

Tactic:
have : y.toNat ≤ y.toNat * (x.toNat / y.toNat) := by
    apply Nat.le_mul_of_pos_right
    apply Nat.div_pos y_le_x
    omega

Result:
case neg.succ
w : Nat
x y : BitVec (w + 1)
msb_x : x.msb = true
x_lt_y : ¬x < y
y_le_x : y.toNat ≤ x.toNat
hy : y.toNat ≠ 0
msb_y : 2 ^ w ≤ y.toNat
this : y.toNat ≤ y.toNat * (x.toNat / y.toNat)
⊢ x.toNat % y.toNat < 2 ^ w

Proof state:
w : Nat
x y : BitVec w
msb_x : x.msb = true
hy : ¬y = 0
this : 2 ^ (w - 1) ≤ x.toNat % y.toNat ↔ x < y
⊢ decide (2 ^ (w - 1) ≤ x.toNat % y.toNat) = (true && (decide (x < y) || y == 0#w))

Tactic:
simp_all

Result:
no goals

Proof state:
case pos
w : Nat
x y : BitVec w
msb_x : x.msb = true
hy : ¬y = 0
x_lt_y : x < y
⊢ 2 ^ (w - 1) ≤ x.toNat % y.toNat ↔ x < y

Tactic:
simp_all [Nat.mod_eq_of_lt x_lt_y, msb_eq_decide]

Result:
no goals

Proof state:
case neg.succ
w : Nat
x y : BitVec (w + 1)
msb_x : x.msb = true
x_lt_y : ¬x < y
y_le_x : y.toNat ≤ x.toNat
hy : y.toNat ≠ 0
msb_y : 2 ^ w ≤ y.toNat
this✝ : y.toNat ≤ y.toNat * (x.toNat / y.toNat)
this : x.toNat % y.toNat ≤ x.toNat - y.toNat
⊢ x.toNat % y.toNat < 2 ^ w

Tactic:
omega

Result:
no goals

Proof state:
case neg
w : Nat
x y : BitVec w
msb_x : x.msb = true
hy : ¬y = 0
x_lt_y : ¬x < y
⊢ x.toNat % y.toNat < 2 ^ (w - 1)

Tactic:
have y_le_x : y.toNat ≤ x.toNat := by
  simpa using x_lt_y

Result:
case neg
w : Nat
x y : BitVec w
msb_x : x.msb = true
hy : ¬y = 0
x_lt_y : ¬x < y
y_le_x : y.toNat ≤ x.toNat
⊢ x.toNat % y.toNat < 2 ^ (w - 1)

Proof state:
case pos
w : Nat
x y : BitVec w
msb_x : x.msb = true
hy : ¬y = 0
x_lt_y : x < y
⊢ 2 ^ (w - 1) ≤ x.toNat % y.toNat ↔ x < y

case neg
w : Nat
x y : BitVec w
msb_x : x.msb = true
hy : ¬y = 0
x_lt_y : ¬x < y
⊢ 2 ^ (w - 1) ≤ x.toNat % y.toNat ↔ x < y

Tactic:
. simp_all [Nat.mod_eq_of_lt x_lt_y, msb_eq_decide]

Result:
case neg
w : Nat
x y : BitVec w
msb_x : x.msb = true
hy : ¬y = 0
x_lt_y : ¬x < y
⊢ 2 ^ (w - 1) ≤ x.toNat % y.toNat ↔ x < y

Proof state:
case false
w : Nat
x y : BitVec w
msb_x : x.msb = false
⊢ decide (2 ^ (w - 1) ≤ x.toNat % y.toNat) = (false && (decide (x < y) || y == 0#w))

Tactic:
suffices x.toNat % y.toNat < 2 ^ (w - 1) by simpa

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

Proof state:
w : Nat
x y : BitVec w
msb_x : x.msb = true
hy : ¬y = 0
x_lt_y : ¬x < y
this : x.toNat % y.toNat < 2 ^ (w - 1)
⊢ 2 ^ (w - 1) ≤ x.toNat % y.toNat ↔ x < y

Tactic:
simpa [x_lt_y]

Result:
no goals

Proof state:
case pos
w : Nat
x y : BitVec w
msb_x : x.msb = true
x_lt_y : ¬x < y
y_le_x : y.toNat ≤ x.toNat
hy : y.toNat ≠ 0
msb_y : y.toNat < 2 ^ (w - 1)
this : x.toNat % y.toNat < y.toNat
⊢ x.toNat % y.toNat < 2 ^ (w - 1)

Tactic:
omega

Result:
no goals