Skip to content

Commit

Permalink
add bv_toNat attributes
Browse files Browse the repository at this point in the history
  • Loading branch information
@kim-em
kim-em committed Feb 22, 2024
1 parent 0800fd2 commit 469f519
Show file tree
Hide file tree
Showing 2 changed files with 18 additions and 18 deletions.
2 changes: 1 addition & 1 deletion src/Init/Data/BitVec/Basic.lean
View file
Original file line number Diff line number Diff line change
Expand Up @@ -75,7 +75,7 @@ theorem isLt (x : BitVec w) : x.toNat < 2^w := x.toFin.isLt

/-- Theorem for normalizing the bit vector literal representation. -/
-- TODO: This needs more usage data to assess which direction the simp should go.
@[simp] theorem ofNat_eq_ofNat : @OfNat.ofNat (BitVec n) i _ = .ofNat n i := rfl
@[simp, bv_toNat] theorem ofNat_eq_ofNat : @OfNat.ofNat (BitVec n) i _ = .ofNat n i := rfl

-- Note. Mathlib would like this to go the other direction.
@[simp] theorem natCast_eq_ofNat (w x : Nat) : @Nat.cast (BitVec w) _ x = .ofNat w x := rfl
Expand Down
34 changes: 17 additions & 17 deletions src/Init/Data/BitVec/Lemmas.lean
View file
Original file line number Diff line number Diff line change
Expand Up @@ -23,10 +23,10 @@ theorem eq_of_toNat_eq {n} : ∀ {i j : BitVec n}, i.toNat = j.toNat → i = j

@[simp] theorem val_toFin (x : BitVec w) : x.toFin.val = x.toNat := rfl

theorem toNat_eq (x y : BitVec n) : x = y ↔ x.toNat = y.toNat :=
@[bv_toNat] theorem toNat_eq (x y : BitVec n) : x = y ↔ x.toNat = y.toNat :=
Iff.intro (congrArg BitVec.toNat) eq_of_toNat_eq

theorem toNat_ne (x y : BitVec n) : x ≠ y ↔ x.toNat ≠ y.toNat := by
@[bv_toNat] theorem toNat_ne (x y : BitVec n) : x ≠ y ↔ x.toNat ≠ y.toNat := by
rw [Ne, toNat_eq]

