fix: Grind.MatchCond in checkParents (#6776)

This PR fixes the `checkParents` sanity checker used in `grind`. It did
not have support for checking the auxiliary gadget `Grind.MatchCond`.

src/Lean/Meta/AbstractNestedProofs.lean

@@ -4,6 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Leonardo de Moura
 -/
 prelude
+import Init.Grind.Util
 import Lean.Meta.Closure
 
 namespace Lean.Meta
@@ -16,7 +17,12 @@ def getLambdaBody (e : Expr) : Expr :=
 
 def isNonTrivialProof (e : Expr) : MetaM Bool := do
   if !(← isProof e) then
-    pure false
+    return false
+  else if e.isAppOf ``Grind.nestedProof then
+    -- Grind.nestedProof is a gadget created by the `grind` tactic.
+    -- We want to avoid the situation where `grind` keeps creating them,
+    -- and this module, which is used by `grind`, keeps abstracting them.
+    return false
   else
     -- We consider proofs such as `fun x => f x a` as trivial.
     -- For example, we don't want to abstract the body of `def rfl`

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

@@ -14,7 +14,7 @@ namespace Lean.Meta.Grind
 /--
 Returns `true` if `e` is of the form `∀ ..., _ = _ ... -> False`
 -/
-private def isMatchCond (e : Expr) : Bool := Id.run do
+private def isMatchCondCandidate (e : Expr) : Bool := Id.run do
   let mut e := e
   let mut hasEqs := false
   repeat
@@ -31,7 +31,7 @@ conditions corresponding to overlapping patterns.
 private def addMatchCondsToAlt (alt : Expr) : Expr := Id.run do
   let .forallE _ d b _ := alt
     | return alt
-  let d := if isMatchCond d then markAsMatchCond d else d
+  let d := if isMatchCondCandidate d then markAsMatchCond d else d
   return alt.updateForallE! d (addMatchCondsToAlt b)
 
 /--

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

@@ -6,6 +6,7 @@ Authors: Leonardo de Moura
 prelude
 import Lean.Meta.Tactic.Grind.Types
 import Lean.Meta.Tactic.Grind.Proof
+import Lean.Meta.Tactic.Grind.MatchCond
 import Lean.Meta.Tactic.Grind.Arith.Inv
 
 namespace Lean.Meta.Grind
@@ -46,27 +47,48 @@ private def checkEqc (root : ENode) : GoalM Unit := do
   -- The size of the equivalence class is correct.
   assert! root.size == size
 
+def checkChild (e : Expr) (child : Expr) : GoalM Bool := do
+  let some childRoot ← getRoot? child | return false
+  return isSameExpr childRoot e
+
+private def checkMatchCondParent (e : Expr) (parent : Expr) : GoalM Bool := do
+  let_expr Grind.MatchCond parent ← parent | return false
+  let mut curr := parent
+  repeat
+    let .forallE _ d b _ := curr
+      | return false
+    match_expr d with
+    | Eq _ lhs _ => if (← checkChild e lhs) then return true -- found it
+    | HEq α lhs _ _ => if (← checkChild e α <||> checkChild e lhs) then return true -- found it
+    | _ => pure ()
+    curr := b
+  return false
+
 private def checkParents (e : Expr) : GoalM Unit := do
   if (← isRoot e) then
     for parent in (← getParents e) do
-      let mut found := false
-      let checkChild (child : Expr) : GoalM Bool := do
-        let some childRoot ← getRoot? child | return false
-        return isSameExpr childRoot e
-      -- There is an argument `arg` s.t. root of `arg` is `e`.
-      for arg in parent.getAppArgs do
-        if (← checkChild arg) then
-          found := true
-          break
-      -- Recall that we have support for `Expr.forallE` propagation. See `ForallProp.lean`.
-      if let .forallE _ d b _ := parent then
-        if (← checkChild d) then
-          found := true
-        unless b.hasLooseBVars do
-          if (← checkChild b) then
+      if isMatchCond parent then
+        unless (← checkMatchCondParent e parent) do
+          throwError "e: {e}, parent: {parent}"
+        assert! (← checkMatchCondParent e parent)
+      else
+        let mut found := false
+        -- There is an argument `arg` s.t. root of `arg` is `e`.
+        for arg in parent.getAppArgs do
+          if (← checkChild e arg) then
             found := true
-      unless found do
-        assert! (← checkChild parent.getAppFn)
+            break
+        -- Recall that we have support for `Expr.forallE` propagation. See `ForallProp.lean`.
+        if let .forallE _ d b _ := parent then
+          if (← checkChild e d) then
+            found := true
+          unless b.hasLooseBVars do
+            if (← checkChild e b) then
+              found := true
+        unless found do
+          unless (← checkChild e parent.getAppFn) do
+            throwError "e: {e}, parent: {parent}"
+          assert! (← checkChild e parent.getAppFn)
   else
     -- All the parents are stored in the root of the equivalence class.
     assert! (← getParents e).isEmpty

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

@@ -81,6 +81,9 @@ and we have special support for propagating is truth value.
 def markAsMatchCond (e : Expr) : Expr :=
   mkApp (mkConst ``Grind.MatchCond) e
 
+def isMatchCond (e : Expr) : Bool :=
+  e.isAppOfArity ``Grind.MatchCond 1
+
 builtin_dsimproc_decl reduceMatchCond (Grind.MatchCond _) := fun e => do
   let_expr Grind.MatchCond _ ← e | return .continue
   return .done e