move_add
: a tactic for moving summands #
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.
See the docstring for tactic.interactive.move_add
for more information.
Implementation notes #
This file defines a general move_op
tactic, intended for reordering terms in an expression
obtained by repeated applications of a given associative, commutative binary operation. The
user decides the final reordering. Applying move_op
without specifying the order will simply
remove all parentheses from the expression.
The main userfacing tactics are move_add
and move_mul
, dealing with addition and
multiplication, respectively.
In what is below, we talk about move_add
for definiteness, but everything applies
to move_mul
and to the more general move_op
.
The implementation of move_add
only moves the terms specified by the user (and rearranges
parentheses).
Note that the tactic abel
already implements a very solid heuristic for normalizing terms in an
additive commutative semigroup and produces expressions in more or less standard form.
The scope of move_add
is different: it is designed to make it easy to move individual terms
around a sum.
Future work #
 Add support for
neg/div/inv
in additive/multiplicative groups?  Currently the tactic has special support for
+
and*
. Every other operation is outsourced toac_refl
(see the proof ofreorder_hyp
). Should there be the desire for specialized support of other operations (e.g.∪, ∩, ⊓, ⊔, ...
), that is the definition to modify, at least in the first instance.  Add functionality for moving terms across the two sides of an in/dis/equality.
E.g. it might be desirable to have
to_lhs [a]
convertingb + c = a + d
to a + b + c = d
.  Add a nonrecursive version for use in
conv
mode.  Revise tests?
Throughout this file, op : pexpr
denotes an arbitrary (binary) operation. We do not use,
but implicitly imagine, that this operation is associative, since we extract iterations of
such operations, with complete disregard of the order in which these iterations arise.
Given a list un
of α
s and a list bo
of bool
s, return the sublist of un
consisting of the entries of un
whose corresponding entry in bo
is tt
.
Used for error management: un
is the list of user inputs, bo
is the list encoding which input
is unused (tt
) and which input is used (ff
).
return_unused
returns the unused user inputs.
If bo
is shorter than un
, return_unused
will include the remainder of un
.
Equations
 tactic.move_op.return_unused (u :: us) (b :: bs) = ite ↥b (u :: tactic.move_op.return_unused us bs) (tactic.move_op.return_unused us bs)
 tactic.move_op.return_unused (hd :: tl) list.nil = hd :: tl
 tactic.move_op.return_unused list.nil (hd :: tl) = list.nil
 tactic.move_op.return_unused list.nil list.nil = list.nil
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 userspecified 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 reparenthesizing, 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 suboptimal 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.
move_add [vars]? at *
reports globally unused variables and whether all goals are unchanged, not each unchanged goal. If a target of
move_add [vars]? at targets
is left unchanged by the tactic, then this will be flagged (unless we are usingat *
).  If a userprovided 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 thanmove_add
. If the goal is an equality of two sums that are simply obtained by reparenthesizing and permuting summands, thenmove_add [appropriate terms]
can close the goal. Compared toabel
,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 noninteractive tactictactic.move_op
. Still, on several experiments,move_add
had a much quicker performance thanac_change
. Also, formove_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 reordering
of the expressions in the target that we want to achieve will not complain that there are unused
variables, since all the userprovided variables have been matched. Of course, specifying the order
of allbutthelast 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 docstring for tactic.interactive.move_add
and mentally
replace addition with multiplication throughout. ;)