feat(tactic/field_simp): let field_simp use norm_num to prove numeral…

…s are nonzero (#5418)

As suggested by @robertylewis in https://leanprover.zulipchat.com/#narrow/stream/113489-new-members/topic/Solving.20simple.20%28in%29equalities.20gets.20frustrating/near/220278546, change the discharger in `field_simp` to try `assumption` on  goals `x ≠ 0` and `norm_num1` on these goals when `x` is a numeral.

archive/100-theorems-list/42_inverse_triangle_sum.lean

@@ -29,6 +29,6 @@ begin
   simp_rw [if_neg (nat.succ_ne_zero _), nat.succ_eq_add_one],
   have A : (n + 1 + 1 : ℚ) ≠ 0, by { norm_cast, norm_num },
   push_cast,
-  field_simp [nat.cast_add_one_ne_zero, A],
+  field_simp [nat.cast_add_one_ne_zero],
   ring
 end

archive/imo/imo1962_q4.lean

@@ -105,7 +105,7 @@ lemma formula {R : Type*} [integral_domain R] [char_zero R] (a : R) :
 calc a ^ 2 + (2 * a ^ 2 - 1) ^ 2 + (4 * a ^ 3 - 3 * a) ^ 2 = 1
     ↔ a ^ 2 + (2 * a ^ 2 - 1) ^ 2 + (4 * a ^ 3 - 3 * a) ^ 2 - 1 = 0 : by rw ← sub_eq_zero
 ... ↔ 2 * a ^ 2 * (2 * a ^ 2 - 1) * (4 * a ^ 2 - 3) = 0 : by { split; intros h; convert h; ring }
-... ↔ a * (2 * a ^ 2 - 1) * (4 * a ^ 2 - 3) = 0 : by field_simp [(by norm_num : (2:R) ≠ 0)]
+... ↔ a * (2 * a ^ 2 - 1) * (4 * a ^ 2 - 3) = 0 : by simp [(by norm_num : (2:R) ≠ 0)]
 ... ↔ (2 * a ^ 2 - 1) * (4 * a ^ 3 - 3 * a) = 0 : by { split; intros h; convert h using 1; ring }
 
 /-

src/algebra/continued_fractions/convergents_equiv.lean

@@ -6,6 +6,8 @@ Authors: Kevin Kappelmann
 import algebra.continued_fractions.continuants_recurrence
 import algebra.continued_fractions.terminated_stable
 import tactic.linarith
+import tactic.field_simp
+
 /-!
 # Equivalence of Recursive and Direct Computations of `gcf` Convergents
 
@@ -319,7 +321,7 @@ begin
             (continuants_aux_eq_continuants_aux_squash_gcf_of_le n'.le_succ).symm] },
         symmetry,
         simpa only [eq1, eq2, eq3, eq4, mul_div_cancel _  b_ne_zero] },
-      field_simp [b_ne_zero],
+      field_simp,
       congr' 1; ring } }
 end
 

src/algebra/group_with_zero/basic.lean

@@ -120,7 +120,7 @@ are nonzero. -/
 theorem mul_ne_zero_iff : a * b ≠ 0 ↔ a ≠ 0 ∧ b ≠ 0 :=
 (not_congr mul_eq_zero).trans not_or_distrib
 
-theorem mul_ne_zero (ha : a ≠ 0) (hb : b ≠ 0) : a * b ≠ 0 :=
+@[field_simps] theorem mul_ne_zero (ha : a ≠ 0) (hb : b ≠ 0) : a * b ≠ 0 :=
 mul_ne_zero_iff.2 ⟨ha, hb⟩
 
 /-- If `α` has no zero divisors, then for elements `a, b : α`, `a * b` equals zero iff so is

src/analysis/special_functions/trigonometric.lean

@@ -2151,7 +2151,7 @@ lemma cos_eq_cos_iff {x y : ℂ} :
   cos x = cos y ↔ ∃ k : ℤ, y = 2 * k * π + x ∨ y = 2 * k * π - x :=
 calc cos x = cos y ↔ cos x - cos y = 0 : sub_eq_zero.symm
 ... ↔ -2 * sin((x + y)/2) * sin((x - y)/2) = 0 : by rw cos_sub_cos
-... ↔ sin((x + y)/2) = 0 ∨ sin((x - y)/2) = 0 : by { field_simp [(by norm_num : -(2:ℂ) ≠ 0)] }
+... ↔ sin((x + y)/2) = 0 ∨ sin((x - y)/2) = 0 : by simp [(by norm_num : (2:ℂ) ≠ 0)]
 ... ↔ sin((x - y)/2) = 0 ∨ sin((x + y)/2) = 0 : or.comm
 ... ↔ (∃ k : ℤ, y = 2 * k * π + x) ∨ (∃ k :ℤ, y = 2 * k * π - x) :
 begin

src/data/rat/floor.lean

@@ -4,6 +4,8 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Johannes Hölzl, Mario Carneiro, Kevin Kappelmann
 -/
 import algebra.floor
+import tactic.field_simp
+
 /-!
 # Floor Function for Rational Numbers
 

src/data/real/golden_ratio.lean

@@ -36,10 +36,7 @@ lemma inv_gold : φ⁻¹ = -ψ :=
 begin
   have : 1 + real.sqrt 5 ≠ 0,
     from ne_of_gt (add_pos (by norm_num) $ real.sqrt_pos.mpr (by norm_num)),
-  field_simp,
-  apply mul_left_cancel' this,
-  rw mul_div_cancel' _ this,
-  rw [add_comm, ← sq_sub_sq],
+  field_simp [sub_mul, mul_add],
   norm_num
 end
 

src/data/real/nnreal.lean

@@ -432,9 +432,6 @@ begin
     rw [of_real_eq_zero.2 hq, of_real_eq_zero.2 hpq, mul_zero] }
 end
 
