.

src/Init/Data/Nat/Bitwise/Lemmas.lean

@@ -51,24 +51,24 @@ noncomputable def div2Induction {motive : Nat → Sort u}
       apply hyp
       exact Nat.div_lt_self n_pos (Nat.le_refl _)
 
-@[simp] theorem zero_and (x : Nat) : 0 &&& x = 0 := by
+@[simp, grind =] theorem zero_and (x : Nat) : 0 &&& x = 0 := by
   simp only [HAnd.hAnd, AndOp.and, land]
   unfold bitwise
   simp
 
-@[simp] theorem and_zero (x : Nat) : x &&& 0 = 0 := by
+@[simp, grind =] theorem and_zero (x : Nat) : x &&& 0 = 0 := by
   simp only [HAnd.hAnd, AndOp.and, land]
   unfold bitwise
   simp
 
-@[simp] theorem one_and_eq_mod_two (n : Nat) : 1 &&& n = n % 2 := by
+@[simp, grind =] theorem one_and_eq_mod_two (n : Nat) : 1 &&& n = n % 2 := by
   if n0 : n = 0 then
     subst n0; decide
   else
     simp only [HAnd.hAnd, AndOp.and, land]
     cases mod_two_eq_zero_or_one n with | _ h => simp [bitwise, n0, h]
 
-@[simp] theorem and_one_is_mod (x : Nat) : x &&& 1 = x % 2 := by
+@[simp, grind =] theorem and_one_is_mod (x : Nat) : x &&& 1 = x % 2 := by
   if xz : x = 0 then
     simp [xz, zero_and]
   else
@@ -102,11 +102,12 @@ Depending on use cases either `testBit_add_one` or `testBit_div_two`
 may be more useful as a `simp` lemma, so neither is a global `simp` lemma.
 -/
 -- We turn `testBit_add_one` on as a `local simp` for this file.
-@[local simp]
+@[local simp, grind _=_]
 theorem testBit_add_one (x i : Nat) : testBit x (i + 1) = testBit (x/2) i := by
   unfold testBit
   simp [shiftRight_succ_inside]
 
+@[grind _=_]
 theorem testBit_add (x i n : Nat) : testBit x (i + n) = testBit (x / 2 ^ n) i := by
   revert x
   induction n with
@@ -122,6 +123,7 @@ theorem testBit_div_two (x i : Nat) : testBit (x / 2) i = testBit x (i + 1) := b
 theorem testBit_div_two_pow (x i : Nat) : testBit (x / 2 ^ n) i = testBit x (i + n) :=
   testBit_add .. |>.symm
 
+@[grind =]
 theorem testBit_eq_decide_div_mod_eq {x : Nat} : testBit x i = decide (x / 2^i % 2 = 1) := by
   induction i generalizing x with
   | zero =>
@@ -290,7 +292,7 @@ theorem testBit_two_pow_add_gt {i j : Nat} (j_lt_i : j < i) (x : Nat) :
   | d+1 =>
     simp [Nat.pow_succ, Nat.mul_comm _ 2, Nat.mul_add_mod]
 
-@[simp] theorem testBit_mod_two_pow (x j i : Nat) :
+@[simp, grind =] theorem testBit_mod_two_pow (x j i : Nat) :
     testBit (x % 2^j) i = (decide (i < j) && testBit x i) := by
   induction x using Nat.strongRecOn generalizing j i with
   | ind x hyp =>
@@ -322,6 +324,7 @@ theorem not_decide_mod_two_eq_one (x : Nat)
     : (!decide (x % 2 = 1)) = decide (x % 2 = 0) := by
   cases Nat.mod_two_eq_zero_or_one x <;> (rename_i p; simp [p])
 
+@[grind =]
 theorem testBit_two_pow_sub_succ (h₂ : x < 2 ^ n) (i : Nat) :
     testBit (2^n - (x + 1)) i = (decide (i < n) && ! testBit x i) := by
   induction i generalizing n x with
