chore: actually fix inWordCompletion test

src/Init/Data/BitVec/Basic.lean

@@ -23,8 +23,10 @@ of SMT-LIBv2.
 -/
 
 /--
-A bitvector of the specified width. This is represented as the underlying `Nat` number
-in both the runtime and the kernel, inheriting all the special support for `Nat`.
+A bitvector of the specified width.
+
+This is represented as the underlying `Nat` number in both the runtime
+and the kernel, inheriting all the special support for `Nat`.
 -/
 structure BitVec (w : Nat) where
   /-- Construct a `BitVec w` from a number less than `2^w`.
@@ -49,16 +51,20 @@ instance : DecidableEq (BitVec n) := BitVec.decEq
 
 namespace BitVec
 
-/-- `cast eq i` embeds `i` into an equal `BitVec` type. -/
-@[inline] def cast (eq : n = m) (i : BitVec n) : BitVec m :=
-  .ofFin (Fin.cast (congrArg _ eq) i.toFin)
+section Nat
 
-/-- The `BitVec` with value `i mod 2^n`. Treated as an operation on bitvectors,
-this is truncation of the high bits when downcasting and zero-extension when upcasting. -/
+/-- The `BitVec` with value `i`, given a proof that `i < 2^n`. -/
+@[match_pattern]
+protected def ofNatLt {n : Nat} (i : Nat) (p : i < 2^n) : BitVec n where
+  toFin := ⟨i, p⟩
+
+/-- The `BitVec` with value `i mod 2^n`. -/
+@[match_pattern]
 protected def ofNat (n : Nat) (i : Nat) : BitVec n where
   toFin := Fin.ofNat' i (Nat.two_pow_pos n)
 
-instance : NatCast (BitVec w) := ⟨BitVec.ofNat w⟩
+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
 (zero-cost) wrapper around a `Nat`. -/
@@ -67,6 +73,43 @@ protected def toNat (a : BitVec n) : Nat := a.toFin.val
 /-- Return the bound in terms of toNat. -/
 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
+
+-- 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
+
+end Nat
+
+section subsingleton
+
+/-- All empty bitvectors are equal -/
+instance : Subsingleton (BitVec 0) where
+  allEq := by intro ⟨0, _⟩ ⟨0, _⟩; rfl
+
+/-- The empty bitvector -/
+abbrev nil : BitVec 0 := 0
+
+/-- Every bitvector of length 0 is equal to `nil`, i.e., there is only one empty bitvector -/
+theorem eq_nil (x : BitVec 0) : x = nil := Subsingleton.allEq ..
+
+end subsingleton
+
+section zero_allOnes
+
+/-- Return a bitvector `0` of size `n`. This is the bitvector with all zero bits. -/
+protected def zero (n : Nat) : BitVec n := .ofNatLt 0 (Nat.two_pow_pos n)
+instance : Inhabited (BitVec n) where default := .zero n
+
+/-- Bit vector of size `n` where all bits are `1`s -/
+def allOnes (n : Nat) : BitVec n :=
+  .ofNatLt (2^n - 1) (Nat.le_of_eq (Nat.sub_add_cancel (Nat.two_pow_pos n)))
+
+end zero_allOnes
+
+section getXsb
+
 /-- Return the `i`-th least significant bit or `false` if `i ≥ w`. -/
 @[inline] def getLsb (x : BitVec w) (i : Nat) : Bool := x.toNat.testBit i
 
@@ -76,29 +119,48 @@ theorem isLt (x : BitVec w) : x.toNat < 2^w := x.toFin.isLt
 /-- Return most-significant bit in bitvector. -/
 @[inline] protected def msb (a : BitVec n) : Bool := getMsb a 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 a.msb then Int.ofNat a.toNat - Int.ofNat (2^n) else a.toNat
 
-/-- Return a bitvector `0` of size `n`. This is the bitvector with all zero bits. -/
-protected def zero (n : Nat) : BitVec n := ⟨0, Nat.two_pow_pos n⟩
+/-- The `BitVec` with value `(2^n + (i mod 2^n)) mod 2^n`.  -/
+protected def ofInt (n : Nat) (i : Int) : BitVec n :=
+  match i with
+  | Int.ofNat x => .ofNat n x
+  | Int.negSucc x => BitVec.ofNatLt (2^n - x % 2^n - 1) (by omega)
 
-instance : Inhabited (BitVec n) where default := .zero n
+instance : IntCast (BitVec w) := ⟨BitVec.ofInt w⟩
 
