`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 to`simp only [← add_assoc]`

: essentially the tactic removes all visible parentheses.Singleton input:

`move_add [a]`

and`move_add [← a]`

If

`⊢ b + a + c`

is (a summand in) the goal, then`move_add [← a]`

changes the goal to`a + b + c`

(effectively,`a`

moved to the left).`move_add [a]`

changes the goal to`b + c + a`

(effectively,`a`

moved to the right);

The tactic reorders

*all*sub-expressions 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, then`move_add [a]`

changes the goal to`0 < 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 to`0 < 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, applying`move_add [a, b, c, ← d, ← e]`

returns summands of the form`d + e + [...] + a + b + c`

, i.e.`d`

and`e`

have the same relative position in the input list and in the final rearrangement (and similarly for`a, b, c`

). In particular,`move_add [a, b]`

likely has the same effect as`move_add [a]; move_add [b]`

: first, we move`a`

to the right, then we move`b`

also to the right,*after*`a`

. However, if the terms matched by`a`

and`b`

do not overlap, then`move_add [← a, ← b]`

has the same effect as`move_add [b]; move_add [a]`

: first, we move`b`

to the left, then we move`a`

also to the left,*before*`a`

. The behaviour in the situation where`a`

and`b`

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, that`move_add [a, b]`

may differ`move_add [a]; move_add [b]`

, for instance when`a`

and`b`

are`DefEq`

.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 is`2 * 3 + 4 * (5 + 6) + 4 * 7 + 10 * 10`

, then`move_add [4 * _]`

moves the summand`4 * (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`

, then`move_add [_, ← _, 4 * _]`

matches- the first input (
`_`

) with`2 * 3`

; - the second input (
`_`

) with`4 * (5 + 6)`

; - the third input (
`4 * _`

) with`4 * 7`

.

The resulting permutation therefore places

`2 * 3`

and`4 * 7`

to the left (in this order) and`4 * (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`

, `HMul.hMul`

, `And`

, `Or`

, `Max.max`

, `Min.min`

.

These lemmas should be added to `Mathlib.MoveAdd.move_oper_simpCtx`

.

See `test/MoveAdd.lean`

for sample usage of `move_oper`

.

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

- (fn.app arg).getExprInputs = #[fn, arg]
- (Lean.Expr.lam binderName bt bb binderInfo).getExprInputs = #[bt, bb]
- (Lean.Expr.forallE binderName bt bb binderInfo).getExprInputs = #[bt, bb]
- (Lean.Expr.letE declName t v b nonDep).getExprInputs = #[t, v, b]
- (Lean.Expr.mdata data e).getExprInputs = #[e]
- (Lean.Expr.proj typeName idx e).getExprInputs = #[e]
- x.getExprInputs = #[]

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

, then`weight L a`

is strictly negative; - if
`(a, false) ∈ L`

, then`weight L a`

is strictly positive; - if neither
`(a, true)`

nor`(a, false)`

is in`L`

, then`weight 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 with`true`

in`instructions`

appear at the*beginning*of the reordered list, in the order in which they appear in`instructions`

; - similarly, elements of
`toReorder`

that appear with`false`

in`instructions`

appear at the*end*of the reordered list, in the order in which they appear in`instructions`

; - finally, elements of
`toReorder`

that do not appear in`instructions`

appear "in the middle" with the order that they had in`toReorder`

.

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 well-formed
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

- Mathlib.MoveAdd.prepareOp sum = List.foldl (fun (x y : Lean.Expr) => x.app y) sum.getAppFn (List.take (sum.getAppArgs.size - 2) sum.getAppArgs.toList)

## Instances For

`sumList prepOp left_assoc? 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 left_assoc? exs`

returns

`prepOp (prepOp( ... prepOp (prepOp e₁ e₂) e₃) ... eₙ)`

, if`left_assoc?`

is`false`

, and`prepOp e₁ (prepOp e₂ (... prepOp (prepOp eₙ₋₁ eₙ))`

, if`left_assoc?`

is`true`

.

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`

ession`tgt`

, - 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 over-expression.

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

of`mv`

with subexpressions representing`op`

-sums reordered following`instructions`

. - It produces 2 temporary goals by applying
`Eq.mpr`

and unifying the resulting meta-variable with`permuted_mv`

:`[⊢ mv = permuted_mv, ⊢ permuted_mv]`

. - It tries to solve the goal
`mv = permuted_mv`

by a simple-minded`simp`

call, using the`op`

-analogues of`add_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 of`parseArrows`

, - the
`Name`

`op`

of a binary operation, - an
`Expr`

ession`tgt`

. It unifies each`Expr`

ession appearing as a first factor of the array with the atoms for the operation`op`

in the expression`tgt`

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

ean`true`

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.