From 37127ead07980694981d21a5866978ff6828403d Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leomoura@amazon.com>
Date: Sat, 4 Jan 2025 19:45:55 +0100
Subject: [PATCH] fix: missing propagation in `grind` (#6528)

This PR adds a missing propagation rule to the (WIP) `grind` tactic.
---
 src/Lean/Meta/Tactic/Grind/Propagate.lean       | 2 ++
 tests/lean/run/grind_propagate_connectives.lean | 3 +++
 2 files changed, 5 insertions(+)

diff --git a/src/Lean/Meta/Tactic/Grind/Propagate.lean b/src/Lean/Meta/Tactic/Grind/Propagate.lean
index 14a3a786ef..42d1135a14 100644
--- a/src/Lean/Meta/Tactic/Grind/Propagate.lean
+++ b/src/Lean/Meta/Tactic/Grind/Propagate.lean
@@ -99,6 +99,8 @@ builtin_grind_propagator propagateNotUp ↑Not := fun e => do
   else if (← isEqTrue a) then
     -- a = True → (Not a) = False
     pushEqFalse e <| mkApp2 (mkConst ``Lean.Grind.not_eq_of_eq_true) a (← mkEqTrueProof a)
+  else if (← isEqv e a) then
+    closeGoal <| mkApp2 (mkConst ``Lean.Grind.false_of_not_eq_self) a (← mkEqProof e a)
 
 /--
 Propagates truth values downwards for a negation expression `Not a` based on the truth value of `Not a`.
diff --git a/tests/lean/run/grind_propagate_connectives.lean b/tests/lean/run/grind_propagate_connectives.lean
index e4f4a020dc..6cb042ae1b 100644
--- a/tests/lean/run/grind_propagate_connectives.lean
+++ b/tests/lean/run/grind_propagate_connectives.lean
@@ -103,3 +103,6 @@ example (p q r : Prop) : p ∨ (q ↔ r) → ¬r → q → False := by
   grind on_failure do
     Lean.logInfo "hello world"
     fallback
+
+example (a b : Nat) : (a = b) = (b = a) := by
+  grind