Commit 2023-10-09 12:27 768bedaa

View on Github →

feat(Tactic/MoveAdd): port move_add (#6576) This PR is a short implementation of the move_add tactic. It is intended as a preliminary port, featuring the reordering strategy and a very naïve proof-algorithm. A more refined version with a more robust proof will appear in a later PR.

Estimated changes

Modified Mathlib.lean

Modified Mathlib/Tactic.lean

Created Mathlib/Tactic/MoveAdd.lean

added def Lean.Expr.getExprInputs

added def Lean.Expr.size

added def Mathlib.MoveAdd.move_oper_simpCtx

added def Mathlib.MoveAdd.pairUp

added def Mathlib.MoveAdd.parseArrows

added def Mathlib.MoveAdd.permuteExpr

added def Mathlib.MoveAdd.prepareOp

added def Mathlib.MoveAdd.rankSums

added def Mathlib.MoveAdd.reorderAndSimp

added def Mathlib.MoveAdd.reorderUsing

added def Mathlib.MoveAdd.sumList

added def Mathlib.MoveAdd.unifyMovements

added def Mathlib.MoveAdd.uniquify

added def Mathlib.MoveAdd.weight

Created test/MoveAdd.lean