fix(tactic/ring): bugfix ring sub (#1714)

src/tactic/ring.lean

@@ -364,13 +364,15 @@ meta def eval : expr → ring_m (horner_expr × expr)
   (e', p') ← eval_add e₁' e₂',
   p ← ring_m.mk_app ``norm_num.subst_into_sum ``has_add [e₁, e₂, e₁', e₂', e', p₁, p₂, p'],
   return (e', p)
-| `(%%e₁ - %%e₂) := do
-  c ← get_cache,
-  e₂' ← lift $ mk_app ``has_neg.neg [e₂],
-  e ← lift $ mk_app ``has_add.add [e₁, e₂'],
-  (e', p) ← eval e,
-  p' ← ring_m.mk_app ``unfold_sub ``add_group [e₁, e₂, e', p],
-  return (e', p')
+| e@`(@has_sub.sub %%α %%P %%e₁ %%e₂) :=
+  mcond (succeeds (lift $ mk_app ``comm_ring [α] >>= mk_instance))
+    (do
+      e₂' ← lift $ mk_app ``has_neg.neg [e₂],
+      e ← lift $ mk_app ``has_add.add [e₁, e₂'],
+      (e', p) ← eval e,
+      p' ← ring_m.mk_app ``unfold_sub ``add_group [e₁, e₂, e', p],
+      return (e', p'))
+    (eval_atom e)
 | `(- %%e) := do
   (e₁, p₁) ← eval e,
   (e₂, p₂) ← eval_neg e₁,

test/ring.lean

@@ -8,3 +8,4 @@ example (x y : ℚ) : x / 2 + x / 2 = x := by ring
 example (x y : ℚ) : (x + y) ^ 3 = x ^ 3 + y ^ 3 + 3 * (x * y ^ 2 + x ^ 2 * y) := by ring
 example (x y : ℝ) : (x + y) ^ 3 = x ^ 3 + y ^ 3 + 3 * (x * y ^ 2 + x ^ 2 * y) := by ring
 example {α} [comm_semiring α] (x : α) : (x + 1) ^ 6 = (1 + x) ^ 6 := by try_for 15000 {ring}
+example (a n s: ℕ) : a * (n - s) = (n - s) * a := by ring