fix: Fix timeout in bitvector pattern matches. (#501)

Std/Data/BitVec/Basic.lean

@@ -44,11 +44,7 @@ namespace BitVec
 /-- 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. -/
 protected def ofNat (n : Nat) (i : Nat) : BitVec n where
-  toFin :=
-    let p : i &&& 2^n-1 < 2^n := by
-        apply Nat.and_lt_two_pow
-        exact Nat.sub_lt (Nat.pow_two_pos n) (Nat.le_refl 1)
-    ⟨i &&& 2^n-1, p⟩
+  toFin := Fin.ofNat' i (Nat.pow_two_pos n)
 
 /-- Given a bitvector `a`, return the underlying `Nat`. This is O(1) because `BitVec` is a
 (zero-cost) wrapper around a `Nat`. -/

Std/Data/BitVec/Lemmas.lean

@@ -57,7 +57,7 @@ theorem eq_of_getMsb_eq {x y : BitVec w}
 @[simp] theorem toNat_ofFin (x : Fin (2^n)) : (BitVec.ofFin x).toNat = x.val := rfl
 
 theorem toNat_ofNat (x w : Nat) : (BitVec.ofNat w x).toNat = x % 2^w := by
-  simp [BitVec.toNat, BitVec.ofNat]
+  simp [BitVec.toNat, BitVec.ofNat, Fin.ofNat']
 
 @[simp] theorem toNat_zero (n : Nat) : (0#n).toNat = 0 := by trivial
 
@@ -71,7 +71,7 @@ private theorem lt_two_pow_of_le {x m n : Nat} (lt : x < 2 ^ m) (le : m ≤ n) :
   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]
+    simp [h, lt_m, Nat.mod_eq_of_lt, BitVec.toNat, BitVec.ofNat, Fin.ofNat']
   else
     simp [h]
 

test/bitvec.lean

@@ -1,5 +1,5 @@
 import Std.Tactic.GuardExpr
-import Std.Data.BitVec.Basic
+import Std.Data.BitVec
 
 open Std.BitVec
 
@@ -94,6 +94,20 @@ open Std.BitVec
 #guard extractLsb 7 4 0x1234#16 = 3
 #guard extractLsb' 0 4 0x1234#16 = 0x4#4
 
+open Std
+
+/--
+This tests the match compiler with bitvector literals to ensure
+it can successfully generate a pattern for a bitvector literals.
+
+This fixes a regression introduced in PR #366.
+-/
+def testMatch8 (i : BitVec 32) :=
+  let op1 := i.extractLsb 28 25
+  match op1 with
+  | 0b1000#4 => some 0
+  | _ => none
+
 -- Pretty-printing
 
 #guard toString 5#12 = "0x005#12"