fix(tactic/ring): more precise pattern match for div

src/algebra/quadratic_discriminant.lean

@@ -45,10 +45,10 @@ begin
   assume a, rcases (exists_le_mul_self a) with ⟨x, hx⟩,
   cases le_total 0 x with hx' hx',
   { use (x + 1),
-    have : (x+1)*(x+1) = x*x + 2*x + 1, ring,
+    have : (x+1)*(x+1) = x*x + 2*x + 1, {ring},
     exact lt_of_le_of_lt hx (by rw this; linarith) },
   { use (x - 1),
-    have : (x-1)*(x-1) = x*x - 2*x + 1, ring,
+    have : (x-1)*(x-1) = x*x - 2*x + 1, {ring},
     exact lt_of_le_of_lt hx (by rw this; linarith) }
 end
 
@@ -134,13 +134,13 @@ begin
     have h₂ := h x, linarith },
   { cases classical.em (c = 0) with hc' hc',
     { rw hc' at *,
-      have : -(a*-b*-b + b*-b + 0) = (1-a)*(b*b), ring,
+      have : -(a*-b*-b + b*-b + 0) = (1-a)*(b*b), {ring},
       have h := h (-b), rw [← neg_nonpos, this] at h,
-      have : b * b ≤ 0, from nonpos_of_mul_nonpos_left h (by linarith),
+      have : b * b ≤ 0 := nonpos_of_mul_nonpos_left h (by linarith),
       linarith },
     { have h := h (-c/b),
       have : a*(-c/b)*(-c/b) + b*(-c/b) + c = a*((c/b)*(c/b)),
-        rw mul_div_cancel' _ hb, ring,
+      { rw mul_div_cancel' _ hb, ring },
       rw this at h,
       have : 0 ≤ a := nonneg_of_mul_nonneg_right h (mul_self_pos $ div_ne_zero hc' hb),
       linarith [ha] } },
@@ -154,7 +154,7 @@ begin
     4*a* (a*(-(b/a)*(1/2))*(-(b/a)*(1/2)) + b*(-(b/a)*(1/2)) + c)
       = (a*(b/a)) * (a*(b/a)) - 2*(a*(b/a))*b + 4*a*c : by ring
     ... = -(b*b - 4*a*c) : by { simp only [mul_div_cancel' b (ne_of_gt ha)], ring },
-  have ha' : 0 ≤ 4*a, linarith,
+  have ha' : 0 ≤ 4*a, {linarith},
   have h := (mul_nonneg ha' (h (-(b/a) * (1/2)))),
   rw this at h, rwa ← neg_nonneg
 end
@@ -166,11 +166,11 @@ at least when the coefficient of the quadratic term is nonzero.
 lemma discriminant_lt_zero {a b c : α} (ha : a ≠ 0) (h : ∀ x : α,  0 < a*x*x + b*x + c) :
   discrim a b c < 0 :=
 begin
-  have : ∀ x : α,  0 ≤ a*x*x + b*x + c := assume x, le_of_lt (h x),
+  have : ∀ x : α, 0 ≤ a*x*x + b*x + c := assume x, le_of_lt (h x),
   refine lt_of_le_of_ne (discriminant_le_zero this) _,
   assume h',
   have := h (-b / (2 * a)),
   have : a * (-b / (2 * a)) * (-b / (2 * a)) + b * (-b / (2 * a)) + c = 0,
-    rw [quadratic_eq_zero_iff_of_discrim_eq_zero ha h' (-b / (2 * a))],
+  { rw [quadratic_eq_zero_iff_of_discrim_eq_zero ha h' (-b / (2 * a))] },
   linarith
 end

src/linear_algebra/determinant.lean

@@ -6,6 +6,7 @@ Authors: Kenny Lau, Chris Hughes, Tim Baanen
 import data.matrix.basic
 import data.matrix.pequiv
 import group_theory.perm.sign
+import tactic.ring
 
 universes u v
 open equiv equiv.perm finset function
@@ -84,7 +85,7 @@ calc det (M ⬝ N) = univ.sum (λ σ : perm n, (univ.pi (λ a, univ)).sum
   finset.sum_comm
 ... = ((@univ (n → n) _).filter bijective).sum (λ p : n → n, univ.sum
     (λ σ : perm n, ε σ * univ.prod (λ i, M (σ i) (p i) * N (p i) i))) :
-  eq.symm $ sum_subset (filter_subset _) 
+  eq.symm $ sum_subset (filter_subset _)
     (λ f _ hbij, det_mul_aux $ by simpa using hbij)
 ... = (@univ (perm n) _).sum (λ τ, univ.sum
     (λ σ : perm n, ε σ * univ.prod (λ i, M (σ i) (τ i) * N (τ i) i))) :
@@ -142,7 +143,7 @@ end
     conv_lhs { rw [←one_mul (sign τ), ←int.units_pow_two (sign σ)] },
     conv_rhs { rw [←mul_assoc, coe_coe, sign_mul, units.coe_mul, int.cast_mul, ←mul_assoc] },
     congr,
-    { norm_num },
+    { simp [pow_two] },
     { ext i, apply pequiv.equiv_to_pequiv_to_matrix } },
   { intros τ τ' _ _, exact (mul_left_inj σ).mp },
   { intros τ _, use σ⁻¹ * τ, use (mem_univ _), exact (mul_inv_cancel_left _ _).symm }

src/tactic/norm_num.lean

@@ -85,14 +85,19 @@ meta def eval_pow (simp : expr → tactic (expr × expr)) : expr → tactic (exp
   e ← mk_app ``monoid.pow [e₁, e₂],
   (e', p) ← simp e,
   p' ← mk_app ``norm_num.pow_bit0_helper [e₁, e', e₂, p],
-  e'' ← to_expr ``(%%e' * %%e'),
-  return (e'', p')
+  e'' ← mk_app ``has_mul.mul [e', e'],
+  (e'', p₂) ← simp e'',
+  p'' ← mk_eq_trans p' p₂,
+  return (e'', p'')
 | `(monoid.pow %%e₁ (bit1 %%e₂)) := do
   e ← mk_app ``monoid.pow [e₁, e₂],
   (e', p) ← simp e,
   p' ← mk_app ``norm_num.pow_bit1_helper [e₁, e', e₂, p],
-  e'' ← to_expr ``(%%e' * %%e' * %%e₁),
-  return (e'', p')
+  e'' ← mk_app ``has_mul.mul [e', e'],
+  e'' ← mk_app ``has_mul.mul [e'', e₁],
+  (e'', p₂) ← simp e'',
+  p'' ← mk_eq_trans p' p₂,
+  return (e'', p'')
 | `(nat.pow %%e₁ %%e₂) := do
   p₁ ← mk_app ``nat.pow_eq_pow [e₁, e₂] >>= mk_eq_symm,
   e ← mk_app ``monoid.pow [e₁, e₂],
@@ -450,6 +455,9 @@ do e ← instantiate_mvars e,
       `eq e,
     return (e', pr)
 
+/-- This version of `derive` does not fail when the input is already a numeral -/
+meta def derive' : expr → tactic (expr × expr) := derive1 derive
+
 end norm_num
 
 namespace tactic.interactive

src/tactic/ring.lean

@@ -78,13 +78,13 @@ open horner_expr
 meta def horner_expr.to_string : horner_expr → string
 | (const e) := to_string e
 | (xadd e a x (_, n) b) :=
-    "(" ++ a.to_string ++ ") * (" ++ to_string x ++ ")^"
+    "(" ++ a.to_string ++ ") * (" ++ to_string x.1 ++ ")^"
         ++ to_string n ++ " + " ++ b.to_string
 
 meta def horner_expr.pp : horner_expr → tactic format
 | (const e) := pp e
 | (xadd e a x (_, n) b) := do
-  pa ← a.pp, pb ← b.pp, px ← pp x,
+  pa ← a.pp, pb ← b.pp, px ← pp x.1,
   return $ "(" ++ pa ++ ") * (" ++ px ++ ")^" ++ to_string n ++ " + " ++ pb
 
 meta instance : has_to_tactic_format horner_expr := ⟨horner_expr.pp⟩
@@ -313,14 +313,14 @@ meta def eval_pow : horner_expr → expr × ℕ → ring_m (horner_expr × expr)
   p ← lift $ mk_app ``pow_one [e],
   return (e, p)
 | (const e) (e₂, m) := do
-  (e', p) ← lift $ mk_app ``monoid.pow [e, e₂] >>= norm_num.derive,
+  (e', p) ← lift $ mk_app ``monoid.pow [e, e₂] >>= norm_num.derive',
   return (const e', p)
 | he@(xadd e a x n b) m := do
   c ← get_cache,
   let N : expr := expr.const `nat [],
   match b.e.to_nat with
   | some 0 := do
-    (n', h₁) ← lift $ mk_app ``has_mul.mul [n.1, m.1] >>= norm_num,
+    (n', h₁) ← lift $ mk_app ``has_mul.mul [n.1, m.1] >>= norm_num.derive',
     (a', h₂) ← eval_pow a m,
     α0 ← lift $ expr.of_nat c.α 0,
     return (xadd' c a' x (n', n.2 * m.2) (const α0),
@@ -387,18 +387,23 @@ meta def eval : expr → ring_m (horner_expr × expr)
   p ← ring_m.mk_app ``norm_num.subst_into_prod ``has_mul [e₁, e₂, e₁', e₂', e', p₁, p₂, p'],
   return (e', p)
 | e@`(has_inv.inv %%_) := (do
-    (e', p) ← lift $ norm_num.derive e,
+    (e', p) ← lift $ norm_num.derive e <|> refl_conv e,
     lift $ e'.to_rat,
     return (const e', p)) <|> eval_atom e
-| `(%%e₁ / %%e₂) := do
-  e₂' ← lift $ mk_app ``has_inv.inv [e₂],
-  e ← lift $ mk_app ``has_mul.mul [e₁, e₂'],
-  (e', p) ← eval e,
-  p' ← ring_m.mk_app ``unfold_div ``division_ring [e₁, e₂, e', p],
-  return (e', p')
+| e@`(@has_div.div _ %%inst %%e₁ %%e₂) := mcond
+  (succeeds (do
+    inst' ← ring_m.mk_app ``division_ring_has_div ``division_ring [],
+    lift $ is_def_eq inst inst'))
+  (do
+    e₂' ← lift $ mk_app ``has_inv.inv [e₂],
+    e ← lift $ mk_app ``has_mul.mul [e₁, e₂'],
+    (e', p) ← eval e,
+    p' ← ring_m.mk_app ``unfold_div ``division_ring [e₁, e₂, e', p],
+    return (e', p'))
+  (eval_atom e)
 | e@`(@has_pow.pow _ _ %%P %%e₁ %%e₂) := do
-  (e₂', p₂) ← eval e₂,
-  match e₂'.e.to_nat, P with
+  (e₂', p₂) ← lift $ norm_num.derive e₂ <|> refl_conv e₂,
+  match e₂'.to_nat, P with
   | some k, `(monoid.has_pow) := do
     (e₁', p₁) ← eval e₁,
     (e', p') ← eval_pow e₁' (e₂, k),

test/ring.lean

@@ -8,6 +8,20 @@ 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 (n : ℕ) : (n / 2) + (n / 2) = 2 * (n / 2) := by ring
+example {α} [linear_ordered_field α] (a b c : α) :
+  a * (-c / b) * (-c / b) + -c + c = a * (c / b * (c / b)) := by ring
+example {α} [linear_ordered_field α] (a b c : α) :
+  b ^ 2 - 4 * c * a = -(4 * c * a) + b ^ 2 := by ring
+example (x : ℚ) : x ^ (2 + 2) = x^4 := by ring
+example {α} [comm_ring α] (x : α) : x ^ 2 = x * x := by ring
+example {α} [linear_ordered_field α] (a b c : α) :
+  b ^ 2 - 4 * c * a = -(4 * c * a) + b ^ 2 := by ring
+example {α} [linear_ordered_field α] (a b c: α) :
+  b ^ 2 - 4 * a * c = 4 * a * 0 + b * b - 4 * a * c := by ring
+example {α} [comm_semiring α] (x y z : α) (n : ℕ) :
+  (x + y) * (z * (y * y) + (x * x ^ n + (1 + ↑n) * x ^ n * y)) =
+    x * (x * x ^ n) + ((2 + ↑n) * (x * x ^ n) * y + (x * z + (z * y + (1 + ↑n) * x ^ n)) * (y * y)) := by ring
 example (a n s: ℕ) : a * (n - s) = (n - s) * a := by ring
 
 example (x y z : ℚ) (hx : x ≠ 0) (hy : y ≠ 0) (hz : z ≠ 0) :