feat: check cgRoot at Inv.lean

leanprover · Dec 28, 2024 · 0fef828 · 0fef828
1 parent 1059307
commit 0fef828
Showing 1 changed file with 7 additions and 0 deletions.
diff --git a/src/Lean/Meta/Tactic/Grind/Inv.lean b/src/Lean/Meta/Tactic/Grind/Inv.lean
@@ -20,6 +20,13 @@ private def checkEqc (root : ENode) : GoalM Unit := do
     size := size + 1
     -- The root of `curr` must be `root`
     assert! isSameExpr (← getRoot curr) root.self
+    -- Check congruence root
+    if curr.isApp then
+      if let some { e } := (← get).congrTable.find? { e := curr } then
+        if (← hasSameType e.getAppFn curr.getAppFn) then
+          assert! isSameExpr e (← getENode curr).cgRoot
+      else
+        assert! isSameExpr curr (← getENode curr).cgRoot
     -- If the equivalence class does not have HEq proofs, then the types must be definitionally equal.
     unless root.heqProofs do
       assert! (← hasSameType curr root.self)