From 27bf7367caf2df7fb44cfd9a1abed556d14dfde0 Mon Sep 17 00:00:00 2001 From: Kim Morrison Date: Wed, 11 Sep 2024 16:29:00 +1000 Subject: [PATCH] chore: rename Nat bitwise lemmas (#5305) --- src/Init/Data/Nat/Bitwise/Lemmas.lean | 10 +++++++--- 1 file changed, 7 insertions(+), 3 deletions(-) diff --git a/src/Init/Data/Nat/Bitwise/Lemmas.lean b/src/Init/Data/Nat/Bitwise/Lemmas.lean index 4610909acdcd..1a380b01e19c 100644 --- a/src/Init/Data/Nat/Bitwise/Lemmas.lean +++ b/src/Init/Data/Nat/Bitwise/Lemmas.lean @@ -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]