feat(tactic/field_simp): extend field_simp to partial division and …

…units (#14897)

Extend the `field_simp` tactic to deal with inverses of units in a general monoid/ring.

[Zulip thread](https://leanprover.zulipchat.com/#narrow/stream/217875-Is-there-code-for-X.3F/topic/.E2.9C.94.20.60field_simp.60.20for.20units/near/286896891)



Co-authored-by: Jon <jon.eugster@gmx.ch>

src/algebra/group/units.lean

@@ -1,7 +1,7 @@
 /-
 Copyright (c) 2017 Kenny Lau. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
-Authors: Kenny Lau, Mario Carneiro, Johannes Hölzl, Chris Hughes, Jens Wagemaker
+Authors: Kenny Lau, Mario Carneiro, Johannes Hölzl, Chris Hughes, Jens Wagemaker, Jon Eugster
 -/
 import algebra.group.basic
 import logic.nontrivial
@@ -250,6 +250,10 @@ infix ` /ₚ `:70 := divp
 theorem divp_assoc (a b : α) (u : αˣ) : a * b /ₚ u = a * (b /ₚ u) :=
 mul_assoc _ _ _
 
+/-- `field_simp` needs the reverse direction of `divp_assoc` to move all `/ₚ` to the right. -/
+@[field_simps] lemma divp_assoc' (x y : α) (u : αˣ) : x * (y /ₚ u) = (x * y) /ₚ u :=
+(divp_assoc _ _ _).symm
+
 @[simp] theorem divp_inv (u : αˣ) : a /ₚ u⁻¹ = a * u := rfl
 
 @[simp] theorem divp_mul_cancel (a : α) (u : αˣ) : a /ₚ u * u = a :=
@@ -261,31 +265,60 @@ mul_assoc _ _ _
 @[simp] theorem divp_left_inj (u : αˣ) {a b : α} : a /ₚ u = b /ₚ u ↔ a = b :=
 units.mul_left_inj _
 
-theorem divp_divp_eq_divp_mul (x : α) (u₁ u₂ : αˣ) : (x /ₚ u₁) /ₚ u₂ = x /ₚ (u₂ * u₁) :=
+@[field_simps] theorem divp_divp_eq_divp_mul (x : α) (u₁ u₂ : αˣ) :
+  (x /ₚ u₁) /ₚ u₂ = x /ₚ (u₂ * u₁) :=
 by simp only [divp, mul_inv_rev, units.coe_mul, mul_assoc]
 
-theorem divp_eq_iff_mul_eq {x : α} {u : αˣ} {y : α} : x /ₚ u = y ↔ y * u = x :=
+@[field_simps] theorem divp_eq_iff_mul_eq {x : α} {u : αˣ} {y : α} : x /ₚ u = y ↔ y * u = x :=
 u.mul_left_inj.symm.trans $ by rw [divp_mul_cancel]; exact ⟨eq.symm, eq.symm⟩
 
+@[field_simps] theorem eq_divp_iff_mul_eq {x : α} {u : αˣ} {y : α} : x = y /ₚ u ↔ x * u = y :=
+by rw [eq_comm, divp_eq_iff_mul_eq]
+
 theorem divp_eq_one_iff_eq {a : α} {u : αˣ} : a /ₚ u = 1 ↔ a = u :=
 (units.mul_left_inj u).symm.trans $ by rw [divp_mul_cancel, one_mul]
 
 @[simp] theorem one_divp (u : αˣ) : 1 /ₚ u = ↑u⁻¹ :=
 one_mul _
 
+/-- Used for `field_simp` to deal with inverses of units. -/
+@[field_simps] lemma inv_eq_one_divp (u : αˣ) : ↑u⁻¹ = 1 /ₚ u :=
+by rw one_divp
+
+/--
+Used for `field_simp` to deal with inverses of units. This form of the lemma
+is essential since `field_simp` likes to use `inv_eq_one_div` to rewrite
+`↑u⁻¹ = ↑(1 / u)`.
+-/
+@[field_simps] lemma inv_eq_one_divp' (u : αˣ) :
+  ((1 / u : αˣ) : α) = 1 /ₚ u :=
+by rw [one_div, one_divp]
+
+/--
+`field_simp` moves division inside `αˣ` to the right, and this lemma
+lifts the calculation to `α`.
+-/
+@[field_simps] lemma coe_div_eq_divp (u₁ u₂ : αˣ) : ↑(u₁ / u₂) = ↑u₁ /ₚ u₂ :=
+by rw [divp, division_def, units.coe_mul]
+
 end monoid
 
 section comm_monoid
 
 variables [comm_monoid α]
 
-theorem divp_eq_divp_iff {x y : α} {ux uy : αˣ} :
+@[field_simps] theorem divp_mul_eq_mul_divp (x y : α) (u : αˣ) : x /ₚ u * y = x * y /ₚ u :=
+by simp_rw [divp, mul_assoc, mul_comm]
+
+-- Theoretically redundant as `field_simp` lemma.
+@[field_simps] lemma divp_eq_divp_iff {x y : α} {ux uy : αˣ} :
   x /ₚ ux = y /ₚ uy ↔ x * uy = y * ux :=
-by rw [divp_eq_iff_mul_eq, mul_comm, ← divp_assoc, divp_eq_iff_mul_eq, mul_comm y ux]
+by rw [divp_eq_iff_mul_eq, divp_mul_eq_mul_divp, divp_eq_iff_mul_eq]
 
-theorem divp_mul_divp (x y : α) (ux uy : αˣ) :
+-- Theoretically redundant as `field_simp` lemma.
+@[field_simps] lemma divp_mul_divp (x y : α) (ux uy : αˣ) :
   (x /ₚ ux) * (y /ₚ uy) = (x * y) /ₚ (ux * uy) :=
-by rw [← divp_divp_eq_divp_mul, divp_assoc, mul_comm x, divp_assoc, mul_comm]
+by rw [divp_mul_eq_mul_divp, divp_assoc', divp_divp_eq_divp_mul]
 
 end comm_monoid
 

src/algebra/hom/units.lean

@@ -76,7 +76,7 @@ variables [division_monoid α]
 @[simp, norm_cast, to_additive] lemma coe_zpow : ∀ (u : αˣ) (n : ℤ), ((u ^ n : αˣ) : α) = u ^ n :=
 (units.coe_hom α).map_zpow
 
-lemma _root_.divp_eq_div (a : α) (u : αˣ) : a /ₚ u = a / u :=
+@[field_simps] lemma _root_.divp_eq_div (a : α) (u : αˣ) : a /ₚ u = a / u :=
 by rw [div_eq_mul_inv, divp, u.coe_inv]
 
 end division_monoid

src/algebra/ring/basic.lean

@@ -838,6 +838,32 @@ instance : has_neg αˣ := ⟨λu, ⟨-↑u, -↑u⁻¹, by simp, by simp⟩ ⟩
 
 instance : has_distrib_neg αˣ := units.ext.has_distrib_neg _ units.coe_neg units.coe_mul
 
+@[field_simps] lemma neg_divp (a : α) (u : αˣ) : -(a /ₚ u) = (-a) /ₚ u :=
+by simp only [divp, neg_mul]
+
+@[field_simps] lemma divp_add_divp_same (a b : α) (u : αˣ) :
+  a /ₚ u + b /ₚ u = (a + b) /ₚ u :=
+by simp only [divp, add_mul]
+
+@[field_simps] lemma divp_sub_divp_same (a b : α) (u : αˣ) :
+  a /ₚ u - b /ₚ u = (a - b) /ₚ u :=
+by rw [sub_eq_add_neg, sub_eq_add_neg, neg_divp, divp_add_divp_same]
+
+@[field_simps] lemma add_divp (a b : α) (u : αˣ)  : a + b /ₚ u = (a * u + b) /ₚ u :=
+by simp only [divp, add_mul, units.mul_inv_cancel_right]
+
+@[field_simps] lemma sub_divp (a b : α) (u : αˣ) : a - b /ₚ u = (a * u - b) /ₚ u :=
+by simp only [divp, sub_mul, units.mul_inv_cancel_right]
+
+@[field_simps] lemma divp_add (a b : α) (u : αˣ) : a /ₚ u + b = (a + b * u) /ₚ u :=
+by simp only [divp, add_mul, units.mul_inv_cancel_right]
+
+@[field_simps] lemma divp_sub (a b : α) (u : αˣ) : a /ₚ u - b = (a - b * u) /ₚ u :=
+begin
+  simp only [divp, sub_mul, sub_right_inj],
+  assoc_rw [units.mul_inv, mul_one],
+end
+
 end units
 
 lemma is_unit.neg [ring α] {a : α} : is_unit a → is_unit (-a)
@@ -1228,12 +1254,28 @@ lemma mul_self_eq_one_iff [non_assoc_ring R] [no_zero_divisors R] {a : R} :
   a * a = 1 ↔ a = 1 ∨ a = -1 :=
 by rw [←(commute.one_right a).mul_self_eq_mul_self_iff, mul_one]
 
+namespace units
+
+@[field_simps] lemma divp_add_divp [comm_ring α] (a b : α) (u₁ u₂ : αˣ) :
+a /ₚ u₁ + b /ₚ u₂ = (a * u₂ + u₁ * b) /ₚ (u₁ * u₂) :=
+begin
+  simp only [divp, add_mul, mul_inv_rev, coe_mul],
+  rw [mul_comm (↑u₁ * b), mul_comm b],
+  assoc_rw [mul_inv, mul_inv, mul_one, mul_one],
+end
+
+@[field_simps] lemma divp_sub_divp [comm_ring α] (a b : α) (u₁ u₂ : αˣ) :
+  (a /ₚ u₁) - (b /ₚ u₂) = ((a * u₂) - (u₁ * b)) /ₚ (u₁ * u₂) :=
+by simp_rw [sub_eq_add_neg, neg_divp, divp_add_divp, mul_neg]
+
 /-- In the unit group of an integral domain, a unit is its own inverse iff the unit is one or
   one's additive inverse. -/
-lemma units.inv_eq_self_iff [ring R] [no_zero_divisors R] (u : Rˣ) : u⁻¹ = u ↔ u = 1 ∨ u = -1 :=
+lemma inv_eq_self_iff [ring R] [no_zero_divisors R] (u : Rˣ) : u⁻¹ = u ↔ u = 1 ∨ u = -1 :=
 begin
   rw inv_eq_iff_mul_eq_one,
-  simp only [units.ext_iff],
+  simp only [ext_iff],
   push_cast,
   exact mul_self_eq_one_iff
 end
+
+end units

src/tactic/field_simp.lean

@@ -76,6 +76,14 @@ begin
 end
 ```
 
+Moreover, the `field_simp` tactic can also take care of inverses of units in
+a general (commutative) monoid/ring and partial division `/ₚ`, see `algebra.group.units`
+for the definition. Analogue to the case above, the lemma `one_divp` is removed from the simpset
+as this works against the algorithm. If you have objects with a `is_unit x` instance like
+`(x : R) (hx : is_unit x)`, you should lift them with
+`lift x to Rˣ using id hx, rw is_unit.unit_of_coe_units, clear hx`
+before using `field_simp`.
+
 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
@@ -86,7 +94,8 @@ meta def field_simp (no_dflt : parse only_flag) (hs : parse simp_arg_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
+    hs := simp_arg_type.except `one_div :: simp_arg_type.except `mul_eq_zero ::
+          simp_arg_type.except `one_divp :: hs in
 propagate_tags (simp_core cfg.to_simp_config cfg.discharger no_dflt hs attr_names locat >> skip)
 
 add_tactic_doc

test/field_simp.lean

@@ -0,0 +1,51 @@
+import algebra.ring.basic
+import tactic.field_simp
+import tactic.ring
+
+/-!
+## `field_simp` tests.
+
+Check that `field_simp` works for units of a ring.
+-/
+
+variables {R : Type*} [comm_ring R] (a b c d e f g : R) (u₁ u₂ : Rˣ)
+
+/--
+Check that `divp_add_divp_same` takes priority over `divp_add_divp`.
+-/
+example : a /ₚ u₁ + b /ₚ u₁ = (a + b) /ₚ u₁ :=
+by field_simp
+
+/--
+Check that `divp_sub_divp_same` takes priority over `divp_sub_divp`.
+-/
+example : a /ₚ u₁ - b /ₚ u₁ = (a - b) /ₚ u₁ :=
+by field_simp
+
+/--
+Combining `eq_divp_iff_mul_eq` and `divp_eq_iff_mul_eq`.
+-/
+example : a /ₚ u₁ = b /ₚ u₂ ↔ a * u₂ = b * u₁ :=
+by field_simp
+
+/--
+Making sure inverses of units are rewritten properly.
+-/
+example : ↑u₁⁻¹ = 1 /ₚ u₁ :=
+by field_simp
+
+/--
+Checking arithmetic expressions.
+-/
+example : (f - (e + c * -(a /ₚ u₁) * b + d) - g) =
+  (f * u₁ - (e * u₁ + c * (-a) * b + d * u₁) - g * u₁) /ₚ u₁ :=
+by field_simp
+
+/--
+Division of units.
+-/
+example : a /ₚ (u₁ / u₂) = a * u₂ /ₚ u₁ :=
+by field_simp
+
+example : a /ₚ u₁ /ₚ u₂ = a /ₚ (u₂ * u₁) :=
+by field_simp