theorem toNat_lt (x : BitVec n) : x.toNat < 2^n := x.toFin.2
Expand Down Expand Up @@ -93,15 +93,15 @@ theorem ofNat_one (n : Nat) : BitVec.ofNat 1 n = BitVec.ofBool (n % 2 = 1) := b
theorem ofBool_eq_iff_eq : ∀(b b' : Bool), BitVec.ofBool b = BitVec.ofBool b' ↔ b = b' := by
decide

@[simp] theorem toNat_ofFin (x : Fin (2^n)) : (BitVec.ofFin x).toNat = x.val := rfl
@[simp, bv_toNat] theorem toNat_ofFin (x : Fin (2^n)) : (BitVec.ofFin x).toNat = x.val := rfl

@[simp] theorem toNat_ofNatLt (x : Nat) (p : x < 2^w) : (x#'p).toNat = x := rfl

@[simp] theorem getLsb_ofNatLt {n : Nat} (x : Nat) (lt : x < 2^n) (i : Nat) :
getLsb (x#'lt) i = x.testBit i := by
simp [getLsb, BitVec.ofNatLt]

@[simp] theorem toNat_ofNat (x w : Nat) : (x#w).toNat = x % 2^w := by
@[simp, bv_toNat] theorem toNat_ofNat (x w : Nat) : (x#w).toNat = x % 2^w := by
simp [BitVec.toNat, BitVec.ofNat, Fin.ofNat']

-- Remark: we don't use `[simp]` here because simproc` subsumes it for literals.
Expand Down Expand Up @@ -145,7 +145,7 @@ theorem msb_eq_decide (x : BitVec (w + 1)) : BitVec.msb x = decide (2 ^ w ≤ x.

/-! ### cast -/

@[simp] theorem toNat_cast (h : w = v) (x : BitVec w) : (cast h x).toNat = x.toNat := rfl
@[simp, bv_toNat] theorem toNat_cast (h : w = v) (x : BitVec w) : (cast h x).toNat = x.toNat := rfl
@[simp] theorem toFin_cast (h : w = v) (x : BitVec w) :
(cast h x).toFin = x.toFin.cast (by rw [h]) :=
rfl
Expand All @@ -160,12 +160,12 @@ theorem msb_eq_decide (x : BitVec (w + 1)) : BitVec.msb x = decide (2 ^ w ≤ x.

/-! ### zeroExtend and truncate -/

@[simp] theorem toNat_zeroExtend' {m n : Nat} (p : m ≤ n) (x : BitVec m) :
@[simp, bv_toNat] theorem toNat_zeroExtend' {m n : Nat} (p : m ≤ n) (x : BitVec m) :
(zeroExtend' p x).toNat = x.toNat := by
unfold zeroExtend'
simp [p, x.isLt, Nat.mod_eq_of_lt]

theorem toNat_zeroExtend (i : Nat) (x : BitVec n) :
@[bv_toNat] theorem toNat_zeroExtend (i : Nat) (x : BitVec n) :
BitVec.toNat (zeroExtend i x) = x.toNat % 2^i := by
let ⟨x, lt_n⟩ := x
simp only [zeroExtend]
Expand All @@ -175,7 +175,7 @@ theorem toNat_zeroExtend (i : Nat) (x : BitVec n) :
else
simp [n_le_i, toNat_ofNat]

@[simp] theorem toNat_truncate (x : BitVec n) : (truncate i x).toNat = x.toNat % 2^i :=
@[simp, bv_toNat] theorem toNat_truncate (x : BitVec n) : (truncate i x).toNat = x.toNat % 2^i :=
toNat_zeroExtend i x

@[simp] theorem zeroExtend_eq (x : BitVec n) : zeroExtend n x = x := by
Expand Down Expand Up @@ -285,7 +285,7 @@ protected theorem extractLsb_ofNat (x n : Nat) (hi lo : Nat) :

theorem not_def {x : BitVec v} : ~~~x = allOnes v ^^^ x := rfl

@[simp] theorem toNat_not {x : BitVec v} : (~~~x).toNat = 2^v - 1 - x.toNat := by
@[simp, bv_toNat] theorem toNat_not {x : BitVec v} : (~~~x).toNat = 2^v - 1 - x.toNat := by
rw [Nat.sub_sub, Nat.add_comm, not_def, toNat_xor]
apply Nat.eq_of_testBit_eq
intro i
Expand Down Expand Up @@ -315,7 +315,7 @@ theorem not_def {x : BitVec v} : ~~~x = allOnes v ^^^ x := rfl

/-! ### shiftLeft -/

@[simp] theorem toNat_shiftLeft {x : BitVec v} :
@[simp, bv_toNat] theorem toNat_shiftLeft {x : BitVec v} :
BitVec.toNat (x <<< n) = BitVec.toNat x <<< n % 2^v :=
BitVec.toNat_ofNat _ _

Expand Down Expand Up @@ -351,7 +351,7 @@ theorem shiftLeftZeroExtend_eq {x : BitVec w} :

/-! ### ushiftRight -/

@[simp] theorem toNat_ushiftRight (x : BitVec n) (i : Nat) :
@[simp, bv_toNat] theorem toNat_ushiftRight (x : BitVec n) (i : Nat) :
(x >>> i).toNat = x.toNat >>> i := rfl

@[simp] theorem getLsb_ushiftRight (x : BitVec n) (i j : Nat) :
Expand Down Expand Up @@ -428,7 +428,7 @@ theorem add_def {n} (x y : BitVec n) : x + y = .ofNat n (x.toNat + y.toNat) := r
/--
Definition of bitvector addition as a nat.
-/
@[simp] theorem toNat_add (x y : BitVec w) : (x + y).toNat = (x.toNat + y.toNat) % 2^w := rfl
@[simp, bv_toNat] theorem toNat_add (x y : BitVec w) : (x + y).toNat = (x.toNat + y.toNat) % 2^w := rfl
@[simp] theorem toFin_add (x y : BitVec w) : (x + y).toFin = toFin x + toFin y := rfl
@[simp] theorem ofFin_add (x : Fin (2^n)) (y : BitVec n) :
.ofFin x + y = .ofFin (x + y.toFin) := rfl
Expand All @@ -452,7 +452,7 @@ protected theorem add_comm (x y : BitVec n) : x + y = y + x := by

theorem sub_def {n} (x y : BitVec n) : x - y = .ofNat n (x.toNat + (2^n - y.toNat)) := by rfl

@[simp] theorem toNat_sub {n} (x y : BitVec n) :
@[simp, bv_toNat] theorem toNat_sub {n} (x y : BitVec n) :
(x - y).toNat = ((x.toNat + (2^n - y.toNat)) % 2^n) := rfl
@[simp] theorem toFin_sub (x y : BitVec n) : (x - y).toFin = toFin x - toFin y := rfl

Expand All @@ -474,7 +474,7 @@ theorem ofNat_sub_ofNat {n} (x y : Nat) : x#n - y#n = .ofNat n (x + (2^n - y % 2
· simp
· exact Nat.le_of_lt x.isLt

@[simp] theorem toNat_neg (x : BitVec n) : (- x).toNat = (2^n - x.toNat) % 2^n := by
@[simp, bv_toNat] theorem toNat_neg (x : BitVec n) : (- x).toNat = (2^n - x.toNat) % 2^n := by
simp [Neg.neg, BitVec.neg]

theorem sub_toAdd {n} (x y : BitVec n) : x - y = x + - y := by
Expand Down Expand Up @@ -502,12 +502,12 @@ theorem negOne_eq_allOnes : -1#w = allOnes w := by

theorem mul_def {n} {x y : BitVec n} : x * y = (ofFin <| x.toFin * y.toFin) := by rfl

@[simp] theorem toNat_mul (x y : BitVec n) : (x * y).toNat = (x.toNat * y.toNat) % 2 ^ n := rfl
@[simp, bv_toNat] theorem toNat_mul (x y : BitVec n) : (x * y).toNat = (x.toNat * y.toNat) % 2 ^ n := rfl
@[simp] theorem toFin_mul (x y : BitVec n) : (x * y).toFin = (x.toFin * y.toFin) := rfl

/-! ### le and lt -/

theorem le_def (x y : BitVec n) :
@[bv_toNat] theorem le_def (x y : BitVec n) :
x ≤ y ↔ x.toNat ≤ y.toNat := Iff.rfl

@[simp] theorem le_ofFin (x : BitVec n) (y : Fin (2^n)) :
Expand All @@ -517,7 +517,7 @@ theorem le_def (x y : BitVec n) :
@[simp] theorem ofNat_le_ofNat {n} (x y : Nat) : (x#n) ≤ (y#n) ↔ x % 2^n ≤ y % 2^n := by
simp [le_def]

theorem lt_def (x y : BitVec n) :
@[bv_toNat] theorem lt_def (x y : BitVec n) :
x < y ↔ x.toNat < y.toNat := Iff.rfl

@[simp] theorem lt_ofFin (x : BitVec n) (y : Fin (2^n)) :
Expand Down

0 comments on commit 469f519

Please sign in to comment.