# Commit2024-09-04 05:4557e84d67

View on Github →

refactor: handle semirings differently in `linear_combination` (#16103) This PR adjusts the `linear_combination` tactic to treat semirings and rings uniformly. Previously, semirings could only be treated using the `linear_combination2` variant, whose scope is problems such as

``````a b : ℕ
h1 : 3 * a = b + 5
h2 : b + 3 = 2 * a
⊢ 3 * a + b + 3 = 2 * a + b + 5
``````

in which the LHS and RHS of the goal can be produced as the same linear combination of the hypotheses: this problem is solved with `linear_combination2 h1 + h2` because `3 * a + b + 3 = (3 * a) + (b + 3)` and `2 * a + b + 5 = (b + 5) + (2 * a)`. To solve more generic linear-reasoning problems like

``````a b : ℕ
h1 : 3 * a = b + 5
h2 : b + 3 = 2 * a
⊢ a = 2
``````

it was necessary to pad the LHS and RHS with constants until they reached that form:

``````example {a b : ℕ} (h1 : 3 * a = b + 5) (h2 : b + 3 = 2 * a) : a = 2 := by
apply add_right_cancel (b := 2 * a + b + 3)
linear_combination2 h1 + h2
``````

This PR rewrites the `linear_combination` implementation to avoid negation, so that problems such as the above can be solved in semirings without explicit padding. For example, previously the tactic solved the above problem over true rings by reducing to the goal

``````a - 2 - (3 * a + (b + 3) - (b + 5 + 2 * a)) = 0
``````

(which is solved by the normalization tactic `ring1`). By instead reducing to the subtraction-free goal

``````a + (b + 5 + 2 * a) = 2 + (3 * a + (b + 3))
``````

the logic works over semirings as well. Thus this now works:

``````example {a b : ℕ} (h1 : 3 * a = b + 5) (h2 : b + 3 = 2 * a) : a = 2 := by
linear_combination h1 + h2
``````

Similarly, previously reversing an equality required the syntax `←`:

``````example {a : ℕ} (h : a = 3) : 3 = a := by linear_combination2 (← h)
``````

But reversing an equality is the same as formally negating it, so by implementing negation of hypotheses throughout as equation-reversal, we can eliminate this special syntax and instead use the same syntax that works over true rings:

``````example {a : ℕ} (h : a = 3) : 3 = a := by linear_combination -h
``````

(The syntax `←` continues to be required in the backwards-compatible `linear_combination'` and `linear_combination2` variants.)