linear_combination

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.

Users may provide an optional with { exponent := n }. This will raise the goal to the power n before subtracting the linear combination.

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 ring_nf SOP.

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 :=
begin
 linear_combination -2*h2,
 /- Goal: x * y + x * 2 - 1 = 0 -/
end

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

example (x y z : ℚ) (h : x = y) (h2 : x * y = 0) : x + y*z = 0 :=
by linear_combination (-y * z ^ 2 + x) * h + (z ^ 2 + 2 * z + 1) * h2 with { exponent := 2 }

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
```

move_add

Calling move_add [a, ← b, c], recursively looks inside the goal for expressions involving a sum. Whenever it finds one, it moves the summands that unify to a, b, c, removing all parentheses. Repetitions are allowed, and are processed following the user-specified ordering. The terms preceded by a ← get placed to the left, the ones without the arrow get placed to the right. Unnamed terms stay in place. Due to re-parenthesizing, doing move_add with no argument may change the goal. Also, the order in which the terms are provided matters: the tactic reads them from left to right. This is especially important if there are multiple matches for the typed terms in the given expressions.

A single call of move_add moves terms across different sums in the same expression. Here is an example.

import tactic.move_add

example {a b c d : ℕ} (h : c = d) : c + b + a = b + a + d :=
begin
  move_add [← a, b],  -- Goal: `a + c + b = a + d + b`  -- both sides changed
  congr,
  exact h
end

example {a b c d : ℕ} (h : c = d) : c + b * c + a * c = a * d + d + b * d :=
begin
  move_add [_ * c, ← _ * c], -- Goal: `a * c + c + b * c = a * d + d + b * d`
  -- the first `_ * c` unifies with `b * c` and moves to the right
  -- the second `_ * c` unifies with `a * c` and moves to the left
  congr;
  assumption
end

The list of expressions that move_add takes is optional and a single expression can be passed without brackets. Thus move_add ← f and move_add [← f] mean the same.

Finally, move_add can also target one or more hypotheses. If hp₁, hp₂ are in the local context, then move_add [f, ← g] at hp₁ hp₂ performs the rearranging at hp₁ and hp₂. As usual, passing ⊢ refers to acting on the goal.

Reporting sub-optimal usage #

The tactic could fail to prove the reordering. One potential cause is when there are multiple matches for the rearrangements and an earlier rewrite makes a subsequent one fail. Another possibility is that the rearranged expression changes the Type of some expression and the tactic gets stumped. Please, report bugs and failures in the Zulip chat!

There are three kinds of unwanted use for move_add that result in errors, where the tactic fails and flags the unwanted use.

1. move_add [vars]? at * reports globally unused variables and whether all goals are unchanged, not each unchanged goal.
2. If a target of move_add [vars]? at targets is left unchanged by the tactic, then this will be flagged (unless we are using at *).
3. If a user-provided expression never unifies, then the variable is flagged.

In these cases, the tactic produces an error, reporting unused inputs and unchanged targets as appropriate.

For instance, move_add ← _ always fails reporting an unchanged goal, but never an unused variable.

Comparison with existing tactics #

• tactic.interactive.abel performs a "reduction to normal form" that allows it to close goals involving sums with higher success rate than move_add. If the goal is an equality of two sums that are simply obtained by reparenthesizing and permuting summands, then move_add [appropriate terms] can close the goal. Compared to abel, move_add has the advantage of allowing the user to specify the beginning and the end of the final sum, so that from there the user can continue with the proof.

• tactic.interactive.ac_change supports a wide variety of operations. At the moment, move_add works with addition, move_mul works with multiplication. There is the possibility of supporting other operations, using the non-interactive tactic tactic.move_op. Still, on several experiments, move_add had a much quicker performance than ac_change. Also, for move_add the user need only specify a few terms: the tactic itself takes care of producing the full rearrangement and proving it "behind the scenes".

Remark: #

It is still possible that the same output of move_add [exprs] can be achieved by a proper sublist of [exprs], even if the tactic does not flag anything. For instance, giving the full re-ordering of the expressions in the target that we want to achieve will not complain that there are unused variables, since all the user-provided variables have been matched. Of course, specifying the order of all-but-the-last variable suffices to determine the permutation. E.g., with a goal of a + b = 0, applying either one of move_add [b,a], or move_add a, or move_add ← b has the same effect and changes the goal to b + a = 0. These are all valid uses of move_add.

move_mul

See the doc-string for tactic.interactive.move_add and mentally replace addition with multiplication throughout. ;-)