@@ -357,6 +360,7 @@ theorem testBit_one_eq_true_iff_self_eq_zero {i : Nat} :
     Nat.testBit 1 i = true ↔ i = 0 := by
   cases i <;> simp
 
+@[grind =]
 theorem testBit_two_pow {n m : Nat} : testBit (2 ^ n) m = decide (n = m) := by
   rw [testBit, shiftRight_eq_div_pow]
   by_cases h : n = m
@@ -482,18 +486,20 @@ theorem bitwise_mod_two_pow (of_false_false : f false false = false := by rfl) :
 
 /-! ### and -/
 
-@[simp] theorem testBit_and (x y i : Nat) : (x &&& y).testBit i = (x.testBit i && y.testBit i) := by
+@[simp, grind =] theorem testBit_and (x y i : Nat) : (x &&& y).testBit i = (x.testBit i && y.testBit i) := by
   simp [HAnd.hAnd, AndOp.and, land, testBit_bitwise ]
 
 
-@[simp] protected theorem and_self (x : Nat) : x &&& x = x := by
+@[simp, grind =] protected theorem and_self (x : Nat) : x &&& x = x := by
    apply Nat.eq_of_testBit_eq
    simp
 
+@[grind =]
 protected theorem and_comm (x y : Nat) : x &&& y = y &&& x := by
    apply Nat.eq_of_testBit_eq
    simp [Bool.and_comm]
 
+@[grind _=_]
 protected theorem and_assoc (x y z : Nat) : (x &&& y) &&& z = x &&& (y &&& z) := by
    apply Nat.eq_of_testBit_eq
    simp [Bool.and_assoc]
@@ -537,54 +543,63 @@ abbrev and_pow_two_sub_one_of_lt_two_pow := @and_two_pow_sub_one_of_lt_two_pow
   rw [testBit_and]
   simp
 
+@[grind _=_]
 theorem and_div_two_pow : (a &&& b) / 2 ^ n = a / 2 ^ n &&& b / 2 ^ n :=
   bitwise_div_two_pow
 
+@[grind _=_]
 theorem and_div_two : (a &&& b) / 2 = a / 2 &&& b / 2 :=
   and_div_two_pow (n := 1)
 
+@[grind _=_]
 theorem and_mod_two_pow : (a &&& b) % 2 ^ n = (a % 2 ^ n) &&& (b % 2 ^ n) :=
   bitwise_mod_two_pow
 
 /-! ### lor -/
 
-@[simp] theorem zero_or (x : Nat) : 0 ||| x = x := by
+@[simp, grind =] theorem zero_or (x : Nat) : 0 ||| x = x := by
   simp only [HOr.hOr, OrOp.or, lor]
   unfold bitwise
   simp [@eq_comm _ 0]
 
-@[simp] theorem or_zero (x : Nat) : x ||| 0 = x := by
+@[simp, grind =] theorem or_zero (x : Nat) : x ||| 0 = x := by
   simp only [HOr.hOr, OrOp.or, lor]
   unfold bitwise
   simp [@eq_comm _ 0]
 
-@[simp] theorem testBit_or (x y i : Nat) : (x ||| y).testBit i = (x.testBit i || y.testBit i) := by
+@[simp, grind =] theorem testBit_or (x y i : Nat) : (x ||| y).testBit i = (x.testBit i || y.testBit i) := by
   simp [HOr.hOr, OrOp.or, lor, testBit_bitwise ]
 
-@[simp] protected theorem or_self (x : Nat) : x ||| x = x := by
+@[simp, grind =] protected theorem or_self (x : Nat) : x ||| x = x := by
    apply Nat.eq_of_testBit_eq
    simp
 
+@[grind =]
 protected theorem or_comm (x y : Nat) : x ||| y = y ||| x := by
    apply Nat.eq_of_testBit_eq
    simp [Bool.or_comm]
 
+@[grind _=_]
 protected theorem or_assoc (x y z : Nat) : (x ||| y) ||| z = x ||| (y ||| z) := by
    apply Nat.eq_of_testBit_eq
    simp [Bool.or_assoc]
 
