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

feat: Nat.shiftLeft_shiftRight (#4199)

Browse source 
Show that shifting a natural number left and then shifting right by the
same amount is a no-op.

I originally proved this in a different PR, ended up not needing the
fact after all, but it still seemed like a generally useful simp lemma
to have.
This commit is contained in:
Alex Keizer 2024-05-20 08:50:28 +02:00 • committed by GitHub
parent f53b778c0d
commit 42215cc072
No known key found for this signature in database
GPG key ID: B5690EEEBB952194
1 changed files with 3 additions and 0 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

3
src/Init/Data/Nat/Lemmas.lean
View file

@ -794,6 +794,9 @@ theorem shiftLeft_shiftLeft (m n : Nat) : ∀ k, (m <<< n) <<< k = m <<< (n + k)
| 0 => rfl | 0 => rfl
| k + 1 => by simp [← Nat.add_assoc, shiftLeft_shiftLeft _ _ k, shiftLeft_succ] | k + 1 => by simp [← Nat.add_assoc, shiftLeft_shiftLeft _ _ k, shiftLeft_succ]
@[simp] theorem shiftLeft_shiftRight (x n : Nat) : x <<< n >>> n = x := by
rw [Nat.shiftLeft_eq, Nat.shiftRight_eq_div_pow, Nat.mul_div_cancel _ (Nat.two_pow_pos _)]
theorem mul_add_div {m : Nat} (m_pos : m > 0) (x y : Nat) : (m * x + y) / m = x + y / m := by theorem mul_add_div {m : Nat} (m_pos : m > 0) (x y : Nat) : (m * x + y) / m = x + y / m := by
match x with match x with
| 0 => simp | 0 => simp