Skip to content
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.

Sign up for GitHub

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

Jump to bottom

feat: add BitVec zero/one simplifications #29

Draft
wants to merge 1 commit into
base: master
Choose a base branch
from
Draft

feat: add BitVec zero/one simplifications #29

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
1 commit
Select commit
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
29 changes: 24 additions & 5 deletions src/Init/Data/BitVec/Lemmas.lean
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -1062,7 +1062,7 @@ theorem not_eq_comm {x y : BitVec w} : ~~~ x = y ↔ x = ~~~ y := by
BitVec.toFin (x <<< n) = Fin.ofNat' (2^w) (x.toNat <<< n) := rfl

@[simp]
theorem shiftLeft_zero_eq (x : BitVec w) : x <<< 0 = x := by
theorem shiftLeft_zero (x : BitVec w) : x <<< 0 = x := by
apply eq_of_toNat_eq
simp

Expand Down Expand Up @@ -1232,7 +1232,11 @@ theorem ushiftRight_or_distrib (x y : BitVec w) (n : Nat) :
simp

@[simp]
theorem ushiftRight_zero_eq (x : BitVec w) : x >>> 0 = x := by
theorem ushiftRight_zero (x : BitVec w) : x >>> 0 = x := by
simp [bv_toNat]

@[simp]
theorem zero_ushiftRight {n : Nat} : 0#w >>> n = 0#w := by
simp [bv_toNat]

/--
Expand Down Expand Up @@ -1387,6 +1391,10 @@ theorem msb_sshiftRight {n : Nat} {x : BitVec w} :
ext i
simp [getLsbD_sshiftRight]