+@[grind _=_]
 theorem and_or_distrib_left (x y z : Nat) : x &&& (y ||| z) = (x &&& y) ||| (x &&& z) := by
    apply Nat.eq_of_testBit_eq
    simp [Bool.and_or_distrib_left]
 
+@[grind _=_]
 theorem and_distrib_right (x y z : Nat) : (x ||| y) &&& z = (x &&& z) ||| (y &&& z) := by
    apply Nat.eq_of_testBit_eq
    simp [Bool.and_or_distrib_right]
 
+@[grind _=_]
 theorem or_and_distrib_left (x y z : Nat) : x ||| (y &&& z) = (x ||| y) &&& (x ||| z) := by
    apply Nat.eq_of_testBit_eq
    simp [Bool.or_and_distrib_left]
 
+@[grind _=_]
 theorem or_and_distrib_right (x y z : Nat) : (x &&& y) ||| z = (x ||| z) &&& (y ||| z) := by
    apply Nat.eq_of_testBit_eq
    simp [Bool.or_and_distrib_right]
@@ -610,37 +625,42 @@ theorem or_lt_two_pow {x y n : Nat} (left : x < 2^n) (right : y < 2^n) : x ||| y
   rw [testBit_or]
   simp
 
+@[grind _=_]
 theorem or_div_two_pow : (a ||| b) / 2 ^ n = a / 2 ^ n ||| b / 2 ^ n :=
   bitwise_div_two_pow
 
+@[grind _=_]
 theorem or_div_two : (a ||| b) / 2 = a / 2 ||| b / 2 :=
   or_div_two_pow (n := 1)
 
+@[grind _=_]
 theorem or_mod_two_pow : (a ||| b) % 2 ^ n = a % 2 ^ n ||| b % 2 ^ n :=
   bitwise_mod_two_pow
 
 /-! ### xor -/
 
-@[simp] theorem testBit_xor (x y i : Nat) :
+@[simp, grind =] theorem testBit_xor (x y i : Nat) :
     (x ^^^ y).testBit i = ((x.testBit i) ^^ (y.testBit i)) := by
   simp [HXor.hXor, Xor.xor, xor, testBit_bitwise ]
 
-@[simp] theorem zero_xor (x : Nat) : 0 ^^^ x = x := by
+@[simp, grind =] theorem zero_xor (x : Nat) : 0 ^^^ x = x := by
    apply Nat.eq_of_testBit_eq
    simp
 
-@[simp] theorem xor_zero (x : Nat) : x ^^^ 0 = x := by
+@[simp, grind =] theorem xor_zero (x : Nat) : x ^^^ 0 = x := by
    apply Nat.eq_of_testBit_eq
    simp
 
-@[simp] protected theorem xor_self (x : Nat) : x ^^^ x = 0 := by
+@[simp, grind =] protected theorem xor_self (x : Nat) : x ^^^ x = 0 := by
    apply Nat.eq_of_testBit_eq
    simp
 
+@[grind =]
 protected theorem xor_comm (x y : Nat) : x ^^^ y = y ^^^ x := by
    apply Nat.eq_of_testBit_eq
    simp [Bool.xor_comm]
 
+@[grind _=_]
 protected theorem xor_assoc (x y z : Nat) : (x ^^^ y) ^^^ z = x ^^^ (y ^^^ z) := by
    apply Nat.eq_of_testBit_eq
    simp
@@ -658,10 +678,12 @@ instance : Std.LawfulCommIdentity (α := Nat) (· ^^^ ·) 0 where
 theorem xor_lt_two_pow {x y n : Nat} (left : x < 2^n) (right : y < 2^n) : x ^^^ y < 2^n :=
   bitwise_lt_two_pow left right
 
+@[grind _=_]
 theorem and_xor_distrib_right {a b c : Nat} : (a ^^^ b) &&& c = (a &&& c) ^^^ (b &&& c) := by
   apply Nat.eq_of_testBit_eq
   simp [Bool.and_xor_distrib_right]
 
