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_combination e 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).
