# linear_combination' Tactic #

In this file, the `linear_combination'` tactic is created. This tactic, which works over `CommRing`s, 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.

## 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 left-hand side of the new goal and the left-hand side of the new weighted sum. Lastly, calls a normalization tactic on this target.

This file contains the `linear_combination'` tactic (note the '): the original Lean 4 implementation of the "linear combination" idea, written at the time of the port from Lean 3. Notably, its scope includes certain nonlinear operations. The `linear_combination` tactic (in a separate file) is a variant implementation, but this version is provided for backward-compatibility.

## References #

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

source
theorem Mathlib.Tactic.LinearCombination'.pf_add_c {α : Type u_1} {a b : α} [Add α] (p : a = b) (c : α) :
a + c = b + c
source
theorem Mathlib.Tactic.LinearCombination'.c_add_pf {α : Type u_1} {b c : α} [Add α] (p : b = c) (a : α) :
a + b = a + c
source
theorem Mathlib.Tactic.LinearCombination'.add_pf {α : Type u_1} {a₁ a₂ b₁ b₂ : α} [Add α] (p₁ : a₁ = b₁) (p₂ : a₂ = b₂) :
a₁ + a₂ = b₁ + b₂
source
theorem Mathlib.Tactic.LinearCombination'.pf_sub_c {α : Type u_1} {a b : α} [Sub α] (p : a = b) (c : α) :
a - c = b - c
source
theorem Mathlib.Tactic.LinearCombination'.c_sub_pf {α : Type u_1} {b c : α} [Sub α] (p : b = c) (a : α) :
a - b = a - c
source
theorem Mathlib.Tactic.LinearCombination'.sub_pf {α : Type u_1} {a₁ a₂ b₁ b₂ : α} [Sub α] (p₁ : a₁ = b₁) (p₂ : a₂ = b₂) :
a₁ - a₂ = b₁ - b₂
source
theorem Mathlib.Tactic.LinearCombination'.neg_pf {α : Type u_1} {a b : α} [Neg α] (p : a = b) :
-a = -b
source
theorem Mathlib.Tactic.LinearCombination'.pf_mul_c {α : Type u_1} {a b : α} [Mul α] (p : a = b) (c : α) :
a * c = b * c
source
theorem Mathlib.Tactic.LinearCombination'.c_mul_pf {α : Type u_1} {b c : α} [Mul α] (p : b = c) (a : α) :
a * b = a * c
source
theorem Mathlib.Tactic.LinearCombination'.mul_pf {α : Type u_1} {a₁ a₂ b₁ b₂ : α} [Mul α] (p₁ : a₁ = b₁) (p₂ : a₂ = b₂) :
a₁ * a₂ = b₁ * b₂
source
theorem Mathlib.Tactic.LinearCombination'.inv_pf {α : Type u_1} {a b : α} [Inv α] (p : a = b) :
a⁻¹ = b⁻¹
source
theorem Mathlib.Tactic.LinearCombination'.pf_div_c {α : Type u_1} {a b : α} [Div α] (p : a = b) (c : α) :
a / c = b / c
source
theorem Mathlib.Tactic.LinearCombination'.c_div_pf {α : Type u_1} {b c : α} [Div α] (p : b = c) (a : α) :
a / b = a / c
source
theorem Mathlib.Tactic.LinearCombination'.div_pf {α : Type u_1} {a₁ a₂ b₁ b₂ : α} [Div α] (p₁ : a₁ = b₁) (p₂ : a₂ = b₂) :
a₁ / a₂ = b₁ / b₂
source
inductive Mathlib.Tactic.LinearCombination'.Expanded :
Type

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

- proof (pf : Lean.Term) : Expanded

  A proof of `a = b`.

- const (c : Lean.Term) : Expanded

  A value, equivalently a proof of `c = c`.

Instances For

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

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

- `.proof 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`.
- `.const c` means that the input expression is not an equation but a value.

source
theorem Mathlib.Tactic.LinearCombination'.eq_trans₃ {α : Type u_1} {a a' b b' : α} (p : a = b) (p₁ : a = a') (p₂ : b = b') :
a' = b'
source
theorem Mathlib.Tactic.LinearCombination'.eq_of_add {α : Type u_1} {a a' b b' : α} [AddGroup α] (p : a = b) (H : a' - b' - (a - b) = 0) :
a' = b'
source
theorem Mathlib.Tactic.LinearCombination'.eq_of_add_pow {α : Type u_1} {a a' b b' : α} [Ring α] [NoZeroDivisors α] (n : ℕ) (p : a = b) (H : (a' - b') ^ n - (a - b) = 0) :
a' = b'
source
def Mathlib.Tactic.LinearCombination'.elabLinearCombination' (tk : Lean.Syntax) (norm? : Option Lean.Syntax.Tactic) (exp? : Option Lean.NumLit) (input : Option Lean.Term) (twoGoals : 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.

Instances For

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

Instances For

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

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

Equations

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

Instances For

source
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 `norm` field of the tactic is set to `skip`, then the tactic will simply set the user up to prove their target using the linear combination instead of normalizing the subtraction.

Note: There is also a similar tactic `linear_combination` (no prime); this version is provided for backward compatibility. Compared to this tactic, `linear_combination`:

- drops the `←` syntax for reversing an equation, instead offering this operation using the `-` syntax
- does not support multiplication of two hypotheses (`h1 * h2`), division by a hypothesis (`3 / h`), or inversion of a hypothesis (`h⁻¹`)
- produces noisy output when the user adds or subtracts a constant to a hypothesis (`h + 3`)

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_combination' (exp := n) e` will take the goal to the `n`th 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 feature is not supported for `linear_combination2`.
- `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.

Instances For

source
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 `norm` field of the tactic is set to `skip`, then the tactic will simply set the user up to prove their target using the linear combination instead of normalizing the subtraction.

Note: There is also a similar tactic `linear_combination` (no prime); this version is provided for backward compatibility. Compared to this tactic, `linear_combination`:

- drops the `←` syntax for reversing an equation, instead offering this operation using the `-` syntax
- does not support multiplication of two hypotheses (`h1 * h2`), division by a hypothesis (`3 / h`), or inversion of a hypothesis (`h⁻¹`)
- produces noisy output when the user adds or subtracts a constant to a hypothesis (`h + 3`)

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_combination' (exp := n) e` will take the goal to the `n`th 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 feature is not supported for `linear_combination2`.
- `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.

Instances For