-@[field_simps] theorem mul_ne_zero' {a b : ℝ≥0} (h₁ : a ≠ 0) (h₂ : b ≠ 0) : a * b ≠ 0 :=
-mul_ne_zero h₁ h₂
-
 end mul
 
 section sub

src/field_theory/splitting_field.lean

@@ -11,6 +11,7 @@ import ring_theory.algebraic
 import ring_theory.polynomial
 import field_theory.minimal_polynomial
 import linear_algebra.finite_dimensional
+import tactic.field_simp
 
 noncomputable theory
 open_locale classical big_operators
@@ -380,7 +381,7 @@ begin
     rw [roots_normalize, normalize_apply, coe_norm_unit_of_ne_zero hzero] at hprod,
     calc (C p.leading_coeff) * (multiset.map (λ (a : α), X - C a) p.roots).prod
         = p * C ((p.leading_coeff)⁻¹ * p.leading_coeff) : by rw [hprod, mul_comm, mul_assoc, ← C_mul]
-    ... = p * C 1 : by field_simp [hcoeff]
+    ... = p * C 1 : by field_simp
     ... = p : by simp only [mul_one, ring_hom.map_one], },
 end
 

src/linear_algebra/affine_space/ordered.lean

@@ -5,6 +5,7 @@ Author: Yury G. Kudryashov
 -/
 import linear_algebra.affine_space.midpoint
 import algebra.module.ordered
+import tactic.field_simp
 
 /-!
 # Ordered modules as affine spaces

src/number_theory/pythagorean_triples.lean

@@ -8,6 +8,7 @@ import ring_theory.int.basic
 import algebra.group_with_zero.power
 import tactic.ring
 import tactic.ring_exp
+import tactic.field_simp
 
 /-!
 # Pythagorean Triples
@@ -247,7 +248,7 @@ def circle_equiv_gen (hk : ∀ x : K, 1 + x^2 ≠ 0) :
   begin
     have h2 : (1 + 1 : K) = 2 := rfl,
     have h3 : (2 : K) ≠ 0, { convert hk 1, rw [one_pow 2, h2] },
