fix: disequality ctor propagation in grind (#11133)

This PR fixes disequality propagation for constructor applications in
`grind`. The equivalence class representatives may be distinct
constructor applications, but we must ensure they have the same type.
Examples that were panic'ing before this PR:
```lean
example (a b : List Nat)
    : a ≍ ([] : List Int) → b ≍ ([1] : List Int) → a = b ∨ p → p := by
  grind

example (a b : List Nat)
    : a = [] → a ≍ ([] : List Int) → b = [1] → a = b ∨ p → p := by
  grind

example (a b : List Nat)
    : a = [] → a ≍ ([] : List Int) → b = [1] → b ≍ [(1 : Int)] → a = b ∨ p → p := by
  grind

example (a b : List Nat)
    : a = [] → b = [1] → a = b ∨ p → p := by
  grind

example (a b : List Nat)
    : a = [] → a ≍ ([] : List Int) → b = [1] → a = b ∨ p → p := by
  grind
```

Closes #11124

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

@@ -161,12 +161,50 @@ builtin_grind_propagator propagateEqUp ↑Eq := fun e => do
   else unless (← isEqFalse e) do
     if aRoot.ctor && bRoot.ctor && aRoot.self.getAppFn != bRoot.self.getAppFn then
       -- ¬a = b
-      let hne ← withLocalDeclD `h (← mkEq a b) fun h => do
-        let hf ← mkEqTrans (← mkEqProof aRoot.self a) h
-        let hf ← mkEqTrans hf (← mkEqProof b bRoot.self)
-        let hf ← mkNoConfusion (← getFalseExpr) hf
-        mkLambdaFVars #[h] hf
-      pushEqFalse e <| mkApp2 (mkConst ``eq_false) e hne
+      /-
+      **Note**: `a` and `b` have the same type because `e` is a type correct term and is of the form `@Eq α a b`
+      However, `a` and `aRoot` may not. Same for `b` and `bRoot`, and `aRoot` and `bRoot`.
+      We must check that. If this is not the case, we should search their equivalence classes looking
+      for distinct constructor applications with the same type.
+      -/
+
+      /-
+      Helper function. Give `aCtor` and `bCtor` s.t.
+      - `a` and `aCtor` are in the same equivalence class.
+      - `b` and `bCtor` are in the same equivalence class.
+      - `aCtor` and `bCtor` have the same type **and** are distinct constructor applications
+
+      Returns a proof that `a ≠ b`
+      -/
+      let mkNe (aCtor bCtor : Expr) : GoalM Expr := do
+        withLocalDeclD `h (← mkEq a b) fun hab => do
+          let hf ← match (← hasSameType a aCtor), (← hasSameType b bCtor) with
+          | true,  true  =>
+            let hf ← mkEqTrans (← mkEqProof aCtor a) hab
+            mkEqTrans hf (← mkEqProof b bCtor)
+          | _,  _ =>
+            let hf ← mkHEqTrans (← mkHEqProof aCtor a) (← mkHEqOfEq hab)
+            let hf ← mkHEqTrans hf (← mkHEqProof b bCtor)
+            mkEqOfHEq hf
+          let hf ← mkNoConfusion (← getFalseExpr) hf
+          mkLambdaFVars #[hab] hf
+      if (← hasSameType aRoot.self bRoot.self) then
+        let hne ← mkNe aRoot.self bRoot.self
+        pushEqFalse e <| mkApp2 (mkConst ``eq_false) e hne
+      else
+        /-
+        `aRoot.self` and `bRoot.self` do **not** have the same type. Thus, we search
+        if there are other constructor applications in their equivalence classes.
+        -/
+        discard <| findEqc a fun aNode' => do
+          unless aNode'.ctor do return false
+          findEqc b fun bNode' => do
+            unless bNode'.ctor do return false
+            if aNode'.self.getAppFn == bNode'.self.getAppFn then return false
+            unless (← hasSameType aNode'.self bNode'.self) do return false
+            let hne ← mkNe aNode'.self bNode'.self
+            pushEqFalse e <| mkApp2 (mkConst ``eq_false) e hne
+            return true
 
 /-- Propagates `Eq` downwards -/
 builtin_grind_propagator propagateEqDown ↓Eq := fun e => do

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

@@ -1393,6 +1393,18 @@ def getExprs : GoalM (PArray Expr) := do
     if isSameExpr n.next e then return ()
     curr := n.next
 
+/--
+Executes `f` to each term in the equivalence class containing `e`, and stops as soon as `f` returns `true`.
+-/
+@[inline] def findEqc (e : Expr) (f : ENode → GoalM Bool) : GoalM Bool := do
+  let mut curr := e
+  repeat
+    let n ← getENode curr
+    if (← f n) then return true
+    if isSameExpr n.next e then break
+    curr := n.next
+  return false
+
 /-- Folds using `f` and `init` over the equivalence class containing `e` -/
 @[inline] def foldEqc (e : Expr) (init : α) (f : ENode → α → GoalM α) : GoalM α := do
   let mut curr := e

tests/lean/run/grind_11124.lean

@@ -0,0 +1,160 @@
+example (a b : List Nat)
+    : a ≍ ([] : List Int) → b ≍ ([1] : List Int) → a = b ∨ p → p := by
+  grind
+
+example (a b : List Nat)
+    : a = [] → a ≍ ([] : List Int) → b = [1] → a = b ∨ p → p := by
+  grind
+
+example (a b : List Nat)
+    : a = [] → a ≍ ([] : List Int) → b = [1] → b ≍ [(1 : Int)] → a = b ∨ p → p := by
+  grind
+
+example (a b : List Nat)
+    : a = [] → b = [1] → a = b ∨ p → p := by
+  grind
+
+example (a b : List Nat)
+    : a = [] → a ≍ ([] : List Int) → b = [1] → a = b ∨ p → p := by
+  grind
+
+/--
+error: `grind` failed
+case grind
+p : Prop
+a b : List Nat
+h : a = []
+h_1 : b ≍ [1]
+h_2 : a = b ∨ p
+h_3 : ¬p
+⊢ False
+-/
+#guard_msgs in
+example (a b : List Nat)
+    : a = [] → b ≍ ([1] : List Int) → a = b ∨ p → p := by
+  grind -verbose
+
+
+section Mathlib.Data.List.Sigma
+
+namespace List
+
+variable {β : α → Type}
+
+def keys : List (Sigma β) → List α :=
+  map Sigma.fst
+
+@[grind =]
+theorem mem_keys {a} {l : List (Sigma β)} : a ∈ l.keys ↔ ∃ b : β a, Sigma.mk a b ∈ l := sorry
+
+def NodupKeys (l : List (Sigma β)) : Prop :=
+  l.keys.Nodup
+
+theorem notMem_keys_of_nodupKeys_cons {s : Sigma β} {l : List (Sigma β)} (h : NodupKeys (s :: l)) :
+    s.1 ∉ l.keys := sorry
+
+variable [DecidableEq α]
+
+def dlookup (a : α) : List (Sigma β) → Option (β a)
+  | [] => none
+  | ⟨a', b⟩ :: l => if h : a' = a then some (Eq.recOn h b) else dlookup a l
+
+@[grind =]
+theorem dlookup_cons_eq (l) (a : α) (b : β a) : dlookup a (⟨a, b⟩ :: l) = some b := sorry
+
+theorem dlookup_eq_none {a : α} {l : List (Sigma β)} : dlookup a l = none ↔ a ∉ l.keys := sorry
+
+theorem of_mem_dlookup {a : α} {b : β a} {l : List (Sigma β)} :
+    b ∈ dlookup a l → Sigma.mk a b ∈ l := sorry
+
+theorem map_dlookup_eq_find (a : α) (l : List (Sigma β)) :
+    (dlookup a l).map (Sigma.mk a) = find? (fun s => a = s.1) l := sorry
+
+theorem lookup_ext {l₀ l₁ : List (Sigma β)} (nd₀ : l₀.NodupKeys) (nd₁ : l₁.NodupKeys)
+    (h : ∀ x y, y ∈ l₀.dlookup x ↔ y ∈ l₁.dlookup x) : l₀ ~ l₁ := sorry
+
+def kerase (a : α) : List (Sigma β) → List (Sigma β) :=
+  eraseP fun s => a = s.1
+
+def kunion : List (Sigma β) → List (Sigma β) → List (Sigma β)
+  | [], l₂ => l₂
+  | s :: l₁, l₂ => s :: kunion l₁ (kerase s.1 l₂)
+
+end List
+
+end Mathlib.Data.List.Sigma
+
+section Mathlib.Data.List.AList
+
+open List
+
+variable {α : Type} {β : α → Type}
+
+structure AList (β : α → Type) where
+  entries : List (Sigma β)
+
+namespace AList
+
+def keys (s : AList β) : List α := sorry
+
+variable [DecidableEq α]
+
+instance : Union (AList β) := sorry
+
+theorem union_entries {s₁ s₂ : AList β} : (s₁ ∪ s₂).entries = kunion s₁.entries s₂.entries :=
+  sorry
+
+/-- Two associative lists are disjoint if they have no common keys. -/
+def Disjoint (s₁ s₂ : AList β) : Prop :=
+  ∀ k ∈ s₁.keys, k ∉ s₂.keys
+
+/--
+error: `grind` failed
+case grind.1.1.2.2.1.1.1
+α : Type
+β : α → Type
+inst : (a b : α) → Decidable (a = b)
+s₁ s₂ : AList β
+h : s₁.Disjoint s₂
+x : α
+y : β x
+h_1 : (y ∈ dlookup x (s₁.entries.kunion s₂.entries)) = ¬y ∈ dlookup x (s₂.entries.kunion s₁.entries)
+left : y ∈ dlookup x (s₁.entries.kunion s₂.entries)
+right : ¬y ∈ dlookup x (s₂.entries.kunion s₁.entries)
+left_1 : dlookup x (s₂.entries.kunion s₁.entries) = none
+right_1 : ¬x ∈ (s₂.entries.kunion s₁.entries).keys
+left_2 : ¬dlookup x (s₁.entries.kunion s₂.entries) = none
+right_2 : x ∈ (s₁.entries.kunion s₂.entries).keys
+w : β x
+h_5 : ⟨x, w⟩ ∈ s₁.entries.kunion s₂.entries
+left_3 : ¬find? (fun s => decide (x = s.fst)) (s₁.entries.kunion s₂.entries) = none
+right_3 : ¬∀ (x_1 : Sigma β), x_1 ∈ s₁.entries.kunion s₂.entries → decide (x = x_1.fst) = false
+w_1 : Sigma β
+h_8 : ¬(w_1 ∈ s₁.entries.kunion s₂.entries → decide (x = w_1.fst) = false)
+w_2 : Sigma β
+h_10 : ¬(w_2 ∈ s₁.entries.kunion s₂.entries → decide (w_1.fst = w_2.fst) = false)
+w_3 : Sigma β
+h_12 : ¬(w_3 ∈ s₁.entries.kunion s₂.entries → decide (w_2.fst = w_3.fst) = false)
+h_13 : (fun s => decide (w_1.fst = s.fst)) = fun s => decide (x = s.fst)
+left_4 : ⟨x, cast ⋯ w_1.snd⟩ ∈ ⟨x, w⟩ :: s₂.entries.kunion s₁.entries
+right_4 : ⟨x, cast ⋯ w_1.snd⟩ = ⟨x, w⟩ ∨ ⟨x, cast ⋯ w_1.snd⟩ ∈ s₂.entries.kunion s₁.entries
+h_15 : (fun s => decide (w_2.fst = s.fst)) = fun s => decide (x = s.fst)
+⊢ False
+-/
+#guard_msgs in
+theorem union_comm_of_disjoint {s₁ s₂ : AList β} (h : Disjoint s₁ s₂) :
+    (s₁ ∪ s₂).entries ~ (s₂ ∪ s₁).entries :=
+  lookup_ext sorry sorry
+    (by
+      intros; simp only [union_entries]
+      grind -verbose [
+      dlookup_eq_none,
+      map_dlookup_eq_find,
+      of_mem_dlookup,
+      notMem_keys_of_nodupKeys_cons
+      ]
+    )
+
+end AList
+
+end Mathlib.Data.List.AList