fix: missing propagation in grind (#6528)

This PR adds a missing propagation rule to the (WIP) `grind` tactic.
leanprover · Jan 4, 2025 · 37127ea · 37127ea
1 parent 31435e9
commit 37127ea
Show file tree

Hide file tree

Showing 2 changed files with 5 additions and 0 deletions.
diff --git 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
@@ -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