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

chore: Nat.testBit_add_one should not be a global simp lemma (#5262)

Browse source
This commit is contained in:
Kim Morrison 2024-09-06 10:43:38 +10:00 • committed by GitHub
parent c8c35ad3b9
commit 3ec55d3d49
No known key found for this signature in database
GPG key ID: B5690EEEBB952194
2 changed files with 9 additions and 3 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

4
src/Init/Data/BitVec/Lemmas.lean
View file

@ -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]

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

@ -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]