oops

src/Lean/Meta/Tactic/Grind.lean

@@ -32,6 +32,7 @@ import Lean.Meta.Tactic.Grind.Diseq
 import Lean.Meta.Tactic.Grind.MBTC
 import Lean.Meta.Tactic.Grind.Lookahead
 import Lean.Meta.Tactic.Grind.LawfulEqCmp
+import Lean.Meta.Tactic.Grind.ReflCmp
 
 namespace Lean
 

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

@@ -21,6 +21,7 @@ import Lean.Meta.Tactic.Grind.Solve
 import Lean.Meta.Tactic.Grind.SimpUtil
 import Lean.Meta.Tactic.Grind.Cases
 import Lean.Meta.Tactic.Grind.LawfulEqCmp
+import Lean.Meta.Tactic.Grind.ReflCmp
 
 namespace Lean.Meta.Grind
 
@@ -44,6 +45,7 @@ def mkMethods (fallback : Fallback) : CoreM Methods := do
     fallback
     propagateUp := fun e => do
      propagateForallPropUp e
+     propagateReflCmp e
      let .const declName _ := e.getAppFn | return ()
      propagateProjEq e
      if let some prop := builtinPropagators.up[declName]? then

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

@@ -0,0 +1,53 @@
+/-
+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: Kim Morrison
+-/
+prelude
+import Lean.Meta.Tactic.Grind.Types
+
+/-!
+Support for type class `ReflCmp`.
+-/
+/-
+Note: we will have similar support for `Associative` and `Commutative`. In the future, we should have
+a mechanism for letting users to install their own handlers.
+-/
+
+namespace Lean.Meta.Grind
+
+/--
+If `op` implements `ReflCmp`, then returns the proof term for
+`∀ a b, a = b → op a b = .eq`
+-/
+def getReflCmpThm? (op : Expr) : GrindM (Option Expr) := do
+  if let some thm? := (← get).reflCmpMap.find? { expr := op } then
+    return thm?
+  let thm? ← go?
+  modify fun s => { s with reflCmpMap := s.reflCmpMap.insert { expr := op } thm? }
+  return thm?
+where
+  go? : MetaM (Option Expr) := do
+    unless (← getEnv).contains ``Std.ReflCmp do return none
+    let opType ← whnf (← inferType op)
+    let .forallE _ α b _ := opType | return none
+    if b.hasLooseBVars then return none
+    let .forallE _ α' b _ ← whnf b | return none
+    unless b.isConstOf ``Ordering do return none
+    unless (← isDefEq α α') do return none
+    let u ← getLevel α
+    let some u ← decLevel? u | return none
+    let reflCmp := mkApp2 (mkConst ``Std.ReflCmp [u]) α op
+    let .some reflCmpInst ← trySynthInstance reflCmp | return none
+    return some <| mkApp3 (mkConst ``Std.ReflCmp.cmp_eq_of_eq [u]) α op reflCmpInst
+
+def propagateReflCmp (e : Expr) : GoalM Unit := do
+  let some op := getBinOp e | return ()
+  let some thm ← getReflCmpThm? op | return ()
+  let a := e.appFn!.appArg!
+  let b := e.appArg!
+  unless (← isEqv a b) do return ()
+  let oeq ← getOrderingEqExpr
+  pushEq e oeq <| mkApp3 thm a b (← mkEqProof a b)
+
+end Lean.Meta.Grind

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

@@ -194,6 +194,11 @@ structure State where
   if it implements the `LawfulEqCmp` type class.
   -/
   lawfulEqCmpMap : PHashMap ExprPtr (Option Expr) := {}
+  /--
+  Mapping from binary functions `f` to a theorem `thm : ∀ a, f a a = .eq`
+  if it implements the `ReflCmp` type class.
+  -/
+  reflCmpMap : PHashMap ExprPtr (Option Expr) := {}
 
 private opaque MethodsRefPointed : NonemptyType.{0}
 private def MethodsRef : Type := MethodsRefPointed.type

src/Std/Classes/Ord/Basic.lean

@@ -28,6 +28,13 @@ class ReflCmp {α : Type u} (cmp : α → α → Ordering) : Prop where
   /-- Comparison is reflexive. -/
   compare_self {a : α} : cmp a a = .eq
 
+namespace ReflCmp
+
+theorem cmp_eq_of_eq {α : Type u} {cmp : α → α → Ordering} [Std.ReflCmp cmp] {a b : α} : a = b → cmp a b = .eq := by
+  intro h; subst a; apply compare_self
+
+end ReflCmp
+
 /-- A typeclasses for ordered types for which `compare a a = .eq` for all `a`. -/
 abbrev ReflOrd (α : Type u) [Ord α] := ReflCmp (compare : α → α → Ordering)
 

tests/lean/run/grind_refl_cmp.lean

@@ -0,0 +1,7 @@
+import Std
+
+example (f : α → α → Ordering) [Std.ReflCmp f] (a : α) : f a a = .eq := by
+  grind
+
+example (f : α → α → Ordering) [Std.ReflCmp f] (a b : α) (h : a = b) : f a b = .eq := by
+  grind