field_simp tactic #
Tactic to clear denominators in algebraic expressions, based on
simp with a specific simpset.
Discharge strategy for the field_simp tactic.
The goal of
field_simp is to reduce an expression in a field to an expression of the form
n / d
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
field_simp [hx, hy] is a short form for
simp (discharger := Tactic.FieldSimp.discharge) [-one_div, -mul_eq_zero, hx, hy, 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.
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.
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) := by field_simp ring
field_simp tactic can also take care of inverses of units in
a general (commutative) monoid/ring and partial division
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
IsUnit x instance like
(x : R) (hx : IsUnit x), you should lift them with
lift x to Rˣ using id hx, rw [IsUnit.unit_of_val_units] clear hx
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.
- One or more equations did not get rendered due to their size.