mathlib3 documentation

tactic.field_simp

field_simp tactic #

Tactic to clear denominators in algebraic expressions, based on simp with a specific simpset.

source
meta def tactic.field_simp.ne_zero  :
tactic unit

Try to prove a goal of the form x ≠ 0 by calling assumption, or norm_num1 if x is a numeral.

source
meta def tactic.interactive.field_simp (no_dflt : interactive.parse interactive.types.only_flag) (hs : interactive.parse tactic.simp_arg_list) (attr_names : interactive.parse interactive.types.with_ident_list) (locat : interactive.parse interactive.types.location) (cfg : tactic.simp_config_ext := {to_simp_config := {max_steps := simp.default_max_steps, contextual := bool.ff, lift_eq := bool.tt, canonize_instances := bool.tt, canonize_proofs := bool.ff, use_axioms := bool.tt, zeta := bool.tt, beta := bool.tt, eta := bool.tt, proj := bool.tt, iota := bool.tt, iota_eqn := bool.ff, constructor_eq := bool.tt, single_pass := bool.ff, fail_if_unchanged := bool.tt, memoize := bool.tt, trace_lemmas := bool.ff}, discharger := tactic.field_simp.ne_zero}) :
tactic unit

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 := tactic.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,

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

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 entirely remove (numeric) division from the expression by multiplying by a factor.

source
def tactic_doc.tactic.field_simp  :
tactic_doc_entry

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 := tactic.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,

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

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 entirely remove (numeric) division from the expression by multiplying by a factor.