feat(tactic/field_simp): tactic to reduce to one division in fields (#…

…1792)

* feat(algebra/field): simp set to reduce to one division in fields

* tactic field_simp

* fix docstring

* fix build

docs/tactics.md

@@ -227,6 +227,49 @@ example (a b : ℤ) (n : ℕ) : (a + b)^(n + 2) = (a^2 + b^2 + a * b + b * a) *
 example (x y : ℕ) : x + id y = y + id x := by ring_exp!
 ```
 
+### field_simp
+
+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_eq_inv, 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_eq_inv` (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
+```
+
 ### congr'
 
 Same as the `congr` tactic, but takes an optional argument which gives

src/algebra/char_zero.lean

@@ -58,7 +58,7 @@ not_congr cast_eq_zero
 
 end nat
 
-lemma two_ne_zero' {α : Type*} [add_monoid α] [has_one α] [char_zero α] : (2:α) ≠ 0 :=
+@[field_simps] lemma two_ne_zero' {α : Type*} [add_monoid α] [has_one α] [char_zero α] : (2:α) ≠ 0 :=
 have ((2:ℕ):α) ≠ 0, from nat.cast_ne_zero.2 dec_trivial,
 by rwa [nat.cast_succ, nat.cast_one] at this
 

src/algebra/field.lean

@@ -165,9 +165,23 @@ lemma div_eq_div_iff (hb : b ≠ 0) (hd : d ≠ 0) : a / b = c / d ↔ a * d = c
 by rw [← mul_assoc, div_mul_cancel _ hb,
        ← mul_assoc, mul_right_comm, div_mul_cancel _ hd]
 
+lemma div_eq_iff (hb : b ≠ 0) : a / b = c ↔ a = c * b :=
+by simpa using @div_eq_div_iff _ _ a b c 1 hb one_ne_zero
+
+lemma eq_div_iff (hb : b ≠ 0) : c = a / b ↔ c * b = a :=
+by simpa using @div_eq_div_iff _ _ c 1 a b one_ne_zero hb
+
 lemma field.div_div_cancel (ha : a ≠ 0) (hb : b ≠ 0) : a / (a / b) = b :=
 by rw [div_eq_mul_inv, inv_div ha hb, mul_div_cancel' _ ha]
 
+lemma add_div' (a b c : α) (hc : c ≠ 0) :
+  b + a / c = (b * c + a) / c :=
+by simpa using div_add_div b a one_ne_zero hc
+
+lemma div_add' (a b c : α) (hc : c ≠ 0) :
+  a / c + b = (a + b * c) / c :=
+by simpa using div_add_div b a one_ne_zero hc
+
 end
 
 section
@@ -244,3 +258,21 @@ lemma map_div : f (x / y) = f x / f y :=
 end
 
 end is_ring_hom
+
+section field_simp
+
+mk_simp_attribute field_simps "The simpset `field_simps` is used by the tactic `field_simp` to
+reduce an expression in a field to an expression of the form `n / d` where `n` and `d` are
+division-free."
+
+lemma mul_div_assoc' {α : Type*} [division_ring α] (a b c : α) : a * (b / c) = (a * b) / c :=
+by simp [mul_div_assoc]
+
+lemma neg_div' {α : Type*} [division_ring α] (a b : α) : - (b / a) = (-b) / a :=
+by simp [neg_div]
+
+attribute [field_simps] div_add_div_same inv_eq_one_div div_mul_eq_mul_div div_add' add_div'
+div_div_eq_div_mul mul_div_assoc' div_eq_div_iff div_eq_iff eq_div_iff mul_ne_zero'
+div_div_eq_mul_div neg_div' two_ne_zero
+
+end field_simp

src/algebra/group_power.lean

@@ -486,7 +486,7 @@ begin
   exact or.cases_on (mul_eq_zero.1 H) id ih
 end
 
-theorem pow_ne_zero [domain α] {a : α} (n : ℕ) (h : a ≠ 0) : a ^ n ≠ 0 :=
+@[field_simps] theorem pow_ne_zero [domain α] {a : α} (n : ℕ) (h : a ≠ 0) : a ^ n ≠ 0 :=
 mt pow_eq_zero h
 
 @[simp] theorem one_div_pow [division_ring α] {a : α} (ha : a ≠ 0) (n : ℕ) : (1 / a) ^ n = 1 / a ^ n :=
@@ -510,9 +510,12 @@ by induction n with n ih; [exact (abs_one).symm,
 lemma abs_neg_one_pow [decidable_linear_ordered_comm_ring α] (n : ℕ) : abs ((-1 : α)^n) = 1 :=
 by rw [←pow_abs, abs_neg, abs_one, one_pow]
 
-lemma inv_pow' [discrete_field α] (a : α) (n : ℕ) : (a ^ n)⁻¹ = a⁻¹ ^ n :=
+@[field_simps] lemma inv_pow' [discrete_field α] (a : α) (n : ℕ) : a⁻¹ ^ n = (a ^ n)⁻¹ :=
 by induction n; simp [*, pow_succ, mul_inv', mul_comm]
 
+@[field_simps] lemma pow_div [discrete_field α] (a b : α) (n : ℕ) : (a / b)^n = a^n / b^n :=
+by simp [div_eq_mul_inv, mul_pow, inv_pow']
+
 lemma pow_inv [division_ring α] (a : α) : ∀ n : ℕ, a ≠ 0 → (a^n)⁻¹ = (a⁻¹)^n
 | 0     ha := inv_one
 | (n+1) ha := by rw [pow_succ, pow_succ', mul_inv_eq (pow_ne_zero _ ha) ha, pow_inv _ ha]

src/data/real/nnreal.lean

@@ -389,7 +389,7 @@ by simp [zero_lt_iff_ne_zero]
 protected lemma mul_inv {r p : ℝ≥0} : (r * p)⁻¹ = p⁻¹ * r⁻¹ := nnreal.eq $ mul_inv' _ _
 
 protected lemma inv_pow' {r : ℝ≥0} {n : ℕ} : (r^n)⁻¹ = (r⁻¹)^n :=
-nnreal.eq $ by { push_cast, apply inv_pow' }
+nnreal.eq $ by { push_cast, exact (inv_pow' _ _).symm }
 
 @[simp] lemma inv_mul_cancel {r : ℝ≥0} (h : r ≠ 0) : r⁻¹ * r = 1 :=
 nnreal.eq $ inv_mul_cancel $ mt (@nnreal.eq_iff r 0).1 h

src/field_theory/perfect_closure.lean

@@ -150,7 +150,7 @@ instance [comm_ring α] (p : ℕ) [nat.prime p] [char_p α p] : comm_ring (perfe
 
 instance [discrete_field α] (p : ℕ) [nat.prime p] [char_p α p] : has_inv (perfect_closure α p) :=
 ⟨quot.lift (λ x:ℕ×α, quot.mk (r α p) (x.1, x.2⁻¹)) (λ x y (H : r α p x y), match x, y, H with
-| _, _, r.intro _ n x := quot.sound $ by simp only [frobenius]; rw inv_pow'; apply r.intro
+| _, _, r.intro _ n x := quot.sound $ by simp only [frobenius]; rw ← inv_pow'; apply r.intro
 end)⟩
 
 theorem eq_iff' [comm_ring α] (p : ℕ) [nat.prime p] [char_p α p]

src/tactic/interactive.lean

@@ -518,6 +518,54 @@ tactic.choose tgt (first :: names),
 try (interactive.simp none tt [simp_arg_type.expr ``(exists_prop)] [] (loc.ns $ some <$> names)),
 try (tactic.clear tgt)
 
+/--
+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_eq_inv, 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_eq_inv` (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
+```
+-/
+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_eq_inv :: hs in
+propagate_tags (simp_core cfg.to_simp_config cfg.discharger no_dflt hs attr_names locat)
+
 meta def guard_expr_eq' (t : expr) (p : parse $ tk ":=" *> texpr) : tactic unit :=
 do e ← to_expr p, is_def_eq t e
 

test/ring.lean

@@ -9,3 +9,17 @@ example (x y : ℚ) : (x + y) ^ 3 = x ^ 3 + y ^ 3 + 3 * (x * y ^ 2 + x ^ 2 * y)
 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
+
+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],
+  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],
+  ring
+end

test/ring_exp.lean

@@ -122,6 +122,14 @@ by ring_exp
 -- Instead, we follow the `ring` tactic in interpreting `-c / b` as `-c * b⁻¹`,
 -- with only `b⁻¹` an atom.
 example {α} [linear_ordered_field α] (a b c : α) : a*(-c/b)*(-c/b) = a*((c/b)*(c/b)) := by ring_exp
+
+-- test that `field_simp` works fine with powers and `ring_exp`.
+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
+  field_simp [hx, hy],
+  ring_exp
+end
 end complicated
 
 section benchmark