Roots of quadratic polynomials

Stream: mathlib4

[Christopher Hoskin]

In #25605 I lift the result for finding the solution to a quadratic equation to finding the roots of a quadratic polynomial.

I was hoping to show

variable [Field R]

variable {a b c : R}

theorem quadratic_roots_of_discrim_eq_sq [DecidableEq R] [NeZero (2 : R)] (ha : a ≠ 0) {s : R}
    (h : discrim a b c = s * s) :
    (a • X ^ 2 + b • X + C c).roots = {(-b + s) / (2 * a), (-b - s) / (2 * a)} := sorry

But the closest I could get was:

(a • X ^ 2 + b • X + C c).roots.toFinset = {(-b + s) / (2 * a), (-b - s) / (2 * a)}

Not being very familiar with multisets, I couldn't see what to do next.

Is providing this result for polynomials a useful thing to do in mathlib?

Christopher

[Kenny Lau]

@Christopher Hoskin you need to use docs#Polynomial.roots_mul after factorising the polynomial

[Kenny Lau]

let me know if you want more explicit instructions

[Christopher Hoskin]

So, something like:

theorem quadratic_roots_of_discrim_eq_sq [DecidableEq R] [NeZero (2 : R)] (ha : a ≠ 0) {s : R}
    (h : discrim a b c = s * s) :
    (a • X ^ 2 + b • X + C c).roots = {(-b + s) / (2 * a), (-b - s) / (2 * a)} := by
  have e1 : a • X ^ 2 + b • X + C c =
      a • (X - C ((-b + s) / (2 * a))) * (X - C ((-b - s) / (2 * a))) := by
    sorry
  rw [e1, Polynomial.roots_mul (by rw [← e1]; exact quadratic_ne_zero ha)]
  simp_all only [ne_eq, Algebra.smul_mul_assoc, not_false_eq_true, roots_smul_nonzero,
    roots_X_sub_C, Multiset.singleton_add, Multiset.insert_eq_cons]

?

[Kenny Lau]

@Christopher Hoskin precisely!

[Christopher Hoskin]

This is where I've got to:

section

variable {K : Type*} [Field K] [NeZero (2 : K)] {a b c : K}

theorem quadratic_factor (ha : a ≠ 0) {s : K} (h : discrim a b c = s * s) (x : K) :
    a * (x * x) + b * x + c = a * (x - (-b + s) / (2 * a)) * (x - (-b - s) / (2 * a)) := by
  ring_nf
  rw [sq s, ← h, discrim]
  ring_nf
  have p2 : (2 : K) ^ 2 = (4 : K) := by norm_num
  rw [add_comm _ (a * x ^ 2), mul_assoc, inv_mul_cancel₀ two_ne_zero, mul_one, mul_comm _ a⁻¹,
    ← mul_assoc, ← mul_assoc, inv_mul_cancel₀ ha, one_mul, ← p2, mul_assoc, ← mul_pow,
    inv_mul_cancel₀ two_ne_zero, one_pow, mul_one, mul_comm _ c, mul_assoc, ← mul_pow,
    mul_inv_cancel₀ ha, one_pow, mul_one]

end

section

variable [Field R]
variable {a b c : R}

theorem quadratic_roots_of_discrim_eq_sq [DecidableEq R] [NeZero (2 : R)] (ha : a ≠ 0) {s : R}
    (h : discrim a b c = s * s) :
    (a • X ^ 2 + b • X + C c).roots = {(-b + s) / (2 * a), (-b - s) / (2 * a)} := by
  have e0 (x : R) : eval x (a • X ^ 2 + b • X + C c) =
      eval x (a • (X - C ((-b + s) / (2 * a))) * (X - C ((-b - s) / (2 * a)))) := by
    simp only [eval_add, eval_smul, eval_pow, eval_X, smul_eq_mul, eval_C, Algebra.smul_mul_assoc,
      eval_mul, eval_sub]
    rw [sq]
    rw [quadratic_factor ha h]
    rw [mul_assoc]
  have e1 : a • X ^ 2 + b • X + C c =
      a • (X - C ((-b + s) / (2 * a))) * (X - C ((-b - s) / (2 * a))) := by
    convert e0
    sorry
  rw [e1, Polynomial.roots_mul (by rw [← e1]; exact quadratic_ne_zero ha)]
  simp_all only [ne_eq, Algebra.smul_mul_assoc, not_false_eq_true, roots_smul_nonzero,
    roots_X_sub_C, Multiset.singleton_add, Multiset.insert_eq_cons]

end

I seem to be missing an `ext` like result to remove the sorry.

Christopher

end

[Kenny Lau]

@Christopher Hoskin that ext result is injectivity of evaluation, which is not a trivial result and more importantly is not good algebraically (for example, it doesn't work for all rings, not even all fields)!

[Kenny Lau]

you should not rely on evaluation

[Kenny Lau]

you can directly prove that the two polynomials are equal

[Christopher Hoskin]

@Kenny Lau this is what I came up with: https://github.com/leanprover-community/mathlib4/pull/25605/files#diff-a9afed80ac129a470049fe0c31179050f0585e2c5c7228c49cee9331db88182aR146-R175

[Kenny Lau]

@Christopher Hoskin Well done! I've golfed it and added as suggestion.

[Kenny Lau]

(if you want some explanations, basically right now ring doesn't know about polynomials, so it can't "group X terms together etc.", so I've helped it do that manually first, and then the goals will discharge much easier

[Kenny Lau]

it's certainly going to get better in the future once we have more tactics to deal with polynomials

[Christopher Hoskin]

I've migrated the PR with the scripts/migrate_to_fork.py script, so it's now #25905.

[Kenny Lau]

@Christopher Hoskin I have golfed all your proofs and changed the names to conform to the current style

[Kenny Lau]

@Christopher Hoskin after rereading the whole file I found that there might be some refactoring that might be beneficial, namely roots_quadratic_eq_pair_iff_of_ne_zero seems useful, and the step roots_of_ne_zero_of_vieta inside it could be factored out, and the step inside about factorising the quadratic should also be factored out, and this would make a better flow of the theorems you proved as well, would you mind if I PR to your PR?

[Kenny Lau]

I'll duplicate this comment inside your PR with more instructions.

[Kenny Lau]

Honestly the entire first section might benefit from some refactoring. I don't have a concrete plan yet, but this idea is just sitting in front of my brain.

[Kenny Lau]

And I apologise in advance for bring more work to you :melt: