test: grind test with many equalities

`unreachable!` does not interrupt execution by default, but prints an
error message and returns a default element. Thus, `getEqc` may
diverge if invoked on terms that have not been internalize.

src/Lean/Meta/Tactic/Grind/Types.lean

@@ -257,7 +257,8 @@ def getENode? (e : Expr) : GoalM (Option ENode) :=
 
 /-- Returns node associated with `e`. It assumes `e` has already been internalized. -/
 def getENode (e : Expr) : GoalM ENode := do
-  let some n := (← get).enodes.find? (unsafe ptrAddrUnsafe e) | unreachable!
+  let some n := (← get).enodes.find? (unsafe ptrAddrUnsafe e)
+    | throwError "internal `grind` error, term has not been internalized{indentExpr e}"
   return n
 
 /-- Returns `true` is the root of its equivalence class. -/

tests/lean/run/grind_canon_insts.lean

@@ -7,6 +7,8 @@ elab "grind_test" : tactic => withMainContext do
     let nodes ← filterENodes fun e => return e.self.isAppOf ``HMul.hMul
     logInfo (nodes.toList.map (·.self))
 
+set_option grind.debug true
+
 class Semigroup (α : Type u) extends Mul α where
   mul_assoc (a b c : α) : a * b * c = a * (b * c)
 

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

tests/lean/run/grind_nested_proofs.lean

@@ -8,17 +8,43 @@ elab "grind_test" : tactic => withMainContext do
   Meta.Grind.preprocessAndProbe (← getMainGoal) declName do
     let nodes ← filterENodes fun e => return e.self.isAppOf ``Lean.Grind.nestedProof
     logInfo (nodes.toList.map (·.self))
+    let nodes ← filterENodes fun e => return e.self.isAppOf ``GetElem.getElem
+    let [_, n, _] := nodes.toList | unreachable!
+    logInfo (← getEqc n.self)
 
 set_option grind.debug true
 
+/-
+Recall that array access terms, such as `a[i]`, have nested proofs.
+The following test relies on `grind` `nestedProof` wrapper to
+detect equalities between array access terms.
+-/
+
 /--
 info: [Lean.Grind.nestedProof (i < a.toList.length) (_example.proof_1 i j a b h1 h2),
  Lean.Grind.nestedProof (j < a.toList.length) h1,
  Lean.Grind.nestedProof (j < b.toList.length) h]
 ---
+info: [a[i], b[j], a[j]]
+---
 warning: declaration uses 'sorry'
 -/
 #guard_msgs in
 example (i j : Nat) (a b : Array Nat) (h1 : j < a.size) (h : j < b.size) (h2 : i ≤ j) : a[i] < a[j] + b[j] → i = j → a = b → False := by
   grind_test
   sorry
+
+
+/--
+info: [Lean.Grind.nestedProof (i < a.toList.length) (_example.proof_1 i j a b h1 h2),
+ Lean.Grind.nestedProof (j < a.toList.length) h1,
+ Lean.Grind.nestedProof (j < b.toList.length) h]
+---
+info: [a[i], a[j]]
+---
+warning: declaration uses 'sorry'
+-/
+#guard_msgs in
+example (i j : Nat) (a b : Array Nat) (h1 : j < a.size) (h : j < b.size) (h2 : i ≤ j) : a[i] < a[j] + b[j] → i = j → False := by
+  grind_test
+  sorry