# Commit 2024-09-04 05:45 57e84d67

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.)