@[simp] theorem zero_sshiftRight {n : Nat} : (0#w).sshiftRight n = 0#w := by
ext i
simp [getLsbD_sshiftRight]

theorem sshiftRight_add {x : BitVec w} {m n : Nat} :
x.sshiftRight (m + n) = (x.sshiftRight m).sshiftRight n := by
ext i
Expand Down Expand Up @@ -2153,18 +2161,23 @@ instance : Std.LawfulCommIdentity (fun (x y : BitVec w) => x * y) (1#w) where
right_id := BitVec.mul_one

@[simp]
theorem BitVec.mul_zero {x : BitVec w} : x * 0#w = 0#w := by
theorem mul_zero {x : BitVec w} : x * 0#w = 0#w := by
apply eq_of_toNat_eq
simp [toNat_mul]

theorem BitVec.mul_add {x y z : BitVec w} :
@[simp]
theorem zero_mul {x : BitVec w} : 0#w * x = 0#w := by
apply eq_of_toNat_eq
simp [toNat_mul]

theorem mul_add {x y z : BitVec w} :
x * (y + z) = x * y + x * z := by
apply eq_of_toNat_eq
simp only [toNat_mul, toNat_add, Nat.add_mod_mod, Nat.mod_add_mod]
rw [Nat.mul_mod, Nat.mod_mod (y.toNat + z.toNat),
← Nat.mul_mod, Nat.mul_add]

theorem mul_succ {x y : BitVec w} : x * (y + 1#w) = x * y + x := by simp [BitVec.mul_add]
theorem mul_succ {x y : BitVec w} : x * (y + 1#w) = x * y + x := by simp [mul_add]
theorem succ_mul {x y : BitVec w} : (x + 1#w) * y = x * y + y := by simp [BitVec.mul_comm, BitVec.mul_add]

theorem mul_two {x : BitVec w} : x * 2#w = x + x := by
Expand Down Expand Up @@ -3179,4 +3192,10 @@ abbrev and_one_eq_zeroExtend_ofBool_getLsbD := @and_one_eq_setWidth_ofBool_getLs
@[deprecated msb_sshiftRight (since := "2024-10-03")]
abbrev sshiftRight_msb_eq_msb := @msb_sshiftRight

@[deprecated shiftLeft_zero (since := "2024-10-27")]
abbrev shiftLeft_zero_eq := @shiftLeft_zero

@[deprecated ushiftRight_zero (since := "2024-10-27")]
abbrev ushiftRight_zero_eq := @ushiftRight_zero

end BitVec
62 changes: 13 additions & 49 deletions src/Std/Tactic/BVDecide/Normalize/BitVec.lean
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -104,15 +104,8 @@ attribute [bv_normalize] BitVec.not_not

end Constant

@[bv_normalize]
theorem BitVec.zero_and (a : BitVec w) : 0#w &&& a = 0#w := by
ext
simp

@[bv_normalize]
theorem BitVec.and_zero (a : BitVec w) : a &&& 0#w = 0#w := by
ext
simp
attribute [bv_normalize] BitVec.zero_and
attribute [bv_normalize] BitVec.and_zero

-- Used in simproc because of - normalization
theorem BitVec.ones_and (a : BitVec w) : (-1#w) &&& a = a := by
Expand All @@ -124,10 +117,7 @@ theorem BitVec.and_ones (a : BitVec w) : a &&& (-1#w) = a := by
ext
simp [BitVec.negOne_eq_allOnes]

@[bv_normalize]
theorem BitVec.and_self (a : BitVec w) : a &&& a = a := by
ext
simp
attribute [bv_normalize] BitVec.and_self

@[bv_normalize]
theorem BitVec.and_contra (a : BitVec w) : a &&& ~~~a = 0#w := by
Expand Down Expand Up @@ -202,56 +192,30 @@ theorem BitVec.add_const_right (a b c : BitVec w) : a + (b + c) = (a + c) + b :=
theorem BitVec.add_const_left' (a b c : BitVec w) : (a + b) + c = (a + c) + b := by ac_rfl
theorem BitVec.add_const_right' (a b c : BitVec w) : (a + b) + c = (b + c) + a := by ac_rfl

@[bv_normalize]
theorem BitVec.zero_sshiftRight : BitVec.sshiftRight 0#w a = 0#w := by
ext
simp [BitVec.getLsbD_sshiftRight]

@[bv_normalize]
theorem BitVec.sshiftRight_zero : BitVec.sshiftRight a 0 = a := by
ext
simp [BitVec.getLsbD_sshiftRight]

@[bv_normalize]
theorem BitVec.mul_zero (a : BitVec w) : a * 0#w = 0#w := by
simp [bv_toNat]
attribute [bv_normalize] BitVec.mul_zero
attribute [bv_normalize] BitVec.zero_mul

@[bv_normalize]
theorem BitVec.zero_mul (a : BitVec w) : 0#w * a = 0#w := by
simp [bv_toNat]
attribute [bv_normalize] BitVec.shiftLeft_zero
attribute [bv_normalize] BitVec.zero_shiftLeft

@[bv_normalize]
theorem BitVec.shiftLeft_zero (n : BitVec w) : n <<< 0#w' = n := by
theorem BitVec.shiftLeft_zero' (n : BitVec w) : n <<< 0#w' = n := by
ext i
simp only [(· <<< ·)]
simp

@[bv_normalize]
theorem BitVec.shiftLeft_zero' (n : BitVec w) : n <<< 0 = n := by
ext i
simp

@[bv_normalize]
theorem BitVec.zero_shiftLeft (n : Nat) : 0#w <<< n = 0#w := by
ext
simp
attribute [bv_normalize] BitVec.zero_sshiftRight
attribute [bv_normalize] BitVec.sshiftRight_zero

@[bv_normalize]
theorem BitVec.zero_shiftRight (n : Nat) : 0#w >>> n = 0#w := by
ext
simp
attribute [bv_normalize] BitVec.zero_ushiftRight
attribute [bv_normalize] BitVec.ushiftRight_zero

@[bv_normalize]
theorem BitVec.shiftRight_zero (n : BitVec w) : n >>> 0#w' = n := by
theorem BitVec.ushiftRight_zero' (n : BitVec w) : n >>> 0#w' = n := by
ext i
simp only [(· >>> ·)]
simp

@[bv_normalize]
theorem BitVec.shiftRight_zero' (n : BitVec w) : n >>> 0 = n := by
ext i
simp

theorem BitVec.zero_lt_iff_zero_neq (a : BitVec w) : (0#w < a) ↔ (a ≠ 0#w) := by
constructor <;>
simp_all only [BitVec.lt_def, BitVec.toNat_ofNat, Nat.zero_mod, ne_eq, BitVec.toNat_eq] <;>
Expand Down
Loading