-- 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:
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)

Tactic:
rcases w with _|w

Result:
case neg.zero
x y : BitVec 0
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 ^ (0 - 1)
⊢ x.toNat % y.toNat < 2 ^ (0 - 1)

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 : ¬y.toNat < 2 ^ (w + 1 - 1)
⊢ x.toNat % y.toNat < 2 ^ (w + 1 - 1)

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) ≤ x.toNat - y.toNat

Tactic:
omega

Result:
no goals

Proof state:
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 < y.toNat

Tactic:
omega

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)
⊢ x.toNat % y.toNat < 2 ^ (w - 1)

Tactic:
have : x.toNat % y.toNat < y.toNat := Nat.mod_lt _ (by omega)

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)
this : x.toNat % y.toNat < y.toNat
⊢ x.toNat % y.toNat < 2 ^ (w - 1)

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

Tactic:
cases msb_x : x.msb

Result:
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))

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))

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 : ¬y.toNat < 2 ^ (w + 1 - 1)
⊢ x.toNat % y.toNat < 2 ^ (w + 1 - 1)

Tactic:
simp only [Nat.add_one_sub_one]

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 : ¬y.toNat < 2 ^ (w + 1 - 1)
⊢ x.toNat % y.toNat < 2 ^ w

Proof state:
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:
suffices x.toNat % y.toNat < 2 ^ (w - 1) by
  simpa [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
⊢ x.toNat % y.toNat < 2 ^ (w - 1)

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 : ¬y.toNat < 2 ^ (w + 1 - 1)
⊢ 2 ^ w ≤ y.toNat

Tactic:
simpa using msb_y

Result:
no goals

Proof state:
w : Nat
x y : BitVec w
msb_x : x.msb = true
hy : ¬y = 0
x_lt_y : ¬x < y
⊢ y.toNat ≤ x.toNat

Tactic:
simpa using x_lt_y

Result:
no goals

Proof state:
case neg.zero
x y : BitVec 0
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 ^ (0 - 1)
⊢ x.toNat % y.toNat < 2 ^ (0 - 1)

Tactic:
contradiction

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 : ¬y.toNat < 2 ^ (w + 1 - 1)
⊢ x.toNat % y.toNat < 2 ^ w

Tactic:
replace msb_y : 2 ^ w ≤ y.toNat := by
  simpa using msb_y

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
⊢ x.toNat % y.toNat < 2 ^ w

Proof state:
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

Tactic:
apply Nat.div_pos y_le_x

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 < y.toNat

Proof state:
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)

Tactic:
replace hy : y.toNat ≠ 0 :=
  toNat_ne_iff_ne.mpr hy

Result:
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)