max/lean4-htt
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions 2

feat: Nat.bitwise lemmas (#5209)

Browse source
This commit is contained in:
Kim Morrison 2024-08-30 12:37:11 +10:00 • committed by GitHub
parent a24370b049
commit 16aa80306e
No known key found for this signature in database
GPG key ID: B5690EEEBB952194
1 changed files with 12 additions and 0 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

12
src/Init/Data/Nat/Bitwise/Lemmas.lean
View file

@ -463,6 +463,10 @@ theorem and_pow_two_identity {x : Nat} (lt : x < 2^n) : x &&& 2^n-1 = x := by
rw [testBit_and]
simp
theorem and_div_two : (a &&& b) / 2 = a / 2 &&& b / 2 := by
apply Nat.eq_of_testBit_eq
simp [testBit_and, ← testBit_add_one]
/-! ### lor -/
@[simp] theorem zero_or (x : Nat) : 0 ||| x = x := by
@ -486,6 +490,10 @@ theorem or_lt_two_pow {x y n : Nat} (left : x < 2^n) (right : y < 2^n) : x ||| y
rw [testBit_or]
simp
theorem or_div_two : (a ||| b) / 2 = a / 2 ||| b / 2 := by
apply Nat.eq_of_testBit_eq
simp [testBit_or, ← testBit_add_one]
/-! ### xor -/
@[simp] theorem testBit_xor (x y i : Nat) :
@ -508,6 +516,10 @@ theorem and_xor_distrib_left {a b c : Nat} : a &&& (b ^^^ c) = (a &&& b) ^^^ (a
rw [testBit_xor]
simp
theorem xor_div_two : (a ^^^ b) / 2 = a / 2 ^^^ b / 2 := by
apply Nat.eq_of_testBit_eq
simp [testBit_xor, ← testBit_add_one]
/-! ### Arithmetic -/
theorem testBit_mul_pow_two_add (a : Nat) {b i : Nat} (b_lt : b < 2^i) (j : Nat) :