diff --git a/src/Init/Data/BitVec/Lemmas.lean b/src/Init/Data/BitVec/Lemmas.lean index b62d1020296d..ad6cd521f71b 100644 --- a/src/Init/Data/BitVec/Lemmas.lean +++ b/src/Init/Data/BitVec/Lemmas.lean @@ -1127,6 +1127,11 @@ theorem not_eq_comm {x y : BitVec w} : ~~~ x = y ↔ x = ~~~ y := by BitVec.toNat (x <<< n) = BitVec.toNat x <<< n % 2^v := BitVec.toNat_ofNat _ _ +@[simp] theorem toInt_shiftLeft {n : Nat} {x : BitVec v} : + BitVec.toInt (x <<< n) = Int.bmod (BitVec.toInt x * 2^n) (2^v) := by + simp [toInt_eq_toNat_bmod, Nat.shiftLeft_eq] + norm_cast + @[simp] theorem toFin_shiftLeft {n : Nat} (x : BitVec w) : BitVec.toFin (x <<< n) = Fin.ofNat' (2^w) (x.toNat <<< n) := rfl @@ -1826,6 +1831,14 @@ theorem msb_append {x : BitVec w} {y : BitVec v} : ext simp only [getLsbD_append, getLsbD_zero, Bool.cond_self] +@[simp] theorem append_zero {n m : Nat} {x : BitVec n} : + x ++ 0#m = x.setWidth (n + m) <<< m := by + induction m + case zero => + simp + case succ i ih => + sorry + def lhs (x : BitVec n) (y : BitVec m) : Int := (x++y).toInt def rhs (x : BitVec n) (y : BitVec m) : Int := if n == 0 then y.toInt else (x.toInt * (2^m)) + y.toNat @@ -1851,7 +1864,27 @@ def test : Bool := Id.run do · subst n0 simp [BitVec.eq_nil x] · simp [n0] - sorry + by_cases y0 : y = 0 + · + have xlt := BitVec.isLt x + have hh : 2 ^ n < 2 ^ (n + m) := sorry + have h2 : x.toNat <<< m % 2 ^ (n + m) = x.toNat <<< m := sorry + simp only [y0] + simp only [ofNat_eq_ofNat, append_zero] + rw [toInt_eq_toNat_cond] + rw [toInt_eq_toNat_cond] + split + <;> split + <;> norm_cast + <;> simp + <;> rw [Nat.mod_eq_of_lt (a := x.toNat) (by omega)] + <;> norm_cast + <;> simp [h2] + rw [Nat.shiftLeft_eq] + <;> simp_all + · sorry + · sorry + · simp [Nat.shiftLeft_eq, Int.sub_mul, Nat.pow_add] @[simp] theorem cast_append_right (h : w + v = w + v') (x : BitVec w) (y : BitVec v) : cast h (x ++ y) = x ++ cast (by omega) y := by