linear_combination Tactic

In this file, the linear_combination tactic is created. This tactic, which works over CommRings, attempts to simplify the target by creating a linear combination of a list of equalities and subtracting it from the target. A Syntax.Tactic object can also be passed into the tactic, allowing the user to specify a normalization tactic.

Over ordered algebraic objects (such as LinearOrderedCommRing), taking linear combinations of inequalities is also supported.

Implementation Notes

This tactic works by creating a weighted sum of the given equations with the given coefficients. Then, it subtracts the right side of the weighted sum from the left side so that the right side equals 0, and it does the same with the target. Afterwards, it sets the goal to be the equality between the lefthand side of the new goal and the lefthand side of the new weighted sum. Lastly, calls a normalization tactic on this target.

References

• https://leanprover.zulipchat.com/#narrow/stream/239415-metaprogramming-.2F.20tactics/topic/Linear.20algebra.20tactic/near/213928196

inductive Mathlib.Tactic.LinearCombination.Expanded : Type

Result of expandLinearCombo, either an equality/inequality proof or a value.

• proof (rel : Mathlib.Ineq) (pf : Lean.Term) : Mathlib.Tactic.LinearCombination.Expanded

  A proof of a = b, a ≤ b, or a < b (according to the value of Ineq).

• const (c : Lean.Term) : Mathlib.Tactic.LinearCombination.Expanded

  A value, equivalently a proof of c = c.

def Mathlib.Tactic.LinearCombination.rescale (lems : Mathlib.Ineq.WithStrictness → Lean.Name) (ty : Option Lean.Expr) (p c : Lean.Term) : Mathlib.Ineq → Lean.Elab.TermElabM Mathlib.Tactic.LinearCombination.Expanded

The handling in linear_combination of left- and right-multiplication and scalar-multiplication and of division all five proceed according to the same logic, specified here: given a proof p of an (in)equality and a constant c,

• if p is a proof of an equation, multiply/divide through by c;
• if p is a proof of a non-strict inequality, run positivity to find a proof that c is nonnegative, then multiply/divide through by c, invoking the nonnegativity of c where needed;
• if p is a proof of a strict inequality, run positivity to find a proof that c is positive (if possible) or nonnegative (if not), then multiply/divide through by c, invoking the positivity or nonnegativity of c where needed.

This generic logic takes as a parameter the object lems: the four lemmas corresponding to the four cases.

Equations

• One or more equations did not get rendered due to their size.

partial def Mathlib.Tactic.LinearCombination.expandLinearCombo (ty : Option Lean.Expr) (stx : Lean.Term) : Lean.Elab.TermElabM Mathlib.Tactic.LinearCombination.Expanded

Performs macro expansion of a linear combination expression, using +/-/*// on equations and values.

• .proof eq p means that p is a syntax corresponding to a proof of an equation. For example, if h : a = b then expandLinearCombo (2 * h) returns .proof (c_add_pf 2 h) which is a proof of 2 * a = 2 * b. Similarly, .proof le p means that p is a syntax corresponding to a proof of a non-strict inequality, and .proof lt p means that p is a syntax corresponding to a proof of a strict inequality.
• .const c means that the input expression is not an equation but a value.

def Mathlib.Tactic.LinearCombination.elabLinearCombination (tk : Lean.Syntax) (norm? : Option Lean.Syntax.Tactic) (exp? : Option Lean.NumLit) (input : Option Lean.Term) : Lean.Elab.Tactic.TacticM Unit

Implementation of linear_combination.

Equations

• One or more equations did not get rendered due to their size.

def Mathlib.Tactic.LinearCombination.normStx : Lean.ParserDescr

The (norm := $tac) syntax says to use tac as a normalization postprocessor for linear_combination. The default normalizer is ring1, but you can override it with ring_nf to get subgoals from linear_combination or with skip to disable normalization.

Equations

• One or more equations did not get rendered due to their size.

def Mathlib.Tactic.LinearCombination.expStx : Lean.ParserDescr

The (exp := n) syntax for linear_combination says to take the goal to the nth power before subtracting the given combination of hypotheses.

Equations

• One or more equations did not get rendered due to their size.

def Mathlib.Tactic.LinearCombination.linearCombination : Lean.ParserDescr

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

Equations

• One or more equations did not get rendered due to their size.