-instance instOfNat : OfNat (BitVec n) i where ofNat := .ofNat n i
+end Int
+
+section Syntax
 
 /-- Notation for bit vector literals. `i#n` is a shorthand for `BitVec.ofNat n i`. -/
 scoped syntax:max term:max noWs "#" noWs term:max : term
 macro_rules | `($i#$n) => `(BitVec.ofNat $n $i)
 
-/- Support for `i#n` notation in patterns.  -/
-attribute [match_pattern] BitVec.ofNat
-
 /-- Unexpander for bit vector literals. -/
 @[app_unexpander BitVec.ofNat] def unexpandBitVecOfNat : Lean.PrettyPrinter.Unexpander
   | `($(_) $n $i) => `($i#$n)
   | _ => throw ()
 
+/-- Notation for bit vector literals without truncation. `i#'lt` is a shorthand for `BitVec.ofNatLt i lt`. -/
+scoped syntax:max term:max noWs "#'" noWs term:max : term
+macro_rules | `($i#'$p) => `(BitVec.ofNatLt $i $p)
+
+/-- Unexpander for bit vector literals without truncation. -/
+@[app_unexpander BitVec.ofNatLt] def unexpandBitVecOfNatLt : Lean.PrettyPrinter.Unexpander
+  | `($(_) $i $p) => `($i#'$p)
+  | _ => throw ()
+
+end Syntax
+
+section repr_toString
+
 /-- Convert bitvector into a fixed-width hex number. -/
 protected def toHex {n : Nat} (x : BitVec n) : String :=
   let s := (Nat.toDigits 16 x.toNat).asString
@@ -106,13 +168,11 @@ protected def toHex {n : Nat} (x : BitVec n) : String :=
   t ++ s
 
 instance : Repr (BitVec n) where reprPrec a _ := "0x" ++ (a.toHex : Format) ++ "#" ++ repr n
-
 instance : ToString (BitVec n) where toString a := toString (repr a)
 
-/-- 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 _ = BitVec.ofNat n i := rfl
-@[simp] theorem natCast_eq_ofNat : Nat.cast x = x#w := rfl
+end repr_toString
+
+section arithmetic
 
 /--
 Addition for bit vectors. This can be interpreted as either signed or unsigned addition
@@ -120,14 +180,14 @@ modulo `2^n`.
 
 SMT-Lib name: `bvadd`.
 -/
-protected def add (x y : BitVec n) : BitVec n where toFin := x.toFin + y.toFin
+protected def add (x y : BitVec n) : BitVec n := .ofNat n (x.toNat + y.toNat)
 instance : Add (BitVec n) := ⟨BitVec.add⟩
 
 /--
 Subtraction for bit vectors. This can be interpreted as either signed or unsigned subtraction
 modulo `2^n`.
 -/
-protected def sub (x y : BitVec n) : BitVec n where toFin := x.toFin - y.toFin
+protected def sub (x y : BitVec n) : BitVec n := .ofNat n (x.toNat + (2^n - y.toNat))
 instance : Sub (BitVec n) := ⟨BitVec.sub⟩
 
 /--
@@ -136,12 +196,9 @@ modulo `2^n`.
 
 SMT-Lib name: `bvneg`.
 -/
-protected def neg (x : BitVec n) : BitVec n := .sub 0 x
+protected def neg (x : BitVec n) : BitVec n := .ofNat n (2^n - x.toNat)
 instance : Neg (BitVec n) := ⟨.neg⟩
 
-/-- Bit vector of size `n` where all bits are `1`s -/
-def allOnes (n : Nat) : BitVec n := -1
-
 /--
 Return the absolute value of a signed bitvector.
 -/
@@ -153,13 +210,14 @@ modulo `2^n`.
 
 SMT-Lib name: `bvmul`.
 -/
-protected def mul (x y : BitVec n) : BitVec n := ofFin <| x.toFin * y.toFin
+protected def mul (x y : BitVec n) : BitVec n := BitVec.ofNat n (x.toNat * y.toNat)
 instance : Mul (BitVec n) := ⟨.mul⟩
 
 /--
 Unsigned division for bit vectors using the Lean convention where division by zero returns zero.
 -/
-def udiv (x y : BitVec n) : BitVec n := ofFin <| x.toFin / y.toFin
+def udiv (x y : BitVec n) : BitVec n :=
+  (x.toNat / y.toNat)#'(Nat.lt_of_le_of_lt (Nat.div_le_self _ _) x.isLt)
 instance : Div (BitVec n) := ⟨.udiv⟩
 
 /--
@@ -167,7 +225,8 @@ Unsigned modulo for bit vectors.
 
 SMT-Lib name: `bvurem`.
 -/
-def umod (x y : BitVec n) : BitVec n := ofFin <| x.toFin % y.toFin
+def umod (x y : BitVec n) : BitVec n :=
+  (x.toNat % y.toNat)#'(Nat.lt_of_le_of_lt (Nat.mod_le _ _) x.isLt)
 instance : Mod (BitVec n) := ⟨.umod⟩
 
 /--
@@ -177,7 +236,7 @@ where division by zero returns the `allOnes` bitvector.
 
 SMT-Lib name: `bvudiv`.
 -/
-def smtUDiv (x y : BitVec n) : BitVec n := if y = 0 then -1 else .udiv x y
+def smtUDiv (x y : BitVec n) : BitVec n := if y = 0 then allOnes n else udiv x y
 
 /--
 Signed t-division for bit vectors using the Lean convention where division
@@ -230,35 +289,54 @@ SMT_Lib name: `bvsmod`.
 -/
 def smod (s t : BitVec m) : BitVec m :=
   match s.msb, t.msb with
-  | false, false => .umod s t
+  | false, false => umod s t
   | false, true =>
-    let u := .umod s (.neg t)
-    (if u = BitVec.ofNat m 0 then u else .add u t)
+    let u := umod s (.neg t)
+    (if u = .zero m then u else .add u t)
   | true, false =>
-    let u := .umod (.neg s) t
-    (if u = BitVec.ofNat m 0 then u else .sub t u)
-  | true, true => .neg (.umod (.neg s) (.neg t))
+    let u := umod (.neg s) t
+    (if u = .zero m then u else .sub t u)
+  | true, true => .neg (umod (.neg s) (.neg t))
+
+end arithmetic
+
+
+section bool
+
+/-- Turn a `Bool` into a bitvector of length `1` -/
+def ofBool (b : Bool) : BitVec 1 := cond b 1 0
+
+@[simp] theorem ofBool_false : ofBool false = 0 := by trivial
+@[simp] theorem ofBool_true  : ofBool true  = 1 := by trivial
+
+/-- Fills a bitvector with `w` copies of the bit `b`. -/
+def fill (w : Nat) (b : Bool) : BitVec w := bif b then -1 else 0
+
+end bool
+
+section relations
 
 /--
 Unsigned less-than for bit vectors.
 
 SMT-Lib name: `bvult`.
 -/
-protected def ult (x y : BitVec n) : Bool := x.toFin < y.toFin
-instance : LT (BitVec n) where lt x y := x.toFin < y.toFin
+protected def ult (x y : BitVec n) : Bool := x.toNat < y.toNat
+
+instance : LT (BitVec n) where lt := (·.toNat < ·.toNat)
 instance (x y : BitVec n) : Decidable (x < y) :=
-  inferInstanceAs (Decidable (x.toFin < y.toFin))
+  inferInstanceAs (Decidable (x.toNat < y.toNat))
 
 /--
 Unsigned less-than-or-equal-to for bit vectors.
 
 SMT-Lib name: `bvule`.
 -/
-protected def ule (x y : BitVec n) : Bool := x.toFin ≤ y.toFin
+protected def ule (x y : BitVec n) : Bool := x.toNat ≤ y.toNat
 
-instance : LE (BitVec n) where le x y := x.toFin ≤ y.toFin
+instance : LE (BitVec n) where le := (·.toNat ≤ ·.toNat)
 instance (x y : BitVec n) : Decidable (x ≤ y) :=
-  inferInstanceAs (Decidable (x.toFin ≤ y.toFin))
+  inferInstanceAs (Decidable (x.toNat ≤ y.toNat))
 
 /--
 Signed less-than for bit vectors.
@@ -278,6 +356,87 @@ SMT-Lib name: `bvsle`.
 -/
 protected def sle (x y : BitVec n) : Bool := x.toInt ≤ y.toInt
 
+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)
+
+@[simp] theorem cast_ofNat {n m : Nat} (h : n = m) (x : Nat) :
+    cast h (BitVec.ofNat n x) = BitVec.ofNat m x := by
+  subst h; rfl
+
+@[simp] theorem cast_cast {n m k : Nat} (h₁ : n = m) (h₂ : m = k) (x : BitVec n) :
+    cast h₂ (cast h₁ x) = cast (h₁ ▸ h₂) x :=
+  rfl
+
+@[simp] theorem cast_eq {n : Nat} (h : n = n) (x : BitVec n) : cast h x = x := rfl
+
+/--
+Extraction of bits `start` to `start + len - 1` from a bit vector of size `n` to yield a
+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)
+
+/--
+Extraction of bits `hi` (inclusive) down to `lo` (inclusive) from a bit vector of size `n` to
+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
+
+/--
+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 :=
+  x.toNat#'(by
+    apply Nat.lt_of_lt_of_le x.isLt
+    exact Nat.pow_le_pow_of_le_right (by trivial) le)
+
+/--
+`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) :=
+  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)
+  (msbs.toNat <<< m)#'(shiftLeftLt msbs.isLt m)
+
+/--
+Zero extend vector `x` of length `w` by adding zeros in the high bits until it has length `v`.
+If `v < w` then it truncates the high bits instead.
+
+SMT-Lib name: `zero_extend`.
+-/
+def zeroExtend (v : Nat) (x : BitVec w) : BitVec v :=
+  if h : w ≤ v then
+    zeroExtend' h x
+  else
+    .ofNat v x.toNat
+
+/--
+Truncate the high bits of bitvector `x` of length `w`, resulting in a vector of length `v`.
+If `v > w` then it zero-extends the vector instead.
+-/
+abbrev truncate := @zeroExtend
+
+/--
+Sign extend a vector of length `w`, extending with `i` additional copies of the most significant
+bit in `x`. If `x` is an empty vector, then the sign is treated as zero.
+
+SMT-Lib name: `sign_extend`.
+-/
+def signExtend (v : Nat) (x : BitVec w) : BitVec v := .ofInt v x.toInt
+
+end cast
+
+section bitwise
+
 /--
 Bitwise AND for bit vectors.
 
@@ -287,8 +446,8 @@ Bitwise AND for bit vectors.
 
 SMT-Lib name: `bvand`.
 -/
-protected def and (x y : BitVec n) : BitVec n where toFin :=
-   ⟨x.toNat &&& y.toNat, Nat.and_lt_two_pow x.toNat y.isLt⟩
+protected def and (x y : BitVec n) : BitVec n :=
+  (x.toNat &&& y.toNat)#'(Nat.and_lt_two_pow x.toNat y.isLt)
 instance : AndOp (BitVec w) := ⟨.and⟩
 
 /--
@@ -300,8 +459,8 @@ Bitwise OR for bit vectors.
 
 SMT-Lib name: `bvor`.
 -/
-protected def or (x y : BitVec n) : BitVec n where toFin :=
-   ⟨x.toNat ||| y.toNat, Nat.or_lt_two_pow x.isLt y.isLt⟩
+protected def or (x y : BitVec n) : BitVec n :=
+  (x.toNat ||| y.toNat)#'(Nat.or_lt_two_pow x.isLt y.isLt)
 instance : OrOp (BitVec w) := ⟨.or⟩
 
 /--
@@ -313,8 +472,8 @@ instance : OrOp (BitVec w) := ⟨.or⟩
 
 SMT-Lib name: `bvxor`.
 -/
-protected def xor (x y : BitVec n) : BitVec n where toFin :=
-   ⟨x.toNat ^^^ y.toNat, Nat.xor_lt_two_pow x.isLt y.isLt⟩
+protected def xor (x y : BitVec n) : BitVec n :=
+  (x.toNat ^^^ y.toNat)#'(Nat.xor_lt_two_pow x.isLt y.isLt)
 instance : Xor (BitVec w) := ⟨.xor⟩
 
 /--
@@ -325,25 +484,16 @@ Bitwise NOT for bit vectors.
 ```
 SMT-Lib name: `bvnot`.
 -/
