linear_combination Tactic

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

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

theorem Mathlib.Tactic.LinearCombination.pf_add_c {α : Type u_1} {a : α} {b : α} [Add α] (p : a = b) (c : α) : a + c = b + c

theorem Mathlib.Tactic.LinearCombination.c_add_pf {α : Type u_1} {b : α} {c : α} [Add α] (p : b = c) (a : α) : a + b = a + c

theorem Mathlib.Tactic.LinearCombination.add_pf {α : Type u_1} {a₁ : α} {b₁ : α} {a₂ : α} {b₂ : α} [Add α] (p₁ : a₁ = b₁) (p₂ : a₂ = b₂) : a₁ + a₂ = b₁ + b₂

theorem Mathlib.Tactic.LinearCombination.pf_sub_c {α : Type u_1} {a : α} {b : α} [Sub α] (p : a = b) (c : α) : a - c = b - c

theorem Mathlib.Tactic.LinearCombination.c_sub_pf {α : Type u_1} {b : α} {c : α} [Sub α] (p : b = c) (a : α) : a - b = a - c

theorem Mathlib.Tactic.LinearCombination.sub_pf {α : Type u_1} {a₁ : α} {b₁ : α} {a₂ : α} {b₂ : α} [Sub α] (p₁ : a₁ = b₁) (p₂ : a₂ = b₂) : a₁ - a₂ = b₁ - b₂

theorem Mathlib.Tactic.LinearCombination.neg_pf {α : Type u_1} {a : α} {b : α} [Neg α] (p : a = b) : -a = -b

theorem Mathlib.Tactic.LinearCombination.pf_mul_c {α : Type u_1} {a : α} {b : α} [Mul α] (p : a = b) (c : α) : a * c = b * c

theorem Mathlib.Tactic.LinearCombination.c_mul_pf {α : Type u_1} {b : α} {c : α} [Mul α] (p : b = c) (a : α) : a * b = a * c

theorem Mathlib.Tactic.LinearCombination.mul_pf {α : Type u_1} {a₁ : α} {b₁ : α} {a₂ : α} {b₂ : α} [Mul α] (p₁ : a₁ = b₁) (p₂ : a₂ = b₂) : a₁ * a₂ = b₁ * b₂

theorem Mathlib.Tactic.LinearCombination.inv_pf {α : Type u_1} {a : α} {b : α} [Inv α] (p : a = b) : a⁻¹ = b⁻¹

theorem Mathlib.Tactic.LinearCombination.pf_div_c {α : Type u_1} {a : α} {b : α} [Div α] (p : a = b) (c : α) : a / c = b / c

theorem Mathlib.Tactic.LinearCombination.c_div_pf {α : Type u_1} {b : α} {c : α} [Div α] (p : b = c) (a : α) : a / b = a / c

theorem Mathlib.Tactic.LinearCombination.div_pf {α : Type u_1} {a₁ : α} {b₁ : α} {a₂ : α} {b₂ : α} [Div α] (p₁ : a₁ = b₁) (p₂ : a₂ = b₂) : a₁ / a₂ = b₁ / b₂

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

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

• some 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 some (c_add_pf 2 h) which is a proof of 2 * a = 2 * b.
• none means that the input expression is not an equation but a value; the input syntax itself is used in this case.

structure Mathlib.Tactic.LinearCombination.Config : Type

• normalize : Bool

  whether or not the normalization step should be used

• twoGoals : Bool

  whether to make separate subgoals for both sides or just one for lhs - rhs = 0

• normTac : Lean.Syntax.Tactic

  the tactic used for normalization when checking if the weighted sum is equivalent to the goal (when normalize is true).

A configuration object for linear_combination.

instance Mathlib.Tactic.LinearCombination.instInhabitedConfig : Inhabited Mathlib.Tactic.LinearCombination.Config

Equations

• Mathlib.Tactic.LinearCombination.instInhabitedConfig = { default := { normalize := default, twoGoals := default, normTac := default } }

def Mathlib.Tactic.LinearCombination.elabConfig : Lean.Syntax → Lean.Elab.TermElabM Mathlib.Tactic.LinearCombination.Config

Function elaborating LinearCombination.Config

Equations

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

theorem Mathlib.Tactic.LinearCombination.eq_trans₃ {α : Sort u_1} {a : α} {b : α} {a' : α} {b' : α} (p : a = b) (p₁ : a = a') (p₂ : b = b') : a' = b'

theorem Mathlib.Tactic.LinearCombination.eq_of_add {α : Type u_1} {a : α} {b : α} {a' : α} {b' : α} [AddGroup α] (p : a = b) (H : a' - b' - (a - b) = 0) : a' = b'

def Mathlib.Tactic.LinearCombination.elabLinearCombination (norm? : Option Lean.Syntax.Tactic) (input : Option Lean.Term) (twoGoals : optParam Bool false) : Lean.Elab.Tactic.TacticM Unit

Implementation of linear_combination and linear_combination2.

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.linearCombination : Lean.ParserDescr

linear_combination attempts to simplify the target by creating a linear combination of a list of equalities and subtracting it from the target. The tactic will create a linear combination by adding the equalities together from left to right, so the order of the input hypotheses does matter. If the normalize field of the configuration is set to false, then the tactic will simply set the user up to prove their target using the linear combination instead of normalizing the subtraction.

Note: The left and right sides of all the equalities should have the same type, and the coefficients should also have this type. There must be instances of Mul and AddGroup for this type.

