Commit 2022-11-17 05:45 3d0ca446

feat: linear_combination tactic (#605) I made some opinionated changes in this reimplementation:

• The default behavior has been changed to call ring1 as the normalization tactic instead of ring_nf. In particular, it neither normalizes in atoms, nor does it produce subgoals (it is a finishing tactic). You can use (norm := skip) to do the equivalent of {normalize := ff}, and (norm := ring_nf) to use it nonterminally.
• The linear_combination2 tactic produces two subgoals instead of one, showing that the weighted sums of the LHSs adds up to the LHS of the goal and similarly for the RHSs. Also useful to this end is the <- h operator (reappropriating the <- e term syntax new in lean 4), which reverses an equation, making it contribute its LHS to the RHS and vice versa. Also you can now do constant additions h + x which are necessary to make the LHS and RHS both line up. This makes it usable even on semirings. cc: @robertylewis @hrmacbeth