Tactic for normalizing expressions in multiplicative groups, without assuming
commutativity, using only the group axioms without any information about which group
is manipulated.
(For additive commutative groups, use the abel tactic instead.)
Example:
example{G:Type}[GroupG](abcd:G)(h:c=(a*b^2)*((b*b)⁻¹*a⁻¹)*d):a*c*d⁻¹=a:=G:Typeinst✝:GroupGa:Gb:Gc:Gd:Gh:c=a*b^2*((b*b)⁻¹*a⁻¹)*d⊢ a*c*d⁻¹=aG:Typeinst✝:GroupGa:Gb:Gc:Gd:Gh:c=d⊢ a*c*d⁻¹=a -- normalizes `h` which becomes `h : c = d`
G:Typeinst✝:GroupGa:Gb:Gc:Gd:Gh:c=d⊢ a*d*d⁻¹=a -- the goal is now `a*d*d⁻¹ = a`
All goals completed! 🐙 -- which then normalized and closed
Tactic for evaluating expressions in commutative (semi)rings, allowing for variables in the
exponent. If the goal is not appropriate for ring (e.g. not an equality) ring_nf will be
suggested.
ring! will use a more aggressive reducibility setting to determine equality of atoms.
Given a goal which is an equality in a type M (with M an AddCommMonoid), parse the LHS and
RHS of the goal as linear combinations of M-atoms over some commutative semiring R, and prove
the goal by checking that the LHS- and RHS-coefficients of each atom are the same up to
ring-normalization in R.
(If the proofs of coefficient-wise equality will require more reasoning than just
ring-normalization, use the tactic match_scalars instead, and then prove coefficient-wise equality
by hand.)
The linear_combination tactic attempts to prove an (in)equality goal by exhibiting it as a
specified linear combination of (in)equality hypotheses, or other (in)equality proof terms, modulo
(A) moving terms between the LHS and RHS of the (in)equalities, and (B) a normalization tactic
which by default is ring-normalization.
Example usage:
example {a b : ℚ} (h1 : a = 1) (h2 : b = 3) : (a + b) / 2 = 2 := by
linear_combination (h1 + h2) / 2
example {a b : ℚ} (h1 : a ≤ 1) (h2 : b ≤ 3) : (a + b) / 2 ≤ 2 := by
linear_combination (h1 + h2) / 2
example {a b : ℚ} : 2 * a * b ≤ a ^ 2 + b ^ 2 := by
linear_combination sq_nonneg (a - b)
example {x y z w : ℤ} (h₁ : x * z = y ^ 2) (h₂ : y * w = z ^ 2) :
z * (x * w - y * z) = 0 := by
linear_combination w * h₁ + y * h₂
example {x : ℚ} (h : x ≥ 5) : x ^ 2 > 2 * x + 11 := by
linear_combination (x + 3) * h
example {R : Type*} [CommRing R] {a b : R} (h : a = b) : a ^ 2 = b ^ 2 := by
linear_combination (a + b) * h
example {A : Type*} [AddCommGroup A]
{x y z : A} (h1 : x + y = 10 • z) (h2 : x - y = 6 • z) :
2 • x = 2 • (8 • z) := by
linear_combination (norm := abel) h1 + h2
example (x y : ℤ) (h1 : x * y + 2 * x = 1) (h2 : x = y) :
x * y = -2 * y + 1 := by
linear_combination (norm := ring_nf) -2 * h2
-- leaves goal `⊢ x * y + x * 2 - 1 = 0`
The input e in linear_combinatione is a linear combination of proofs of (in)equalities,
given as a sum/difference of coefficients multiplied by expressions.
The coefficients may be arbitrary expressions (with nonnegativity constraints in the case of
inequalities).
The expressions can be arbitrary proof terms proving (in)equalities;
most commonly they are hypothesis names h1, h2, ....
The left and right sides of all the (in)equalities should have the same type α, and the
coefficients should also have type α. For full functionality α should be a commutative ring --
strictly speaking, a commutative semiring with "cancellative" addition (in the semiring case,
negation and subtraction will be handled "formally" as if operating in the enveloping ring). If a
nonstandard normalization is used (for example abel or skip), the tactic will work over types
α with less algebraic structure: for equalities, the minimum is instances of
[Addα][IsRightCancelAddα] together with instances of whatever operations are used in the tactic
call.
The variant linear_combination(norm:=tac)e specifies explicitly the "normalization tactic"
tac to be run on the subgoal(s) after constructing the linear combination.
The default normalization tactic is ring1 (for equalities) or Mathlib.Tactic.Ring.prove{LE,LT}
(for inequalities). These are finishing tactics: they close the goal or fail.
When working in algebraic categories other than commutative rings -- for example fields, abelian
groups, modules -- it is sometimes useful to use normalization tactics adapted to those categories
(field_simp, abel, module).
To skip normalization entirely, use skip as the normalization tactic.
The linear_combination tactic creates a linear combination by adding the provided (in)equalities
together from left to right, so if tac is not invariant under commutation of additive
expressions, then the order of the input hypotheses can matter.
The variant linear_combination(exp:=n)e will take the goal to the nth power before
subtracting the combination e. In other words, if the goal is t1=t2,
linear_combination(exp:=n)e will change the goal to (t1-t2)^n=0 before proceeding as
above. This variant is implemented only for linear combinations of equalities (i.e., not for
inequalities).
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.
field_simp[hx,hy] is a short form for
simp(disch:=field_simp_discharge)[-one_div,-one_divp,-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.
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 an IsUnitx instance like
(x:R)(hx:IsUnitx), you should lift them with
liftxtoRˣusingidhx;rw[IsUnit.unit_of_val_units]clearhx
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.
cancel_denoms attempts to remove numerals from the denominators of fractions.
It works on propositions that are field-valued inequalities.
variable [LinearOrderedField α] (a b c : α)
example (h : a / 5 + b / 4 < c) : 4*a + 5*b < 20*c := by
cancel_denoms at h
exact h
example (h : a > 0) : a / 5 > 0 := by
cancel_denoms
exact h
Tactic that, given RingHoms, adds the corresponding Algebra and (if possible)
IsScalarTower instances, as well as Algebra corresponding to RingHom properties available
as hypotheses.
Example: given f:A→+*B and g:B→+*C, and hf:f.FiniteType, algebraize[f,g] will
add the instances AlgebraAB, AlgebraBC, and Algebra.FiniteTypeAB.
See the algebraize tag for instructions on what properties can be added.
The tactic also comes with a configuration option properties. If set to true (default), the
tactic searches through the local context for RingHom properties that can be converted to
Algebra properties. The macro algebraize_only calls
algebraize-properties,
so in other words it only adds Algebra and IsScalarTower instances.
The tactic reduce_mod_char looks for numeric expressions in characteristic p
and reduces these to lie between 0 and p.
For example:
example : (5 : ZMod 4) = 1 := by reduce_mod_char
example : (X ^ 2 - 3 * X + 4 : (ZMod 4)[X]) = X ^ 2 + X := by reduce_mod_char
It also handles negation, turning it into multiplication by p-1,
and similarly subtraction.
This tactic uses the type of the subexpression to figure out if it is indeed of positive
characteristic, for improved performance compared to trying to synthesise a CharP instance.
The variant reduce_mod_char! also tries to use CharPRn hypotheses in the context.
(Limitations of the typeclass system mean the tactic can't search for a CharPRn instance if
n is not yet known; use have:CharPRn:=inferInstance;reduce_mod_char! as a workaround.)
compute_degree is a tactic to solve goals of the form
natDegreef=d,
degreef=d,
natDegreef≤d (or <),
degreef≤d (or <),
coefffd=r, if d is the degree of f.
The tactic may leave goals of the form d'=d, d'≤d, d'<d, or r≠0, where d' in ℕ
or WithBotℕ is the tactic's guess of the degree, and r is the coefficient's guess of the
leading coefficient of f.
compute_degree applies norm_num to the left-hand side of all side goals, trying to close them.
The variant compute_degree! first applies compute_degree.
Then it uses norm_num on all the remaining goals and tries assumption.
monicity tries to solve a goal of the form Monicf.
It converts the goal into a goal of the form natDegreef≤n and one of the form f.coeffn=1
and calls compute_degree on those two goals.