• The input e in linear_combination e is a linear combination of proofs of equalities, given as a sum/difference of coefficients multiplied by expressions. The coefficients may be arbitrary expressions. The expressions can be arbitrary proof terms proving equalities. Most commonly they are hypothesis names h1, h2, ....
• linear_combination (norm := tac) e runs the "normalization tactic" tac on the subgoal(s) after constructing the linear combination.
  • The default normalization tactic is ring1, which closes the goal or fails.
  • To get a subgoal in the case that it is not immediately provable, use ring_nf as the normalization tactic.
  • To avoid normalization entirely, use skip as the normalization tactic.
• linear_combination2 e is the same as linear_combination e but it produces two subgoals instead of one: rather than proving that (a - b) - (a' - b') = 0 where a' = b' is the linear combination from e and a = b is the goal, it instead attempts to prove a = a' and b = b'. Because it does not use subtraction, this form is applicable also to semirings.
  • Note that a goal which is provable by linear_combination e may not be provable by linear_combination2 e; in general you may need to add a coefficient to e to make both sides match, as in linear_combination2 e + c.
  • You can also reverse equalities using ← h, so for example if h₁ : a = b then 2 * (← h) is a proof of 2 * b = 2 * a.

Example Usage:

example (x y : ℤ) (h1 : x*y + 2*x = 1) (h2 : x = y) : x*y = -2*y + 1 := by
  linear_combination 1*h1 - 2*h2

example (x y : ℤ) (h1 : x*y + 2*x = 1) (h2 : x = y) : x*y = -2*y + 1 := by
  linear_combination h1 - 2*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
  /- Goal: x * y + x * 2 - 1 = 0 -/

example (x y z : ℝ) (ha : x + 2*y - z = 4) (hb : 2*x + y + z = -2)
    (hc : x + 2*y + z = 2) :
    -3*x - 3*y - 4*z = 2 := by
  linear_combination ha - hb - 2*hc

example (x y : ℚ) (h1 : x + y = 3) (h2 : 3*x = 7) :
    x*x*y + y*x*y + 6*x = 3*x*y + 14 := by
  linear_combination x*y*h1 + 2*h2

example (x y : ℤ) (h1 : x = -3) (h2 : y = 10) : 2*x = -6 := by
  linear_combination (norm := skip) 2*h1
  simp

axiom qc : ℚ
axiom hqc : qc = 2*qc

example (a b : ℚ) (h : ∀ p q : ℚ, p = q) : 3*a + qc = 3*b + 2*qc := by
  linear_combination 3 * h a b + hqc

Equations

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

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

linear_combination attempts to simplify the target by creating a linear combination of a list of equalities and subtracting it from the target. The tactic will create a linear combination by adding the equalities together from left to right, so the order of the input hypotheses does matter. If the normalize field of the configuration is set to false, then the tactic will simply set the user up to prove their target using the linear combination instead of normalizing the subtraction.

Note: The left and right sides of all the equalities should have the same type, and the coefficients should also have this type. There must be instances of Mul and AddGroup for this type.

• The input e in linear_combination e is a linear combination of proofs of equalities, given as a sum/difference of coefficients multiplied by expressions. The coefficients may be arbitrary expressions. The expressions can be arbitrary proof terms proving equalities. Most commonly they are hypothesis names h1, h2, ....
• linear_combination (norm := tac) e runs the "normalization tactic" tac on the subgoal(s) after constructing the linear combination.
  • The default normalization tactic is ring1, which closes the goal or fails.
  • To get a subgoal in the case that it is not immediately provable, use ring_nf as the normalization tactic.
  • To avoid normalization entirely, use skip as the normalization tactic.
• linear_combination2 e is the same as linear_combination e but it produces two subgoals instead of one: rather than proving that (a - b) - (a' - b') = 0 where a' = b' is the linear combination from e and a = b is the goal, it instead attempts to prove a = a' and b = b'. Because it does not use subtraction, this form is applicable also to semirings.
  • Note that a goal which is provable by linear_combination e may not be provable by linear_combination2 e; in general you may need to add a coefficient to e to make both sides match, as in linear_combination2 e + c.
  • You can also reverse equalities using ← h, so for example if h₁ : a = b then 2 * (← h) is a proof of 2 * b = 2 * a.

Example Usage:

example (x y : ℤ) (h1 : x*y + 2*x = 1) (h2 : x = y) : x*y = -2*y + 1 := by
  linear_combination 1*h1 - 2*h2

example (x y : ℤ) (h1 : x*y + 2*x = 1) (h2 : x = y) : x*y = -2*y + 1 := by
  linear_combination h1 - 2*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
  /- Goal: x * y + x * 2 - 1 = 0 -/

example (x y z : ℝ) (ha : x + 2*y - z = 4) (hb : 2*x + y + z = -2)
    (hc : x + 2*y + z = 2) :
    -3*x - 3*y - 4*z = 2 := by
  linear_combination ha - hb - 2*hc

example (x y : ℚ) (h1 : x + y = 3) (h2 : 3*x = 7) :
    x*x*y + y*x*y + 6*x = 3*x*y + 14 := by
  linear_combination x*y*h1 + 2*h2

example (x y : ℤ) (h1 : x = -3) (h2 : y = 10) : 2*x = -6 := by
  linear_combination (norm := skip) 2*h1
  simp

axiom qc : ℚ
axiom hqc : qc = 2*qc

example (a b : ℚ) (h : ∀ p q : ℚ, p = q) : 3*a + qc = 3*b + 2*qc := by
  linear_combination 3 * h a b + hqc

Equations

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