-protected def not (x : BitVec n) : BitVec n :=
-  allOnes n ^^^ x
+protected def not (x : BitVec n) : BitVec n := allOnes n ^^^ x
 instance : Complement (BitVec w) := ⟨.not⟩
 
-/-- The `BitVec` with value `(2^n + (i mod 2^n)) mod 2^n`.  -/
-protected def ofInt (n : Nat) (i : Int) : BitVec n :=
-  match i with
-  | Int.ofNat a => .ofNat n a
-  | Int.negSucc a => ~~~.ofNat n a
-
-instance : IntCast (BitVec w) := ⟨BitVec.ofInt w⟩
-
 /--
 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`.
 
 SMT-Lib name: `bvshl` except this operator uses a `Nat` shift value.
 -/
-protected def shiftLeft (a : BitVec n) (s : Nat) : BitVec n := .ofNat n (a.toNat <<< s)
+protected def shiftLeft (a : BitVec n) (s : Nat) : BitVec n := (a.toNat <<< s)#n
 instance : HShiftLeft (BitVec w) Nat (BitVec w) := ⟨.shiftLeft⟩
 
 /--
@@ -353,11 +503,11 @@ As a numeric operation, this is equivalent to `a / 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
+  (a.toNat >>> s)#'(by
   let ⟨a, lt⟩ := a
   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]
