Commit 2024-09-13 09:21 8dc7c801
View on Github →refactor: downgrade linear_combination
(#15899)
This PR drops support from several operations from the linear_combination
tactic:
- multiplication of two hypotheses
- division by a hypothesis
- inversion of a hypothesis
- addition or subtraction of a constant and a hypothesis
The first three operations are removed in order to make
linear_combination
perform only genuinely linear operations; this makes the tactic more predictable and also allows for more flexibility in refactors/reimplementations. The last operation is removed because, after of the removal of the other three, it is redundant (adding a constant to both sides of an equation doesn't change the difference of the two sides). The old operations are still available using thecongr(...)
term elaborator or using the legacylinear_combination'
tactic. A side effect that be seen inMathlib/AlgebraicGeometry/EllipticCurve/Weierstrass.lean
is that elaboration changes slightly; previously⁻¹
was one of the supported operations on hypotheses, so⁻¹
got handled differently in constants too. In that example, previously the atom which got pre-elaborated wasC'.u
; now the atom which gets pre-elaborated isC'.u⁻¹
. Discussion on Zulip