Commit 2024-09-04 05:45 57e84d67

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