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

chore: rename Nat bitwise lemmas (#5305)

Browse source
This commit is contained in:
Kim Morrison 2024-09-11 16:29:00 +10:00 • committed by GitHub
parent d4cc934149
commit 27bf7367ca
No known key found for this signature in database
GPG key ID: B5690EEEBB952194
1 changed files with 7 additions and 3 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

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

@ -476,16 +476,20 @@ theorem and_lt_two_pow (x : Nat) {y n : Nat} (right : y < 2^n) : (x &&& y) < 2^n
exact pow_le_pow_of_le_right Nat.zero_lt_two i_ge_n
simp [testBit_and, yf]
@[simp] theorem and_pow_two_is_mod (x n : Nat) : x &&& (2^n-1) = x % 2^n := by
@[simp] theorem and_pow_two_sub_one_eq_mod (x n : Nat) : x &&& 2^n - 1 = x % 2^n := by
apply eq_of_testBit_eq
intro i
simp only [testBit_and, testBit_mod_two_pow]
cases testBit x i <;> simp
theorem and_pow_two_identity {x : Nat} (lt : x < 2^n) : x &&& 2^n-1 = x := by
rw [and_pow_two_is_mod]
@[deprecated and_pow_two_sub_one_eq_mod (since := "2024-09-11")] abbrev and_pow_two_is_mod := @and_pow_two_sub_one_eq_mod
theorem and_pow_two_sub_one_of_lt_two_pow {x : Nat} (lt : x < 2^n) : x &&& 2^n - 1 = x := by
rw [and_pow_two_sub_one_eq_mod]
apply Nat.mod_eq_of_lt lt
@[deprecated and_pow_two_sub_one_of_lt_two_pow (since := "2024-09-11")] abbrev and_two_pow_identity := @and_pow_two_sub_one_of_lt_two_pow
@[simp] theorem and_mod_two_eq_one : (a &&& b) % 2 = 1 ↔ a % 2 = 1 ∧ b % 2 = 1 := by
simp only [mod_two_eq_one_iff_testBit_zero]
rw [testBit_and]