English
The cast preserves testBit: for all m,n, testBit m n equals Nat.testBit (cast m) n.
Русский
Приведение сохраняет testBit: для всех m,n тестируется, что testBit m n равно Nat.testBit (cast m) n.
LaTeX
$$$\mathrm{castNum}(m).\mathrm{testBit} n = \mathrm{Nat}.\mathrm{testBit}(m) n$$$
Lean4
@[simp]
theorem castNum_testBit (m n) : testBit m n = Nat.testBit m n := by
cases m with dsimp only [testBit]
| zero => rw [show (Num.zero : Nat) = 0 from rfl, Nat.zero_testBit]
| pos m =>
rw [cast_pos]
induction n generalizing m <;> obtain - | m | m := m <;> simp only [PosNum.testBit]
· rfl
· rw [PosNum.cast_bit1, ← two_mul, ← congr_fun Nat.bit_true, Nat.testBit_bit_zero]
· rw [PosNum.cast_bit0, ← two_mul, ← congr_fun Nat.bit_false, Nat.testBit_bit_zero]
· simp [Nat.testBit_add_one]
case succ.bit1 n IH => rw [PosNum.cast_bit1, ← two_mul, ← congr_fun Nat.bit_true, Nat.testBit_bit_succ, IH]
case succ.bit0 n IH => rw [PosNum.cast_bit0, ← two_mul, ← congr_fun Nat.bit_false, Nat.testBit_bit_succ, IH]
