From e7be64b274417a8410b4e7276bcfa90560a61f61 Mon Sep 17 00:00:00 2001 From: Tobias Grosser Date: Tue, 6 Aug 2024 16:29:43 +0100 Subject: [PATCH 1/9] chore: use x/y consistently to name bitvectors This is purely a naming change to make our bitvector proofs more consistent. --- src/Init/Data/BitVec/Lemmas.lean | 18 +++++++++--------- 1 file changed, 9 insertions(+), 9 deletions(-) diff --git a/src/Init/Data/BitVec/Lemmas.lean b/src/Init/Data/BitVec/Lemmas.lean index da1ca96bc924..49a6ee4e6c70 100644 --- a/src/Init/Data/BitVec/Lemmas.lean +++ b/src/Init/Data/BitVec/Lemmas.lean @@ -23,7 +23,7 @@ theorem ofFin_eq_ofNat : @BitVec.ofFin w (Fin.mk x lt) = BitVec.ofNat w x := by simp only [BitVec.ofNat, Fin.ofNat', lt, Nat.mod_eq_of_lt] /-- Prove equality of bitvectors in terms of nat operations. -/ -theorem eq_of_toNat_eq {n} : ∀ {i j : BitVec n}, i.toNat = j.toNat → i = j +theorem eq_of_toNat_eq {n} : ∀ {x y : BitVec n}, x.toNat = y.toNat → x = y | ⟨_, _⟩, ⟨_, _⟩, rfl => rfl @[simp] theorem val_toFin (x : BitVec w) : x.toFin.val = x.toNat := rfl @@ -228,12 +228,12 @@ theorem toNat_ge_of_msb_true {x : BitVec n} (p : BitVec.msb x = true) : x.toNat /-! ### toInt/ofInt -/ /-- Prove equality of bitvectors in terms of nat operations. -/ -theorem toInt_eq_toNat_cond (i : BitVec n) : - i.toInt = - if 2*i.toNat < 2^n then - (i.toNat : Int) +theorem toInt_eq_toNat_cond (x : BitVec n) : + x.toInt = + if 2*x.toNat < 2^n then + (x.toNat : Int) else - (i.toNat : Int) - (2^n : Nat) := + (x.toNat : Int) - (2^n : Nat) := rfl theorem msb_eq_false_iff_two_mul_lt (x : BitVec w) : x.msb = false ↔ 2 * x.toNat < 2^w := by @@ -260,13 +260,13 @@ theorem toInt_eq_toNat_bmod (x : BitVec n) : x.toInt = Int.bmod x.toNat (2^n) := omega /-- Prove equality of bitvectors in terms of nat operations. -/ -theorem eq_of_toInt_eq {i j : BitVec n} : i.toInt = j.toInt → i = j := by +theorem eq_of_toInt_eq {x y : BitVec n} : x.toInt = y.toInt → x = y := by intro eq simp [toInt_eq_toNat_cond] at eq apply eq_of_toNat_eq revert eq - have _ilt := i.isLt - have _jlt := j.isLt + have _xlt := x.isLt + have _ylt := y.isLt split <;> split <;> omega theorem toInt_inj (x y : BitVec n) : x.toInt = y.toInt ↔ x = y := From 0d1ba73a3a29869da9870b672facd0cf347a97f2 Mon Sep 17 00:00:00 2001 From: Tobias Grosser Date: Tue, 6 Aug 2024 16:38:41 +0100 Subject: [PATCH 2/9] chore: canonicalize BitVec.Basic --- src/Init/Data/BitVec/Basic.lean | 48 ++++++++++++++++----------------- 1 file changed, 24 insertions(+), 24 deletions(-) diff --git a/src/Init/Data/BitVec/Basic.lean b/src/Init/Data/BitVec/Basic.lean index 5c16ca74c4d1..818178944db5 100644 --- a/src/Init/Data/BitVec/Basic.lean +++ b/src/Init/Data/BitVec/Basic.lean @@ -42,8 +42,8 @@ Bitvectors have decidable equality. This should be used via the instance `Decida -- We manually derive the `DecidableEq` instances for `BitVec` because -- we want to have builtin support for bit-vector literals, and we -- need a name for this function to implement `canUnfoldAtMatcher` at `WHNF.lean`. -def BitVec.decEq (a b : BitVec n) : Decidable (a = b) := - match a, b with +def BitVec.decEq (x y : BitVec n) : Decidable (x = y) := + match x, y with | ⟨n⟩, ⟨m⟩ => if h : n = m then isTrue (h ▸ rfl) @@ -71,7 +71,7 @@ instance natCastInst : NatCast (BitVec w) := ⟨BitVec.ofNat w⟩ /-- Given a bitvector `a`, return the underlying `Nat`. This is O(1) because `BitVec` is a (zero-cost) wrapper around a `Nat`. -/ -protected def toNat (a : BitVec n) : Nat := a.toFin.val +protected def toNat (x : BitVec n) : Nat := x.toFin.val /-- Return the bound in terms of toNat. -/ theorem isLt (x : BitVec w) : x.toNat < 2^w := x.toFin.isLt @@ -123,18 +123,18 @@ section getXsb @[inline] def getMsb (x : BitVec w) (i : Nat) : Bool := i < w && getLsb x (w-1-i) /-- Return most-significant bit in bitvector. -/ -@[inline] protected def msb (a : BitVec n) : Bool := getMsb a 0 +@[inline] protected def msb (x : BitVec n) : Bool := getMsb x 0 end getXsb section Int /-- Interpret the bitvector as an integer stored in two's complement form. -/ -protected def toInt (a : BitVec n) : Int := - if 2 * a.toNat < 2^n then - a.toNat +protected def toInt (x : BitVec n) : Int := + if 2 * x.toNat < 2^n then + x.toNat else - (a.toNat : Int) - (2^n : Nat) + (x.toNat : Int) - (2^n : Nat) /-- The `BitVec` with value `(2^n + (i mod 2^n)) mod 2^n`. -/ protected def ofInt (n : Nat) (i : Int) : BitVec n := .ofNatLt (i % (Int.ofNat (2^n))).toNat (by @@ -215,7 +215,7 @@ instance : Neg (BitVec n) := ⟨.neg⟩ /-- Return the absolute value of a signed bitvector. -/ -protected def abs (s : BitVec n) : BitVec n := if s.msb then .neg s else s +protected def abs (x : BitVec n) : BitVec n := if x.msb then .neg x else x /-- Multiplication for bit vectors. This can be interpreted as either signed or unsigned negation @@ -373,8 +373,8 @@ end relations section cast -/-- `cast eq i` embeds `i` into an equal `BitVec` type. -/ -@[inline] def cast (eq : n = m) (i : BitVec n) : BitVec m := .ofNatLt i.toNat (eq ▸ i.isLt) +/-- `cast eq x` embeds `x` into an equal `BitVec` type. -/ +@[inline] def cast (eq : n = m) (x : BitVec n) : BitVec m := .ofNatLt x.toNat (eq ▸ x.isLt) @[simp] theorem cast_ofNat {n m : Nat} (h : n = m) (x : Nat) : cast h (BitVec.ofNat n x) = BitVec.ofNat m x := by @@ -391,7 +391,7 @@ Extraction of bits `start` to `start + len - 1` from a bit vector of size `n` to new bitvector of size `len`. If `start + len > n`, then the vector will be zero-padded in the high bits. -/ -def extractLsb' (start len : Nat) (a : BitVec n) : BitVec len := .ofNat _ (a.toNat >>> start) +def extractLsb' (start len : Nat) (x : BitVec n) : BitVec len := .ofNat _ (x.toNat >>> start) /-- Extraction of bits `hi` (inclusive) down to `lo` (inclusive) from a bit vector of size `n` to @@ -399,12 +399,12 @@ yield a new bitvector of size `hi - lo + 1`. SMT-Lib name: `extract`. -/ -def extractLsb (hi lo : Nat) (a : BitVec n) : BitVec (hi - lo + 1) := extractLsb' lo _ a +def extractLsb (hi lo : Nat) (x : BitVec n) : BitVec (hi - lo + 1) := extractLsb' lo _ x /-- A version of `zeroExtend` that requires a proof, but is a noop. -/ -def zeroExtend' {n w : Nat} (le : n ≤ w) (x : BitVec n) : BitVec w := +def zeroExtend' {n w : Nat} (le : n ≤ w) (x : BitVec n) : BitVec w := x.toNat#'(by apply Nat.lt_of_lt_of_le x.isLt exact Nat.pow_le_pow_of_le_right (by trivial) le) @@ -413,7 +413,7 @@ def zeroExtend' {n w : Nat} (le : n ≤ w) (x : BitVec n) : BitVec w := `shiftLeftZeroExtend x n` returns `zeroExtend (w+n) x <<< n` without needing to compute `x % 2^(2+n)`. -/ -def shiftLeftZeroExtend (msbs : BitVec w) (m : Nat) : BitVec (w+m) := +def shiftLeftZeroExtend (msbs : BitVec w) (m : Nat) : BitVec (w + m) := let shiftLeftLt {x : Nat} (p : x < 2^w) (m : Nat) : x <<< m < 2^(w+m) := by simp [Nat.shiftLeft_eq, Nat.pow_add] apply Nat.mul_lt_mul_of_pos_right p @@ -502,24 +502,24 @@ instance : Complement (BitVec w) := ⟨.not⟩ /-- Left shift for bit vectors. The low bits are filled with zeros. As a numeric operation, this is -equivalent to `a * 2^s`, modulo `2^n`. +equivalent to `x * 2^s`, modulo `2^n`. SMT-Lib name: `bvshl` except this operator uses a `Nat` shift value. -/ -protected def shiftLeft (a : BitVec n) (s : Nat) : BitVec n := BitVec.ofNat n (a.toNat <<< s) +protected def shiftLeft (x : BitVec n) (s : Nat) : BitVec n := BitVec.ofNat n (x.toNat <<< s) instance : HShiftLeft (BitVec w) Nat (BitVec w) := ⟨.shiftLeft⟩ /-- (Logical) right shift for bit vectors. The high bits are filled with zeros. -As a numeric operation, this is equivalent to `a / 2^s`, rounding down. +As a numeric operation, this is equivalent to `x / 2^s`, rounding down. SMT-Lib name: `bvlshr` except this operator uses a `Nat` shift value. -/ -def ushiftRight (a : BitVec n) (s : Nat) : BitVec n := - (a.toNat >>> s)#'(by - let ⟨a, lt⟩ := a +def ushiftRight (x : BitVec n) (s : Nat) : BitVec n := + (x.toNat >>> s)#'(by + let ⟨x, lt⟩ := x simp only [BitVec.toNat, Nat.shiftRight_eq_div_pow, Nat.div_lt_iff_lt_mul (Nat.two_pow_pos s)] - rw [←Nat.mul_one a] + rw [←Nat.mul_one x] exact Nat.mul_lt_mul_of_lt_of_le' lt (Nat.two_pow_pos s) (Nat.le_refl 1)) instance : HShiftRight (BitVec w) Nat (BitVec w) := ⟨.ushiftRight⟩ @@ -527,11 +527,11 @@ instance : HShiftRight (BitVec w) Nat (BitVec w) := ⟨.ushiftRight⟩ /-- Arithmetic right shift for bit vectors. The high bits are filled with the most-significant bit. -As a numeric operation, this is equivalent to `a.toInt >>> s`. +As a numeric operation, this is equivalent to `x.toInt >>> s`. SMT-Lib name: `bvashr` except this operator uses a `Nat` shift value. -/ -def sshiftRight (a : BitVec n) (s : Nat) : BitVec n := .ofInt n (a.toInt >>> s) +def sshiftRight (x : BitVec n) (s : Nat) : BitVec n := .ofInt n (x.toInt >>> s) instance {n} : HShiftLeft (BitVec m) (BitVec n) (BitVec m) := ⟨fun x y => x <<< y.toNat⟩ instance {n} : HShiftRight (BitVec m) (BitVec n) (BitVec m) := ⟨fun x y => x >>> y.toNat⟩ From 6612208d163f0fc2070d88753bf5e79b5525c844 Mon Sep 17 00:00:00 2001 From: Tobias Grosser Date: Tue, 6 Aug 2024 17:51:57 +0100 Subject: [PATCH 3/9] rename l r -> x y --- src/Init/Data/BitVec/Bitblast.lean | 26 +++++++++++++------------- 1 file changed, 13 insertions(+), 13 deletions(-) diff --git a/src/Init/Data/BitVec/Bitblast.lean b/src/Init/Data/BitVec/Bitblast.lean index 53d8bec42a38..a60b8d4dc628 100644 --- a/src/Init/Data/BitVec/Bitblast.lean +++ b/src/Init/Data/BitVec/Bitblast.lean @@ -289,18 +289,18 @@ theorem sle_eq_carry (x y : BitVec w) : A recurrence that describes multiplication as repeated addition. Is useful for bitblasting multiplication. -/ -def mulRec (l r : BitVec w) (s : Nat) : BitVec w := - let cur := if r.getLsb s then (l <<< s) else 0 +def mulRec (x y : BitVec w) (s : Nat) : BitVec w := + let cur := if y.getLsb s then (x <<< s) else 0 match s with | 0 => cur - | s + 1 => mulRec l r s + cur + | s + 1 => mulRec x y s + cur -theorem mulRec_zero_eq (l r : BitVec w) : - mulRec l r 0 = if r.getLsb 0 then l else 0 := by +theorem mulRec_zero_eq (x y : BitVec w) : + mulRec x y 0 = if y.getLsb 0 then x else 0 := by simp [mulRec] -theorem mulRec_succ_eq (l r : BitVec w) (s : Nat) : - mulRec l r (s + 1) = mulRec l r s + if r.getLsb (s + 1) then (l <<< (s + 1)) else 0 := rfl +theorem mulRec_succ_eq (x y : BitVec w) (s : Nat) : + mulRec x y (s + 1) = mulRec x y s + if y.getLsb (s + 1) then (x <<< (s + 1)) else 0 := rfl /-- Recurrence lemma: truncating to `i+1` bits and then zero extending to `w` @@ -329,12 +329,12 @@ theorem zeroExtend_truncate_succ_eq_zeroExtend_truncate_add_twoPow (x : BitVec w Recurrence lemma: multiplying `l` with the first `s` bits of `r` is the same as truncating `r` to `s` bits, then zero extending to the original length, and performing the multplication. -/ -theorem mulRec_eq_mul_signExtend_truncate (l r : BitVec w) (s : Nat) : - mulRec l r s = l * ((r.truncate (s + 1)).zeroExtend w) := by +theorem mulRec_eq_mul_signExtend_truncate (x y : BitVec w) (s : Nat) : + mulRec x y s = x * ((y.truncate (s + 1)).zeroExtend w) := by induction s case zero => simp only [mulRec_zero_eq, ofNat_eq_ofNat, Nat.reduceAdd] - by_cases r.getLsb 0 + by_cases y.getLsb 0 case pos hr => simp only [hr, ↓reduceIte, truncate, zeroExtend_one_eq_ofBool_getLsb_zero, hr, ofBool_true, ofNat_eq_ofNat] @@ -345,10 +345,10 @@ theorem mulRec_eq_mul_signExtend_truncate (l r : BitVec w) (s : Nat) : case succ s' hs => rw [mulRec_succ_eq, hs] have heq : - (if r.getLsb (s' + 1) = true then l <<< (s' + 1) else 0) = - (l * (r &&& (BitVec.twoPow w (s' + 1)))) := by + (if y.getLsb (s' + 1) = true then x <<< (s' + 1) else 0) = + (x * (y &&& (BitVec.twoPow w (s' + 1)))) := by simp only [ofNat_eq_ofNat, and_twoPow] - by_cases hr : r.getLsb (s' + 1) <;> simp [hr] + by_cases hr : y.getLsb (s' + 1) <;> simp [hr] rw [heq, ← BitVec.mul_add, ← zeroExtend_truncate_succ_eq_zeroExtend_truncate_add_twoPow] theorem getLsb_mul (x y : BitVec w) (i : Nat) : From 3861dda47026cf21a36eedc59dd32f9b23820400 Mon Sep 17 00:00:00 2001 From: Tobias Grosser Date: Tue, 6 Aug 2024 17:53:21 +0100 Subject: [PATCH 4/9] Recurrence --- src/Init/Data/BitVec/Bitblast.lean | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/src/Init/Data/BitVec/Bitblast.lean b/src/Init/Data/BitVec/Bitblast.lean index a60b8d4dc628..017dd6f27d55 100644 --- a/src/Init/Data/BitVec/Bitblast.lean +++ b/src/Init/Data/BitVec/Bitblast.lean @@ -326,8 +326,8 @@ theorem zeroExtend_truncate_succ_eq_zeroExtend_truncate_add_twoPow (x : BitVec w by_cases hi : x.getLsb i <;> simp [hi] <;> omega /-- -Recurrence lemma: multiplying `l` with the first `s` bits of `r` is the -same as truncating `r` to `s` bits, then zero extending to the original length, +Recurrence lemma: multiplying `x` with the first `s` bits of `y` is the +same as truncating `y` to `s` bits, then zero extending to the original length, and performing the multplication. -/ theorem mulRec_eq_mul_signExtend_truncate (x y : BitVec w) (s : Nat) : mulRec x y s = x * ((y.truncate (s + 1)).zeroExtend w) := by From fb4436d27d92966eeaf399d8794700f9779c8aa9 Mon Sep 17 00:00:00 2001 From: Tobias Grosser Date: Wed, 7 Aug 2024 11:02:29 +0100 Subject: [PATCH 5/9] Update src/Init/Data/BitVec/Basic.lean Co-authored-by: AnotherAlexHere <153999274+AnotherAlexHere@users.noreply.github.com> --- src/Init/Data/BitVec/Basic.lean | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/Init/Data/BitVec/Basic.lean b/src/Init/Data/BitVec/Basic.lean index 818178944db5..f994b3e8aa91 100644 --- a/src/Init/Data/BitVec/Basic.lean +++ b/src/Init/Data/BitVec/Basic.lean @@ -414,7 +414,7 @@ def zeroExtend' {n w : Nat} (le : n ≤ w) (x : BitVec n) : BitVec w := needing to compute `x % 2^(2+n)`. -/ def shiftLeftZeroExtend (msbs : BitVec w) (m : Nat) : BitVec (w + m) := - let shiftLeftLt {x : Nat} (p : x < 2^w) (m : Nat) : x <<< m < 2^(w+m) := by + let shiftLeftLt {x : Nat} (p : x < 2^w) (m : Nat) : x <<< m < 2^(w + m) := by simp [Nat.shiftLeft_eq, Nat.pow_add] apply Nat.mul_lt_mul_of_pos_right p exact (Nat.two_pow_pos m) From 3ba61bba51d6733849f1beda9a24919f5ba02128 Mon Sep 17 00:00:00 2001 From: Tobias Grosser Date: Wed, 7 Aug 2024 11:35:03 +0100 Subject: [PATCH 6/9] Rename 's t : BitVec' to 'x y : BitVec' --- src/Init/Data/BitVec/Basic.lean | 52 ++++++++++++++++----------------- 1 file changed, 26 insertions(+), 26 deletions(-) diff --git a/src/Init/Data/BitVec/Basic.lean b/src/Init/Data/BitVec/Basic.lean index f994b3e8aa91..fa0572725cf1 100644 --- a/src/Init/Data/BitVec/Basic.lean +++ b/src/Init/Data/BitVec/Basic.lean @@ -262,12 +262,12 @@ sdiv 5#4 -2 = -2#4 sdiv (-7#4) (-2) = 3#4 ``` -/ -def sdiv (s t : BitVec n) : BitVec n := - match s.msb, t.msb with - | false, false => udiv s t - | false, true => .neg (udiv s (.neg t)) - | true, false => .neg (udiv (.neg s) t) - | true, true => udiv (.neg s) (.neg t) +def sdiv (x y : BitVec n) : BitVec n := + match x.msb, y.msb with + | false, false => udiv x y + | false, true => .neg (udiv x (.neg y)) + | true, false => .neg (udiv (.neg x) y) + | true, true => udiv (.neg x) (.neg y) /-- Signed division for bit vectors using SMTLIB rules for division by zero. @@ -276,40 +276,40 @@ Specifically, `smtSDiv x 0 = if x >= 0 then -1 else 1` SMT-Lib name: `bvsdiv`. -/ -def smtSDiv (s t : BitVec n) : BitVec n := - match s.msb, t.msb with - | false, false => smtUDiv s t - | false, true => .neg (smtUDiv s (.neg t)) - | true, false => .neg (smtUDiv (.neg s) t) - | true, true => smtUDiv (.neg s) (.neg t) +def smtSDiv (x y : BitVec n) : BitVec n := + match x.msb, y.msb with + | false, false => smtUDiv x y + | false, true => .neg (smtUDiv x (.neg y)) + | true, false => .neg (smtUDiv (.neg x) y) + | true, true => smtUDiv (.neg x) (.neg y) /-- Remainder for signed division rounding to zero. SMT_Lib name: `bvsrem`. -/ -def srem (s t : BitVec n) : BitVec n := - match s.msb, t.msb with - | false, false => umod s t - | false, true => umod s (.neg t) - | true, false => .neg (umod (.neg s) t) - | true, true => .neg (umod (.neg s) (.neg t)) +def srem (x y : BitVec n) : BitVec n := + match x.msb, y.msb with + | false, false => umod x y + | false, true => umod x (.neg y) + | true, false => .neg (umod (.neg x) y) + | true, true => .neg (umod (.neg x) (.neg y)) /-- Remainder for signed division rounded to negative infinity. SMT_Lib name: `bvsmod`. -/ -def smod (s t : BitVec m) : BitVec m := - match s.msb, t.msb with - | false, false => umod s t +def smod (x y : BitVec m) : BitVec m := + match x.msb, y.msb with + | false, false => umod x y | false, true => - let u := umod s (.neg t) - (if u = .zero m then u else .add u t) + let u := umod x (.neg y) + (if u = .zero m then u else .add u y) | true, false => - let u := umod (.neg s) t - (if u = .zero m then u else .sub t u) - | true, true => .neg (umod (.neg s) (.neg t)) + let u := umod (.neg x) y + (if u = .zero m then u else .sub y u) + | true, true => .neg (umod (.neg x) (.neg y)) end arithmetic From 579f2b28e5f3fd971981a7180d127703ff97fa60 Mon Sep 17 00:00:00 2001 From: Tobias Grosser Date: Wed, 7 Aug 2024 14:06:17 +0100 Subject: [PATCH 7/9] Update src/Init/Data/BitVec/Basic.lean Co-authored-by: AnotherAlexHere <153999274+AnotherAlexHere@users.noreply.github.com> --- src/Init/Data/BitVec/Basic.lean | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/Init/Data/BitVec/Basic.lean b/src/Init/Data/BitVec/Basic.lean index fa0572725cf1..d29cd2d1e6f1 100644 --- a/src/Init/Data/BitVec/Basic.lean +++ b/src/Init/Data/BitVec/Basic.lean @@ -69,7 +69,7 @@ protected def ofNat (n : Nat) (i : Nat) : BitVec n where instance instOfNat : OfNat (BitVec n) i where ofNat := .ofNat n i instance natCastInst : NatCast (BitVec w) := ⟨BitVec.ofNat w⟩ -/-- Given a bitvector `a`, return the underlying `Nat`. This is O(1) because `BitVec` is a +/-- Given a bitvector `x`, return the underlying `Nat`. This is O(1) because `BitVec` is a (zero-cost) wrapper around a `Nat`. -/ protected def toNat (x : BitVec n) : Nat := x.toFin.val From c7c566fbd155e2f1c2309850f5c4caea480c9909 Mon Sep 17 00:00:00 2001 From: Tobias Grosser Date: Wed, 7 Aug 2024 14:21:41 +0100 Subject: [PATCH 8/9] hr -> hy --- src/Init/Data/BitVec/Bitblast.lean | 12 ++++++------ 1 file changed, 6 insertions(+), 6 deletions(-) diff --git a/src/Init/Data/BitVec/Bitblast.lean b/src/Init/Data/BitVec/Bitblast.lean index 017dd6f27d55..e57f1c501d43 100644 --- a/src/Init/Data/BitVec/Bitblast.lean +++ b/src/Init/Data/BitVec/Bitblast.lean @@ -335,20 +335,20 @@ theorem mulRec_eq_mul_signExtend_truncate (x y : BitVec w) (s : Nat) : case zero => simp only [mulRec_zero_eq, ofNat_eq_ofNat, Nat.reduceAdd] by_cases y.getLsb 0 - case pos hr => - simp only [hr, ↓reduceIte, truncate, zeroExtend_one_eq_ofBool_getLsb_zero, - hr, ofBool_true, ofNat_eq_ofNat] + case pos hy => + simp only [hy, ↓reduceIte, truncate, zeroExtend_one_eq_ofBool_getLsb_zero, + ofBool_true, ofNat_eq_ofNat] rw [zeroExtend_ofNat_one_eq_ofNat_one_of_lt (by omega)] simp - case neg hr => - simp [hr, zeroExtend_one_eq_ofBool_getLsb_zero] + case neg hy => + simp [hy, zeroExtend_one_eq_ofBool_getLsb_zero] case succ s' hs => rw [mulRec_succ_eq, hs] have heq : (if y.getLsb (s' + 1) = true then x <<< (s' + 1) else 0) = (x * (y &&& (BitVec.twoPow w (s' + 1)))) := by simp only [ofNat_eq_ofNat, and_twoPow] - by_cases hr : y.getLsb (s' + 1) <;> simp [hr] + by_cases hy : y.getLsb (s' + 1) <;> simp [hy] rw [heq, ← BitVec.mul_add, ← zeroExtend_truncate_succ_eq_zeroExtend_truncate_add_twoPow] theorem getLsb_mul (x y : BitVec w) (i : Nat) : From 3fff2e2d1733aa24ee30e863911d76aac4b1e293 Mon Sep 17 00:00:00 2001 From: Tobias Grosser Date: Wed, 7 Aug 2024 14:26:55 +0100 Subject: [PATCH 9/9] rename two leftover instances --- src/Init/Data/BitVec/Lemmas.lean | 8 ++++---- 1 file changed, 4 insertions(+), 4 deletions(-) diff --git a/src/Init/Data/BitVec/Lemmas.lean b/src/Init/Data/BitVec/Lemmas.lean index 49a6ee4e6c70..7eada78a7ef4 100644 --- a/src/Init/Data/BitVec/Lemmas.lean +++ b/src/Init/Data/BitVec/Lemmas.lean @@ -869,15 +869,15 @@ theorem append_def (x : BitVec v) (y : BitVec w) : (x ++ y).toNat = x.toNat <<< n ||| y.toNat := rfl -@[simp] theorem getLsb_append {v : BitVec n} {w : BitVec m} : - getLsb (v ++ w) i = bif i < m then getLsb w i else getLsb v (i - m) := by +@[simp] theorem getLsb_append {x : BitVec n} {y : BitVec m} : + getLsb (x ++ y) i = bif i < m then getLsb y i else getLsb x (i - m) := by simp only [append_def, getLsb_or, getLsb_shiftLeftZeroExtend, getLsb_zeroExtend'] by_cases h : i < m · simp [h] · simp [h]; simp_all -@[simp] theorem getMsb_append {v : BitVec n} {w : BitVec m} : - getMsb (v ++ w) i = bif n ≤ i then getMsb w (i - n) else getMsb v i := by +@[simp] theorem getMsb_append {x : BitVec n} {y : BitVec m} : + getMsb (x ++ y) i = bif n ≤ i then getMsb y (i - n) else getMsb x i := by simp [append_def] by_cases h : n ≤ i · simp [h]