fix: equality propagation in grind order

This PR fixes a bug in the equality propagation procedure in
`grind.order`. Specifically, it affects the procedure that asserts
equalities in the `grind` core state that are implied by (ring) inequalities
in the `grind.order` module.

closes #10622

Author: leodemoura

src/Init/Grind/Order.lean

@@ -107,6 +107,11 @@ Helper theorem for equality propagation
 theorem eq_of_le_of_le {α} [LE α] [Std.IsPartialOrder α] {a b : α} : a ≤ b → b ≤ a → a = b :=
   Std.IsPartialOrder.le_antisymm _ _
 
+theorem eq_of_le_of_le_0 {α} [LE α] [Std.IsPartialOrder α] [Ring α]
+    {a b : α} : a ≤ b + Int.cast (R := α) 0 → b ≤ a + Int.cast (R := α) 0 → a = b := by
+  simp [Ring.intCast_zero, Semiring.add_zero]
+  apply Std.IsPartialOrder.le_antisymm
+
 /-!
 Transitivity
 -/

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

@@ -210,8 +210,19 @@ public def mkUnsatProof (u v : Expr) (k₁ : Weight) (h₁ : Expr) (k₂ : Weigh
   else
     mkUnsatProofCore u v k₁ h₁ k₂ h₂
 
-public def mkEqProofOfLeOfLe (u v : Expr) (h₁ : Expr) (h₂ : Expr) : OrderM Expr := do
+public def mkEqProofOfLeOfLeCore (u v : Expr) (h₁ : Expr) (h₂ : Expr) : OrderM Expr := do
   let h ← mkLePartialPrefix ``Grind.Order.eq_of_le_of_le
   return mkApp4 h u v h₁ h₂
 
+public def mkEqProofOfLeOfLeOffset (u v : Expr) (h₁ : Expr) (h₂ : Expr) : OrderM Expr := do
+  let h ← mkLePartialPrefix ``Grind.Order.eq_of_le_of_le_0
+  let h := mkApp h (← getStruct).ringInst?.get!
+  return mkApp4 h u v h₁ h₂
+
+public def mkEqProofOfLeOfLe (u v : Expr) (h₁ : Expr) (h₂ : Expr) : OrderM Expr := do
+  if (← isRing) then
+    mkEqProofOfLeOfLeOffset  u v h₁ h₂
+  else
+    mkEqProofOfLeOfLeCore u v h₁ h₂
+
 end Lean.Meta.Grind.Order

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

@@ -33,6 +33,11 @@ structure Cnstr (α : Type) where
   k      : Int := 0
   /-- Denotation of this constraint as an expression. -/
   e      : Expr
+  /--
+  If `h? := some h`, then `h` is proof for that the expression associated with this constraint
+  is equal to `e`. Recall that the input constraints are normalized. For example, given `x y : Int`,
+  `x ≤ y` is internally represented as `x ≤ y + 0`
+  -/
   h?     : Option Expr := none
   deriving Inhabited
 

tests/lean/run/grind_10622.lean

@@ -0,0 +1,11 @@
+def Int.leastOfBdd {P : Int → Prop} [DecidablePred P] (b : Int) (Hb : ∀ z : Int, P z → b ≤ z)
+    (Hinh : ∃ z : Int, P z) : { lb : Int // P lb ∧ ∀ z : Int, P z → lb ≤ z } :=
+  sorry
+
+theorem Int.coe_leastOfBdd_eq {P : Int → Prop} [DecidablePred P] {b b' : Int} (Hb : ∀ z : Int, P z → b ≤ z)
+    (Hb' : ∀ z : Int, P z → b' ≤ z) (Hinh : ∃ z : Int, P z) :
+    (leastOfBdd b Hb Hinh : Int) = leastOfBdd b' Hb' Hinh := by
+  grind
+
+example (f : Int → Int) (x y : Int) : x ≤ y → y ≤ x → f x = f y := by
+  grind -cutsat -linarith