From 3ec55d3d498ce361f5886afee516d16df5cbd6fc Mon Sep 17 00:00:00 2001 From: Kim Morrison Date: Fri, 6 Sep 2024 10:43:38 +1000 Subject: [PATCH] chore: Nat.testBit_add_one should not be a global simp lemma (#5262) --- src/Init/Data/BitVec/Lemmas.lean | 4 ++-- src/Init/Data/Nat/Bitwise/Lemmas.lean | 8 +++++++- 2 files changed, 9 insertions(+), 3 deletions(-) diff --git a/src/Init/Data/BitVec/Lemmas.lean b/src/Init/Data/BitVec/Lemmas.lean index 3ee9b34ee3..a537d40707 100644 --- a/src/Init/Data/BitVec/Lemmas.lean +++ b/src/Init/Data/BitVec/Lemmas.lean @@ -1391,14 +1391,14 @@ theorem eq_msb_cons_truncate (x : BitVec (w+1)) : x = (cons x.msb (x.truncate w) cases b · simp · rintro (_ | i) - <;> simp [Nat.add_mod, Nat.add_comm, Nat.add_mul_div_right] + <;> simp [Nat.add_mod, Nat.add_comm, Nat.add_mul_div_right, Nat.testBit_add_one] theorem getLsbD_concat (x : BitVec w) (b : Bool) (i : Nat) : (concat x b).getLsbD i = if i = 0 then b else x.getLsbD (i - 1) := by simp only [concat, getLsbD, toNat_append, toNat_ofBool, Nat.testBit_or, Nat.shiftLeft_eq] cases i · simp [Nat.mod_eq_of_lt b.toNat_lt] - · simp [Nat.div_eq_of_lt b.toNat_lt] + · simp [Nat.div_eq_of_lt b.toNat_lt, Nat.testBit_add_one] @[simp] theorem getLsbD_concat_zero : (concat x b).getLsbD 0 = b := by simp [getLsbD_concat] diff --git a/src/Init/Data/Nat/Bitwise/Lemmas.lean b/src/Init/Data/Nat/Bitwise/Lemmas.lean index d6bff78bdb..4610909acd 100644 --- a/src/Init/Data/Nat/Bitwise/Lemmas.lean +++ b/src/Init/Data/Nat/Bitwise/Lemmas.lean @@ -96,7 +96,13 @@ theorem testBit_succ (x i : Nat) : testBit x (succ i) = testBit (x/2) i := by unfold testBit simp [shiftRight_succ_inside] -@[simp] theorem testBit_add_one (x i : Nat) : testBit x (i + 1) = testBit (x/2) i := by +/-- +Depending on use cases either `testBit_add_one` or `testBit_div_two` +may be more useful as a `simp` lemma, so neither is a global `simp` lemma. +-/ +-- We turn `testBit_add_one` on as a `local simp` for this file. +@[local simp] +theorem testBit_add_one (x i : Nat) : testBit x (i + 1) = testBit (x/2) i := by unfold testBit simp [shiftRight_succ_inside]