feat: decidable quantifers for BitVec (#5418)

src/Init/Data/BitVec/Lemmas.lean

@@ -1476,7 +1476,7 @@ theorem setWidth_succ (x : BitVec w) :
     have j_lt : j.val < i := Nat.lt_of_le_of_ne (Nat.le_of_succ_le_succ j.isLt) j_eq
     simp [j_eq, j_lt]
 
-theorem eq_msb_cons_setWidth (x : BitVec (w+1)) : x = (cons x.msb (x.setWidth w)) := by
+@[simp] theorem cons_msb_setWidth (x : BitVec (w+1)) : (cons x.msb (x.setWidth w)) = x := by
   ext i
   simp
   split <;> rename_i h
@@ -1485,6 +1485,10 @@ theorem eq_msb_cons_setWidth (x : BitVec (w+1)) : x = (cons x.msb (x.setWidth w)
     · simp_all
     · omega
 
+@[deprecated "Use the reverse direction of `cons_msb_setWidth`"]
+theorem eq_msb_cons_setWidth (x : BitVec (w+1)) : x = (cons x.msb (x.setWidth w)) := by
+  simp
+
 @[simp] theorem not_cons (x : BitVec w) (b : Bool) : ~~~(cons b x) = cons (!b) (~~~x) := by
   simp [cons]
 
@@ -2195,6 +2199,71 @@ theorem toNat_sub_of_le {x y : BitVec n} (h : y ≤ x) :
   · have : 2 ^ n - y.toNat + x.toNat = 2 ^ n + (x.toNat - y.toNat) := by omega
     rw [this, Nat.add_mod_left, Nat.mod_eq_of_lt (by omega)]
 
+/-! ### Decidable quantifiers -/
+
+theorem forall_zero_iff {P : BitVec 0 → Prop} :
+    (∀ v, P v) ↔ P 0#0 := by
+  constructor
+  · intro h
+    apply h
+  · intro h v
+    obtain (rfl : v = 0#0) := (by ext ⟨i, h⟩; simp at h)
+    apply h
+
+theorem forall_cons_iff {P : BitVec (n + 1) → Prop} :
+    (∀ v : BitVec (n + 1), P v) ↔ (∀ (x : Bool) (v : BitVec n), P (v.cons x)) := by
+  constructor
+  · intro h _ _
+    apply h
+  · intro h v
+    have w : v = (v.setWidth n).cons v.msb := by simp
+    rw [w]
+    apply h
+
+instance instDecidableForallBitVecZero (P : BitVec 0 → Prop) :
+    ∀ [Decidable (P 0#0)], Decidable (∀ v, P v)
+  | .isTrue h => .isTrue fun v => by
+    obtain (rfl : v = 0#0) := (by ext ⟨i, h⟩; cases h)
+    exact h
+  | .isFalse h => .isFalse (fun w => h (w _))
+
+instance instDecidableForallBitVecSucc (P : BitVec (n+1) → Prop) [DecidablePred P]
+    [Decidable (∀ (x : Bool) (v : BitVec n), P (v.cons x))] : Decidable (∀ v, P v) :=
+  decidable_of_iff' (∀ x (v : BitVec n), P (v.cons x)) forall_cons_iff
+
+instance instDecidableExistsBitVecZero (P : BitVec 0 → Prop) [Decidable (P 0#0)] :
+    Decidable (∃ v, P v) :=
+  decidable_of_iff (¬ ∀ v, ¬ P v) Classical.not_forall_not
+
+instance instDecidableExistsBitVecSucc (P : BitVec (n+1) → Prop) [DecidablePred P]
+    [Decidable (∀ (x : Bool) (v : BitVec n), ¬ P (v.cons x))] : Decidable (∃ v, P v) :=
+  decidable_of_iff (¬ ∀ v, ¬ P v) Classical.not_forall_not
+
+/--
+For small numerals this isn't necessary (as typeclass search can use the above two instances),
+but for large numerals this provides a shortcut.
+Note, however, that for large numerals the decision procedure may be very slow,
+and you should use `bv_decide` if possible.
+-/
+instance instDecidableForallBitVec :
+    ∀ (n : Nat) (P : BitVec n → Prop) [DecidablePred P], Decidable (∀ v, P v)
+  | 0, _, _ => inferInstance
+  | n + 1, _, _ =>
+    have := instDecidableForallBitVec n
+    inferInstance
+
+/--
+For small numerals this isn't necessary (as typeclass search can use the above two instances),
+but for large numerals this provides a shortcut.
+Note, however, that for large numerals the decision procedure may be very slow.
+-/
+instance instDecidableExistsBitVec :
+    ∀ (n : Nat) (P : BitVec n → Prop) [DecidablePred P], Decidable (∃ v, P v)
+  | 0, _, _ => inferInstance
+  | n + 1, _, _ =>
+    have := instDecidableExistsBitVec n
+    inferInstance
+
 /-! ### Deprecations -/
 
 set_option linter.missingDocs false

tests/lean/run/bitvec.lean

@@ -75,17 +75,17 @@ open BitVec
 
 -- get/extract
 
-#guard !getMsb 0b0101#4 0
-#guard getMsb 0b0101#4 1
-#guard !getMsb 0b0101#4 2
-#guard getMsb 0b0101#4 3
-#guard !getMsb 0b1111#4 4
-
-#guard getLsb 0b0101#4 0
-#guard !getLsb 0b0101#4 1
-#guard getLsb 0b0101#4 2
-#guard !getLsb 0b0101#4 3
-#guard !getLsb 0b1111#4 4
+#guard !getMsbD 0b0101#4 0
+#guard getMsbD 0b0101#4 1
+#guard !getMsbD 0b0101#4 2
+#guard getMsbD 0b0101#4 3
+#guard !getMsbD 0b1111#4 4
+
+#guard getLsbD 0b0101#4 0
+#guard !getLsbD 0b0101#4 1
+#guard getLsbD 0b0101#4 2
+#guard !getLsbD 0b0101#4 3
+#guard !getLsbD 0b1111#4 4
 
 #guard extractLsb 3 0 0x1234#16 = 4
 #guard extractLsb 7 4 0x1234#16 = 3
@@ -114,3 +114,10 @@ def testMatch8 (i : BitVec 32) :=
 
 example (n w : Nat) (p : n < 2^w) : { toFin := { val := n, isLt := p } : BitVec w} = .ofNat w n := by
   simp only [ofFin_eq_ofNat]
+
+-- Decidable quantifiers
+
+example : ∀ v : BitVec 2, (v[1] && v[0]) = (v[0] && v[1]) := by decide
+
+ -- `bv_decide` doesn't yet do existentials:
+example : ∃ x y : BitVec 5, x ^^^ y = allOnes 5 := by decide