feat: add Grind.mkDiseqProof? (#7231)

This PR implements functions for constructing disequality proofs in
`grind`.

src/Init/Grind/Lemmas.lean

@@ -69,6 +69,11 @@ theorem eq_eq_of_eq_true_right {a b : Prop} (h : b = True) : (a = b) = a := by s
 theorem eq_congr  {α : Sort u} {a₁ b₁ a₂ b₂ : α} (h₁ : a₁ = a₂) (h₂ : b₁ = b₂) : (a₁ = b₁) = (a₂ = b₂) := by simp [*]
 theorem eq_congr' {α : Sort u} {a₁ b₁ a₂ b₂ : α} (h₁ : a₁ = b₂) (h₂ : b₁ = a₂) : (a₁ = b₁) = (a₂ = b₂) := by rw [h₁, h₂, Eq.comm (a := a₂)]
 
+/-! Ne -/
+
+theorem ne_of_ne_of_eq_left {α : Sort u} {a b c : α} (h₁ : a = b) (h₂ : b ≠ c) : a ≠ c := by simp [*]
+theorem ne_of_ne_of_eq_right {α : Sort u} {a b c : α} (h₁ : a = c) (h₂ : b ≠ c) : b ≠ a := by simp [*]
+
 /-! Bool.and -/
 
 theorem Bool.and_eq_of_eq_true_left {a b : Bool} (h : a = true) : (a && b) = b := by simp [h]

src/Lean/Meta/Tactic/Grind.lean

@@ -28,6 +28,7 @@ import Lean.Meta.Tactic.Grind.Arith
 import Lean.Meta.Tactic.Grind.Ext
 import Lean.Meta.Tactic.Grind.MatchCond
 import Lean.Meta.Tactic.Grind.MatchDiscrOnly
+import Lean.Meta.Tactic.Grind.Diseq
 
 namespace Lean
 

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

@@ -226,11 +226,11 @@ where
     propagateBeta lams₁ fns₁
     propagateBeta lams₂ fns₂
     resetParentsOf lhsRoot.self
+    propagateOffsetEq rhsRoot lhsRoot
+    propagateCutsatEq rhsRoot lhsRoot
     copyParentsTo parents rhsNode.root
     unless (← isInconsistent) do
       updateMT rhsRoot.self
-    propagateOffsetEq rhsRoot lhsRoot
-    propagateCutsatEq rhsRoot lhsRoot
     unless (← isInconsistent) do
       for parent in parents do
         propagateUp parent

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

@@ -0,0 +1,87 @@
+/-
+Copyright (c) 2025 Amazon.com, Inc. or its affiliates. All Rights Reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Leonardo de Moura
+-/
+prelude
+import Init.Grind.Lemmas
+import Lean.Meta.Tactic.Grind.Types
+
+namespace Lean.Meta.Grind
+
+/--
+Returns `true` if type of `t` is definitionally equal to `α`
+-/
+private def hasType (t α : Expr) : MetaM Bool :=
+  withDefault do isDefEq (← inferType t) α
+
+/--
+Returns `some (c = d)` if
+- `c = d` and `False` are in the same equivalence class, and
+- `a` (`b`) and `c` are in the same equivalence class, and
+- `b` (`a`) and `d` are in the same equivalence class.
+Otherwise return `none`.
+
+Remark `a` and `b` are assumed to have the same type.
+-/
+private def getDiseqFor? (a b : Expr) : GoalM (Option Expr) := do
+  /-
+  In Z3, we use the congruence table to find equalities more efficiently,
+  but this optimization would be more complicated here because equalities have
+  the type as an implicit argument, and `grind`s congruence table assumes it is
+  hash-consed and canonicalized. So, we use the "slower" approach of visiting
+  parents.
+  -/
+  let aRoot ← getRoot a
+  let bRoot ← getRoot b
+  let aParents ← getParents aRoot
+  let bParents ← getParents bRoot
+  if aParents.size ≤ bParents.size then
+    go aParents
+  else
+    go bParents
+where
+  go (parents : ParentSet) : GoalM (Option Expr) := do
+    for parent in parents do
+      let_expr Eq α c d := parent | continue
+      if (← isEqFalse parent) then
+        -- Remark: we expect `hasType` test to seldom fail, but it can happen because of
+        -- heterogeneous equalities
+        if (← isEqv a c <&&> isEqv b d <&&> hasType a α) then
+          return some parent
+        if (← isEqv a d <&&> isEqv b c <&&> hasType a α) then
+          return some parent
+    return none
+
+/--
+Returns `true` if `a` and `b` are known to be disequal.
+See `getDiseqFor?`
+-/
+def isDiseq (a b : Expr) : GoalM Bool := do
+  return (← getDiseqFor? a b).isSome
+
+/--
+Returns a proof for `true` if `a` and `b` are known to be disequal.
+See `getDiseqFor?`
+-/
+def mkDiseqProof? (a b : Expr) : GoalM (Option Expr) := do
+  let some eq ← getDiseqFor? a b | return none
+  let_expr f@Eq α c d := eq | unreachable!
+  let u := f.constLevels!
+  let h ← mkOfEqFalse (← mkEqFalseProof eq)
+  let (c, d, h) ← if (← isEqv a c <&&> isEqv b d) then
+    pure (c, d, h)
+  else
+    pure (d, c, mkApp4 (mkConst ``Ne.symm u) α c d h)
+  -- We have `a = c` and `b = d`
+  let h ← if isSameExpr a c then
+    pure h
+  else
+    pure <| mkApp6 (mkConst ``Grind.ne_of_ne_of_eq_left u) α a c d (← mkEqProof a c) h
+  -- `h : a ≠ d
+  if isSameExpr b d then
+    return h
+  else
+    return mkApp6 (mkConst ``Grind.ne_of_ne_of_eq_right u) α b a d (← mkEqProof b d) h
+
+end Lean.Meta.Grind

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

@@ -6,6 +6,7 @@ Authors: Leonardo de Moura
 prelude
 import Init.Grind.Tactics
 import Init.Data.Queue
+import Std.Data.TreeSet
 import Lean.Util.ShareCommon
 import Lean.HeadIndex
 import Lean.Meta.Basic
@@ -396,7 +397,7 @@ instance : BEq (CongrKey enodes) where
 abbrev CongrTable (enodes : ENodeMap) := PHashSet (CongrKey enodes)
 
 -- Remark: we cannot use pointer addresses here because we have to traverse the tree.
-abbrev ParentSet := RBTree Expr Expr.quickComp
+abbrev ParentSet := Std.TreeSet Expr Expr.quickComp
 abbrev ParentMap := PHashMap ENodeKey ParentSet
 
 /--

tests/lean/run/grind_diseq_api.lean

@@ -0,0 +1,80 @@
+import Lean
+
+opaque a : Nat
+opaque b : Nat
+
+-- Prints the equivalence class containing a `f` application
+open Lean Meta Grind in
+def fallback : Fallback := do
+  let a ← shareCommon <| mkConst ``a
+  let b ← shareCommon <| mkConst ``b
+  let some h ← mkDiseqProof? a b |
+    throwError "terms are not diseq"
+  check h
+  trace[Meta.debug] "{h} : {← inferType h}"
+  assert! (← isDiseq a b)
+  assert! (← isDiseq b a)
+  let some h' ← mkDiseqProof? b a |
+    throwError "terms are not diseq"
+  let h' ← mkAppM ``Ne.symm #[h']
+  assert! (← isDefEq h h')
+  (← get).mvarId.admit
+
+set_option trace.Meta.debug true
+
+/--
+info: [Meta.debug] Lean.Grind.ne_of_ne_of_eq_right h_2 (Lean.Grind.ne_of_ne_of_eq_left h (Ne.symm h_1)) : a ≠ b
+-/
+#guard_msgs (info) in
+example (x y : Nat) : a = x → y ≠ x → b = y → False := by
+  grind on_failure fallback
+
+/--
+info: [Meta.debug] Lean.Grind.ne_of_ne_of_eq_right h_2 (Lean.Grind.ne_of_ne_of_eq_left h h_1) : a ≠ b
+-/
+#guard_msgs (info) in
+example (x y : Nat) : a = x → x ≠ y → b = y → False := by
+  grind on_failure fallback
+
+/--
+info: [Meta.debug] Lean.Grind.ne_of_ne_of_eq_right h_3 (Lean.Grind.ne_of_ne_of_eq_left (Eq.trans h (Eq.symm h_1)) h_2) : a ≠ b
+-/
+#guard_msgs (info) in
+example (x y z : Nat) : a = x → z = x → z ≠ y → b = y → False := by
+  grind on_failure fallback
+
+/-- info: [Meta.debug] Lean.Grind.ne_of_ne_of_eq_left h (Ne.symm h_1) : a ≠ b -/
+#guard_msgs (info) in
+example (x : Nat) : a = x → b ≠ x → False := by
+  grind on_failure fallback
+
+/-- info: [Meta.debug] Lean.Grind.ne_of_ne_of_eq_left h h_1 : a ≠ b -/
+#guard_msgs (info) in
+example (x : Nat) : a = x → x ≠ b → False := by
+  grind on_failure fallback
+
+
+/-- info: [Meta.debug] Lean.Grind.ne_of_ne_of_eq_right h h_1 : a ≠ b -/
+#guard_msgs (info) in
+example (x : Nat) : b = x → a ≠ x → False := by
+  grind on_failure fallback
+
+/-- info: [Meta.debug] Lean.Grind.ne_of_ne_of_eq_right h (Ne.symm h_1) : a ≠ b -/
+#guard_msgs (info) in
+example (x : Nat) : b = x → x ≠ a → False := by
+  grind on_failure fallback
+
+/-- info: [Meta.debug] Lean.Grind.ne_of_ne_of_eq_left h (Ne.symm h_1) : a ≠ b -/
+#guard_msgs (info) in
+example (x : Nat) : a = x → b ≠ x → False := by
+  grind on_failure fallback
+
+/-- info: [Meta.debug] h : ¬a = b -/
+#guard_msgs (info) in
+example : a ≠ b → False := by
+  grind on_failure fallback
+
+/-- info: [Meta.debug] Ne.symm h : a ≠ b -/
+#guard_msgs (info) in
+example : b ≠ a → False := by
+  grind on_failure fallback