feat: close goals using match-expression conditions in grind (#6783)

This PR adds support for closing goals using `match`-expression
conditions that are known to be true in the `grind` tactic state.
`grind` can now solve goals such as:
```lean
def f : List Nat → List Nat → Nat
  | _, 1 :: _ :: _ => 1
  | _, _ :: _ => 2
  | _, _  => 0

example : z = a :: as → y = z → f x y > 0
```
Without `grind`, we would use the `split` tactic. The first two goals,
corresponding to the first two alternatives, are closed using `simp`,
and the the third using the `match`-expression condition produced by
`split`. The proof would proceed as follows.
```lean
example : z = a :: as → y = z → f x y > 0 := by
  intros
  unfold f
  split
  next => simp
  next => simp
  next h =>
    /-
    ...
    _ : z = a :: as
    _ : y = z
    ...
    h : ∀ (head : Nat) (tail : List Nat), y = head :: tail → False
    |- 0 > 0
    -/
    subst_vars
    /-
    ...
    h : ∀ (head : Nat) (tail : List Nat), a :: as = head :: tail → False
    |- 0 > 0
    -/
    have : False := h a as rfl
    contradiction
```
Here is the same proof using `grind`.
```lean
example : z = a :: as → y = z → f x y > 0 := by
  grind [f.eq_def]
```

src/Lean/Meta/Tactic/Contradiction.lean

@@ -96,12 +96,12 @@ private abbrev isGenDiseq (e : Expr) : Bool :=
 
   See `processGenDiseq`
 -/
-private def mkGenDiseqMask (e : Expr) : Array Bool :=
+def mkGenDiseqMask (e : Expr) : Array Bool :=
   go e #[]
 where
   go (e : Expr) (acc : Array Bool) : Array Bool :=
     match e with
-    | Expr.forallE _ d b _ => go b (acc.push (!b.hasLooseBVar 0 && (d.isEq || d.isHEq)))
+    | .forallE _ d b _ => go b (acc.push (!b.hasLooseBVar 0 && (d.isEq || d.isHEq)))
     | _ => acc
 
 /--

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

@@ -234,7 +234,8 @@ private def popNextEq? : GoalM (Option NewEq) := do
     modify fun s => { s with newEqs := s.newEqs.pop }
   return r
 
-private def processNewEqs : GoalM Unit := do
+@[export lean_grind_process_new_eqs]
+private def processNewEqsImpl : GoalM Unit := do
   repeat
     if (← isInconsistent) then
       resetNewEqs
@@ -246,7 +247,7 @@ private def processNewEqs : GoalM Unit := do
 
 private def addEqCore (lhs rhs proof : Expr) (isHEq : Bool) : GoalM Unit := do
   addEqStep lhs rhs proof isHEq
-  processNewEqs
+  processNewEqsImpl
 
 /-- Adds a new equality `lhs = rhs`. It assumes `lhs` and `rhs` have already been internalized. -/
 private def addEq (lhs rhs proof : Expr) : GoalM Unit := do
@@ -311,56 +312,4 @@ where
 def addHypothesis (fvarId : FVarId) (generation := 0) : GoalM Unit := do
   add (← fvarId.getType) (mkFVar fvarId) generation
 
-/--
-Helper function for executing `x` with a fresh `newEqs` and without modifying
-the goal state.
- -/
-private def withoutModifyingState (x : GoalM α) : GoalM α := do
-  let saved ← get
-  modify fun goal => { goal with newEqs := {} }
-  try
-    x
-  finally
-    set saved
-
-/--
-If `e` has not been internalized yet, simplify it, and internalize the result.
--/
-private def simpAndInternalize (e : Expr) (gen : Nat := 0) : GoalM Simp.Result := do
-  if (← alreadyInternalized e) then
-    return { expr := e }
-  else
-    let r ← simp e
-    internalize r.expr gen
-    return r
-
-/--
-Try to construct a proof that `lhs = rhs` using the information in the
-goal state. If `lhs` and `rhs` have not been internalized, this function
-will internalize then, process propagated equalities, and then check
-whether they are in the same equivalence class or not.
-The goal state is not modified by this function.
-This function mainly relies on congruence closure, and constraint
-propagation. It will not perform case analysis.
--/
-def proveEq? (lhs rhs : Expr) : GoalM (Option Expr) := do
-  if (← alreadyInternalized lhs <&&> alreadyInternalized rhs) then
-    if (← isEqv lhs rhs) then
-      return some (← mkEqProof lhs rhs)
-    else
-      return none
-  else withoutModifyingState do
-    let lhs ← simpAndInternalize lhs
-    let rhs ← simpAndInternalize rhs
-    processNewEqs
-    unless (← isEqv lhs.expr rhs.expr) do return none
-    unless (← hasSameType lhs.expr rhs.expr) do return none
-    let h ← mkEqProof lhs.expr rhs.expr
-    let h ← match lhs.proof?, rhs.proof? with
-      | none,    none    => pure h
-      | none,    some h₂ => mkEqTrans h (← mkEqSymm h₂)
-      | some h₁, none    => mkEqTrans h₁ h
-      | some h₁, some h₂ => mkEqTrans (← mkEqTrans h₁ h) (← mkEqSymm h₂)
-    return some h
-
 end Lean.Meta.Grind

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

@@ -6,7 +6,9 @@ Authors: Leonardo de Moura
 prelude
 import Init.Grind
 import Init.Simproc
+import Lean.Meta.Tactic.Contradiction
 import Lean.Meta.Tactic.Simp.Simproc
+import Lean.Meta.Tactic.Grind.ProveEq
 import Lean.Meta.Tactic.Grind.PropagatorAttr
 
 namespace Lean.Meta.Grind
@@ -318,10 +320,94 @@ where
     else
       return none
 
-def tryToProveFalse (e : Expr) : GoalM Unit := do
+/--
+Given a `match`-expression condition `e` that is known to be equal to `True`,
+try to close the goal by proving `False`. We use the following to example to illustrate
+the purpose of this function.
+```
+def f : List Nat → List Nat → Nat
+  | _, 1 :: _ :: _ => 1
+  | _, _ :: _ => 2
+  | _, _  => 0
+
+example : z = a :: as → y = z → f x y > 0 := by
+  grind [f.eq_def]
+```
+After `grind` unfolds `f`, it case splits on the `match`-expression producing
+three subgoals. The first two are easily closed by it. In the third one,
+we have the following two `match`-expression conditions stating that we
+are **not** in the first and second cases.
+```
+Lean.Grind.MatchCond (∀ (head : Nat) (tail : List Nat), x✝² = 1 :: head :: tail → False)
+Lean.Grind.MatchCond (∀ (head : Nat) (tail : List Nat), x✝² = head :: tail → False)
+```
+Moreover, we have the following equivalence class.
+```
+{z, y, x✝², a :: as}
+```
+Thus, we can close the goal by using the second `match`-expression condition,
+we just have to instantiate `head` and `tail` with `a` and `as` respectively,
+and use the fact that `x✝²` is equal to `a :: as`.
+-/
+partial def tryToProveFalse (e : Expr) : GoalM Unit := do
   trace_goal[grind.debug.matchCond.proveFalse] "{e}"
-  -- TODO
-  return ()
+  let_expr Grind.MatchCond body ← e | return ()
+  let proof? ← withNewMCtxDepth do
+    let (args, _, _) ← forallMetaTelescope body
+    let mask := mkGenDiseqMask body
+    for arg in args, target in mask do
+      if target then
+        let some (α?, lhs, rhs) := isEqHEq? (← inferType arg)
+          | return none
+        let lhs' ← go lhs
+        trace[grind.debug.matchCond.proveFalse] "{lhs'} =?= {rhs}"
+        unless (← withDefault <| isDefEq lhs' rhs) do
+          return none
+        let isHEq := α?.isSome
+        let some lhsEqLhs' ← if isHEq then proveHEq? lhs lhs' else proveEq? lhs lhs'
+          | return none
+        unless (← isDefEq arg lhsEqLhs') do
+          return none
+    let he := mkOfEqTrueCore e (← mkEqTrueProof e)
+    let falseProof ← instantiateMVars (mkAppN he args)
+    if (← hasAssignableMVar falseProof) then
+      return none
+    trace[grind.debug.matchCond.proveFalse] "{falseProof} : {← inferType falseProof}"
+    return some falseProof
+  let some proof := proof? | return ()
+  closeGoal proof
+where
+  /--
+  Returns a term that is equal to `e`, but containing constructor applications
+  and literal values. `e` is the left-hand side of the equations in a `match`-expression
+  condition.
+  Remark: we could use the right-hand side to interrupt the recursion. For example,
+  suppose the equation is `x = ?head :: ?tail`. We only need to show that `x` is equal to
+  some term of the form `a :: as` to satisfy it. This function may return `a₁ :: b :: bs`,
+  which still allows us to satisfy the equation, but may have a bigger proof (e.g.,
+  a proof that `as` is equal to `b::bs`)
+  -/
+  go (e : Expr) : GoalM Expr := do
+    let root ← getRootENode e
+    if root.ctor then
+      let ctor := root.self
+      let some ctorInfo ← isConstructorApp? ctor | return ctor
+      let mut ctorArgs := ctor.getAppArgs
+      let mut modified := false
+      for i in [ctorInfo.numParams : ctorInfo.numParams + ctorInfo.numFields] do
+        let arg  := ctorArgs[i]!
+        let arg' ← go arg
+        unless isSameExpr arg arg' do
+          ctorArgs := ctorArgs.set! i arg'
+          modified := true
+      if modified then
+        shareCommon <| mkAppN ctor.getAppFn ctorArgs
+      else
+        return root.self
+    else if root.interpreted then
+      return root.self
+    else
+      return e
 
 /-- Propagates `MatchCond` upwards -/
 builtin_grind_propagator propagateMatchCondUp ↑Grind.MatchCond := fun e => do

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

@@ -0,0 +1,85 @@
+/-
+Copyright (c) 2025 Amazon.com, Inc. or its affiliates. All Rights Reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Leonardo de Moura
+-/
+prelude
+import Lean.Meta.Tactic.Grind.Types
+import Lean.Meta.Tactic.Grind.Simp
+
+namespace Lean.Meta.Grind
+
+/--
+Helper function for executing `x` with a fresh `newEqs` and without modifying
+the goal state.
+ -/
+private def withoutModifyingState (x : GoalM α) : GoalM α := do
+  let saved ← get
+  modify fun goal => { goal with newEqs := {} }
+  try
+    x
+  finally
+    set saved
+
+/--
+If `e` has not been internalized yet, simplify it, and internalize the result.
+-/
+private def simpAndInternalize (e : Expr) (gen : Nat := 0) : GoalM Simp.Result := do
+  if (← alreadyInternalized e) then
+    return { expr := e }
+  else
+    let r ← simp e
+    internalize r.expr gen
+    return r
+
+/--
+Try to construct a proof that `lhs = rhs` using the information in the
+goal state. If `lhs` and `rhs` have not been internalized, this function
+will internalize then, process propagated equalities, and then check
+whether they are in the same equivalence class or not.
+The goal state is not modified by this function.
+This function mainly relies on congruence closure, and constraint
+propagation. It will not perform case analysis.
+-/
+def proveEq? (lhs rhs : Expr) : GoalM (Option Expr) := do
+  if (← alreadyInternalized lhs <&&> alreadyInternalized rhs) then
+    if (← isEqv lhs rhs) then
+      return some (← mkEqProof lhs rhs)
+    else
+      return none
+  else withoutModifyingState do
+    let lhs ← simpAndInternalize lhs
+    let rhs ← simpAndInternalize rhs
+    processNewEqs
+    unless (← isEqv lhs.expr rhs.expr) do return none
+    unless (← hasSameType lhs.expr rhs.expr) do return none
+    let h ← mkEqProof lhs.expr rhs.expr
+    let h ← match lhs.proof?, rhs.proof? with
+      | none,    none    => pure h
+      | none,    some h₂ => mkEqTrans h (← mkEqSymm h₂)
+      | some h₁, none    => mkEqTrans h₁ h
+      | some h₁, some h₂ => mkEqTrans (← mkEqTrans h₁ h) (← mkEqSymm h₂)
+    return some h
+
+/-- Similiar to `proveEq?`, but for heterogeneous equality. -/
+def proveHEq? (lhs rhs : Expr) : GoalM (Option Expr) := do
+  if (← alreadyInternalized lhs <&&> alreadyInternalized rhs) then
+    if (← isEqv lhs rhs) then
+      return some (← mkHEqProof lhs rhs)
+    else
+      return none
+  else withoutModifyingState do
+    let lhs ← simpAndInternalize lhs
+    let rhs ← simpAndInternalize rhs
+    processNewEqs
+    unless (← isEqv lhs.expr rhs.expr) do return none
+    let h ← mkHEqProof lhs.expr rhs.expr
+    let h ← match lhs.proof?, rhs.proof? with
+      | none,    none    => pure h
+      | none,    some h₂ => mkHEqTrans h (← mkHEqSymm h₂)
+      | some h₁, none    => mkHEqTrans h₁ h
+      | some h₁, some h₂ => mkHEqTrans (← mkHEqTrans h₁ h) (← mkHEqSymm h₂)
+    return some h
+
+
+end Lean.Meta.Grind

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

@@ -744,6 +744,10 @@ opaque mkHEqProof (a b : Expr) : GoalM Expr
 @[extern "lean_grind_internalize"]
 opaque internalize (e : Expr) (generation : Nat) (parent? : Option Expr := none) : GoalM Unit
 
+-- Forward definition
+@[extern "lean_grind_process_new_eqs"]
+opaque processNewEqs : GoalM Unit
+
 /--
 Returns a proof that `a = b` if they have the same type. Otherwise, returns a proof of `HEq a b`.
 It assumes `a` and `b` are in the same equivalence class.

tests/lean/run/grind_match_cond_contra.lean

@@ -0,0 +1,7 @@
+def f : List Nat → List Nat → Nat
+  | _, 1 :: _ :: _ => 1
+  | _, _ :: _ => 2
+  | _, _  => 0
+
+example : z = a :: as → y = z → f x y > 0 := by
+  grind [f.eq_def]