-
Notifications
You must be signed in to change notification settings - Fork 446
New issue
Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.
By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.
Already on GitHub? Sign in to your account
feat: BitVec.shiftLeft_shiftLeft, BitVec.shiftRight_shiftRight #4148
Conversation
As requested by @hargoniX, closes two `sorry`s at https://github.com/leanprover/leansat/pull/64/files.
Mathlib CI status (docs):
|
src/Init/Data/BitVec/Lemmas.lean
Outdated
-- omega claims that the system cannot be proven, so we case bash. | ||
-- The entire proof below should be redundant once omega is complete. |
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
decide
statements are out of scope for omega
!
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
If you want to case bash and then hand off to omega
, use:
theorem BitVec.shiftLeft_shiftLeft (w : Nat) (x : BitVec w) (n m : Nat) :
(x <<< n) <<< m = x <<< (n + m) := by
ext i
simp only [getLsb_shiftLeft, Fin.is_lt, decide_True, Bool.true_and]
rw [show i - (n + m) = (i - m - n) by omega]
cases h₂ : decide (i < m) <;> cases h₃ : decide (i - m < w) <;> cases h₄ : decide (i - m < n) <;> cases h₅ : decide (i < n + m) <;>
simp at * <;> omega
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
Sweet, thanks for the tutorial! rw [show _ by omega]
is a neat one, I'm going to remember this golf trick :)
Co-authored-by: Kim Morrison <scott@tqft.net>
As taught by Kim Morrison.
Fixes double namespace introduced in #4148
Closes two
sorry
s at https://github.com/leanprover/leansat/pull/64/files.