Commit 2024-11-11 01:53 81eef402

feat: extend linear_combination to prove inequalities (#16841) This PR extends the linear_combination tactic to prove inequalities as well as equalities. From the test file:

example (a b : ℚ) (h1 : a ≤ 1) (h2 : b = 1) : (a + b) / 2 ≤ 1 := by
  linear_combination (h1 + h2) / 2
example {x y : ℤ} (hx : x + 3 ≤ 2) (hy : y + 2 * x ≥ 3) : y > 3 := by
  linear_combination hy + 2 * hx
example {x y z : ℚ} (h1 : 4 * x + y + 3 * z ≤ 25) (h2 : -x + 2 * y + z = 3)
    (h3 : 5 * x + 7 * z = 43) :
    x ≤ 4 := by
  linear_combination (14 * h1 - 7 * h2 - 5 * h3) / 38
example {t : ℚ} (ht : t ≥ 10) : t ^ 2 - 3 * t - 17 ≥ 5 := by
  linear_combination (t + 7) * ht