From e46b5f39bf77dffed3af8bfe154c73c2b772107f Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Thu, 2 Jan 2025 20:08:02 +0100 Subject: [PATCH] fix: congruence closure in the `grind` tactic (#6509) This PR fixes a bug in the congruence closure data structure used in the `grind` tactic. The new test includes an example that previously caused a panic. A similar panic was also occurring in the test `grind_nested_proofs.lean`. --- src/Lean/Meta/Tactic/Grind/Core.lean | 10 ++++++---- src/Lean/Meta/Tactic/Grind/EMatch.lean | 6 +++--- src/Lean/Meta/Tactic/Grind/Internalize.lean | 2 +- src/Lean/Meta/Tactic/Grind/Inv.lean | 4 ++-- src/Lean/Meta/Tactic/Grind/Types.lean | 21 +++++++++++++++++---- tests/lean/run/grind_ematch2.lean | 12 ++++++++++++ tests/lean/run/grind_nested_proofs.lean | 5 ++--- 7 files changed, 43 insertions(+), 17 deletions(-) diff --git a/src/Lean/Meta/Tactic/Grind/Core.lean b/src/Lean/Meta/Tactic/Grind/Core.lean index 0a80f7e753..747e9eb987 100644 --- a/src/Lean/Meta/Tactic/Grind/Core.lean +++ b/src/Lean/Meta/Tactic/Grind/Core.lean @@ -41,8 +41,9 @@ This is an auxiliary function performed while merging equivalence classes. private def removeParents (root : Expr) : GoalM ParentSet := do let parents ← getParentsAndReset root for parent in parents do - trace[grind.debug.parent] "remove: {parent}" - modify fun s => { s with congrTable := s.congrTable.erase { e := parent } } + if (← isCongrRoot parent) then + trace[grind.debug.parent] "remove: {parent}" + modify fun s => { s with congrTable := s.congrTable.erase { e := parent } } return parents /-- @@ -51,8 +52,9 @@ This is an auxiliary function performed while merging equivalence classes. -/ private def reinsertParents (parents : ParentSet) : GoalM Unit := do for parent in parents do - trace[grind.debug.parent] "reinsert: {parent}" - addCongrTable parent + if (← isCongrRoot parent) then + trace[grind.debug.parent] "reinsert: {parent}" + addCongrTable parent /-- Closes the goal when `True` and `False` are in the same equivalence class. -/ private def closeGoalWithTrueEqFalse : GoalM Unit := do diff --git a/src/Lean/Meta/Tactic/Grind/EMatch.lean b/src/Lean/Meta/Tactic/Grind/EMatch.lean index 762048e120..1d19b860ba 100644 --- a/src/Lean/Meta/Tactic/Grind/EMatch.lean +++ b/src/Lean/Meta/Tactic/Grind/EMatch.lean @@ -122,7 +122,7 @@ private partial def processMatch (c : Choice) (p : Expr) (e : Expr) : M Unit := let n ← getENode curr if n.generation <= maxGeneration -- uses heterogeneous equality or is the root of its congruence class - && (n.heqProofs || isSameExpr curr n.cgRoot) + && (n.heqProofs || n.isCongrRoot) && eqvFunctions pFn curr.getAppFn && curr.getAppNumArgs == numArgs then if let some c ← matchArgs? c p curr |>.run then @@ -140,7 +140,7 @@ private def processContinue (c : Choice) (p : Expr) : M Unit := do for app in apps do let n ← getENode app if n.generation <= maxGeneration - && (n.heqProofs || isSameExpr n.cgRoot app) then + && (n.heqProofs || n.isCongrRoot) then if let some c ← matchArgs? c p app |>.run then let gen := n.generation let c := { c with gen := Nat.max gen c.gen } @@ -225,7 +225,7 @@ private def main (p : Expr) (cnstrs : List Cnstr) : M Unit := do for app in apps do if (← checkMaxInstancesExceeded) then return () let n ← getENode app - if (n.heqProofs || isSameExpr n.cgRoot app) && + if (n.heqProofs || n.isCongrRoot) && (!useMT || n.mt == gmt) then if let some c ← matchArgs? { cnstrs, assignment, gen := n.generation } p app |>.run then modify fun s => { s with choiceStack := [c] } diff --git a/src/Lean/Meta/Tactic/Grind/Internalize.lean b/src/Lean/Meta/Tactic/Grind/Internalize.lean index fb4986404e..6231923227 100644 --- a/src/Lean/Meta/Tactic/Grind/Internalize.lean +++ b/src/Lean/Meta/Tactic/Grind/Internalize.lean @@ -25,7 +25,7 @@ def addCongrTable (e : Expr) : GoalM Unit := do trace[grind.debug.congr] "{e} = {e'}" pushEqHEq e e' congrPlaceholderProof let node ← getENode e - setENode e { node with cgRoot := e' } + setENode e { node with congr := e' } else modify fun s => { s with congrTable := s.congrTable.insert { e } } diff --git a/src/Lean/Meta/Tactic/Grind/Inv.lean b/src/Lean/Meta/Tactic/Grind/Inv.lean index b0e77d7a30..c09ad807e7 100644 --- a/src/Lean/Meta/Tactic/Grind/Inv.lean +++ b/src/Lean/Meta/Tactic/Grind/Inv.lean @@ -24,9 +24,9 @@ private def checkEqc (root : ENode) : GoalM Unit := do 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 + assert! isSameExpr e (← getCongrRoot curr) else - assert! isSameExpr curr (← getENode curr).cgRoot + assert! (← isCongrRoot curr) -- 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) diff --git a/src/Lean/Meta/Tactic/Grind/Types.lean b/src/Lean/Meta/Tactic/Grind/Types.lean index 2f62f59b72..1065c7b4d3 100644 --- a/src/Lean/Meta/Tactic/Grind/Types.lean +++ b/src/Lean/Meta/Tactic/Grind/Types.lean @@ -173,8 +173,12 @@ structure ENode where next : Expr /-- Root (aka canonical representative) of the equivalence class -/ root : Expr - /-- Root of the congruence class. This is field is a don't care if `e` is not an application. -/ - cgRoot : Expr + /-- + `congr` is the term `self` is congruent to. + We say `self` is the congruence class root if `isSameExpr congr self`. + This field is initialized to `self` even if `e` is not an application. + -/ + congr : Expr /-- When `e` was added to this equivalence class because of an equality `h : e = target`, then we store `target` here, and `h` at `proof?`. @@ -206,6 +210,9 @@ structure ENode where -- TODO: see Lean 3 implementation deriving Inhabited, Repr +def ENode.isCongrRoot (n : ENode) := + isSameExpr n.self n.congr + /-- New equality to be processed. -/ structure NewEq where lhs : Expr @@ -540,7 +547,7 @@ def setENode (e : Expr) (n : ENode) : GoalM Unit := def mkENodeCore (e : Expr) (interpreted ctor : Bool) (generation : Nat) : GoalM Unit := do setENode e { - self := e, next := e, root := e, cgRoot := e, size := 1 + self := e, next := e, root := e, congr := e, size := 1 flipped := false heqProofs := false hasLambdas := e.isLambda @@ -562,7 +569,13 @@ def mkENode (e : Expr) (generation : Nat) : GoalM Unit := do /-- Returns `true` is `e` is the root of its congruence class. -/ def isCongrRoot (e : Expr) : GoalM Bool := do - return isSameExpr e (← getENode e).cgRoot + return (← getENode e).isCongrRoot + +/-- Returns the root of the congruence class containing `e`. -/ +partial def getCongrRoot (e : Expr) : GoalM Expr := do + let n ← getENode e + if isSameExpr n.congr e then return e + getCongrRoot n.congr /-- Return `true` if the goal is inconsistent. -/ def isInconsistent : GoalM Bool := diff --git a/tests/lean/run/grind_ematch2.lean b/tests/lean/run/grind_ematch2.lean index 08d2238d17..2d4f1c850b 100644 --- a/tests/lean/run/grind_ematch2.lean +++ b/tests/lean/run/grind_ematch2.lean @@ -17,3 +17,15 @@ example (as bs cs : Array α) (v₁ v₂ : α) (h₆ : j < as.size) : cs[j] = as[j] := by grind + +example (as bs cs : Array α) (v₁ v₂ : α) + (i₁ i₂ j : Nat) + (h₁ : i₁ < as.size) + (h₂ : as.set i₁ v₁ = bs) + (h₃ : i₂ < bs.size) + (h₃ : bs.set i₂ v₂ = cs) + (h₄ : i₁ ≠ j ∧ j ≠ i₂) + (h₅ : j < cs.size) + (h₆ : j < as.size) + : cs[j] = as[j] := by + grind diff --git a/tests/lean/run/grind_nested_proofs.lean b/tests/lean/run/grind_nested_proofs.lean index 12bc224f99..bee9020b60 100644 --- a/tests/lean/run/grind_nested_proofs.lean +++ b/tests/lean/run/grind_nested_proofs.lean @@ -12,9 +12,8 @@ elab "grind_test" : tactic => withMainContext do let [_, n, _] := nodes.toList | unreachable! logInfo (← getEqc n.self) --- TODO: fix --- set_option grind.debug true --- set_option grind.debug.proofs true +set_option grind.debug true +set_option grind.debug.proofs true /- Recall that array access terms, such as `a[i]`, have nested proofs.