fix: grind proof instability (#10881)

This PR fixes a proof instability source in `grind`.

We say a proof is *unstable* if minor changes in the `.lean` file
containing the proof **affect** it.

Author: leodemoura

src/Lean/Meta/Tactic/Grind/Arith/Cutsat/MBTC.lean

@@ -22,7 +22,7 @@ private def getAssignmentExt? (e : Expr) : GoalM (Option Rat) := do
     return none
   else if type == Nat.mkType then
     -- TODO: improve this case.
-    for parent in (← getParents e) do
+    for parent in (← getParents e).elems do
       let_expr NatCast.natCast _ inst _ := parent | pure ()
       let_expr instNatCastInt := inst | pure ()
       return (← getAssignment? (← get) parent)

src/Lean/Meta/Tactic/Grind/Arith/ModelUtil.lean

@@ -22,7 +22,7 @@ Returns `true` if adding the assignment `e := v` to `a` will falsify any asserte
 -/
 private partial def satisfyDiseqs (goal : Goal) (a : Std.HashMap Expr Rat) (e : Expr) (v : Int) : Bool := Id.run do
   let some parents := goal.parents.find? { expr := e } | return true
-  for parent in parents do
+  for parent in parents.elems do
     let_expr Eq _ lhs rhs := parent | continue
     let some root := goal.getRoot? parent | continue
     if root.isConstOf ``False then

src/Lean/Meta/Tactic/Grind/Core.lean

@@ -48,7 +48,7 @@ This is an auxiliary function performed while merging equivalence classes.
 -/
 private def removeParents (root : Expr) : GoalM ParentSet := do
   let parents ← getParents root
-  for parent in parents do
+  for parent in parents.elems do
     -- Recall that we may have `Expr.forallE` in `parents` because of `ForallProp.lean`
     if (← pure (isCongrRelevant parent) <&&> isCongrRoot parent) then
       trace_goal[grind.debug.parent] "remove: {parent}"
@@ -60,7 +60,7 @@ Reinserts parents into the congruence table and detect new equalities.
 This is an auxiliary function performed while merging equivalence classes.
 -/
 private def reinsertParents (parents : ParentSet) : GoalM Unit := do
-  for parent in parents do
+  for parent in parents.elems do
     if (← pure (isCongrRelevant parent) <&&> isCongrRoot parent) then
       trace_goal[grind.debug.parent] "reinsert: {parent}"
       addCongrTable parent
@@ -88,7 +88,7 @@ The modification time is used to decide which terms are considered during e-matc
 -/
 private partial def updateMT (root : Expr) : GoalM Unit := do
   let gmt := (← get).ematch.gmt
-  for parent in (← getParents root) do
+  for parent in (← getParents root).elems do
     let node ← getENode parent
     if node.mt < gmt then
       setENode parent { node with mt := gmt }
@@ -103,8 +103,8 @@ def propagateBeta (lams : Array Expr) (fns : Array Expr) : GoalM Unit := do
   let lamRoot ← getRoot lams.back!
   trace_goal[grind.debug.beta] "fns: {fns}, lams: {lams}"
   for fn in fns do
-    trace_goal[grind.debug.beta] "fn: {fn}, parents: {(← getParents fn).toArray}"
-    for parent in (← getParents fn) do
+    trace_goal[grind.debug.beta] "fn: {fn}, parents: {(← getParents fn).elems}"
+    for parent in (← getParents fn).elems do
       let mut args := #[]
       let mut curr := parent
       trace_goal[grind.debug.beta] "parent: {parent}"
@@ -230,7 +230,7 @@ where
     unless (← isInconsistent) do
       updateMT rhsRoot.self
     unless (← isInconsistent) do
-      for parent in parents do
+      for parent in parents.elems do
         propagateUp parent
       for e in toPropagateDown do
         propagateDown e

src/Lean/Meta/Tactic/Grind/Inv.lean

@@ -66,7 +66,7 @@ def checkMatchCondParent (e : Expr) (parent : Expr) : GoalM Bool := do
 
 def checkParents (e : Expr) : GoalM Unit := do
   if (← isRoot e) then
-    for parent in (← getParents e) do
+    for parent in (← getParents e).elems do
       if isMatchCond parent then
         unless (← checkMatchCondParent e parent) do
           throwError "e: {e}, parent: {parent}"

src/Lean/Meta/Tactic/Grind/Types.lean

@@ -598,8 +598,40 @@ instance : BEq (CongrKey enodeMap) where
 
 abbrev CongrTable (enodeMap : ENodeMap) := PHashSet (CongrKey enodeMap)
 
--- Remark: we cannot use pointer addresses here because we have to traverse the tree.
-abbrev ParentSet := Std.TreeSet Expr Expr.quickComp
+/-
+**Note**: If inserting elements in a `ParentSet` becomes a performance bottleneck,
+we can add an extra field `Std.HashSet ExprPtr` for detecting whether the `ParentSet` already
+contains an element or not.
+
+**Note**: We used to implement `ParentSet`s as
+```abbrev ParentSet := Std.TreeSet Expr Expr.quickComp```
+This representation created proof stability issues.
+For example, we traverse this set to implement congruence closure.
+There is no non-determinism here, but the traversal depends on the `Expr`
+hash code, which is very sensitive to changes in a `.lean` file.
+Thus, minor changes may affect the proof found by `grind`. We found examples
+where proving the same goal multiple times in the same file produced different
+proofs.
+When we inspected the hash codes, they were completely different.
+Using `Expr.comp` does not help because it still relies on internal free variable IDs.
+One might think we can just reset them at the beginning of the `grind` search, but
+this is not sufficient. When tactics such as `finish?` generate the final tactic
+script, we remove unnecessary case splits. Removing case splits affects the generated
+free variable IDs, which in turn affects the result of Expr.comp :(
+-/
+structure ParentSet where
+  parents : List Expr := []
+  deriving Inhabited
+
+def ParentSet.insert (ps : ParentSet) (p : Expr) : ParentSet :=
+  { ps with parents := ps.parents.insert p }
+
+def ParentSet.isEmpty (ps : ParentSet) : Bool :=
+  ps.parents.isEmpty
+
+def ParentSet.elems (ps : ParentSet) : List Expr :=
+  ps.parents
+
 abbrev ParentMap := PHashMap ExprPtr ParentSet
 
 /--
@@ -1124,7 +1156,7 @@ Copy `parents` to the parents of `root`.
 -/
 def copyParentsTo (parents : ParentSet) (root : Expr) : GoalM Unit := do
   let mut curr := if let some parents := (← get).parents.find? { expr := root } then parents else {}
-  for parent in parents do
+  for parent in parents.elems do
     curr := curr.insert parent
   modify fun s => { s with parents := s.parents.insert { expr := root } curr }
 
@@ -1172,7 +1204,7 @@ For each equality `b = c` in `parents`, executes `k b c` IF
 - `b = c` is equal to `False`, and
 -/
 @[inline] def forEachDiseq (parents : ParentSet) (k : (lhs : Expr) → (rhs : Expr) → GoalM Unit) : GoalM Unit := do
-  for parent in parents do
+  for parent in parents.elems do
     let_expr Eq _ b c := parent | continue
     if (← isEqFalse parent) then
       if (← isEqv b c) then

tests/lean/run/grind_indexmap_trace.lean

@@ -147,8 +147,7 @@ example (m : IndexMap α β) (a : α) (h : a ∈ m) :
 info: Try this:
   [apply] ⏎
     instantiate only [= mem_indices_of_mem, insert]
-    instantiate only [=_ HashMap.contains_iff_mem, = getElem?_neg, = getElem?_pos]
-    instantiate only [=_ HashMap.contains_iff_mem]
+    instantiate only [= getElem?_neg, = getElem?_pos, =_ HashMap.contains_iff_mem]
     cases #4ed2
     next =>
       cases #ffdf
@@ -176,12 +175,11 @@ example (m : IndexMap α β) (a a' : α) (b : β) :
     a' ∈ m.insert a b ↔ a' = a ∨ a' ∈ m := by
   grind => finish?
 
--- **TODO**: Investigate whey the following `finish?` has one fewer step.
 /--
 info: Try this:
   [apply] ⏎
     instantiate only [= mem_indices_of_mem, insert]
-    instantiate only [=_ HashMap.contains_iff_mem, = getElem?_neg, = getElem?_pos]
+    instantiate only [= getElem?_neg, = getElem?_pos, =_ HashMap.contains_iff_mem]
     cases #4ed2
     next =>
       cases #ffdf