feat: more grind tests (#6650)

This PR adds some tests for `grind`, working on `List` lemmas.

tests/lean/run/grind_assoc.lean

@@ -0,0 +1,37 @@
+def α : Type := sorry
+instance : Mul α := sorry
+
+@[grind _=_] theorem assoc {a b c : α} : (a * b) * c = a * (b * c) := sorry
+
+example {a b c : α} : (a * b) * c = a * (b * c) := by grind
+example {a1 : α} (_ : a1 * a2 = b3) (_ : b3 * a3 = b4) : a1 * (a2 * a3) = b4 := by grind
+example {a1 : α} (_ : a1 * a2 = b3) (_ : b3 * a3 = b4) (_ : b4 * a4 = b5) : a1 * (a2 * (a3 * a4)) = b5 := by grind
+example {a1 : α} (_ : a1 * a2 = b3) (_ : b3 * a3 = b4) (_ : b4 * a4 = b5) (_ : b5 * a5 = b6) :
+    a1 * (a2 * (a3 * (a4 * a5))) = b6 := by grind
+example {a1 : α} (_ : a1 * a2 = b3) (_ : b3 * a3 = b4) (_ : b4 * a4 = b5) (_ : b5 * a5 = b6) (_ : b6 * a6 = b7) :
+    a1 * (a2 * (a3 * (a4 * (a5 * a6)))) = b7 := by grind
+example {a1 : α} (_ : a1 * a2 = b3) (_ : b3 * a3 = b4) (_ : b4 * a4 = b5) (_ : b5 * a5 = b6) (_ : b6 * a6 = b7) (_ : b7 * a7 = b8) :
+    a1 * (a2 * (a3 * (a4 * (a5 * (a6 * a7))))) = b8 := by grind
+
+example {a1 : α} (_ : a3 * a4 = x) (_ : ∀ y, x * y = x) (_ : ∀ y, y * x = x):
+    a1 * (a2 * (a3 * (a4 * (a5 * (a6 * a7))))) = x := by grind
+
+example {a1 : α} (w : (((a1 * a2) * a3) * a4) * ((a5 * a6) * a7) = x) :
+    a1 * (a2 * (a3 * (a4 * (a5 * (a6 * a7))))) = x := by grind
+
+example {a1 : α} (w : (((a1 * a2) * a3) * a4) = ((b1 * b2) * (b3 * b4)))
+    (h : (b4 * (a5 * a6)) = c1) :
+    a1 * (a2 * (a3 * (a4 * (a5 * (a6 * a7))))) = (b1 * b2 * b3 * c1 * a7) := by grind
+
+-- 4-fold product (17ms)
+example {a1 : α} (_ : (((a1 * a2) * a3) * a4) = b1 * (b2 * b3)) (_ : ((b1 * b2) * b3) = c1 * c2) (_ : (c1 * c2) = d1) : a1 * (a2 * (a3 * a4)) = d1 := by grind
+-- 6-fold product (75 ms)
+example {a1 : α} (_ : (((((a1 * a2) * a3) * a4) * a5) * a6) = b1 * (b2 * (b3 * (b4 * b5)))) (_ : ((((b1 * b2) * b3) * b4) * b5) = c1 * (c2 * (c3 * c4))) (_ : (((c1 * c2) * c3) * c4) = d1 * (d2 * d3)) (_ : ((d1 * d2) * d3) = e1 * e2) (_ : (e1 * e2) = f1) : a1 * (a2 * (a3 * (a4 * (a5 * a6)))) = f1 := by grind
+-- 8-fold product (260ms)
+-- example {a1 : α} (_ : (((((((a1 * a2) * a3) * a4) * a5) * a6) * a7) * a8) = b1 * (b2 * (b3 * (b4 * (b5 * (b6 * b7)))))) (_ : ((((((b1 * b2) * b3) * b4) * b5) * b6) * b7) = c1 * (c2 * (c3 * (c4 * (c5 * c6))))) (_ : (((((c1 * c2) * c3) * c4) * c5) * c6) = d1 * (d2 * (d3 * (d4 * d5)))) (_ : ((((d1 * d2) * d3) * d4) * d5) = e1 * (e2 * (e3 * e4))) (_ : (((e1 * e2) * e3) * e4) = f1 * (f2 * f3)) (_ : ((f1 * f2) * f3) = g1 * g2) (_ : (g1 * g2) = h1) : a1 * (a2 * (a3 * (a4 * (a5 * (a6 * (a7 * a8)))))) = h1 := by grind
+-- 10-fold product (800ms)
+-- example {a1 : α} (_ : (((((((((a1 * a2) * a3) * a4) * a5) * a6) * a7) * a8) * a9) * a10) = b1 * (b2 * (b3 * (b4 * (b5 * (b6 * (b7 * (b8 * b9)))))))) (_ : ((((((((b1 * b2) * b3) * b4) * b5) * b6) * b7) * b8) * b9) = c1 * (c2 * (c3 * (c4 * (c5 * (c6 * (c7 * c8))))))) (_ : (((((((c1 * c2) * c3) * c4) * c5) * c6) * c7) * c8) = d1 * (d2 * (d3 * (d4 * (d5 * (d6 * d7)))))) (_ : ((((((d1 * d2) * d3) * d4) * d5) * d6) * d7) = e1 * (e2 * (e3 * (e4 * (e5 * e6))))) (_ : (((((e1 * e2) * e3) * e4) * e5) * e6) = f1 * (f2 * (f3 * (f4 * f5)))) (_ : ((((f1 * f2) * f3) * f4) * f5) = g1 * (g2 * (g3 * g4))) (_ : (((g1 * g2) * g3) * g4) = h1 * (h2 * h3)) (_ : ((h1 * h2) * h3) = i1 * i2) (_ : (i1 * i2) = j1) : a1 * (a2 * (a3 * (a4 * (a5 * (a6 * (a7 * (a8 * (a9 * a10)))))))) = j1 := by grind
+-- 12-fold product (1700ms)
+-- example {a1 : α} (_ : (((((((((((a1 * a2) * a3) * a4) * a5) * a6) * a7) * a8) * a9) * a10) * a11) * a12) = b1 * (b2 * (b3 * (b4 * (b5 * (b6 * (b7 * (b8 * (b9 * (b10 * b11)))))))))) (_ : ((((((((((b1 * b2) * b3) * b4) * b5) * b6) * b7) * b8) * b9) * b10) * b11) = c1 * (c2 * (c3 * (c4 * (c5 * (c6 * (c7 * (c8 * (c9 * c10))))))))) (_ : (((((((((c1 * c2) * c3) * c4) * c5) * c6) * c7) * c8) * c9) * c10) = d1 * (d2 * (d3 * (d4 * (d5 * (d6 * (d7 * (d8 * d9)))))))) (_ : ((((((((d1 * d2) * d3) * d4) * d5) * d6) * d7) * d8) * d9) = e1 * (e2 * (e3 * (e4 * (e5 * (e6 * (e7 * e8))))))) (_ : (((((((e1 * e2) * e3) * e4) * e5) * e6) * e7) * e8) = f1 * (f2 * (f3 * (f4 * (f5 * (f6 * f7)))))) (_ : ((((((f1 * f2) * f3) * f4) * f5) * f6) * f7) = g1 * (g2 * (g3 * (g4 * (g5 * g6))))) (_ : (((((g1 * g2) * g3) * g4) * g5) * g6) = h1 * (h2 * (h3 * (h4 * h5)))) (_ : ((((h1 * h2) * h3) * h4) * h5) = i1 * (i2 * (i3 * i4))) (_ : (((i1 * i2) * i3) * i4) = j1 * (j2 * j3)) (_ : ((j1 * j2) * j3) = k1 * k2) (_ : (k1 * k2) = l1) : a1 * (a2 * (a3 * (a4 * (a5 * (a6 * (a7 * (a8 * (a9 * (a10 * (a11 * a12)))))))))) = l1 := by grind
+-- 14-fold product (grind fails with maxHeartbeats)
+-- example {a1 : α} (_ : (((((((((((((a1 * a2) * a3) * a4) * a5) * a6) * a7) * a8) * a9) * a10) * a11) * a12) * a13) * a14) = b1 * (b2 * (b3 * (b4 * (b5 * (b6 * (b7 * (b8 * (b9 * (b10 * (b11 * (b12 * b13)))))))))))) (_ : ((((((((((((b1 * b2) * b3) * b4) * b5) * b6) * b7) * b8) * b9) * b10) * b11) * b12) * b13) = c1 * (c2 * (c3 * (c4 * (c5 * (c6 * (c7 * (c8 * (c9 * (c10 * (c11 * c12))))))))))) (_ : (((((((((((c1 * c2) * c3) * c4) * c5) * c6) * c7) * c8) * c9) * c10) * c11) * c12) = d1 * (d2 * (d3 * (d4 * (d5 * (d6 * (d7 * (d8 * (d9 * (d10 * d11)))))))))) (_ : ((((((((((d1 * d2) * d3) * d4) * d5) * d6) * d7) * d8) * d9) * d10) * d11) = e1 * (e2 * (e3 * (e4 * (e5 * (e6 * (e7 * (e8 * (e9 * e10))))))))) (_ : (((((((((e1 * e2) * e3) * e4) * e5) * e6) * e7) * e8) * e9) * e10) = f1 * (f2 * (f3 * (f4 * (f5 * (f6 * (f7 * (f8 * f9)))))))) (_ : ((((((((f1 * f2) * f3) * f4) * f5) * f6) * f7) * f8) * f9) = g1 * (g2 * (g3 * (g4 * (g5 * (g6 * (g7 * g8))))))) (_ : (((((((g1 * g2) * g3) * g4) * g5) * g6) * g7) * g8) = h1 * (h2 * (h3 * (h4 * (h5 * (h6 * h7)))))) (_ : ((((((h1 * h2) * h3) * h4) * h5) * h6) * h7) = i1 * (i2 * (i3 * (i4 * (i5 * i6))))) (_ : (((((i1 * i2) * i3) * i4) * i5) * i6) = j1 * (j2 * (j3 * (j4 * j5)))) (_ : ((((j1 * j2) * j3) * j4) * j5) = k1 * (k2 * (k3 * k4))) (_ : (((k1 * k2) * k3) * k4) = l1 * (l2 * l3)) (_ : ((l1 * l2) * l3) = m1 * m2) (_ : (m1 * m2) = n1) : a1 * (a2 * (a3 * (a4 * (a5 * (a6 * (a7 * (a8 * (a9 * (a10 * (a11 * (a12 * (a13 * a14)))))))))))) = n1 := by grind

tests/lean/run/grind_list.lean

@@ -0,0 +1,34 @@
+namespace List
+
+attribute [local grind =] List.length_cons in
+example : 0 < (x :: t).length := by grind
+
+attribute [local grind →] getElem?_eq_getElem in
+attribute [local grind =] length_replicate in
+attribute [local grind =] getElem_replicate in
+attribute [local grind =] getElem?_eq_none in
+theorem getElem?_replicate' : (replicate n a)[m]? = if m < n then some a else none := by
+  grind
+
+attribute [local grind =] getElem?_eq_some_iff in
+attribute [local grind =] getElem!_pos in
+theorem getElem!_of_getElem?' [Inhabited α] :
+    ∀ {l : List α} {i : Nat}, l[i]? = some b → l[i]! = b := by
+  grind
+
+attribute [local grind =] Option.map_some' Option.map_none' in
+attribute [local grind =] getElem?_map in
+attribute [local grind =] getElem?_replicate in
+theorem map_replicate' : (replicate n a).map f = replicate n (f a) := by
+  ext i
+  grind
+
+attribute [local grind =] getLast?_eq_some_iff in
+attribute [local grind] mem_concat_self in
+theorem mem_of_getLast?_eq_some' {xs : List α} {a : α} (h : xs.getLast? = some a) : a ∈ xs := by
+  grind
+
+attribute [local grind =] getElem_cons_zero in
+attribute [local grind =] getElem?_cons_zero in
+example (h : (a :: t)[0]? = some b) : (a :: t)[0] = b := by
+  grind