From 87dae299b89f7dffebae8ccd9bb8111250ef4a98 Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leomoura@amazon.com>
Date: Sun, 27 Jul 2025 19:51:23 +0200
Subject: [PATCH] fix: `ite` and `dite` should not be used in E-matching
 patterns (#9579)
MIME-Version: 1.0
Content-Type: text/plain; charset=UTF-8
Content-Transfer-Encoding: 8bit

This PR ensures `ite` and `dite` are to selected as E-matching patterns.
They are bad patterns because the then/else branches are only
internalized after `grind` decided whether the condition is
`True`/`False`.

The issue reported by #9572 has been fixed, but the fix exposed another
issue. The patterns for `List.Pairwise` produce an unbounded number of
E-matching instances.
```lean
example (l : List α) : l.Pairwise R := by
  grind
```
---
 src/Init/Grind/Tactics.lean    |  8 ++++++-
 tests/lean/run/grind_9572.lean | 41 ++++++++++++++++++++++++++++++++++
 2 files changed, 48 insertions(+), 1 deletion(-)
 create mode 100644 tests/lean/run/grind_9572.lean

diff --git a/src/Init/Grind/Tactics.lean b/src/Init/Grind/Tactics.lean
index bc320bda42..956c7e622e 100644
--- a/src/Init/Grind/Tactics.lean
+++ b/src/Init/Grind/Tactics.lean
@@ -425,7 +425,13 @@ Sets symbol priorities for the E-matching pattern inference procedure used in `g
 -/
 
 -- The following symbols are never used in E-matching patterns
-attribute [grind symbol 0] Eq HEq Iff And Or Not
+attribute [grind symbol 0] Eq HEq Iff And Or Not ite dite
+/-
+Remark for `ite` and `dite`: recall the then/else branches
+are only internalized after `grind` decided whether the condition is
+`True`/`False`. Thus, they **must** not be used a `grind` patterns.
+-/
+
 -- The following symbols are only used as the root pattern symbol if there isn't another option
 attribute [grind symbol low] HAdd.hAdd HSub.hSub HMul.hMul Dvd.dvd HDiv.hDiv HMod.hMod
 
diff --git a/tests/lean/run/grind_9572.lean b/tests/lean/run/grind_9572.lean
new file mode 100644
index 0000000000..c6da2b815c
--- /dev/null
+++ b/tests/lean/run/grind_9572.lean
@@ -0,0 +1,41 @@
+def List.Disjoint (l₁ l₂ : List α) : Prop :=
+  ∀ ⦃a⦄, a ∈ l₁ → a ∈ l₂ → False
+
+
+/--
+error: `grind` failed
+case grind
+i n : Nat
+f : Nat → List (List Nat)
+l : List Nat
+h :
+  ¬List.Pairwise
+      (fun x y =>
+        (if x ^ i ≤ n then List.map (fun m => x :: m) (f x) else []).Disjoint
+          (if y ^ i ≤ n then List.map (fun m => y :: m) (f y) else []))
+      l
+⊢ False
+[grind] Goal diagnostics
+  [facts] Asserted facts
+    [prop] ¬List.Pairwise
+            (fun x y =>
+              (if x ^ i ≤ n then List.map (fun m => x :: m) (f x) else []).Disjoint
+                (if y ^ i ≤ n then List.map (fun m => y :: m) (f y) else []))
+            l
+  [eqc] False propositions
+    [prop] List.Pairwise
+          (fun x y =>
+            (if x ^ i ≤ n then List.map (fun m => x :: m) (f x) else []).Disjoint
+              (if y ^ i ≤ n then List.map (fun m => y :: m) (f y) else []))
+          l
+-/
+#guard_msgs in
+theorem test (f : Nat → List (List Nat)) {l : List Nat} :
+    l.Pairwise
+      (fun x y ↦
+        (if x ^ i ≤ n then List.map (fun m ↦ x :: m) (f x) else []).Disjoint
+        (if y ^ i ≤ n then List.map (fun m ↦ y :: m) (f y) else [])) := by
+  -- TODO: fix patterns in standard library
+  -- We had to disable `List.pairwise_iff_forall_sublist` otherwise an unbounded
+  -- number of instances is produced.
+  grind [-List.pairwise_iff_forall_sublist]