From 3881f21df1177a2eca01d26f47490be9b43b4fad Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leomoura@amazon.com>
Date: Tue, 21 Jan 2025 14:19:24 -0800
Subject: [PATCH] fix: redundant information in the offset constraint module
 (#6734)

This PR ensures there are no redundant entries in the offset constraint
model produced by `grind`
---
 src/Lean/Meta/Tactic/Grind/Arith/Model.lean |  2 +-
 src/Lean/Meta/Tactic/Grind/PP.lean          |  1 +
 tests/lean/run/grind_t1.lean                | 25 +++++++++++++++++++++
 3 files changed, 27 insertions(+), 1 deletion(-)

diff --git a/src/Lean/Meta/Tactic/Grind/Arith/Model.lean b/src/Lean/Meta/Tactic/Grind/Arith/Model.lean
index 4e06105eb0..0df1287161 100644
--- a/src/Lean/Meta/Tactic/Grind/Arith/Model.lean
+++ b/src/Lean/Meta/Tactic/Grind/Arith/Model.lean
@@ -39,7 +39,7 @@ def mkModel (goal : Goal) : MetaM (Array (Expr × Nat)) := do
     We should not include the assignment for auxiliary offset terms since
     they do not provide any additional information.
     -/
-    if (isNatOffset? e).isNone && isNatNum? e != some 0 then
+    if !(← isLitValue e) && (isNatOffset? e).isNone && isNatNum? e != some 0 then
       r := r.push (e, val)
   return r
 
diff --git a/src/Lean/Meta/Tactic/Grind/PP.lean b/src/Lean/Meta/Tactic/Grind/PP.lean
index db7766c846..516379a603 100644
--- a/src/Lean/Meta/Tactic/Grind/PP.lean
+++ b/src/Lean/Meta/Tactic/Grind/PP.lean
@@ -121,6 +121,7 @@ private def ppOffset : M Unit := do
   let nodes := s.nodes
   if nodes.isEmpty then return ()
   let model ← Arith.Offset.mkModel goal
+  if model.isEmpty then return ()
   let mut ms := #[]
   for (e, val) in model do
     ms := ms.push <| .trace { cls := `assign } m!"{e} := {val}" #[]
diff --git a/tests/lean/run/grind_t1.lean b/tests/lean/run/grind_t1.lean
index f4edea106a..39c8e89109 100644
--- a/tests/lean/run/grind_t1.lean
+++ b/tests/lean/run/grind_t1.lean
@@ -325,3 +325,28 @@ example (x y : S) : x.a = y.a → y.b = x.b → x = y := by
 
 example (x : S) : x.a = 10 → false ≠ x.b → x = { a := 10, b := true } := by
   grind
+
+
+-- In the following test, we should not display `10 := 10` and `20 := 20` in the
+-- assignment produced by the offset module
+/--
+error: `grind` failed
+case grind
+a : Nat
+b : Bool
+a✝¹ : (if b = true then 10 else 20) = a
+a✝ : b = true
+⊢ False
+[grind] Diagnostics
+  [facts] Asserted facts
+    [prop] (if b = true then 10 else 20) = a
+    [prop] b = true
+  [eqc] True propositions
+    [prop] b = true
+  [eqc] Equivalence classes
+    [eqc] {a, if b = true then 10 else 20, 10}
+    [eqc] {b, true}
+-/
+#guard_msgs (error) in
+example (b : Bool) : (if b then 10 else 20) = a → b = true → False := by
+  grind