From cf48c6004dd14438f78ffcf16b4bd87fa5678b29 Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Sun, 3 Aug 2025 14:27:26 +0200 Subject: [PATCH] fix: assertion violations at `grind` `checkInvariants` (#9700) This PR fixes assertion violations when `checkInvariants` is enabled in `grind` --- src/Lean/Meta/Tactic/Grind/Core.lean | 1 + src/Lean/Meta/Tactic/Grind/Internalize.lean | 4 ++-- 2 files changed, 3 insertions(+), 2 deletions(-) diff --git a/src/Lean/Meta/Tactic/Grind/Core.lean b/src/Lean/Meta/Tactic/Grind/Core.lean index 800af64a2f..cf2dd92656 100644 --- a/src/Lean/Meta/Tactic/Grind/Core.lean +++ b/src/Lean/Meta/Tactic/Grind/Core.lean @@ -384,6 +384,7 @@ where -- We must swap the congruence root to ensure `isDiseq` and `getDiseqFor?` work properly modify fun s => { s with congrTable := s.congrTable.insert { e := n.self } } setENode n.self { n with congr := n.self } + setENode e { (← getENode e) with congr := n.self } /-- Ensures collection of equations to be processed is empty. -/ private def resetNewFacts : GoalM Unit := diff --git a/src/Lean/Meta/Tactic/Grind/Internalize.lean b/src/Lean/Meta/Tactic/Grind/Internalize.lean index 09277f4772..09a44aa70e 100644 --- a/src/Lean/Meta/Tactic/Grind/Internalize.lean +++ b/src/Lean/Meta/Tactic/Grind/Internalize.lean @@ -47,8 +47,8 @@ def addCongrTable (e : Expr) : GoalM Unit := do we must ensure that `e` is still the congruence root. -/ modify fun s => { s with congrTable := s.congrTable.insert { e } } - let node ← getENode e' - setENode e' { node with congr := e } + setENode e' { (← getENode e') with congr := e } + setENode e { (← getENode e) with congr := e } else let node ← getENode e setENode e { node with congr := e' }