-  exact Nat.mul_lt_mul_of_lt_of_le' lt (Nat.two_pow_pos s) (Nat.le_refl 1)⟩
+  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⟩
 
@@ -395,25 +545,6 @@ SMT-Lib name: `rotate_right` except this operator uses a `Nat` shift amount.
 -/
 def rotateRight (x : BitVec w) (n : Nat) : BitVec w := x >>> n ||| x <<< (w - n)
 
-/--
-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 :=
-  ⟨x.toNat, by
-    apply Nat.lt_of_lt_of_le x.isLt
-    exact Nat.pow_le_pow_of_le_right (by trivial) le⟩
-
-/--
-`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) :=
-  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)
-  ⟨msbs.toNat <<< m, shiftLeftLt msbs.isLt m⟩
-
 /--
 Concatenation of bitvectors. This uses the "big endian" convention that the more significant
 input is on the left, so `0xAB#8 ++ 0xCD#8 = 0xABCD#16`.
@@ -425,21 +556,6 @@ def append (msbs : BitVec n) (lsbs : BitVec m) : BitVec (n+m) :=
 
 instance : HAppend (BitVec w) (BitVec v) (BitVec (w + v)) := ⟨.append⟩
 
-/--
-Extraction of bits `start` to `start + len - 1` from a bit vector of size `n` to yield a
-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)
-
-/--
-Extraction of bits `hi` (inclusive) down to `lo` (inclusive) from a bit vector of size `n` to
-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
-
 -- TODO: write this using multiplication
 /-- `replicate i x` concatenates `i` copies of `x` into a new vector of length `w*i`. -/
 def replicate : (i : Nat) → BitVec w → BitVec (w*i)