-    field_simp [hk x, h2, h3, add_assoc, add_comm, add_sub_cancel'_right, mul_comm],
+    field_simp [hk x, h2, add_assoc, add_comm, add_sub_cancel'_right, mul_comm],
   end,
   right_inv := λ ⟨⟨x, y⟩, hxy, hy⟩,
   begin
@@ -258,8 +259,8 @@ def circle_equiv_gen (hk : ∀ x : K, 1 + x^2 ≠ 0) :
     have h4 : (2 : K) ≠ 0, { convert hk 1, rw one_pow 2, refl },
     simp only [prod.mk.inj_iff, subtype.mk_eq_mk],
     split,
-    { field_simp [h2, h3, h4], ring },
-    { field_simp [h2, h3, h4], rw [← add_neg_eq_iff_eq_add.mpr hxy.symm], ring }
+    { field_simp [h3], ring },
+    { field_simp [h3], rw [← add_neg_eq_iff_eq_add.mpr hxy.symm], ring }
   end }
 
 @[simp] lemma circle_equiv_apply (hk : ∀ x : K, 1 + x^2 ≠ 0) (x : K) :

src/ring_theory/fractional_ideal.lean

@@ -6,6 +6,7 @@ Authors: Anne Baanen
 import ring_theory.localization
 import ring_theory.noetherian
 import ring_theory.principal_ideal_domain
+import tactic.field_simp
 
 /-!
 # Fractional ideals
@@ -1028,7 +1029,7 @@ begin
   { intros x hx,
     rw [val_eq_coe, coe_div h_spand, submodule.mem_div_iff_forall_mul_mem] at hx,
     specialize hx d (mem_span_singleton_self d),
-    have h_xd : x = d⁻¹ * (x * d), { field_simp [hd] },
+    have h_xd : x = d⁻¹ * (x * d), { field_simp },
     rw [val_eq_coe, coe_mul, one_div_span_singleton, h_xd],
     exact submodule.mul_mem_mul (mem_span_singleton_self _) hx },
   { rw [le_div_iff_mul_le h_spand, mul_assoc, mul_left_comm, one_div_span_singleton,

src/ring_theory/perfection.lean

@@ -345,7 +345,7 @@ instance : integral_domain (pre_tilt K v O hv p) :=
 { exists_pair_ne := (char_p.nontrivial_of_char_ne_one hp.ne_one).1,
   eq_zero_or_eq_zero_of_mul_eq_zero := λ f g hfg,
     by { simp_rw ← map_eq_zero at hfg ⊢, contrapose! hfg, rw valuation.map_mul,
-      exact nnreal.mul_ne_zero' hfg.1 hfg.2 },
+      exact mul_ne_zero hfg.1 hfg.2 },
   .. (infer_instance : comm_ring (pre_tilt K v O hv p)) }
 
 end pre_tilt

src/tactic/field_simp.lean

@@ -0,0 +1,99 @@
+/-
+Copyright (c) 2019 Sébastien Gouëzel. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Sébastien Gouëzel
+-/
+
+import tactic.interactive
+import tactic.norm_num
+
+/-!
+# `field_simp` tactic
+
+Tactic to clear denominators in algebraic expressions, based on `simp` with a specific simpset.
+-/
+
+namespace tactic
+
+/-- Try to prove a goal of the form `x ≠ 0` by calling `assumption`, or `norm_num1` if `x` is
+a numeral. -/
+meta def field_simp.ne_zero : tactic unit := do
+  goal ← tactic.target,
+  match goal with
+  | `(%%e ≠ 0) := assumption <|> do n ← e.to_rat, `[norm_num1]
+  | _ := tactic.fail "goal should be of the form `x ≠ 0`"
+  end
+
+namespace interactive
+open interactive interactive.types
+
+/--
+The goal of `field_simp` is to reduce an expression in a field to an expression of the form `n / d`
+where neither `n` nor `d` contains any division symbol, just using the simplifier (with a carefully
+crafted simpset named `field_simps`) to reduce the number of division symbols whenever possible by
+iterating the following steps:
+
+- write an inverse as a division
+- in any product, move the division to the right
+- if there are several divisions in a product, group them together at the end and write them as a
+  single division
+- reduce a sum to a common denominator
+
+If the goal is an equality, this simpset will also clear the denominators, so that the proof
+can normally be concluded by an application of `ring` or `ring_exp`.
+
+`field_simp [hx, hy]` is a short form for
+`simp [-one_div, -mul_eq_zero, hx, hy] with field_simps {discharger := [field_simp.ne_zero]}`
+
+Note that this naive algorithm will not try to detect common factors in denominators to reduce the
+complexity of the resulting expression. Instead, it relies on the ability of `ring` to handle
+complicated expressions in the next step.
+
+As always with the simplifier, reduction steps will only be applied if the preconditions of the
+lemmas can be checked. This means that proofs that denominators are nonzero should be included. The
+fact that a product is nonzero when all factors are, and that a power of a nonzero number is
+nonzero, are included in the simpset, but more complicated assertions (especially dealing with sums)
+should be given explicitly. If your expression is not completely reduced by the simplifier
+invocation, check the denominators of the resulting expression and provide proofs that they are
+nonzero to enable further progress.
+
+To check that denominators are nonzero, `field_simp` will look for facts in the context, and
+will try to apply `norm_num` to close numerical goals.
+
+The invocation of `field_simp` removes the lemma `one_div` from the simpset, as this lemma
+works against the algorithm explained above. It also removes
+`mul_eq_zero : x * y = 0 ↔ x = 0 ∨ y = 0`, as `norm_num` can not work on disjunctions to
+close goals of the form `24 ≠ 0`, and replaces it with `mul_ne_zero : x ≠ 0 → y ≠ 0 → x * y ≠ 0`
+creating two goals instead of a disjunction.
+
+For example,
+```lean
+example (a b c d x y : ℂ) (hx : x ≠ 0) (hy : y ≠ 0) :
+  a + b / x + c / x^2 + d / x^3 = a + x⁻¹ * (y * b / y + (d / x + c) / x) :=
+begin
+  field_simp,
+  ring
+end
+```
+
+See also the `cancel_denoms` tactic, which tries to do a similar simplification for expressions
+that have numerals in denominators.
+The tactics are not related: `cancel_denoms` will only handle numeric denominators, and will try to
+entirely remove (numeric) division from the expression by multiplying by a factor.
+-/
+meta def field_simp (no_dflt : parse only_flag) (hs : parse simp_arg_list)
+  (attr_names : parse with_ident_list)
+  (locat : parse location)
+  (cfg : simp_config_ext := {discharger := field_simp.ne_zero}) : tactic unit :=
+let attr_names := `field_simps :: attr_names,
+    hs := simp_arg_type.except `one_div :: simp_arg_type.except `mul_eq_zero :: hs in
+propagate_tags (simp_core cfg.to_simp_config cfg.discharger no_dflt hs attr_names locat)
+
+add_tactic_doc
+{ name       := "field_simp",
+  category   := doc_category.tactic,
+  decl_names := [`tactic.interactive.field_simp],
+  tags       := ["simplification", "arithmetic"] }
+
+end interactive
+end tactic

src/tactic/interactive.lean

@@ -606,66 +606,6 @@ add_tactic_doc
   decl_names := [`tactic.interactive.h_generalize],
   tags       := ["context management"] }
 
-/--
-The goal of `field_simp` is to reduce an expression in a field to an expression of the form `n / d`
-where neither `n` nor `d` contains any division symbol, just using the simplifier (with a carefully
-crafted simpset named `field_simps`) to reduce the number of division symbols whenever possible by
-iterating the following steps:
-
-- write an inverse as a division
-- in any product, move the division to the right
-- if there are several divisions in a product, group them together at the end and write them as a
-  single division
-- reduce a sum to a common denominator
-
-If the goal is an equality, this simpset will also clear the denominators, so that the proof
-can normally be concluded by an application of `ring` or `ring_exp`.
-
-`field_simp [hx, hy]` is a short form for `simp [-one_div, hx, hy] with field_simps`
-
-Note that this naive algorithm will not try to detect common factors in denominators to reduce the
-complexity of the resulting expression. Instead, it relies on the ability of `ring` to handle
-complicated expressions in the next step.
-
-As always with the simplifier, reduction steps will only be applied if the preconditions of the
-lemmas can be checked. This means that proofs that denominators are nonzero should be included. The
-fact that a product is nonzero when all factors are, and that a power of a nonzero number is
-nonzero, are included in the simpset, but more complicated assertions (especially dealing with sums)
-should be given explicitly. If your expression is not completely reduced by the simplifier
-invocation, check the denominators of the resulting expression and provide proofs that they are
-nonzero to enable further progress.
-
-The invocation of `field_simp` removes the lemma `one_div` (which is marked as a simp lemma
-in core) from the simpset, as this lemma works against the algorithm explained above.
-
-For example,
-```lean
-example (a b c d x y : ℂ) (hx : x ≠ 0) (hy : y ≠ 0) :
-  a + b / x + c / x^2 + d / x^3 = a + x⁻¹ * (y * b / y + (d / x + c) / x) :=
-begin
-  field_simp [hx, hy],
-  ring
-end
-
-See also the `cancel_denoms` tactic, which tries to do a similar simplification for expressions
-that have numerals in denominators.
-The tactics are not related: `cancel_denoms` will only handle numeric denominators, and will try to
-entirely remove (numeric) division from the expression by multiplying by a factor.
-```
--/
-meta def field_simp (no_dflt : parse only_flag) (hs : parse simp_arg_list)
-  (attr_names : parse with_ident_list)
-  (locat : parse location) (cfg : simp_config_ext := {}) : tactic unit :=
-let attr_names := `field_simps :: attr_names,
-    hs := simp_arg_type.except `one_div :: hs in
-propagate_tags (simp_core cfg.to_simp_config cfg.discharger no_dflt hs attr_names locat)
-
-add_tactic_doc
-{ name       := "field_simp",
-  category   := doc_category.tactic,
-  decl_names := [`tactic.interactive.field_simp],
-  tags       := ["simplification", "arithmetic"] }
-
 /-- Tests whether `t` is definitionally equal to `p`. The difference with `guard_expr_eq` is that
   this uses definitional equality instead of alpha-equivalence. -/
 meta def guard_expr_eq' (t : expr) (p : parse $ tk ":=" *> texpr) : tactic unit :=

