Documentation

Mathlib.Tactic.MoveAdd

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.

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 Expressions.

Equations
Instances For
    partial def Lean.Expr.size (e : Lean.Expr) :

    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,

    def Mathlib.MoveAdd.uniquify {α : Type u_1} [BEq α] :
    List αList (α × )

    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
    Instances For
      def Mathlib.MoveAdd.weight {α : Type u_1} [BEq α] (L : List (α × Bool)) (a : α) :

      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
        def Mathlib.MoveAdd.reorderUsing {α : Type u_1} [BEq α] (toReorder : List α) (instructions : List (α × Bool)) :
        List α

        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,

        Equations
        • One or more equations did not get rendered due to their size.
        Instances For

          prepareOp sum takes an Expression 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
          Instances For
            partial def Mathlib.MoveAdd.sumList (prepOp : Lean.Expr) (left_assoc? : Bool) :

            sumList prepOp left_assoc? exs assumes that prepOp is an Expression 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 Expressions, 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 Expression 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_sums 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 Expression 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
                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 Expression tgt. It unifies each Expression 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 Boolean;
                      • 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 Expression corresponding to the parsed term,
                        • the Boolean 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 maxs.

                          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 maxs.

                            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 maxs.

                              Equations
                              • One or more equations did not get rendered due to their size.
                              Instances For