interaction between `simp?`, `norm_cast`, and `grind`

[kim-em]

Jireh Loreaux reported this example:

import Mathlib.Algebra.Order.Ring.Int

example {n a b : Nat}
    (this : (b : Int) ^ (n + 1) + ↑(n + 1) * ↑b ^ (n + 1 - 1) * (↑a - ↑b) ≤ (↑b + (↑a - ↑b)) ^ (n + 1)) :
    (n + 1) * a * b ^ n ≤ a ^ (n + 1) + n * b * b ^ n := by
  simp? [mul_sub, ← add_sub_assoc] at this
    -- The `simp only` doesn't use `add_sub_cancel`
    says simp only [Nat.cast_add, Nat.cast_one, Nat.add_one_sub_one, mul_sub, ← add_sub_assoc,
      add_sub_cancel, tsub_le_iff_right] at this
  norm_cast at this
  grind -- removing the `says` fixes this `grind` call

where simp call gives a goal that can then be replaced by norm_cast at this; grind, however replace the simp with its simp? suggestion fails.

We can minimize this as:

section Mathlib.Algebra.Group.Defs

class Monoid (M : Type u) extends Mul M where

class AddGroup (G : Type u) extends Add G, Neg G, Sub G where

theorem add_sub_assoc {G : Type} [AddGroup G] (a b c : G) : a + b - c = a + (b - c) := by
  sorry

end Mathlib.Algebra.Group.Defs

abbrev Function.swap {φ : α → β → Sort u₃} (f : ∀ x y, φ x y) : ∀ y x, φ x y := fun y x => f x y

section Mathlib.Algebra.Group.Basic

@[simp]
theorem add_sub_cancel {G} [AddGroup G](a b : G) : a + (b - a) = b := by
  sorry

end Mathlib.Algebra.Group.Basic

section Mathlib.Algebra.Order.Monoid.Unbundled.Defs

open Function

variable (M N : Type) (μ : M → N → N) (r : N → N → Prop)

def Covariant : Prop :=
  ∀ (m) {n₁ n₂}, r n₁ n₂ → r (μ m n₁) (μ m n₂)

class CovariantClass : Prop where
  protected elim : Covariant M N μ r

abbrev AddLeftMono [Add M] [LE M] : Prop :=
  CovariantClass M M (· + ·) (· ≤ ·)

abbrev AddRightMono [Add M] [LE M] : Prop :=
  CovariantClass M M (swap (· + ·)) (· ≤ ·)

instance covariant_swap_add_of_covariant_add [Add N]
    [CovariantClass N N (· + ·) r] : CovariantClass N N (swap (· + ·)) r where
  elim := sorry

end Mathlib.Algebra.Order.Monoid.Unbundled.Defs

section Mathlib.Algebra.Order.Monoid.Unbundled.Basic

instance Int.instAddLeftMono : AddLeftMono Int where
  elim := sorry

end Mathlib.Algebra.Order.Monoid.Unbundled.Basic

section Mathlib.Algebra.Order.Sub.Defs

class OrderedSub (α : Type) [LE α] [Add α] [Sub α] : Prop where

@[simp]
theorem tsub_le_iff_right {α : Type}  [LE α] [Add α] [Sub α] [OrderedSub α] {a b c : α} :
    a - b ≤ c ↔ a ≤ c + b := sorry

end Mathlib.Algebra.Order.Sub.Defs

section Mathlib.Algebra.Order.Monoid.Unbundled.Basic

instance AddGroup.toOrderedSub {α : Type} [AddGroup α] [LE α]
    [AddRightMono α] : OrderedSub α := sorry

end Mathlib.Algebra.Order.Monoid.Unbundled.Basic

section Mathlib.Data.Nat.Cast.Defs

class AddMonoidWithOne (R : Type) extends NatCast R, Add R where

theorem Nat.cast_add [AddMonoidWithOne R] (m n : Nat) : ((m + n : Nat) : R) = m + n := sorry

end Mathlib.Data.Nat.Cast.Defs

section Mathlib.Data.Int.Cast.Defs

