fix: stackoverflow during proof construction in grind

This PR fixes a stack overflow that occurs when constructing a proof
term in `grind`.

Closes 11081

src/Init/Grind/Lemmas.lean

@@ -78,6 +78,9 @@ theorem eq_congr' {α : Sort u} {a₁ b₁ a₂ b₂ : α} (h₁ : a₁ = b₂)
 theorem heq_congr  {α : Sort u} {β : Sort u} {a₁ b₁ : α} {a₂ b₂ : β} (h₁ : a₁ ≍ a₂) (h₂ : b₁ ≍ b₂) : (a₁ = b₁) = (a₂ = b₂) := by cases h₁; cases h₂; rfl
 theorem heq_congr' {α : Sort u} {β : Sort u} {a₁ b₁ : α} {a₂ b₂ : β} (h₁ : a₁ ≍ b₂) (h₂ : b₁ ≍ a₂) : (a₁ = b₁) = (a₂ = b₂) := by cases h₁; cases h₂; rw [@Eq.comm _ a₁]
 
+theorem eq_symm {α : Sort u} {a b : α} : (a = b) = (b = a) := by
+  apply propext; constructor <;> intro <;> simp [*]
+
 /-! Ne -/
 
 theorem ne_of_ne_of_eq_left {α : Sort u} {a b c : α} (h₁ : a = b) (h₂ : b ≠ c) : a ≠ c := by simp [*]

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

@@ -216,7 +216,27 @@ mutual
         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)
-    else if (← get).hasSameRoot a₁ a₂ && (← get).hasSameRoot b₁ b₂ then
+    else if isSameExpr a₁ b₂ && isSameExpr b₁ a₂ 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`.
+      Note that this can only happen if `α₁` is a `Prop`.
+      -/
+      return mkApp3 (mkConst ``Grind.eq_symm us) α₁ a₁ b₁
+    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)
     else
       assert! (← get).hasSameRoot a₁ b₂ && (← get).hasSameRoot b₁ a₂

tests/lean/run/grind_11081.lean

@@ -0,0 +1,79 @@
+namespace List
+
+protected def diff {α} [BEq α] : List α → List α → List α
+  | l, [] => l
+  | l₁, a :: l₂ => if l₁.elem a then List.diff (l₁.erase a) l₂ else List.diff l₁ l₂
+
+def Subperm (l₁ l₂ : List α) : Prop := ∃ l, l ~ l₁ ∧ l <+ l₂
+
+open Perm (swap)
+
+theorem Perm.subperm_left {l l₁ l₂ : List α} (p : l₁ ~ l₂) : Subperm l l₁ ↔ Subperm l l₂ :=
+  sorry
+
+theorem Sublist.subperm {l₁ l₂ : List α} (s : l₁ <+ l₂) : Subperm l₁ l₂ := sorry
+
+theorem Subperm.perm_of_length_le {l₁ l₂ : List α} :
+    Subperm l₁ l₂ → length l₂ ≤ length l₁ → l₁ ~ l₂ :=
+  sorry
+
+end List
+
+variable {α : Type} [DecidableEq α] {l₁ l₂ : List α}
+
+open List
+
+/--
+error: `grind` failed
+case grind.1.1.1.1.1.1.1.1.1
+α : Type
+inst : (a b : α) → Decidable (a = b)
+l₁ l₂ : List α
+hl : l₂.Subperm l₁
+p : α → Bool
+h : ¬countP p l₁ = countP p (l₁.diff l₂ ++ l₂)
+w : α
+h_2 : ¬count w (l₁.diff l₂ ++ l₂) = count w l₁
+w_1 : α
+h_4 : ¬count w_1 l₁ = count w_1 (l₁.diff l₂ ++ l₂)
+left : l₂ ⊆ l₁
+right : ∀ {a : α}, a ∈ l₂ → a ∈ l₁
+left_1 : filter p l₂ <+ filter p l₁
+w_2 : List α
+left_2 : w_2 <+ l₁
+right_2 : filter p l₂ = filter p w_2
+w_3 : List α
+left_3 : w_3 <+ l₁
+right_3 : filter p l₂ = filter p w_3
+h_9 : (filter p l₂).length = (filter p l₁).length
+w_4 : α
+h_11 : ¬count w_4 (l₁.diff l₂ ++ l₂) = count w_4 l₂
+w_5 : α
+h_13 : ¬count w_5 l₂ = count w_5 (l₁.diff l₂ ++ l₂)
+left_4 : l₁.diff l₂ ~ l₁
+right_4 : ∀ (a : α), count a (l₁.diff l₂) = count a l₁
+w_6 : α
+h_16 : ¬count w_6 (l₁.diff l₂ ++ l₂) = count w_6 (l₁.diff l₂)
+w_7 : α
+h_18 : ¬count w_7 (l₁.diff l₂) = count w_7 (l₁.diff l₂ ++ l₂)
+left_5 : l₁.diff l₂ ~ l₂
+right_5 : ∀ (a : α), count a (l₁.diff l₂) = count a l₂
+left_6 : l₂ ~ l₁
+right_6 : ∀ (a : α), count a l₂ = count a l₁
+left_7 : l₂ ~ l₁.diff l₂
+right_7 : ∀ (a : α), count a l₂ = count a (l₁.diff l₂)
+left_8 : l₁ ~ l₁.diff l₂
+right_8 : ∀ (a : α), count a l₁ = count a (l₁.diff l₂)
+left_9 : l₁ ~ l₂
+right_9 : ∀ (a : α), count a l₁ = count a l₂
+⊢ False
+-/
+#guard_msgs in
+theorem countP_diff (hl : Subperm l₂ l₁) (p : α → Bool) :
+    countP p l₁ = countP p (l₁.diff l₂ ++ l₂) := by
+  grind -verbose [
+    List.Perm.subperm_left,
+    List.Sublist.subperm,
+    List.Subperm.perm_of_length_le,
+    List.Perm.countP_congr
+  ]