test/ring.lean

@@ -31,15 +31,22 @@ 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) :
   x / (y / z) + y ⁻¹ + 1 / (y * -x) = -1/ (x * y) + (x * z + 1) / y :=
 begin
-  field_simp [hx, hy, hz],
+  field_simp,
   ring
 end
 
 example (a b c d x y : ℚ) (hx : x ≠ 0) (hy : y ≠ 0) :
   a + b / x - c / x^2 + d / x^3 = a + x⁻¹ * (y * b / y + (d / x - c) / x) :=
 begin
-  field_simp [hx, hy],
+  field_simp,
   ring
 end
 
 example : (876544 : ℤ) * -1 + (1000000 - 123456) = 0 := by ring
+
+example (x y : ℝ) (hx : x ≠ 0) (hy : y ≠ 0) :
+  2 * x ^ 3 * 2 / (24 * x) = x ^ 2 / 6 :=
+begin
+  field_simp,
+  ring
+end

test/ring_exp.lean

@@ -1,6 +1,7 @@
 import tactic.ring_exp
 import tactic.zify
 import algebra.group_with_zero.power
+import tactic.field_simp
 
 universes u
 
@@ -134,8 +135,7 @@ example {α} [linear_ordered_field α] (a b c : α) : a*(-c/b)*(-c/b) = a*((c/b)
 example (x y : ℚ) (n : ℕ) (hx : x ≠ 0) (hy : y ≠ 0) :
   1/ (2/(x / y))^(2 * n) + y / y^(n+1) - (x/y)^n * (x/(2 * y))^n / 2 ^n = 1/y^n :=
 begin
-  simp [sub_eq_add_neg],
-  field_simp [hx, hy],
+  field_simp,
   ring_exp
 end
 end complicated