class AddGroupWithOne (R : Type) extends IntCast R, AddMonoidWithOne R, AddGroup R where

end Mathlib.Data.Int.Cast.Defs

section Mathlib.Data.Int.Cast.Basic

namespace Int

variable {R : Type} [AddGroupWithOne R]

@[norm_cast]
theorem cast_subNatNat (m n) : ((Int.subNatNat m n : Int) : R) = m - n := sorry

end Int

end Mathlib.Data.Int.Cast.Basic

section Mathlib.Algebra.Group.Int.Defs

namespace Int

instance instCommMonoid : Monoid Int where

instance instAddCommGroup : AddGroup Int where

instance instCommSemigroup : Mul Int := by infer_instance

end Int

end Mathlib.Algebra.Group.Int.Defs

section Mathlib.Algebra.Ring.Defs

class NonAssocSemiring (α : Type) extends Add α, Mul α, Zero α

class NonAssocRing (α : Type) extends AddGroup α, NonAssocSemiring α

class Ring (R : Type) extends NonAssocSemiring R, AddGroupWithOne R

section NonAssocRing

variable {α : Type} [NonAssocRing α]

theorem mul_sub_left_distrib (a b c : α) : a * (b - c) = a * b - a * c := sorry

end NonAssocRing

section Ring

variable {α : Type} [Ring α]

instance (priority := 100) Ring.toNonAssocRing : NonAssocRing α :=
  { ‹Ring α› with }

end Ring

class CommRing (α : Type) extends Ring α, Monoid α

end Mathlib.Algebra.Ring.Defs

section Mathlib.Algebra.Ring.Int.Defs

namespace Int

instance instCommRing : CommRing Int where
  intCast := (·)

end Int

end Mathlib.Algebra.Ring.Int.Defs


/-!
# simp? produces simp only that breaks grind

Example from https://leanprover.zulipchat.com/#narrow/channel/287929-mathlib4/topic/.60simp.20only.60.20.2B.20.60grind.60.20failure/near/560621777

The `simp only` output from `simp?` doesn't work with grind,
but using `simp` directly does work.
-/

-- This version works: using simp directly
example {a b : Nat}
  (this : (b : Int) + ↑b * (↑a - ↑b) ≤ (↑b + (↑a - ↑b))) :
    a * b ≤ a + b * b := by
  simp [mul_sub_left_distrib, ← add_sub_assoc] at this
  norm_cast at this
  grind

/--
info: Try this:
  [apply] simp only [mul_sub_left_distrib, ← add_sub_assoc, add_sub_cancel, tsub_le_iff_right] at this
-/
#guard_msgs in
example {a b : Nat}
  (this : (b : Int) + ↑b * (↑a - ↑b) ≤ (↑b + (↑a - ↑b))) :
    a * b ≤ a + b * b := by
  simp? [mul_sub_left_distrib, ← add_sub_assoc] at this
  norm_cast at this
  grind

-- Replacing the `simp?` with its suggestion causes `grind` to fail
/--
warning: declaration uses 'sorry'
---
warning: This simp argument is unused:
  add_sub_cancel

Hint: Omit it from the simp argument list.
  simp only [mul_sub_left_distrib, ← add_sub_assoc, a̵d̵d̵_̵s̵u̵b̵_̵c̵a̵n̵c̵e̵l̵,̵ ̵tsub_le_iff_right] at this

Note: This linter can be disabled with `set_option linter.unusedSimpArgs false`
-/
#guard_msgs in
example {a b : Nat}
  (this : (b : Int) + ↑b * (↑a - ↑b) ≤ (↑b + (↑a - ↑b))) :
    a * b ≤ a + b * b := by
  simp only [mul_sub_left_distrib, ← add_sub_assoc, add_sub_cancel, tsub_le_iff_right] at this
  norm_cast at this
  fail_if_success grind
  sorry

There seem to be three things independently going wrong here.

1. The simp? should ideally give a set of simp lemmas that produce the same results!
2. After simp only, norm_cast does something bad, introducing an Int.subNatNat in the goal.
3. Nevertheless, grind should probably solve this goal anyway, by knowing what to do with Int.subNatNat.