test: grind test with many equalities

tests/lean/run/grind_many_eqs.lean

@@ -0,0 +1,34 @@
+import Lean
+
+def f (a : Nat) := a + a + a
+def g (a : Nat) := a + a
+def h (n : Nat) : Prop :=
+  match n with
+  | 0   => f 0 = f 1
+  | n+1 => f (n+1) = f n ∧ g (2*n + 1) = g (2*n) ∧ h n
+
+-- Prints the equivalence class containing a `f` application
+open Lean Meta Elab Tactic Grind in
+elab "grind_test" n:num : tactic => withMainContext do
+  let n := n.getNat
+  let declName := (← Term.getDeclName?).getD `_main
+  Meta.Grind.preprocessAndProbe (← getMainGoal) declName do
+    let f0 ← Grind.shareCommon (mkApp (mkConst ``f) (mkNatLit 0))
+    -- The `f 0` equivalence class contains `n+1` elements
+    assert! (← getEqc f0).length == n + 1
+    forEachENode fun node => do
+      if node.self.isAppOf ``g then
+        -- Any equivalence class containing a `g`-application contains 2 elements
+        assert! (← getEqc (← getRoot node.self)).length == 2
+
+set_option grind.debug true in
+example : h 5 → False := by
+  simp [h]
+  grind_test 5
+  sorry
+
+set_option maxRecDepth 2048
+example : h 100 → False := by
+  simp [h]
+  grind_test 100
+  sorry