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

@@ -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
 

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}" #[]

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