Given a list lp of bool × pexpr and a list l_un of expr, scan the elements of lp one at a time and produce 3 sublists of l_un.

If (tf,pe) is the first element of lp, we look for the first element of l_un that unifies with pe.to_expr. If no such element exists, then we discard (tf,pe) and move along. If eu ∈ l_un is the first element of l_un that unifies with pe.to_expr, then we add eu as the next element of either the first or the second list, depending on the boolean tf and we remove eu from the list l_un. In this case, we continue our scanning with the next element of lp, replacing l_un by l_un.erase eu.

Once we exhaust the elements of lp, we return the four lists:

• l_tt: the list of elements of l_un that came from an element of lp whose boolean was tt,
• l_ff: the list of elements of l_un that came from an element of lp whose boolean was ff,
• l_un: the un-unified elements of l_un,
• l_m: a "mask" list of booleans corresponding to the elements of lp that were placed in l_un.

The ununified elements of l_un get used for error management: they keep track of which user inputs are superfluous.

We adapt move_left_or_right to our goal:

1. we convert a list of pairs bool × pexpr to a list of pairs bool × expr,
2. we use the extra input sl : list expr to perform the unification and sorting step move_left_or_right,
3. we jam the third factor inside the first two.

as_given_op op e unifies the head term of e, which is a ≥2-argument function application, with the binary operation op, failing if it cannot.

(e, unused) ← reorder_oper op lp e converts an expression e to a similar looking one. The tactic scans the expression e looking for subexpressions that begin with the given binary operation op. As soon as reorder_oper finds one such subexpression,

• it extracts the "op-summands" in the subexpression,
• it rearranges them according to the rules determined by lp,
• it recurses into each op-summand.

The unused output is a list of booleans. It is keeping track of which of the inputs provided by lp is actually used to perform the rearrangements. It is useful to report unused inputs.

Here are two examples:

#eval trace $ reorder_oper ``((=)) [(ff,``(2)), (tt,``(7))] `(∀ x y : ℕ, 2 = 0)
--  (ℕ → ℕ → 0 = 2, [ff, tt])
-- the input `[(ff,``(2)), (tt,``(7))]` instructs Lean to move `2` to the right and `7`
-- to the left.  Lean reports that `2` is not unused and `7` is unused as `[ff, tt]`.

#eval trace $ reorder_oper ``((+)) [(ff,``(2)), (tt,``(5))]
  `(λ (e : ℕ), ∀ (x : ℕ), ∃ (y : ℕ),
      2 + x * (y + (e + 5)) + y = x + 2 + e → 2 + x = x + 5 + (2 + y))
/-  `2` moves to the right, `5` moves to the left.  Lean reports that `2, 5` are not unused
    as `[ff,ff]`
   (λ (e : ℕ), ∀ (x : ℕ), ∃ (y : ℕ),
      x * (5 + y + e) + y + 2   = x + e + 2 → x + 2 = 5 + x + y + 2, [ff, ff]) -/

TODO: use ext_simplify_core instead of traversing the expression manually

Passes the user input na to reorder_oper at a single location, that could either be none (referring to the goal) or some name (referring to hypothesis name). Replaces the given hypothesis/goal with the rearranged one that reorder_hyp receives from reorder_oper. Returns a pair consisting of a boolean and a further list of booleans. The single boolean is tt iff the tactic did not change the goal on which it was acting. The list of booleans records which variable in ll has been unified in the application: tt means that the corresponding variable has not been unified.

This definition is useful to streamline error catching.

move_op_arg is a single elementary argument that move_op takes for the variables to be moved. It is either a pexpr, or a pexpr preceded by a ←.

move_pexpr_list_or_texpr is either a list of move_op_arg, possibly empty, or a single move_op_arg.

move_op args locat op is the non-interactive version of the main tactics move_add and move_mul of this file. Given as input args (a list of terms of a sequence of operands), locat (hypotheses or goal where the tactic should act) and op (the operation to use), move_op attempts to perform the rearrangement of the terms determined by args.

Currently, the tactic uses only add/mul_comm, add/mul_assoc, add/mul_left_comm, so other operations will not actually work.

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.

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

move_oper behaves like move_add except that it also takes an associative, commutative, binary operation as input. The operation must be passed as a list consisting of a single element. For instance

example (a b : ℕ) : max a b = max b a :=
by move_oper [max] [← a, b] at *

solves the goal. For more details, see the move_add doc-string, replacing add with your intended operation.