[Merged by Bors] - feat: delete Nat.shiftr and Nat.shiftl #6356
Conversation
Mathlib/Init/Data/Nat/Bitwise.lean
Outdated
| cases' b <;> simp | ||
|
|
||
| @[simp] | ||
| lemma shiftLeft_eq' {m n : Nat} : shiftLeft m n = m <<< n := rfl |
There was a problem hiding this comment.
Can you add a comment explaining why this name is primed?
There was a problem hiding this comment.
Sure, it's because shiftLeft_eq is already a lemma in Std.Data.Nat.Lemmas and it's also simped (I don't think it should be simped either).
Co-authored-by: Eric Wieser <wieser.eric@gmail.com>
Co-authored-by: Eric Wieser <wieser.eric@gmail.com>
| theorem size_shiftl {m} (h : m ≠ 0) (n) : size (shiftl m n) = size m + n := | ||
| size_shiftl' (shiftl'_ne_zero_left _ h _) | ||
| #align nat.size_shiftl Nat.size_shiftl | ||
| theorem size_shiftLeft {m} (h : m ≠ 0) (n) : size (m <<< n) = size m + n := |
There was a problem hiding this comment.
The mathlib linter is complaining that the LHS is not in simp normal formal. That's because shiftLeft_eq is simp-ed in Std.Data.Nat.Lemmas and it says m <<< n = m*2^n. I don't think that lemma should be simp-ed. It's quite problematic since I keep having to remove it from the simp set when using simp anyway.
There was a problem hiding this comment.
@digama0, what are your thoughts on this?
There was a problem hiding this comment.
bors d=@digama0
This looks good to me, though it's probably good for an Std4 contributor to have a quick skim.
Regarding the simp-nf issue, I'd recommend making a PR to Std4 to remove the lemma, and then discussing further there.
|
✌️ digama0 can now approve this pull request. To approve and merge a pull request, simply reply with |
|
bors r+ |
|
👎 Rejected by label |
|
bors r+ |
|
👎 Rejected by label |
|
bors r+ |
These already exists upstream (with minorly different but equal definitions) as `Nat.shiftRight` and `Nat.shiftLeft`. Co-authored-by: mhk119 <58151072+mhk119@users.noreply.github.com> Co-authored-by: Eric Wieser <wieser.eric@gmail.com>
|
Pull request successfully merged into master. Build succeeded! The publicly hosted instance of bors-ng is deprecated and will go away soon. If you want to self-host your own instance, instructions are here. If you want to switch to GitHub's built-in merge queue, visit their help page. |
bors
bot
changed the title
This makes it match the unprimed `Nat.shiftLeft`. Follows on from #6356 which removed `Nat.shiftl`.
This makes it match the unprimed `Nat.shiftLeft`. Follows on from #6356 which removed `Nat.shiftl`.
These already exists upstream (with minorly different but equal definitions) as
Nat.shiftRightandNat.shiftLeft.