feat: NatCast.natCast unexpander (#7775)

This PR adds an unexpander for `NatCast.natCast`. See new comment for
details.

src/Init/Grind/Util.lean

@@ -78,6 +78,19 @@ def offsetUnexpander : PrettyPrinter.Unexpander := fun stx => do
   | `($_ $lhs:term $rhs:term) => `($lhs + $rhs)
   | _ => throw ()
 
+/-
+Remark: `↑a` is notation for `Nat.cast a`. `Nat.cast` is an abbreviation
+for `NatCast.natCast`. We added it because users wanted to use dot-notation (e.g., `a.cast`).
+`grind` expands all reducible definitions. Thus, a `grind` failure state contains
+many `NatCast.natCast` applications which is too verbose. We add the following
+unexpander to cope with this issue.
+-/
+@[app_unexpander NatCast.natCast]
+def natCastUnexpander : PrettyPrinter.Unexpander := fun stx => do
+  match stx with
+  | `($_ $a:term) => `(↑$a)
+  | _ => throw ()
+
 /--
 A marker to indicate that a proposition has already been normalized and should not
 be processed again.

tests/lean/run/grind_canon_insts.lean

@@ -59,11 +59,11 @@ def fallback : Fallback := do
 set_option trace.Meta.debug true
 
 /--
-info: [Meta.debug] [NatCast.natCast a * (NatCast.natCast b * NatCast.natCast c),
-     NatCast.natCast b * NatCast.natCast c,
-     NatCast.natCast d * (NatCast.natCast b * NatCast.natCast c),
-     -1 * (NatCast.natCast a * (NatCast.natCast b * NatCast.natCast c)),
-     -1 * (NatCast.natCast d * (NatCast.natCast b * NatCast.natCast c)),
+info: [Meta.debug] [↑a * (↑b * ↑c),
+     ↑b * ↑c,
+     ↑d * (↑b * ↑c),
+     -1 * (↑a * (↑b * ↑c)),
+     -1 * (↑d * (↑b * ↑c)),
      a * (b * c),
      b * c,
      d * (b * c)]

tests/lean/run/grind_eq.lean

@@ -72,7 +72,7 @@ info: [grind.assert] x1 = appV a_2 b
 [grind.assert] ¬HEq x2 x4
 [grind.ematch.instance] appV_assoc: HEq (appV a_2 (appV b c)) (appV (appV a_2 b) c)
 [grind.assert] HEq (appV a_2 (appV b c)) (appV (appV a_2 b) c)
-[grind.assert] -1 * NatCast.natCast a ≤ 0
+[grind.assert] -1 * ↑a ≤ 0
 -/
 #guard_msgs (info) in
 example : x1 = appV a b → x2 = appV x1 c → x3 = appV b c → x4 = appV a x3 → HEq x2 x4 := by

tests/lean/run/grind_offset.lean

@@ -51,7 +51,7 @@ info: [grind.assert] f (c + 2) = a
 [grind.assert] ¬a = g (g (f c))
 [grind.ematch.instance] f.eq_2: f (c + 1).succ = g (f (c + 1))
 [grind.assert] f (c + 2) = g (f (c + 1))
-[grind.assert] -1 * NatCast.natCast c ≤ 0
+[grind.assert] -1 * ↑c ≤ 0
 [grind.ematch.instance] f.eq_2: f c.succ = g (f c)
 [grind.assert] f (c + 1) = g (f c)
 -/
@@ -77,8 +77,8 @@ info: [grind.assert] foo (c + 1) = a
 [grind.assert] ¬a = g (foo b)
 [grind.ematch.instance] foo.eq_3: foo b.succ.succ = g (foo b)
 [grind.assert] foo (b + 2) = g (foo b)
-[grind.assert] -1 * NatCast.natCast b ≤ 0
-[grind.assert] -1 * NatCast.natCast c ≤ 0
+[grind.assert] -1 * ↑b ≤ 0
+[grind.assert] -1 * ↑c ≤ 0
 -/
 #guard_msgs (info) in
 example : foo (c + 1) = a → c = b + 1 → a = g (foo b) := by