Given that lhs = rhs, this tactic returns an expr proving that coeff * lhs = coeff * rhs.

• Input:

  • h_equality : an expr, whose type should be an equality between terms of type α, where there is an instance of has_mul α
  • coeff : a pexpr, which should be a value of type α

• Output: an expr, which proves that the result of multiplying both sides of h_equality by the coeff holds

Given two hypotheses that a = b and c = d, this tactic returns an expr proving that a + c = b + d.

• Input:

  • h_equality1 : an expr, whose type should be an equality between terms of type α, where there is an instance of has_add α
  • h_equality2 : an expr, whose type should be an equality between terms of type α

• Output: an expr, which proves that the result of adding the two equalities holds

Given that a = b and c = d, along with a coefficient, this tactic returns an expr proving that a + coeff * c = b + coeff * d.

• Input:

  • h_equality1 : an expr, whose type should be an equality between terms of type α, where there are instances of has_add α and has_mul α
  • h_equality2 : an expr, whose type should be an equality between terms of type α
  • coeff_for_eq2 : a pexpr, which should be a value of type α

• Output: an expr, which proves that the result of adding the first equality to the result of multiplying coeff_for_eq2 by the second equality holds

Given that l_sum1 = r_sum1, l_h1 = r_h1, ..., l_hn = r_hn, and given coefficients c_1, ..., c_n, this tactic returns an expr proving that l_sum1 + (c_1 * l_h1) + ... + (c_n * l_hn) = r_sum1 + (c_1 * r_h1) + ... + (c_n * r_hn)

• Input:

  • expected_tp: the type of the terms being compared in the target equality
  • an option (tactic expr) : none, if there is no sum to add to yet, or some containing the base summation equation
  • a list name : a list of names, referring to equalities in the local context
  • a list pexpr : a list of coefficients to be multiplied with the corresponding equalities in the list of names

• Output: an expr, which proves that the weighted sum of the given equalities added to the base equation holds

Given a list of names referencing equalities and a list of pexprs representing coefficients, this tactic proves that a weighted sum of the equalities (where each equation is multiplied by the corresponding coefficient) holds.

• Input:

  • expected_tp: the type of the terms being compared in the target equality
  • h_eqs_names : a list of names, referring to equalities in the local context
  • coeffs : a list of coefficients to be multiplied with the corresponding equalities in the list of names

• Output: an expr, which proves that the weighted sum of the equalities holds

This tactic proves that the result of moving all the terms in an equality to the left side of the equals sign by subtracting the right side of the equation from the left side holds. In other words, given lhs = rhs, this tactic proves that lhs - rhs = 0.

• Input:

  • h_equality : an expr, whose type should be an equality between terms of type α, where there is an instance of add_group α

• Output: an expr, which proves that lhs - rhs = 0, where lhs and rhs are the left and right sides of h_equality respectively

This tactic replaces the target with the result of moving all the terms in the target to the left side of the equals sign by subtracting the right side of the equation from the left side. In other words, when the target is lhs = rhs, this tactic proves that lhs - rhs = 0 and replaces the target with this new equality. Note: The target must be an equality when this tactic is called, and the equality must have some type α on each side, where there is an instance of add_group α.

• Input: N/A

• Output: N/A

This tactic changes the goal to be that the lefthand side of the target is equal to the lefthand side of the given expression. For example, if hsum_on_left is 5*x - 5*y = 0, and the target is -5*y + 5*x = 0, this tactic will change the target to be -5*y + 5*x = 5*x - 5*y.

This tactic only should be used when the target's type an equality whose right side is 0.

• Input:

  • hsum_on_left : expr, whose type should be an equality with 0 on the right side of the equals sign

• Output: N/A

This tactic attempts to prove the goal by normalizing the target if the normalize field of the given configuration is true.

• Input:

  • config : a linear_combination_config, which determines the tactic used for normalization if normalization is done

• Output: N/A

This is a tactic that attempts to prove the target by creating and applying a linear combination of a list of equalities. (If the normalize field of the configuration is set to ff, then the tactic will simply set the user up to prove their target using the linear combination instead of attempting to finish the proof.)

Note: The left and right sides of all the equalities should have the same ring type, and the coefficients should also have this type. There must be instances of has_mul and add_group for this type. Also note that the target must involve at least one variable.

• Input:

  • h_eqs_names : a list of names, referring to equations in the local context
  • coeffs : a list of coefficients to be multiplied with the corresponding equations in the list of names
  • config : a linear_combination_config, which determines the tactic used for normalization; by default, this value is the standard configuration for a linear_combination_config

• Output: N/A

mk_mul [p₀, p₁, ..., pₙ] produces the pexpr p₀ * p₁ * ... * pₙ.

as_linear_combo neg ms e is used to parse the argument to linear_combination. This argument is a sequence of literals x, -x, or c*x combined with + or -, given by the pexpr e. The neg and ms arguments are used recursively; called at the top level, its usage should be as_linear_combo ff [] e.

linear_combination attempts to prove the target by creating and applying a linear combination of a list of equalities. 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 attempting to finish the proof.

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 has_mul and add_group for this type.

• Input:

  • input : the linear combination of proofs of equalities, given as a sum/difference of coefficients multiplied by expressions. The coefficients may be arbitrary pre-expressions; if a coefficient is an application of + or - it should be surrounded by parentheses. The expressions can be arbitrary proof terms proving equalities. Most commonly they are hypothesis names h1, h2, ....

    If a coefficient is omitted, it is taken to be 1.

  • config : a linear_combination_config, which determines the tactic used for normalization; by default, this value is the standard configuration for a linear_combination_config. In the standard configuration, normalize is set to tt (meaning this tactic is set to use normalization), and normalization_tactic is set to ring1.

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 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 :=
begin
  linear_combination 2*h1 with {normalize := ff},
  simp,
  norm_cast
end

constants (qc : ℚ) (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
```