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

feat: BitVec.shiftLeft_shiftLeft, BitVec.shiftRight_shiftRight (#4148)

Browse source 
Closes two `sorry`s at
https://github.com/leanprover/leansat/pull/64/files.

---------

Co-authored-by: Kim Morrison <scott@tqft.net>
This commit is contained in:
Siddharth 2024-05-13 13:35:59 +01:00 • committed by GitHub
parent 799923d145
commit a17c3f424c
No known key found for this signature in database
GPG key ID: B5690EEEBB952194
1 changed files with 16 additions and 0 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

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

@ -608,6 +608,17 @@ theorem shiftLeftZeroExtend_eq {x : BitVec w} :
(shiftLeftZeroExtend x i).msb = x.msb := by
simp [shiftLeftZeroExtend_eq, BitVec.msb]
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
/-! ### ushiftRight -/
@[simp, bv_toNat] theorem toNat_ushiftRight (x : BitVec n) (i : Nat) :
@ -693,6 +704,11 @@ theorem msb_append {x : BitVec w} {y : BitVec v} :
simp only [getLsb_append, cond_eq_if]
split <;> simp [*]
theorem BitVec.shiftRight_shiftRight (w : Nat) (x : BitVec w) (n m : Nat) :
(x >>> n) >>> m = x >>> (n + m) := by
ext i
simp [Nat.add_assoc n m i]
/-! ### rev -/
theorem getLsb_rev (x : BitVec w) (i : Fin w) :