-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/BitVec/Lemmas.lean
theorem toNat_not {x : BitVec v} : (~~~x).toNat = 2^v - 1 - x.toNat

Proof state:
v : Nat
x : BitVec v
⊢ (allOnes v).toNat ^^^ x.toNat = 2 ^ v - (x.toNat + 1)

Tactic:
apply Nat.eq_of_testBit_eq

Result:
case pred
v : Nat
x : BitVec v
⊢ ∀ (i : Nat), ((allOnes v).toNat ^^^ x.toNat).testBit i = (2 ^ v - (x.toNat + 1)).testBit i

Proof state:
v : Nat
x : BitVec v
i y : Nat
h : x.toNat = y.succ
⊢ (decide (i < v) ^^ (y + 1).testBit i) = (2 ^ v - (y + 1 + 1)).testBit i

Tactic:
rw [Nat.succ_eq_add_one] at h

Result:
v : Nat
x : BitVec v
i y : Nat
h : x.toNat = y + 1
⊢ (decide (i < v) ^^ (y + 1).testBit i) = (2 ^ v - (y + 1 + 1)).testBit i

Proof state:
case true
v : Nat
x : BitVec v
i y : Nat
h : x.toNat = y + 1
w : decide (i < v) = true
⊢ (true ^^ x.toNat.testBit i) = (true && !x.toNat.testBit i)

Tactic:
simp

Result:
no goals

Proof state:
case pred
v : Nat
x : BitVec v
i : Nat
⊢ ((allOnes v).toNat ^^^ x.toNat).testBit i = (2 ^ v - (x.toNat + 1)).testBit i

Tactic:
simp only [toNat_allOnes, Nat.testBit_xor, Nat.testBit_two_pow_sub_one]

Result:
case pred
v : Nat
x : BitVec v
i : Nat
⊢ (decide (i < v) ^^ x.toNat.testBit i) = (2 ^ v - (x.toNat + 1)).testBit i

Proof state:
case false
v : Nat
x : BitVec v
i y : Nat
h : x.toNat = y + 1
w : decide (i < v) = false
⊢ (false ^^ x.toNat.testBit i) = (false && !x.toNat.testBit i)

Tactic:
simp only [decide_eq_false_iff_not, Nat.not_lt] at w

Result:
case false
v : Nat
x : BitVec v
i y : Nat
h : x.toNat = y + 1
w : v ≤ i
⊢ (false ^^ x.toNat.testBit i) = (false && !x.toNat.testBit i)

Proof state:
v : Nat
x : BitVec v
i y : Nat
h : x.toNat = y + 1
⊢ (decide (i < v) ^^ x.toNat.testBit i) = (decide (i < v) && !x.toNat.testBit i)

Tactic:
cases w : decide (i < v)

Result:
case false
v : Nat
x : BitVec v
i y : Nat
h : x.toNat = y + 1
w : decide (i < v) = false
⊢ (false ^^ x.toNat.testBit i) = (false && !x.toNat.testBit i)

case true
v : Nat
x : BitVec v
i y : Nat
h : x.toNat = y + 1
w : decide (i < v) = true
⊢ (true ^^ x.toNat.testBit i) = (true && !x.toNat.testBit i)

Proof state:
case false
v : Nat
x : BitVec v
i y : Nat
h : x.toNat = y + 1
w : v ≤ i
⊢ (false ^^ x.toNat.testBit i) = (false && !x.toNat.testBit i)

Tactic:
simp only [Bool.false_bne, Bool.false_and]

Result:
case false
v : Nat
x : BitVec v
i y : Nat
h : x.toNat = y + 1
w : v ≤ i
⊢ x.toNat.testBit i = false

Proof state:
v : Nat
x : BitVec v
i y : Nat
h : x.toNat = y + 1
⊢ (decide (i < v) ^^ x.toNat.testBit i) = (2 ^ v - (x.toNat + 1)).testBit i

Tactic:
rw [Nat.testBit_two_pow_sub_succ (isLt _)]

Result:
v : Nat
x : BitVec v
i y : Nat
h : x.toNat = y + 1
⊢ (decide (i < v) ^^ x.toNat.testBit i) = (decide (i < v) && !x.toNat.testBit i)

Proof state:
v : Nat
x : BitVec v
i : Nat
h : x.toNat = 0
⊢ (decide (i < v) ^^ Nat.testBit 0 i) = (2 ^ v - (0 + 1)).testBit i

Tactic:
simp

Result:
no goals

Proof state:
v : Nat
x : BitVec v
⊢ (~~~x).toNat = 2 ^ v - 1 - x.toNat

Tactic:
rw [Nat.sub_sub, Nat.add_comm, not_def, toNat_xor]

Result:
v : Nat
x : BitVec v
⊢ (allOnes v).toNat ^^^ x.toNat = 2 ^ v - (x.toNat + 1)

Proof state:
case false
v : Nat
x : BitVec v
i y : Nat
h : x.toNat = y + 1
w : v ≤ i
⊢ x.toNat.testBit i = false

Tactic:
rw [Nat.testBit_lt_two_pow]

Result:
case false
v : Nat
x : BitVec v
i y : Nat
h : x.toNat = y + 1
w : v ≤ i
⊢ x.toNat < 2 ^ i

Proof state:
v : Nat
x : BitVec v
i y : Nat
h : x.toNat = y + 1
⊢ (decide (i < v) ^^ (y + 1).testBit i) = (2 ^ v - (y + 1 + 1)).testBit i

Tactic:
rw [← h]

Result:
v : Nat
x : BitVec v
i y : Nat
h : x.toNat = y + 1
⊢ (decide (i < v) ^^ x.toNat.testBit i) = (2 ^ v - (x.toNat + 1)).testBit i

Proof state:
case pred
v : Nat
x : BitVec v
⊢ ∀ (i : Nat), ((allOnes v).toNat ^^^ x.toNat).testBit i = (2 ^ v - (x.toNat + 1)).testBit i

Tactic:
intro i

Result:
case pred
v : Nat
x : BitVec v
i : Nat
⊢ ((allOnes v).toNat ^^^ x.toNat).testBit i = (2 ^ v - (x.toNat + 1)).testBit i

Proof state:
case false
v : Nat
x : BitVec v
i y : Nat
h : x.toNat = y + 1
w : v ≤ i
⊢ x.toNat < 2 ^ i

Tactic:
calc BitVec.toNat x < 2 ^ v := isLt _
  _ ≤ 2 ^ i := Nat.pow_le_pow_of_le_right Nat.zero_lt_two w

Result:
no goals