From 9096eb168d9f7ec6d5aafbcc0d36e48723fab4e8 Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leomoura@amazon.com>
Date: Sat, 10 May 2025 20:18:18 -0700
Subject: [PATCH] fix: arrow congruence in `grind` (#8280)

This PR the support for arrows in the congruence closure procedure used
in `grind`.
---
 src/Lean/Meta/Tactic/Grind/Core.lean       | 10 ++++++++--
 src/Lean/Meta/Tactic/Grind/ForallProp.lean |  6 +++---
 tests/lean/run/grind_congr.lean            |  3 +++
 3 files changed, 14 insertions(+), 5 deletions(-)

diff --git a/src/Lean/Meta/Tactic/Grind/Core.lean b/src/Lean/Meta/Tactic/Grind/Core.lean
index bf35bed0f8..7fbcc6a2c7 100644
--- a/src/Lean/Meta/Tactic/Grind/Core.lean
+++ b/src/Lean/Meta/Tactic/Grind/Core.lean
@@ -37,6 +37,12 @@ where
       proof?  := proofNew?
     }
 
+/--
+Returns `true` if the parent is relevant for congruence closure.
+-/
+private def isCongrRelevant (parent : Expr) : Bool :=
+  parent.isApp || parent.isArrow
+
 /--
 Removes `root` parents from the congruence table.
 This is an auxiliary function performed while merging equivalence classes.
@@ -45,7 +51,7 @@ private def removeParents (root : Expr) : GoalM ParentSet := do
   let parents ← getParents root
   for parent in parents do
     -- Recall that we may have `Expr.forallE` in `parents` because of `ForallProp.lean`
-    if (← pure parent.isApp <&&> isCongrRoot parent) then
+    if (← pure (isCongrRelevant parent) <&&> isCongrRoot parent) then
       trace_goal[grind.debug.parent] "remove: {parent}"
       modify fun s => { s with congrTable := s.congrTable.erase { e := parent } }
   return parents
@@ -56,7 +62,7 @@ This is an auxiliary function performed while merging equivalence classes.
 -/
 private def reinsertParents (parents : ParentSet) : GoalM Unit := do
   for parent in parents do
-    if (← pure parent.isApp <&&> isCongrRoot parent) then
+    if (← pure (isCongrRelevant parent) <&&> isCongrRoot parent) then
       trace_goal[grind.debug.parent] "reinsert: {parent}"
       addCongrTable parent
 
diff --git a/src/Lean/Meta/Tactic/Grind/ForallProp.lean b/src/Lean/Meta/Tactic/Grind/ForallProp.lean
index 417e1931e0..b26ef02547 100644
--- a/src/Lean/Meta/Tactic/Grind/ForallProp.lean
+++ b/src/Lean/Meta/Tactic/Grind/ForallProp.lean
@@ -37,13 +37,13 @@ def propagateForallPropUp (e : Expr) : GoalM Unit := do
 where
   propagateImpliesUp (a b : Expr) : GoalM Unit := do
     unless (← alreadyInternalized b) do return ()
-    if (← isEqFalse a) then
+    if (← isEqFalse a <&&> isProp b) then
       -- a = False → (a → b) = True
       pushEqTrue e <| mkApp3 (mkConst ``Grind.imp_eq_of_eq_false_left) a b (← mkEqFalseProof a)
-    else if (← isEqTrue a) then
+    else if (← isEqTrue a <&&> isProp b) then
       -- a = True → (a → b) = b
       pushEq e b <| mkApp3 (mkConst ``Grind.imp_eq_of_eq_true_left) a b (← mkEqTrueProof a)
-    else if (← isEqTrue b) then
+    else if (← isEqTrue b <&&> isProp a) then
       -- b = True → (a → b) = True
       pushEqTrue e <| mkApp3 (mkConst ``Grind.imp_eq_of_eq_true_right) a b (← mkEqTrueProof b)
     else if (← isEqFalse b <&&> isEqTrue e <&&> isProp a) then
diff --git a/tests/lean/run/grind_congr.lean b/tests/lean/run/grind_congr.lean
index 7b3f9330b1..72e30aa9fd 100644
--- a/tests/lean/run/grind_congr.lean
+++ b/tests/lean/run/grind_congr.lean
@@ -47,3 +47,6 @@ example (a b c d e v : Nat) : f v = c → f (g b) = d → a = e → b = e → v
 -- arrow congruence test
 example : α = α' → α'' = α' → β' = β → (α → β) = (α'' → β') := by
   grind
+
+example (a b c : Nat) (h₁ : a = c) (h₂ : b = c) : (a = b → Nat) = (b = a → Nat) := by
+  grind