refactor: symmetric equality congruence in grind (#11147)

This PR refactors the implementation of the symmetric equality
congruence rule used in `grind`.

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

@@ -32,27 +32,9 @@ def addCongrTable (e : Expr) : GoalM Unit := do
           reportIssue! "found congruence between{indentExpr e}\nand{indentExpr e'}\nbut functions have different types"
           return ()
     trace_goal[grind.debug.congr] "{e} = {e'}"
-    if (← isEqCongrProp e) then
-      /-
-      **Note**: We added this case to avoid a non-termination during proof construction.
-      We had the following equivalence class
-      ```
-      {p, q, p = q, q = p, True}
-      ```
-      Recall that `True` is always the root of its equivalence class.
-      We had the following two paths in the equivalence class:
-      ```
-      1. p -> p = q -> q = p -> True
-      2. q -> True
-      ```
-      Then, suppose we try to build a proof for `p = True`.
-      We have to construct a proof for `(p = q) = (q = p)`.
-      The equalities are congruent, but if we try to prove `p = q` and `q = p`,
-      We have to construct `p = True` and `True = q`, and we are back to `p = True`.
-      By constructing the congruence proof eagerly we ensure the non-termination cannot happen.
-      Note that this can only happen if `α₁` is a `Prop`.
-      -/
-      pushEqHEq e e' (← mkEqCongrProof e e')
+    if (← isEqCongrSymm e e') then
+      -- **Note**: See comment at `eqCongrSymmPlaceholderProof`
+      pushEqHEq e e' eqCongrSymmPlaceholderProof
     else
       pushEqHEq e e' congrPlaceholderProof
     if (← swapCgrRepr e e') then
@@ -74,9 +56,11 @@ def addCongrTable (e : Expr) : GoalM Unit := do
   else
     modify fun s => { s with congrTable := s.congrTable.insert { e } }
 where
-  isEqCongrProp (e : Expr) : GoalM Bool := do
-    let_expr Eq α _ _ := e | return false
-    return α.isProp
+  isEqCongrSymm (e e' : Expr) : GoalM Bool := do
+    let_expr Eq _ a₁ b₁ := e | return false
+    let_expr Eq _ a₂ b₂ := e' | return false
+    let goal ← get
+    return goal.hasSameRoot a₁ b₂ && goal.hasSameRoot b₁ a₂
 
   swapCgrRepr (e e' : Expr) : GoalM Bool := do
     let_expr Eq _ _ _ := e | return false

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

@@ -210,16 +210,21 @@ mutual
   partial def mkEqCongrProof (lhs rhs : Expr) : GoalM Expr := withIncRecDepth do
     let_expr f@Eq α₁ a₁ b₁ := lhs | unreachable!
     let_expr Eq α₂ a₂ b₂ := rhs | unreachable!
+    assert! (← get).hasSameRoot a₁ a₂ && (← get).hasSameRoot b₁ b₂
     let us := f.constLevels!
     if !isSameExpr α₁ α₂ then
-      if (← get).hasSameRoot a₁ a₂ && (← get).hasSameRoot b₁ b₂ then
-        return mkApp8 (mkConst ``Grind.heq_congr us) α₁ α₂ a₁ b₁ a₂ b₂ (← mkEqProofCore a₁ a₂ true) (← mkEqProofCore b₁ b₂ true)
-      else
-        return mkApp8 (mkConst ``Grind.heq_congr' us) α₁ α₂ a₁ b₁ a₂ b₂ (← mkEqProofCore a₁ b₂ true) (← mkEqProofCore b₁ a₂ true)
-    if (← get).hasSameRoot a₁ a₂ && (← get).hasSameRoot b₁ b₂ then
-      return mkApp7 (mkConst ``Grind.eq_congr us) α₁ a₁ b₁ a₂ b₂ (← mkEqProofCore a₁ a₂ false) (← mkEqProofCore b₁ b₂ false)
+      return mkApp8 (mkConst ``Grind.heq_congr us) α₁ α₂ a₁ b₁ a₂ b₂ (← mkEqProofCore a₁ a₂ true) (← mkEqProofCore b₁ b₂ true)
+    else
+      return mkApp7 (mkConst ``Grind.eq_congr us) α₁ a₁ b₁ a₂ b₂ (← mkEqProofCore a₁ a₂ false) (← mkEqProofCore b₁ b₂ false)
+
+  partial def mkEqCongrSymmProof (lhs rhs : Expr) : GoalM Expr := withIncRecDepth do
+    let_expr f@Eq α₁ a₁ b₁ := lhs | unreachable!
+    let_expr Eq α₂ a₂ b₂ := rhs | unreachable!
+    assert! (← get).hasSameRoot a₁ b₂ && (← get).hasSameRoot b₁ a₂
+    let us := f.constLevels!
+    if !isSameExpr α₁ α₂ then
+      return mkApp8 (mkConst ``Grind.heq_congr' us) α₁ α₂ a₁ b₁ a₂ b₂ (← mkEqProofCore a₁ b₂ true) (← mkEqProofCore b₁ a₂ true)
     else
-      assert! (← get).hasSameRoot a₁ b₂ && (← get).hasSameRoot b₁ a₂
       return mkApp7 (mkConst ``Grind.eq_congr' us) α₁ a₁ b₁ a₂ b₂ (← mkEqProofCore a₁ b₂ false) (← mkEqProofCore b₁ a₂ false)
 
   /-- Constructs a congruence proof for `lhs` and `rhs`. -/
@@ -247,8 +252,11 @@ mutual
         mkHCongrProof lhs rhs heq
 
   private partial def realizeEqProof (lhs rhs : Expr) (h : Expr) (flipped : Bool) (heq : Bool) : GoalM Expr := do
-    let h ← if h == congrPlaceholderProof then
+    if h == congrPlaceholderProof then
       mkCongrProof lhs rhs heq
+    else if h == eqCongrSymmPlaceholderProof then
+      let r ← mkEqCongrSymmProof lhs rhs
+      if heq then mkHEqOfEq r else return r
     else
       flipProof h flipped heq
 

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

@@ -23,6 +23,38 @@ namespace Lean.Meta.Grind
 /-- We use this auxiliary constant to mark delayed congruence proofs. -/
 def congrPlaceholderProof := mkConst (Name.mkSimple "[congruence]")
 
+/--
+We use this auxiliary constant to mark delayed symmetric congruence proofs.
+**Example:** `a = b` is symmetrically congruent to `c = d` if `a = d` and `b = c`.
+
+**Note:** We previously used `congrPlaceholderProof` for this case, but it
+caused non-termination during proof term construction when `a = b = c = d`.
+The issue was that we did not have enough information to determine how
+`a = b` and `c = d` became congruent. The new marker resolves this issue.
+
+If `congrPlaceholderProof` is used, then `a = b` became congruent to `c = d`
+because `a = c` and `b = d`.
+If `eqCongrSymmPlaceholderProof` is used, then it was because `a = d` and `b = c`.
+
+**Example:** suppose we have the following equivalence class:
+```
+{p, q, p = q, q = p, True}
+```
+Recall that `True` is always the root of its equivalence class.
+Assume we also have the following two paths in the class:
+```
+1. p -> p = q -> q = p -> True
+2. q -> True
+```
+Now suppose we try to build a proof for `p = True`.
+We must construct a proof for `(p = q) = (q = p)`.
+These equalities are congruent, but if we try to prove `p = q` and `q = p`
+using the facts `p = True` and `q = True`, we end up trying to prove `p = True` again.
+In other words, we are missing the information that `p = q` became congruent to `q = p`
+because of the symmetric case. By using `eqCongrSymmPlaceholderProof`, we retain this information.
+-/
+def eqCongrSymmPlaceholderProof := mkConst (Name.mkSimple "[eq_congr_symm]")
+
 /-- Similar to `isDefEq`, but ensures default transparency is used. -/
 def isDefEqD (t s : Expr) : MetaM Bool :=
   withDefault <| isDefEq t s
@@ -1122,7 +1154,7 @@ def pushEqCore (lhs rhs proof : Expr) (isHEq : Bool) : GoalM Unit := do
       throwError "`grind` internal error, lhs of new equality has not been internalized{indentExpr lhs}"
     unless (← alreadyInternalized rhs) do
       throwError "`grind` internal error, rhs of new equality has not been internalized{indentExpr rhs}"
-    unless proof == congrPlaceholderProof do
+    if proof != congrPlaceholderProof && proof != eqCongrSymmPlaceholderProof then
       let expectedType ← if isHEq then mkHEq lhs rhs else mkEq lhs rhs
       unless (← withReducible <| isDefEq (← inferType proof) expectedType) do
         throwError "`grind` internal error, trying to assert equality{indentExpr expectedType}\n\