+@[grind _=_]
 theorem and_xor_distrib_left {a b c : Nat} : a &&& (b ^^^ c) = (a &&& b) ^^^ (a &&& c) := by
   apply Nat.eq_of_testBit_eq
   simp [Bool.and_xor_distrib_left]
@@ -671,12 +693,15 @@ theorem and_xor_distrib_left {a b c : Nat} : a &&& (b ^^^ c) = (a &&& b) ^^^ (a
   rw [testBit_xor]
   simp
 
+@[grind _=_]
 theorem xor_div_two_pow : (a ^^^ b) / 2 ^ n = a / 2 ^ n ^^^ b / 2 ^ n :=
   bitwise_div_two_pow
 
+@[grind _=_]
 theorem xor_div_two : (a ^^^ b) / 2 = a / 2 ^^^ b / 2 :=
   xor_div_two_pow (n := 1)
 
+@[grind _=_]
 theorem xor_mod_two_pow : (a ^^^ b) % 2 ^ n = a % 2 ^ n ^^^ b % 2 ^ n :=
   bitwise_mod_two_pow
 
@@ -713,6 +738,7 @@ theorem testBit_two_pow_mul_add (a : Nat) {b i : Nat} (b_lt : b < 2^i) (j : Nat)
 @[deprecated testBit_two_pow_mul_add (since := "2025-03-18")]
 abbrev testBit_mul_pow_two_add := @testBit_two_pow_mul_add
 
+@[grind =]
 theorem testBit_two_pow_mul :
     testBit (2 ^ i * a) j = (decide (j ≥ i) && testBit a (j-i)) := by
   have gen := testBit_two_pow_mul_add a (Nat.two_pow_pos i) j
@@ -721,6 +747,11 @@ theorem testBit_two_pow_mul :
   cases Nat.lt_or_ge j i with
   | _ p => simp [p, Nat.not_le_of_lt, Nat.not_lt_of_le]
 
+@[grind =] -- Ideally `grind` could do this just with `testBit_two_pow_mul`.
+theorem testBit_mul_two_pow (x j i : Nat) :
+    (x * 2 ^ i).testBit j = (decide (i ≤ j) && x.testBit (j - i)) := by
+  rw [Nat.mul_comm, testBit_two_pow_mul]
+
 @[deprecated testBit_two_pow_mul (since := "2025-03-18")]
 abbrev testBit_mul_pow_two := @testBit_two_pow_mul
 
@@ -744,21 +775,17 @@ abbrev mul_add_lt_is_or := @two_pow_add_eq_or_of_lt
 
 /-! ### shiftLeft and shiftRight -/
 
-@[simp] theorem testBit_shiftLeft (x : Nat) : testBit (x <<< i) j =
+@[simp, grind =] theorem testBit_shiftLeft (x : Nat) : testBit (x <<< i) j =
     (decide (j ≥ i) && testBit x (j-i)) := by
   simp [shiftLeft_eq, Nat.mul_comm _ (2^_), testBit_two_pow_mul]
 
-@[simp] theorem testBit_shiftRight (x : Nat) : testBit (x >>> i) j = testBit x (i+j) := by
+@[simp, grind =] theorem testBit_shiftRight (x : Nat) : testBit (x >>> i) j = testBit x (i+j) := by
   simp [testBit, ←shiftRight_add]
 
 @[simp] theorem shiftLeft_mod_two_eq_one : x <<< i % 2 = 1 ↔ i = 0 ∧ x % 2 = 1 := by
   rw [mod_two_eq_one_iff_testBit_zero, testBit_shiftLeft]
   simp
 
-theorem testBit_mul_two_pow (x i n : Nat) :
-    (x * 2 ^ n).testBit i = (decide (n ≤ i) && x.testBit (i - n)) := by
-  rw [← testBit_shiftLeft, shiftLeft_eq]
-
 theorem bitwise_mul_two_pow (of_false_false : f false false = false := by rfl) :
     (bitwise f x y) * 2 ^ n = bitwise f (x * 2 ^ n) (y * 2 ^ n) := by
   apply Nat.eq_of_testBit_eq
@@ -768,16 +795,20 @@ theorem bitwise_mul_two_pow (of_false_false : f false false = false := by rfl) :
   · simp [hn]
   · simp [hn, of_false_false]
 
+@[grind _=_]
 theorem shiftLeft_bitwise_distrib {a b : Nat} (of_false_false : f false false = false := by rfl) :
     (bitwise f a b) <<< i = bitwise f (a <<< i) (b <<< i) := by
   simp [shiftLeft_eq, bitwise_mul_two_pow of_false_false]
 
+@[grind _=_]
 theorem shiftLeft_and_distrib {a b : Nat} : (a &&& b) <<< i = a <<< i &&& b <<< i :=
   shiftLeft_bitwise_distrib
 
+@[grind _=_]
 theorem shiftLeft_or_distrib {a b : Nat} : (a ||| b) <<< i = a <<< i ||| b <<< i :=
   shiftLeft_bitwise_distrib
 
+@[grind _=_]
 theorem shiftLeft_xor_distrib {a b : Nat} : (a ^^^ b) <<< i = a <<< i ^^^ b <<< i :=
   shiftLeft_bitwise_distrib
 
@@ -786,16 +817,20 @@ theorem shiftLeft_xor_distrib {a b : Nat} : (a ^^^ b) <<< i = a <<< i ^^^ b <<<
   simp only [testBit, one_and_eq_mod_two, mod_two_bne_zero]
   exact (Bool.beq_eq_decide_eq _ _).symm
 
+@[grind _=_]
 theorem shiftRight_bitwise_distrib {a b : Nat} (of_false_false : f false false = false := by rfl) :
     (bitwise f a b) >>> i = bitwise f (a >>> i) (b >>> i) := by
   simp [shiftRight_eq_div_pow, bitwise_div_two_pow of_false_false]
 
+@[grind _=_]
 theorem shiftRight_and_distrib {a b : Nat} : (a &&& b) >>> i = a >>> i &&& b >>> i :=
   shiftRight_bitwise_distrib
 
+@[grind _=_]
 theorem shiftRight_or_distrib {a b : Nat} : (a ||| b) >>> i = a >>> i ||| b >>> i :=
   shiftRight_bitwise_distrib
 
+@[grind _=_]
 theorem shiftRight_xor_distrib {a b : Nat} : (a ^^^ b) >>> i = a >>> i ^^^ b >>> i :=
   shiftRight_bitwise_distrib
 

tests/lean/grind/experiments/bitvec.lean

@@ -1,4 +1,3 @@
-set_option linter.missingDocs true
 
 open BitVec
 
@@ -6,95 +5,78 @@ set_option trace.grind.ematch.pattern true
 
 namespace BitVec'
 
-@[simp] theorem mk_zero : BitVec.ofFin (w := w) ⟨0, h⟩ = 0#w := rfl
-@[simp] theorem ofNatLT_zero : BitVec.ofNatLT (w := w) 0 h = 0#w := rfl
+@[simp, grind =] theorem mk_zero : BitVec.ofFin (w := w) ⟨0, h⟩ = 0#w := rfl
+@[simp, grind =] theorem ofNatLT_zero : BitVec.ofNatLT (w := w) 0 h = 0#w := rfl
 
-@[simp] theorem getLsbD_ofFin (x : Fin (2^n)) (i : Nat) :
+@[simp, grind =] theorem getLsbD_ofFin (x : Fin (2^n)) (i : Nat) :
     getLsbD (BitVec.ofFin x) i = x.val.testBit i := rfl
 
-@[simp] theorem getElem_ofFin (x : Fin (2^n)) (i : Nat) (h : i < n) :
+@[simp, grind =] theorem getElem_ofFin (x : Fin (2^n)) (i : Nat) (h : i < n) :
     (BitVec.ofFin x)[i] = x.val.testBit i := rfl
 
-@[simp] theorem getLsbD_of_ge (x : BitVec w) (i : Nat) (ge : w ≤ i) : getLsbD x i = false := by
-  let ⟨x, x_lt⟩ := x
-  simp only [getLsbD_ofFin]
-  apply Nat.testBit_lt_two_pow
-  have p : 2^w ≤ 2^i := Nat.pow_le_pow_right (by omega) ge
-  grind
+grind_pattern Nat.pow_le_pow_right => i ≤ j, n ^ i
+grind_pattern Nat.pow_le_pow_right => i ≤ j, n ^ j
 
-@[simp] theorem getMsbD_of_ge (x : BitVec w) (i : Nat) (ge : w ≤ i) : getMsbD x i = false := by
+@[simp, grind] theorem getLsbD_of_ge (x : BitVec w) (i : Nat) (ge : w ≤ i) : getLsbD x i = false := by
+  let ⟨x, x_lt⟩ := x
+  grind [Nat.testBit_lt_two_pow]
+
+@[simp, grind] theorem getMsbD_of_ge (x : BitVec w) (i : Nat) (ge : w ≤ i) : getMsbD x i = false := by
   grind [getMsbD]
 
-set_option linter.missingDocs false in
-@[deprecated getLsbD_of_ge (since := "2025-04-04")]
-abbrev getLsbD_ge := @getLsbD_of_ge
-
-set_option linter.missingDocs false in
-@[deprecated getMsbD_of_ge (since := "2025-04-04")]
-abbrev getMsbD_ge := @getMsbD_of_ge
-
+-- @[grind →]
 theorem lt_of_getLsbD {x : BitVec w} {i : Nat} : getLsbD x i = true → i < w := by
-  grind [BitVec.getLsbD_of_ge]
+  grind
 
+-- @[grind →]
 theorem lt_of_getMsbD {x : BitVec w} {i : Nat} : getMsbD x i = true → i < w := by
-    grind [BitVec.getMsbD_of_ge]
+  grind
 
 @[simp] theorem getElem?_eq_getElem {l : BitVec w} {n} (h : n < w) : l[n]? = some l[n] := by
-  simp only [getElem?_def, h, ↓reduceDIte]
+  grind
 
 theorem getElem?_eq_some_iff {l : BitVec w} : l[n]? = some a ↔ ∃ h : n < w, l[n] = a := by
-  simp only [getElem?_def]
-  split
-  · simp_all
-  · simp; omega
+  grind
 
-theorem getElem_of_getElem? {l : BitVec w} : l[n]? = some a → ∃ h : n < w, l[n] = a :=
-  getElem?_eq_some_iff.mp
-
-set_option linter.missingDocs false in
-@[deprecated getElem?_eq_some_iff (since := "2025-02-17")]
-abbrev getElem?_eq_some := @getElem?_eq_some_iff
+theorem getElem_of_getElem? {l : BitVec w} : l[n]? = some a → ∃ h : n < w, l[n] = a := by
+  grind
 
 @[simp] theorem getElem?_eq_none_iff {l : BitVec w} : l[n]? = none ↔ w ≤ n := by
   grind
 
-theorem getElem?_eq_none {l : BitVec w} (h : w ≤ n) : l[n]? = none := getElem?_eq_none_iff.mpr h
+theorem getElem?_eq_none {l : BitVec w} (h : w ≤ n) : l[n]? = none := by grind
 
 theorem getElem?_eq (l : BitVec w) (i : Nat) :
     l[i]? = if h : i < w then some l[i] else none := by
-  split <;> simp_all
+  grind
 
 theorem some_getElem_eq_getElem? (l : BitVec w) (i : Nat) (h : i < w) :
     (some l[i] = l[i]?) ↔ True := by
-  simp
+  grind
 
 @[simp] theorem getElem?_eq_some_getElem (l : BitVec w) (i : Nat) (h : i < w) :
     (l[i]? = some l[i]) ↔ True := by
-  simp [h]
+  grind
 
 theorem getElem_eq_iff {l : BitVec w} {n : Nat} {h : n < w} : l[n] = x ↔ l[n]? = some x := by
-  simp only [getElem?_eq_some_iff]
-  exact ⟨fun w => ⟨h, w⟩, fun h => h.2⟩
+  grind
 
 theorem getElem_eq_getElem? (l : BitVec w) (i : Nat) (h : i < w) :
-    l[i] = l[i]?.get (by simp [getElem?_eq_getElem, h]) := by
-  simp [getElem_eq_iff]
+    l[i] = l[i]?.get (by grind) := by
+  grind
 
 theorem getLsbD_eq_getElem?_getD {x : BitVec w} {i : Nat} :
     x.getLsbD i = x[i]?.getD false := by
   rw [getElem?_def]
   split
   · rfl
-  · simp_all
+  · grind
 
 @[simp]
 theorem getElem_of_getLsbD_eq_true {x : BitVec w} {i : Nat} (h : x.getLsbD i = true) :
-    (x[i]'(lt_of_getLsbD h) = true) = True := by
+    (x[i]'(by grind) = true) = True := by
   simp [← BitVec.getLsbD_eq_getElem, h]
 
-/--
-This normalized a bitvec using `ofFin` to `ofNat`.
--/
 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]
 
@@ -108,7 +90,7 @@ theorem toNat_ne_iff_ne {n} {x y : BitVec n} : x.toNat ≠ y.toNat ↔ x ≠ y :
   · rintro h rfl; apply h rfl
   · intro h h_eq; apply h <| eq_of_toNat_eq h_eq
 
-@[simp] theorem val_toFin (x : BitVec w) : x.toFin.val = x.toNat := rfl
+@[simp, grind =] theorem val_toFin (x : BitVec w) : x.toFin.val = x.toNat := rfl
 
 @[bitvec_to_nat] theorem toNat_eq {x y : BitVec n} : x = y ↔ x.toNat = y.toNat :=
   Iff.intro (congrArg BitVec.toNat) eq_of_toNat_eq
@@ -132,39 +114,29 @@ theorem two_pow_le_toNat_of_getElem_eq_true {i : Nat} {x : BitVec w}
   rw [← getElem_eq_testBit_toNat x i hi]
   exact hx
 
-theorem getMsb'_eq_getLsb' (x : BitVec w) (i : Fin w) :
-    x.getMsb' i = x.getLsb' ⟨w - 1 - i, by omega⟩ := by
-  simp only [getMsb', getLsb']
+@[grind =]
+theorem getMsb_eq_getLsb (x : BitVec w) (i : Fin w) :
+    x.getMsb i = x.getLsb ⟨w - 1 - i, by omega⟩ := by
+  simp only [getMsb, getLsb]
 
+@[grind =]
 theorem getMsb?_eq_getLsb? (x : BitVec w) (i : Nat) :
     x.getMsb? i = if i < w then x.getLsb? (w - 1 - i) else none := by
   simp only [getMsb?, getLsb?_eq_getElem?]
-  split <;> simp [getMsb'_eq_getLsb']
+  split <;> simp [getMsb_eq_getLsb]
 
+@[grind =]
 theorem getMsbD_eq_getLsbD (x : BitVec w) (i : Nat) : x.getMsbD i = (decide (i < w) && x.getLsbD (w - 1 - i)) := by
   rw [getMsbD, getLsbD]
 
 theorem getLsbD_eq_getMsbD (x : BitVec w) (i : Nat) : x.getLsbD i = (decide (i < w) && x.getMsbD (w - 1 - i)) := by
-  rw [getMsbD]
-  by_cases h₁ : i < w <;> by_cases h₂ : w - 1 - i < w <;>
-    simp only [h₁, h₂] <;> simp only [decide_true, decide_false, Bool.false_and, Bool.and_false, Bool.true_and, Bool.and_true]
-  · congr
-    omega
-  all_goals
-    apply getLsbD_of_ge
-    omega
+  grind
 
 @[simp] theorem getElem?_of_ge (x : BitVec w) (i : Nat) (ge : w ≤ i) : x[i]? = none := by
-  simp [ge]
+  grind
 
 @[simp] theorem getMsb?_of_ge (x : BitVec w) (i : Nat) (ge : w ≤ i) : getMsb? x i = none := by
-  simp [getMsb?_eq_getLsb?]; omega
-
-set_option linter.missingDocs false in
-@[deprecated getElem?_of_ge (since := "2025-04-04")] abbrev getLsb?_ge := @getElem?_of_ge
-
-set_option linter.missingDocs false in
-@[deprecated getMsb?_of_ge (since := "2025-04-04")] abbrev getMsb?_ge := @getMsb?_of_ge
+  grind
 
 theorem lt_of_getElem?_eq_some (x : BitVec w) (i : Nat) : x[i]? = some b → i < w := by
   cases h : x[i]? with

tests/lean/grind/experiments/nat_div.lean

@@ -0,0 +1,6 @@
+open Nat
+
+grind_pattern div_add_mod => m % n
+grind_pattern div_add_mod => m / n
+
+attribute [grind →] Nat.mul_le_of_le_div

tests/lean/grind/experiments/nat_semiring.lean

@@ -0,0 +1,44 @@
+
+example {a b c d : Nat} (h : a = b + c * d) (w : 1 ≤ d) : a ≥ c := by
+  -- grind -- fails, but would be lovely
+  subst h
+  apply Nat.le_add_left_of_le
+  apply Nat.le_mul_of_pos_right
+  assumption
+
+example {a b c d : Int} (h : a = b + c * d) (hb : 0 ≤ b) (hc : 0 ≤ c) (w : 1 ≤ d) : a ≥ c := by
+  -- grind -- fails also
+  subst h
+  conv => rhs; rw [← Int.zero_add c]
+  apply Int.add_le_add
+  · assumption
+  · have : 0 ≤ c * (d - 1) := Int.mul_nonneg (by omega) (by omega)
+    rw [Int.mul_sub, Int.mul_one, Int.sub_nonneg] at this
+    exact this
+
+-- Note: if we can automate the `Int` version here, we can also automate the `Nat` version just by embedding in `Int`.
+
+open Lean Grind
+
+example {α : Type} [Lean.Grind.IntModule α] [Lean.Grind.Preorder α] [Lean.Grind.IntModule.IsOrdered α] {a b c : α} {d : Int}
+    (wb : 0 ≤ b) (wc : 0 ≤ c)
+    (h : a = b + d * c) (w : 1 ≤ d) : a ≥ c := by
+  subst h
+  conv => rhs; rw [← IntModule.zero_add c]
+  apply IntModule.IsOrdered.add_le_add
+  · exact wb
+  · have := IntModule.IsOrdered.hmul_le_hmul_of_le_of_le_of_nonneg_of_nonneg w (Preorder.le_refl c) (by decide) wc
+    rwa [IntModule.one_hmul] at this
+
+-- We can prove this directly in an ordered NatModule, from the axioms. (But shouldn't, see below.)
+example {α : Type} [Lean.Grind.NatModule α] [Lean.Grind.Preorder α] [Lean.Grind.NatModule.IsOrdered α] {a b c : α} {d : Nat}
+    (wb : 0 ≤ b) (wc : 0 ≤ c)
+    (h : a = b + d * c) (w : 1 ≤ d) : a ≥ c := by
+  subst h
+  conv => rhs; rw [← NatModule.zero_add c]
+  apply NatModule.IsOrdered.add_le_add
+  · exact wb
+  · have := NatModule.IsOrdered.hmul_le_hmul_of_le_of_le_of_nonneg w (Preorder.le_refl c) wc
+    rwa [NatModule.one_hmul] at this
+
+-- The correct proof is to embed a NatModule in its IntModule envelope.