move_add
a tactic for moving summands in expressions #
The tactic move_add
rearranges summands in expressions.
The tactic takes as input a list of terms, each one optionally preceded by ←
.
A term preceded by ←
gets moved to the left, while a term without ←
gets moved to the right.

Empty input:
move_add []
In this case, the effect of
move_add []
is equivalent tosimp only [← add_assoc]
: essentially the tactic removes all visible parentheses. 
Singleton input:
move_add [a]
andmove_add [← a]
If
⊢ b + a + c
is (a summand in) the goal, thenmove_add [← a]
changes the goal toa + b + c
(effectively,a
moved to the left).move_add [a]
changes the goal tob + c + a
(effectively,a
moved to the right);
The tactic reorders all subexpressions of the target at the same same. For instance, if
⊢ 0 < if b + a < b + a + c then a + b else b + a
is the goal, thenmove_add [a]
changes the goal to0 < if b + a < b + c + a then b + a else b + a
(a
moved to the right in three sums);move_add [← a]
changes the goal to0 < if a + b < a + b + c then a + b else a + b
(a
again moved to the left in three sums).

Longer inputs:
move_add [..., a, ..., ← b, ...]
If the list contains more than one term, the tactic effectively tries to move each term preceded by
←
to the left, each term not preceded by←
to the right maintaining the relative order in the call. Thus, applyingmove_add [a, b, c, ← d, ← e]
returns summands of the formd + e + [...] + a + b + c
, i.e.d
ande
have the same relative position in the input list and in the final rearrangement (and similarly fora, b, c
). In particular,move_add [a, b]
likely has the same effect asmove_add [a]; move_add [b]
: first, we movea
to the right, then we moveb
also to the right, aftera
. However, if the terms matched bya
andb
do not overlap, thenmove_add [← a, ← b]
has the same effect asmove_add [b]; move_add [a]
: first, we moveb
to the left, then we movea
also to the left, beforea
. The behaviour in the situation wherea
andb
overlap is unspecified:move_add
will descend into subexpressions, but the order in which they are visited depends on which rearrangements have already happened. Also note, though, thatmove_add [a, b]
may differmove_add [a]; move_add [b]
, for instance whena
andb
areDefEq
. 
Unification of inputs and repetitions:
move_add [_, ← _, a * _]
The matching of the user inputs with the atoms of the summands in the target expression is performed via checking
DefEq
and selecting the first, still available match. Thus, if a sum in the target is2 * 3 + 4 * (5 + 6) + 4 * 7 + 10 * 10
, thenmove_add [4 * _]
moves the summand4 * (5 + 6)
to the right.The unification of later terms only uses the atoms in the target that have not yet been unified. Thus, if again the target contains
2 * 3 + 4 * (5 + 6) + 4 * 7 + 10 * 10
, thenmove_add [_, ← _, 4 * _]
matches the first input (
_
) with2 * 3
;  the second input (
_
) with4 * (5 + 6)
;  the third input (
4 * _
) with4 * 7
.
The resulting permutation therefore places
2 * 3
and4 * 7
to the left (in this order) and4 * (5 + 6)
to the right:2 * 3 + 4 * 7 + 10 * 10 + 4 * (5 + 6)
.  the first input (
For the technical description, look at Mathlib.MoveAdd.weight
and Mathlib.MoveAdd.reorderUsing
.
move_add
is the specialization of a more general move_oper
tactic that takes a binary,
associative, commutative operation and a list of "operand atoms" and rearranges the operation.
Extension notes #
To work with a general associative, commutative binary operation, move_oper
needs to have inbuilt the lemmas asserting the analogues of
add_comm, add_assoc, add_left_comm
for the new operation.
Currently, move_oper
supports HAdd.hAdd
, HAdd.hAdd
, and
, or
, max
, min
.
These lemmas should be added to Mathlib.MoveAdd.move_oper_simpCtx
.
Implementation notes #
The main driver behind the tactic is Mathlib.MoveAdd.reorderAndSimp
.
The tactic takes the target, replaces the maximal subexpressions whose head symbol is the given
operation and replaces them by their reordered versions.
Once that is done, it tries to replace the initial goal with the permuted one by using simp
.
Currently, no attempt is made at guiding simp
by doing a congr
like destruction of the goal.
This will be the content of a later PR.
getExprInputs e
inspects the outermost constructor of e
and returns the array of all the
arguments to that constructor that are themselves Expr
essions.
Equations
 One or more equations did not get rendered due to their size.
Instances For
size e
returns the number of subexpressions of e
.
Reordering the variables #
This section produces the permutations of the variables for move_add
.
The user controls the final order by passing a list of terms to the tactic.
Each term can be preceded by ←
or not.
In the final ordering,
 terms preceded by
←
appear first,  terms not preceded by
←
appear last,  all remaining terms remain in their current relative order.
uniquify L
takes a list L : List α
as input and it returns a list L' : List (α × ℕ)
.
The two lists L
and L'.map Prod.fst
coincide.
The second component of each entry (a, n)
in L'
is the number of times that a
appears in L
before the current location.
The resulting list of pairs has no duplicates.
Equations
 One or more equations did not get rendered due to their size.
 Mathlib.MoveAdd.uniquify [] = []
Instances For
Return a sorting key so that all (a, true)
s are in the list's order
and sorted before all (a, false)
s, which are also in the list's order.
Although weight
does not require this, we use weight
in the case where the list obtained
from L
by only keeping the first component (i.e. L.map Prod.fst
) has no duplicates.
The properties that we mention here assume that this is the case.
Thus, weight L
is a function α → ℤ
with the following properties:
 if
(a, true) ∈ L
, thenweight L a
is strictly negative;  if
(a, false) ∈ L
, thenweight L a
is strictly positive;  if neither
(a, true)
nor(a, false)
is inL
, thenweight L a = 0
.
Moreover, the function weight L
is strictly monotone increasing on both
{a : α  (a, true) ∈ L}
and {a : α  (a, false) ∈ L}
,
in the sense that if a' = (a, true)
and b' = (b, true)
are in L
,
then a'
appears before b'
in L
if and only if weight L a < weight L b
and
similarly for the pairs with second coordinate equal to false
.
Equations
 One or more equations did not get rendered due to their size.
Instances For
reorderUsing toReorder instructions
produces a reordering of toReorder : List α
,
following the requirements imposed by instructions : List (α × Bool)
.
These are the requirements:
 elements of
toReorder
that appear withtrue
ininstructions
appear at the beginning of the reordered list, in the order in which they appear ininstructions
;  similarly, elements of
toReorder
that appear withfalse
ininstructions
appear at the end of the reordered list, in the order in which they appear ininstructions
;  finally, elements of
toReorder
that do not appear ininstructions
appear "in the middle" with the order that they had intoReorder
.
For example,
reorderUsing [0, 1, 2] [(0, false)] = [1, 2, 0]
,reorderUsing [0, 1, 2] [(1, true)] = [1, 0, 2]
,reorderUsing [0, 1, 2] [(1, true), (0, false)] = [1, 2, 0]
.
Equations
 One or more equations did not get rendered due to their size.
Instances For
prepareOp sum
takes an Expr
ession as input. It assumes that sum
is a wellformed
term representing a repeated application of a binary operation and that the summands are the
last two arguments passed to the operation.
It returns the expression consisting of the operation with all its arguments already applied,
except for the last two.
This is similar to Lean.Meta.mkAdd, Lean.Meta.mkMul
, except that the resulting operation is
primed to work with operands of the same type as the ones already appearing in sum
.
This is useful to rearrange the operands.
Equations
 One or more equations did not get rendered due to their size.
Instances For
sumList prepOp exs
assumes that prepOp
is an Expr
ession representing a binary operation
already fully applied up until its last two arguments and assumes that the last two arguments
are the operands of the operation.
Such an expression is the result of prepareOp
.
If exs
is the list [e₁, e₂, ..., eₙ]
of Expr
essions, then sumList prepOp exs
returns
prepOp (prepOp( ... prepOp (prepOp e₁ e₂) e₃) ... eₙ)
.
Equations
 Mathlib.MoveAdd.sumList prepOp x = match x with  [] => default  [a] => a  a :: as => List.foldl (fun (x y : Lean.Expr) => Lean.Expr.app (Lean.Expr.app prepOp x) y) a as
Instances For
If sum
is an expression consisting of repeated applications of op
, then getAddends
returns the Array of those recursively determined arguments whose type is DefEq to R
.
Recursively compute the Array of getAddends
Arrays by recursing into the expression sum
looking for instance of the operation op
.
Possibly returns duplicates!
rankSums op tgt instructions
takes as input
 the name
op
of a binary operation,  an
Expr
essiontgt
,  a list
instructions
of pair(expression, boolean)
.
It extracts the maximal subexpressions of tgt
whose head symbol is op
(i.e. the maximal subexpressions that consist only of applications of the binary operation op
),
it rearranges the operands of such subexpressions following the order implied by instructions
(as in reorderUsing
),
it returns the list of pairs of expressions (old_sum, new_sum)
, for which old_sum ≠ new_sum
sorted by decreasing value of Lean.Expr.size
.
In particular, a subexpression of an old_sum
can only appear after its overexpression.
Equations
 One or more equations did not get rendered due to their size.
Instances For
permuteExpr op tgt instructions
takes the same input as rankSums
and returns the
expression obtained from tgt
by replacing all old_sum
s by the corresponding new_sum
.
If there were no required changes, then permuteExpr
reports this in its second factor.
Equations
 One or more equations did not get rendered due to their size.
Instances For
pairUp L R
takes to lists L R : List Expr
as inputs.
It scans the elements of L
, looking for a corresponding DefEq
Expr
ession in R
.
If it finds one such element d
, then it sets the element d : R
aside, removing it from R
, and
it continues with the matching on the remainder of L
and on R.erase d
.
At the end, it returns the sublist of R
of the elements that were matched to some element of R
,
in the order in which they appeared in L
,
as well as the sublist of L
of elements that were not matched, also in the order in which they
appeared in L
.
Example:
#eval do
let L := [mkNatLit 0, (← mkFreshExprMVar (some (mkConst ``Nat))), mkNatLit 0]  i.e. [0, _, 0]
let R := [mkNatLit 0, mkNatLit 0, mkNatLit 1]  i.e. [0, 1]
dbg_trace f!"{(← pairUp L R)}"
/ output:
`([0, 0], [0])`
the output LHS list `[0, 0]` consists of the first `0` and the `MVarId`.
the output RHS list `[0]` corresponds to the last `0` in `L`.
/
Equations
 One or more equations did not get rendered due to their size.
 Mathlib.MoveAdd.pairUp x✝ x = pure ([], [])
Instances For
move_oper_simpCtx
is the Simp.Context
for the reordering internal to move_oper
.
To support a new binary operation, extend the list in this definition, so that it contains
enough lemmas to allow simp
to close a generic permutation goal for the new binary operation.
Equations
 One or more equations did not get rendered due to their size.
Instances For
reorderAndSimp mv op instr
takes as input an MVarId
mv
, the name op
of a binary
operation and a list of "instructions" instr
that it passes to permuteExpr
.
 It creates a version
permuted_mv
ofmv
with subexpressions representingop
sums reordered followinginstructions
.  It produces 2 temporary goals by applying
Eq.mpr
and unifying the resulting metavariable withpermuted_mv
:[⊢ mv = permuted_mv, ⊢ permuted_mv]
.  It tries to solve the goal
mv = permuted_mv
by a simplemindedsimp
call, using theop
analogues ofadd_comm, add_assoc, add_left_comm
.
Equations
 One or more equations did not get rendered due to their size.
Instances For
unifyMovements
takes as input
 an array of
Expr × Bool × Syntax
, as in the output ofparseArrows
,  the
Name
op
of a binary operation,  an
Expr
essiontgt
. It unifies eachExpr
ession appearing as a first factor of the array with the atoms for the operationop
in the expressiontgt
, returning  the lists of pairs of a matched subexpression with the corresponding
Bool
ean;  a pair of a list of error messages and the corresponding list of Syntax terms where the error should be thrown;
 an array of debugging messages.
Equations
 One or more equations did not get rendered due to their size.
Instances For
parseArrows
parses an input of the form [a, ← b, _ * (1 : ℤ)]
, consisting of a list of
terms, each optionally preceded by the arrow ←
.
It returns an array of triples consisting of
 the
Expr
ession corresponding to the parsed term,  the
Bool
eantrue
if the arrow is present in front of the term,  the underlying
Syntax
of the given term.
E.g. convert [a, ← b, _ * (1 : ℤ)]
to
[(a, false, `(a)), (b, true, `(b)), (_ * 1, false, `(_ * 1))]
.
Equations
 One or more equations did not get rendered due to their size.
Instances For
The tactic move_add
rearranges summands of expressions.
Calling move_add [a, ← b, ...]
matches a, b,...
with summands in the main goal.
It then moves a
to the far right and b
to the far left of each addition in which they appear.
The side to which the summands are moved is determined by the presence or absence of the arrow ←
.
The inputs a, b,...
can be any terms, also with underscores.
The tactic uses the first "new" summand that unifies with each one of the given inputs.
There is a multiplicative variant, called move_mul
.
There is also a general tactic for a "binary associative commutative operation": move_oper
.
In this case the syntax requires providing first a term whose head symbol is the operation.
E.g. move_oper HAdd.hAdd [...]
is the same as move_add
, while move_oper Max.max [...]
rearranges max
s.
Equations
 One or more equations did not get rendered due to their size.
Instances For
The tactic move_add
rearranges summands of expressions.
Calling move_add [a, ← b, ...]
matches a, b,...
with summands in the main goal.
It then moves a
to the far right and b
to the far left of each addition in which they appear.
The side to which the summands are moved is determined by the presence or absence of the arrow ←
.
The inputs a, b,...
can be any terms, also with underscores.
The tactic uses the first "new" summand that unifies with each one of the given inputs.
There is a multiplicative variant, called move_mul
.
There is also a general tactic for a "binary associative commutative operation": move_oper
.
In this case the syntax requires providing first a term whose head symbol is the operation.
E.g. move_oper HAdd.hAdd [...]
is the same as move_add
, while move_oper Max.max [...]
rearranges max
s.
Equations
 One or more equations did not get rendered due to their size.
Instances For
The tactic move_add
rearranges summands of expressions.
Calling move_add [a, ← b, ...]
matches a, b,...
with summands in the main goal.
It then moves a
to the far right and b
to the far left of each addition in which they appear.
The side to which the summands are moved is determined by the presence or absence of the arrow ←
.
The inputs a, b,...
can be any terms, also with underscores.
The tactic uses the first "new" summand that unifies with each one of the given inputs.
There is a multiplicative variant, called move_mul
.
There is also a general tactic for a "binary associative commutative operation": move_oper
.
In this case the syntax requires providing first a term whose head symbol is the operation.
E.g. move_oper HAdd.hAdd [...]
is the same as move_add
, while move_oper Max.max [...]
rearranges max
s.
Equations
 One or more equations did not get rendered due to their size.