@@ -449,70 +565,6 @@ def replicate : (i : Nat) → BitVec w → BitVec (w*i)
       rw [Nat.mul_add, Nat.add_comm, Nat.mul_one]
     hEq ▸ (x ++ replicate n x)
 
-/-- Fills a bitvector with `w` copies of the bit `b`. -/
-def fill (w : Nat) (b : Bool) : BitVec w := bif b then -1 else 0
-
-/--
-Zero extend vector `x` of length `w` by adding zeros in the high bits until it has length `v`.
-If `v < w` then it truncates the high bits instead.
-
-SMT-Lib name: `zero_extend`.
--/
-def zeroExtend (v : Nat) (x : BitVec w) : BitVec v :=
-  if h : w ≤ v then
-    zeroExtend' h x
-  else
-    .ofNat v x.toNat
-
-/--
-Truncate the high bits of bitvector `x` of length `w`, resulting in a vector of length `v`.
-If `v > w` then it zero-extends the vector instead.
--/
-abbrev truncate := @zeroExtend
-
-/--
-Sign extend a vector of length `w`, extending with `i` additional copies of the most significant
-bit in `x`. If `x` is an empty vector, then the sign is treated as zero.
-
-SMT-Lib name: `sign_extend`.
--/
-def signExtend (v : Nat) (x : BitVec w) : BitVec v := .ofInt v x.toInt
-
-/-! We add simp-lemmas that rewrite bitvector operations into the equivalent notation -/
-@[simp] theorem append_eq (x : BitVec w) (y : BitVec v)   : BitVec.append x y = x ++ y        := rfl
-@[simp] theorem shiftLeft_eq (x : BitVec w) (n : Nat)     : BitVec.shiftLeft x n = x <<< n    := rfl
-@[simp] theorem ushiftRight_eq (x : BitVec w) (n : Nat)   : BitVec.ushiftRight x n = x >>> n  := rfl
-@[simp] theorem not_eq (x : BitVec w)                     : BitVec.not x = ~~~x               := rfl
-@[simp] theorem and_eq (x y : BitVec w)                   : BitVec.and x y = x &&& y          := rfl
-@[simp] theorem or_eq (x y : BitVec w)                    : BitVec.or x y = x ||| y           := rfl
-@[simp] theorem xor_eq (x y : BitVec w)                   : BitVec.xor x y = x ^^^ y          := rfl
-@[simp] theorem neg_eq (x : BitVec w)                     : BitVec.neg x = -x                 := rfl
-@[simp] theorem add_eq (x y : BitVec w)                   : BitVec.add x y = x + y            := rfl
-@[simp] theorem sub_eq (x y : BitVec w)                   : BitVec.sub x y = x - y            := rfl
-@[simp] theorem mul_eq (x y : BitVec w)                   : BitVec.mul x y = x * y            := rfl
-@[simp] theorem zero_eq                                   : BitVec.zero n = 0#n               := rfl
-
-@[simp] theorem cast_ofNat {n m : Nat} (h : n = m) (x : Nat) :
-    cast h (BitVec.ofNat n x) = BitVec.ofNat m x := by
-  subst h; rfl
-
-@[simp] theorem cast_cast {n m k : Nat} (h₁ : n = m) (h₂ : m = k) (x : BitVec n) :
-    cast h₂ (cast h₁ x) = cast (h₁ ▸ h₂) x :=
-  rfl
-
-@[simp] theorem cast_eq {n : Nat} (h : n = n) (x : BitVec n) :
-    cast h x = x :=
-  rfl
-
-/-- Turn a `Bool` into a bitvector of length `1` -/
-def ofBool (b : Bool) : BitVec 1 := cond b 1 0
-
-@[simp] theorem ofBool_false : ofBool false = 0 := by trivial
-@[simp] theorem ofBool_true  : ofBool true  = 1 := by trivial
-
-/-- The empty bitvector -/
-abbrev nil : BitVec 0 := 0
-
 /-!
 ### Cons and Concat
 We give special names to the operations of adding a single bit to either end of a bitvector.
