-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/BitVec/Lemmas.lean
theorem not_neg (x : BitVec w) : ~~~(-x) = x + -1#w

Proof state:
w : Nat
x : BitVec (w + 1)
hx : ¬x.toNat = 0
⊢ (x.toNat - 1) % 2 ^ (w + 1) = ?m.355017

Tactic:
rw [Nat.mod_eq_of_lt (by omega)]

Result:
no goals

Proof state:
case succ
w : Nat
x : BitVec (w + 1)
⊢ ~~~(-x) = x + -1#(w + 1)

Tactic:
rw [BitVec.not_eq_comm]

Result:
case succ
w : Nat
x : BitVec (w + 1)
⊢ -x = ~~~(x + -1#(w + 1))

Proof state:
case pos
w : Nat
x : BitVec (w + 1)
hx : x.toNat = 0
⊢ (2 ^ (w + 1) - x.toNat) % 2 ^ (w + 1) = 2 ^ (w + 1) - 1 - (x.toNat + (2 ^ (w + 1) - 1 % 2 ^ (w + 1))) % 2 ^ (w + 1)

Tactic:
simp [hx]

Result:
no goals

Proof state:
case neg
w : Nat
x : BitVec (w + 1)
hx : ¬x.toNat = 0
⊢ 2 ^ (w + 1) - x.toNat = 2 ^ (w + 1) - 1 - (x.toNat - 1)

Tactic:
omega

Result:
no goals

Proof state:
w : Nat
x : BitVec (w + 1)
hx : ¬x.toNat = 0
⊢ 1 < 2 ^ (w + 1)

Tactic:
omega

Result:
no goals

Proof state:
w : Nat
x : BitVec (w + 1)
hx : ¬x.toNat = 0
⊢ x.toNat + (2 ^ (w + 1) - 1) = x.toNat - 1 + 2 ^ (w + 1)

Tactic:
omega

Result:
no goals

Proof state:
w : Nat
x : BitVec (w + 1)
hx : ¬x.toNat = 0
⊢ 2 ^ (w + 1) - 1 % 2 ^ (w + 1) = ?m.353758

Tactic:
rw [Nat.mod_eq_of_lt (by omega)]

Result:
no goals

Proof state:
w : Nat
x : BitVec (w + 1)
hx : ¬x.toNat = 0
⊢ 2 ^ (w + 1) - x.toNat < 2 ^ (w + 1)

Tactic:
omega

Result:
no goals

Proof state:
w : Nat
x : BitVec (w + 1)
hx : ¬x.toNat = 0
⊢ (2 ^ (w + 1) - x.toNat) % 2 ^ (w + 1) = ?m.355258

Tactic:
rw [Nat.mod_eq_of_lt (by omega)]

Result:
no goals

Proof state:
case zero
x : BitVec 0
⊢ ~~~(-x) = x + -1#0

Tactic:
apply Subsingleton.elim

Result:
no goals

Proof state:
w : Nat
x : BitVec w
⊢ ~~~(-x) = x + -1#w

Tactic:
rcases w with _ | w

Result:
case zero
x : BitVec 0
⊢ ~~~(-x) = x + -1#0

case succ
w : Nat
x : BitVec (w + 1)
⊢ ~~~(-x) = x + -1#(w + 1)

Proof state:
case succ
w : Nat
x : BitVec (w + 1)
⊢ -x = ~~~(x + -1#(w + 1))

Tactic:
apply BitVec.eq_of_toNat_eq

Result:
case succ.a
w : Nat
x : BitVec (w + 1)
⊢ (-x).toNat = (~~~(x + -1#(w + 1))).toNat

Proof state:
case succ.a
w : Nat
x : BitVec (w + 1)
⊢ (-x).toNat = (~~~(x + -1#(w + 1))).toNat

Tactic:
simp only [BitVec.toNat_neg, BitVec.toNat_not, BitVec.toNat_add, BitVec.toNat_ofNat,
  Nat.add_mod_mod]

Result:
case succ.a
w : Nat
x : BitVec (w + 1)
⊢ (2 ^ (w + 1) - x.toNat) % 2 ^ (w + 1) = 2 ^ (w + 1) - 1 - (x.toNat + (2 ^ (w + 1) - 1 % 2 ^ (w + 1))) % 2 ^ (w + 1)

Proof state:
case succ.a
w : Nat
x : BitVec (w + 1)
⊢ (2 ^ (w + 1) - x.toNat) % 2 ^ (w + 1) = 2 ^ (w + 1) - 1 - (x.toNat + (2 ^ (w + 1) - 1 % 2 ^ (w + 1))) % 2 ^ (w + 1)

Tactic:
by_cases hx : x.toNat = 0

Result:
case pos
w : Nat
x : BitVec (w + 1)
hx : x.toNat = 0
⊢ (2 ^ (w + 1) - x.toNat) % 2 ^ (w + 1) = 2 ^ (w + 1) - 1 - (x.toNat + (2 ^ (w + 1) - 1 % 2 ^ (w + 1))) % 2 ^ (w + 1)

case neg
w : Nat
x : BitVec (w + 1)
hx : ¬x.toNat = 0
⊢ (2 ^ (w + 1) - x.toNat) % 2 ^ (w + 1) = 2 ^ (w + 1) - 1 - (x.toNat + (2 ^ (w + 1) - 1 % 2 ^ (w + 1))) % 2 ^ (w + 1)

Proof state:
w : Nat
x : BitVec (w + 1)
hx : ¬x.toNat = 0
⊢ x.toNat - 1 < 2 ^ (w + 1)

Tactic:
omega

Result:
no goals

Proof state:
case neg
w : Nat
x : BitVec (w + 1)
hx : ¬x.toNat = 0
⊢ (2 ^ (w + 1) - x.toNat) % 2 ^ (w + 1) = 2 ^ (w + 1) - 1 - (x.toNat + (2 ^ (w + 1) - 1 % 2 ^ (w + 1))) % 2 ^ (w + 1)

Tactic:
rw [show (_ - 1 % _) = _ by rw [Nat.mod_eq_of_lt (by omega)],
  show _ + (_ - 1) = (x.toNat - 1) + 2^(w + 1) by omega,
  Nat.add_mod_right,
  show (x.toNat - 1) % _ = _ by rw [Nat.mod_eq_of_lt (by omega)],
  show (_ - x.toNat) % _ = _ by rw [Nat.mod_eq_of_lt (by omega)]]

Result:
case neg
w : Nat
x : BitVec (w + 1)
hx : ¬x.toNat = 0
⊢ 2 ^ (w + 1) - x.toNat = 2 ^ (w + 1) - 1 - (x.toNat - 1)