chore: update tests/lean/grind todo folder

Remove examples that we have already moved to `tests/lean/run`, and
add notes for possible fixes.

tests/lean/grind/algebra/bitvec.lean

@@ -1,24 +0,0 @@
-example {x : BitVec 2} : x - 2 * x + x = 0 := by
-  grind -- succeeds
-
-example {x : BitVec 2} : x - 2 • x + x = 0 := by
-  grind -- fails
-
--- There are several independent problems here!
-
--- 1. Cutsat doesn't evaluate `2 ^ 2`:
--- [cutsat] Assignment satisfying linear constraints
--- [assign] 「2 ^ 2」 := 0
-
--- 2. We don't normalize `3 * 2 • x` to `6 * x` in the ring solver:
--- [ring] Rings ▼
---   [] Ring `BitVec 2` ▼
---     [diseqs] Disequalities ▼
---       [_] ¬2 * x + 3 * 2 • x = 0
--- This should then give a contradiction because the characteristic of `BitVec 2` is 4.
-
--- 3. In `Int`, we're not normalizing `*` and `•`:
--- [ring] Rings ▼
---   [] Ring `Int` ▼
---     [basis] Basis ▼
---       [_] 2 * ↑x + -1 * ↑(2 • x) + -4 * ((2 * ↑x + -1 * ↑(2 • x)) / 4) + -1 * ((2 * ↑x + -1 * ↑(2 • x)) % 4) = 0

tests/lean/grind/algebra/exponents.lean

@@ -4,12 +4,6 @@ section CommRing
 
 variable (R : Type) [CommRing R]
 
-example (a : R) (n : Nat) : a^(n + 1) = a^n * a := by grind
-example (a : R) (n m : Nat) : a^(n + m) = a^n * a^m := by grind
-example (a : R) (n m : Nat) : a^(n + m) = a^m * a^n := by grind
-example (a : R) (n m : Nat) : a^(n + m + n) = a^m * a^(2*n) := by grind
-
-example (n m : Nat) : (n+m)^2 = n^2 + 2*n*m + m^2 := by grind
 example (a : R) (n m : Nat) : a^((n+m)^2) = a^(n^2 + 2*n*m + m^2) := by grind
 example (a : R) (n m : Nat) : a^((n+m)^2) = a^(n^2) * a^(2*n*m) * a^(m^2) := by grind
 
@@ -25,8 +19,6 @@ section Field
 
 variable (F : Type) [Field F]
 
-example (a : F) (n m : Int) : a^(n + m - n) = a^m := by grind
-
 example (a : F) (n m : Int) : a^(n - m) = a^n / a^m := by grind
 
 example (a : F) (n m : Int) : a^((n - m) * (n + m)) = a^(n^2) / a^(m^2) := by grind

tests/lean/grind/algebra/linarith_cc.lean

@@ -1,4 +1,8 @@
 -- This fails unless we manually substitute `hb`.
 -- `grind` doesn't recognise this as a linear arithmetic problem.
+
+-- Remark: we will handle this kind of example when we add support for
+-- nonlinear monomials to cutsat
+
 example (a : Nat) (ha : a < 8) (b : Nat) (hb : b = 2) : a * b < 8 * b := by
   grind -- fails

tests/lean/grind/algebra/nat_module.lean

@@ -1,17 +1,5 @@
 open Lean.Grind
 
-section IntModule
-
-variable (M : Type) [IntModule M]
-
-example (x y : M) : 2 * x + 3 * y + x = 3 * (x + y) := by grind
-
-variable [LinearOrder M] [OrderedAdd M]
-
-example {x y : M} (h : x ≤ y) : 2 * x + y ≤ 3 * y := by grind
-
-end IntModule
-
 -- We could solve these problems by embedding the NatModule in its Grothendieck completion.
 section NatModule
 

tests/lean/grind/algebra/nat_semiring.lean

@@ -1,3 +1,4 @@
+-- Remark: we need some support for nonlinear in `cutsat`
 
 example {a b c d : Nat} (h : a = b + c * d) (w : 1 ≤ d) : a ≥ c := by
   -- grind -- fails, but would be lovely

tests/lean/grind/algebra/omega.lean

@@ -1,19 +1,5 @@
 -- Comparisons against `omega`:
 
--- The next three problems are solved by
--- grind_pattern Fin.isLt => Fin.val self
--- but I *think* they should be solved anyway via the `ToInt (Fin n)` instances.
-
-theorem Fin.range_natAdd.extracted_1 (m n : Nat) (i : Fin (m + n)) (hi : m ≤ ↑i) : ↑i - m < n := by
-  grind
-
-theorem Fin.image_addNat_Ici.extracted_1 {n : Nat} (m : Nat) (i : Fin n) ⦃j : Fin (n + m)⦄
-    (this : ↑i + m ≤ ↑j) : ↑j - m < n := by
-  grind
-
-theorem List.find?_ofFn_eq_some.extracted_1 {n : Nat} (i : Fin n) (j : Nat) (hj : j < ↑i) : j < n := by
-  grind
-
 -- This one is much slower (~10s in the kernel) than omega (~2s in the kernel).
 example {a b c d e f a' b' c' d' e' f' : Int}
   (h₁ : c = a + 3 * b) (h₂ : c' = a' + b') (h₃ : d = 2 * a + 3 * b) (h₄ : d' = 2 * a' + b') (h₅ : e = a + b)