@@ -530,14 +582,6 @@ def concat {n} (msbs : BitVec n) (lsb : Bool) : BitVec (n+1) := msbs ++ (ofBool
 def cons {n} (msb : Bool) (lsbs : BitVec n) : BitVec (n+1) :=
   ((ofBool msb) ++ lsbs).cast (Nat.add_comm ..)
 
-/-- All empty bitvectors are equal -/
-instance : Subsingleton (BitVec 0) where
-  allEq := by intro ⟨0, _⟩ ⟨0, _⟩; rfl
-
-/-- Every bitvector of length 0 is equal to `nil`, i.e., there is only one empty bitvector -/
-theorem eq_nil : ∀ (x : BitVec 0), x = nil
-  | ofFin ⟨0, _⟩ => rfl
-
 theorem append_ofBool (msbs : BitVec w) (lsb : Bool) :
     msbs ++ ofBool lsb = concat msbs lsb :=
   rfl
@@ -545,3 +589,21 @@ theorem append_ofBool (msbs : BitVec w) (lsb : Bool) :
 theorem ofBool_append (msb : Bool) (lsbs : BitVec w) :
     ofBool msb ++ lsbs = (cons msb lsbs).cast (Nat.add_comm ..) :=
   rfl
+
+end bitwise
+
+section normalization_eqs
+/-! We add simp-lemmas that rewrite bitvector operations into the equivalent notation -/
+@[simp] theorem append_eq (x : BitVec w) (y : BitVec v)   : BitVec.append x y = x ++ y        := rfl
+@[simp] theorem shiftLeft_eq (x : BitVec w) (n : Nat)     : BitVec.shiftLeft x n = x <<< n    := rfl
+@[simp] theorem ushiftRight_eq (x : BitVec w) (n : Nat)   : BitVec.ushiftRight x n = x >>> n  := rfl
+@[simp] theorem not_eq (x : BitVec w)                     : BitVec.not x = ~~~x               := rfl
+@[simp] theorem and_eq (x y : BitVec w)                   : BitVec.and x y = x &&& y          := rfl
+@[simp] theorem or_eq (x y : BitVec w)                    : BitVec.or x y = x ||| y           := rfl
+@[simp] theorem xor_eq (x y : BitVec w)                   : BitVec.xor x y = x ^^^ y          := rfl
+@[simp] theorem neg_eq (x : BitVec w)                     : BitVec.neg x = -x                 := rfl
+@[simp] theorem add_eq (x y : BitVec w)                   : BitVec.add x y = x + y            := rfl
+@[simp] theorem sub_eq (x y : BitVec w)                   : BitVec.sub x y = x - y            := rfl
+@[simp] theorem mul_eq (x y : BitVec w)                   : BitVec.mul x y = x * y            := rfl
+@[simp] theorem zero_eq                                   : BitVec.zero n = 0#n               := rfl
+end normalization_eqs

src/Init/Data/BitVec/Lemmas.lean

@@ -92,6 +92,12 @@ theorem ofBool_eq_iff_eq : ∀(b b' : Bool), BitVec.ofBool b = BitVec.ofBool b'
 
 @[simp] 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 [BitVec.toNat, BitVec.ofNat, Fin.ofNat']
 
@@ -109,18 +115,6 @@ theorem getLsb_ofNat (n : Nat) (x : Nat) (i : Nat) :
 private theorem lt_two_pow_of_le {x m n : Nat} (lt : x < 2 ^ m) (le : m ≤ n) : x < 2 ^ n :=
   Nat.lt_of_lt_of_le lt (Nat.pow_le_pow_of_le_right (by trivial : 0 < 2) le)
 
-@[simp] theorem ofNat_toNat (m : Nat) (x : BitVec n) : x.toNat#m = truncate m x := by
-  let ⟨x, lt_n⟩ := x
-  unfold truncate
-  unfold zeroExtend
-  if h : n ≤ m then
-    unfold zeroExtend'
-    have lt_m : x < 2 ^ m := lt_two_pow_of_le lt_n h
-    simp [h, lt_m, Nat.mod_eq_of_lt, BitVec.toNat, BitVec.ofNat, Fin.ofNat']
-  else
-    simp [h]
-
-
 /-! ### msb -/
 
 theorem msb_eq_decide (x : BitVec (Nat.succ w)) : BitVec.msb x = decide (2 ^ w ≤ x.toNat) := by
@@ -167,6 +161,9 @@ 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 :=
+  toNat_zeroExtend i x
+
 @[simp] theorem zeroExtend_eq (x : BitVec n) : zeroExtend n x = x := by
   apply eq_of_toNat_eq
   let ⟨x, lt_n⟩ := x
@@ -178,8 +175,9 @@ theorem toNat_zeroExtend (i : Nat) (x : BitVec n) :
 
 @[simp] theorem truncate_eq (x : BitVec n) : truncate n x = x := zeroExtend_eq x
 
-@[simp] theorem toNat_truncate (x : BitVec n) : (truncate i x).toNat = x.toNat % 2^i :=
-  toNat_zeroExtend i x
+@[simp] theorem ofNat_toNat (m : Nat) (x : BitVec n) : x.toNat#m = truncate m x := by
+  apply eq_of_toNat_eq
+  simp
 
 @[simp] theorem getLsb_zeroExtend' (ge : m ≥ n) (x : BitVec n) (i : Nat) :
     getLsb (zeroExtend' ge x) i = getLsb x i := by
@@ -219,31 +217,12 @@ protected theorem extractLsb_ofNat (x n : Nat) (hi lo : Nat) :
 
 /-! ### allOnes -/
 
-private theorem allOnes_def :
-    allOnes v = .ofFin (⟨0, Nat.two_pow_pos v⟩ - ⟨1 % 2^v, Nat.mod_lt _ (Nat.two_pow_pos v)⟩) := by
-  rfl
-
 @[simp] theorem toNat_allOnes : (allOnes v).toNat = 2^v - 1 := by
-  simp only [allOnes_def, toNat_ofFin, Fin.coe_sub, Nat.zero_add]
-  by_cases h : v = 0
-  · subst h
-    rfl
-  · rw [Nat.mod_eq_of_lt (Nat.one_lt_two_pow h), Nat.mod_eq_of_lt]
-    exact Nat.pred_lt_self (Nat.two_pow_pos v)
+  unfold allOnes
+  simp
 
 @[simp] theorem getLsb_allOnes : (allOnes v).getLsb i = decide (i < v) := by
-  simp only [allOnes_def, getLsb_ofFin, Fin.coe_sub, Nat.zero_add, Nat.testBit_mod_two_pow]
-  if h : i < v then
-    simp only [h, decide_True, Bool.true_and]
-    match i, v, h with
-    | i, (v + 1), h =>
-      rw [Nat.mod_eq_of_lt (by simp), Nat.testBit_two_pow_sub_one]
-      simp [h]
-  else
-    simp [h]
-
-@[simp] theorem negOne_eq_allOnes : -1#w = allOnes w :=
-  rfl
+  simp [allOnes]
 
 /-! ### or -/
 
@@ -252,10 +231,9 @@ private theorem allOnes_def :
 
 @[simp] theorem toFin_or (x y : BitVec v) :
     BitVec.toFin (x ||| y) = BitVec.toFin x ||| BitVec.toFin y := by
-  simp only [HOr.hOr, OrOp.or, BitVec.or, Fin.lor, val_toFin, Fin.mk.injEq]
+  apply Fin.eq_of_val_eq
   exact (Nat.mod_eq_of_lt <| Nat.or_lt_two_pow x.isLt y.isLt).symm
 
-
 @[simp] theorem getLsb_or {x y : BitVec v} : (x ||| y).getLsb i = (x.getLsb i || y.getLsb i) := by
   rw [← testBit_toNat, getLsb, getLsb]
   simp
@@ -267,7 +245,7 @@ private theorem allOnes_def :
 
 @[simp] theorem toFin_and (x y : BitVec v) :
     BitVec.toFin (x &&& y) = BitVec.toFin x &&& BitVec.toFin y := by
-  simp only [HAnd.hAnd, AndOp.and, BitVec.and, Fin.land, val_toFin, Fin.mk.injEq]
+  apply Fin.eq_of_val_eq
   exact (Nat.mod_eq_of_lt <| Nat.and_lt_two_pow _ y.isLt).symm
 
 @[simp] theorem getLsb_and {x y : BitVec v} : (x &&& y).getLsb i = (x.getLsb i && y.getLsb i) := by
@@ -281,7 +259,7 @@ private theorem allOnes_def :
 
 @[simp] theorem toFin_xor (x y : BitVec v) :
     BitVec.toFin (x ^^^ y) = BitVec.toFin x ^^^ BitVec.toFin y := by
-  simp only [HXor.hXor, Xor.xor, BitVec.xor, Fin.xor, val_toFin, Fin.mk.injEq]
+  apply Fin.eq_of_val_eq
   exact (Nat.mod_eq_of_lt <| Nat.xor_lt_two_pow x.isLt y.isLt).symm
 
 @[simp] theorem getLsb_xor {x y : BitVec v} :
@@ -497,6 +475,15 @@ theorem add_sub_cancel (x y : BitVec w) : x + y - y = x := by
   rw [toNat_sub, toNat_add, Nat.mod_add_mod, Nat.add_assoc, ← Nat.add_sub_assoc y_toNat_le,
     Nat.add_sub_cancel_left, Nat.add_mod_right, toNat_mod_cancel]
 
+theorem negOne_eq_allOnes : -1#w = allOnes w := by
+  apply eq_of_toNat_eq
+  if g : w = 0 then
+    simp [g]
+  else
+    have q : 1 < 2^w := by simp [g]
+    have r : (2^w - 1) < 2^w := by omega
+    simp [Nat.mod_eq_of_lt q, Nat.mod_eq_of_lt r]
+
 /-! ### mul -/
 
 theorem mul_def {n} {x y : BitVec n} : x * y = (ofFin <| x.toFin * y.toFin) := by rfl

tests/lean/interactive/inWordCompletion.lean

@@ -1,15 +1,14 @@
-def gfabc (x : Nat) := x
-def gfacc (x : Nat) := x
-def gfadc (x : Nat) := x
-def gfbbc (x : Nat) := x
+def gfxabc (x : Nat) := x
+def gfxacc (x : Nat) := x
+def gfxadc (x : Nat) := x
+def gfxbbc (x : Nat) := x
+#check gfxabc
+         --^ textDocument/completion
 
-#check gfabc
-        --^ textDocument/completion
+def Boo.gfxabc (x : Nat) := x
+def Boo.gfxacc (x : Nat) := x
+def Boo.gfxadc (x : Nat) := x
+def Boo.gfxbbc (x : Nat) := x
 
-def Boo.gfabc (x : Nat) := x
-def Boo.gfacc (x : Nat) := x
-def Boo.gfadc (x : Nat) := x
-def Boo.gfbbc (x : Nat) := x
-
-#check Boo.gfabc
-            --^ textDocument/completion
+#check Boo.gfxabc
+             --^ textDocument/completion

tests/lean/interactive/inWordCompletion.lean.expected.out

@@ -1,18 +1,14 @@
 {"textDocument": {"uri": "file:///inWordCompletion.lean"},
- "position": {"line": 5, "character": 10}}
+ "position": {"line": 4, "character": 11}}
 {"items":
- [{"label": "gfabc", "kind": 3, "detail": "Nat → Nat"},
-  {"label": "gfacc", "kind": 3, "detail": "Nat → Nat"},
-  {"label": "gfadc", "kind": 3, "detail": "Nat → Nat"},
-  {"label": "Std.BitVec.getLsb_ofNat",
-   "kind": 3,
-   "detail":
-   "∀ (n x i : Nat), Std.BitVec.getLsb (x#n) i = (decide (i < n) && Nat.testBit x i)"}],
+ [{"label": "gfxabc", "kind": 3, "detail": "Nat → Nat"},
+  {"label": "gfxacc", "kind": 3, "detail": "Nat → Nat"},
+  {"label": "gfxadc", "kind": 3, "detail": "Nat → Nat"}],
  "isIncomplete": true}
 {"textDocument": {"uri": "file:///inWordCompletion.lean"},
- "position": {"line": 13, "character": 14}}
+ "position": {"line": 12, "character": 15}}
 {"items":
- [{"label": "gfabc", "kind": 3, "detail": "Nat → Nat"},
-  {"label": "gfacc", "kind": 3, "detail": "Nat → Nat"},
-  {"label": "gfadc", "kind": 3, "detail": "Nat → Nat"}],
+ [{"label": "gfxabc", "kind": 3, "detail": "Nat → Nat"},
+  {"label": "gfxacc", "kind": 3, "detail": "Nat → Nat"},
+  {"label": "gfxadc", "kind": 3, "detail": "Nat → Nat"}],
  "isIncomplete": true}