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 the congr(...) term elaborator or using the legacy linear_combination' tactic. A side effect that be seen in Mathlib/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 was C'.u; now the atom which gets pre-elaborated is C'.u⁻¹. Discussion on Zulip

Estimated changes