Quadratic formula

Stream: new members

[Iocta]

I'm trying to prove the quadratic formula with a = 1 but it's becoming tedious. Is there a better way to do this?

theorem my_monic_complete_square (x b c : ℝ) : x ^ 2 + b * x + c = (x + b/2)^2 - (b/2)^2 + c := by
  nlinarith

theorem my_monic_quadratic_formula (b c x : ℝ) :
  x ^ 2 + b * x + c = 0 ↔
  x = (-b + (Real.sqrt (b ^ 2 - 4 * c) ) ) / 2 ∨
  x = (-b - (Real.sqrt (b ^ 2 - 4 * c) ) ) / 2 := by
  apply Iff.intro
  {
    intro h
    have h: x ^ 2 + 2 * (b/2) * x + c = 0
    linarith
    rw [my_monic_complete_square] at h
    have h: (x + (b / 2)) ^ 2 = (b / 2) ^ 2 - c
    linarith
    have : ((x + b / 2) ≤ 0) ∨ ¬((x + b / 2) ≤ 0)
    apply or_not
    cases this with
    | inl hle => sorry
    | inr nle =>
      have : Real.sqrt ((x + b / 2) ^ 2 ) = Real.sqrt ((b / 2) ^ 2 - c)
      simp_all only [div_pow]
      rw [Real.sqrt_sq] at this
      apply Or.inl
      have : x = Real.sqrt ((b / 2) ^ 2 - c) - b / 2
      linarith
      simp only [div_pow] at this
      norm_num at this
      have sqrt_four : Real.sqrt 4 = 2; sorry
      rw [← mul_div_cancel c four_ne_zero, ←sub_div, sqrt_div, sqrt_four, ←sub_div, ] at this
      ring_nf at this
      ring_nf
      apply this
      sorry
      apply le_of_lt (lt_of_not_le nle)
  }
  {
    sorry
  }

[Kevin Buzzard]

I doubt this is true as stated. What if b^2-4ac is negative? Then the square root will be a junk (real) value but the corresponding junk value of x won't be a solution to the equation (which will have no solutions)

[Matt Diamond]

if you're feeling stuck it could help to see how mathlib proves it (docs#quadratic_eq_zero_iff), though maybe that would defeat the purpose of figuring it out yourself

[Matt Diamond]

also worth noting that the mathlib proofs make use of the linear_combination tactic (docs#Mathlib.Tactic.LinearCombination.linearCombination), so maybe that could be helpful

[Michael Stoll]

... which frequently comes from a suggestion via polyrith.

[Iocta]

Tedious, but done.

theorem my_monic_complete_square (x b c : ℝ) : x ^ 2 + b * x + c = (x + b/2)^2 - (b/2)^2 + c := by
  nlinarith

lemma sqrt_four_eq_two : Real.sqrt 4 = 2 := by
    have : (4:Real) = 2 * 2; norm_num
    rw [this]
    simp only [ofNat_nonneg, sqrt_mul_self]


theorem my_neg_sqrt_eq (a b : Real) (ha : a ≤ 0) (hb : 0 ≤ b) (h : a ^ 2 = b) : -Real.sqrt b = a := by
  have : 0 ≤ -a
  linarith
  have : Real.sqrt b = -a
  apply (sqrt_eq_iff_sq_eq hb this).2
  linarith
  linarith


theorem my_monic_quadratic_formula (b c x : ℝ) (h1 : 0 ≤ b ^ 2 - 4 * c ) :
  x ^ 2 + b * x + c = 0 →
  x = (-b + (Real.sqrt (b ^ 2 - 4 * c) ) ) / 2 ∨
  x = (-b - (Real.sqrt (b ^ 2 - 4 * c) ) ) / 2 := by
  intro h
  have h: x ^ 2 + 2 * (b/2) * x + c = 0
  linarith
  rw [my_monic_complete_square] at h
  have h: (x + (b / 2)) ^ 2 = (b / 2) ^ 2 - c
  linarith
  have : ((x + b / 2) ≤ 0) ∨ ¬((x + b / 2) ≤ 0)
  apply or_not
  cases this with
  | inl hle =>
    apply Or.inr
    have : (x + (b/2)) = (- (Real.sqrt ((b/2)^2 - c)))
    {
      rw [my_neg_sqrt_eq _ _ _]
      linarith
      linarith
      linarith
    }
    have : x = (- (Real.sqrt ((b/2)^2 - c))) - b/2; linarith
    have : x = (- (Real.sqrt ((1/2)^2 * (b^2 - 4 * c )))) - b/2; { ring_nf at *; linarith }
    have : x = (- ((Real.sqrt ((1/2)^2)) * (Real.sqrt (b^2 - 4 * c)))) - b/2; {
      have nn: (0:ℝ) ≤ (1/2)^2; norm_num
      rw [←my_sqrt_mul nn h1]
      apply this
    }
    have : x = (- 1/2 * (Real.sqrt (b^2 - 4 * c ))) - b/2
    {
      have eq_half: Real.sqrt ((1/2)^2) = 1/2;
      {
        norm_num
        simp only [one_div, inv_inj]
        apply sqrt_four_eq_two
      }
      rw [eq_half] at this
      linarith
    }
    linarith
  | inr nle =>
    have : Real.sqrt ((x + b / 2) ^ 2 ) = Real.sqrt ((b / 2) ^ 2 - c)
    simp_all only [div_pow]
    rw [Real.sqrt_sq] at this
    apply Or.inl
    have : x = Real.sqrt ((b / 2) ^ 2 - c) - b / 2; linarith
    simp only [div_pow] at this
    norm_num at this
    rw [← mul_div_cancel c four_ne_zero, ←sub_div, sqrt_div, sqrt_four_eq_two,  ] at this
    ring_nf at this
    ring_nf
    apply this
    linarith
    apply le_of_lt (lt_of_not_le nle)

[Richard Copley]

This way is fairly clean.

import Mathlib.Data.Real.Basic
import Mathlib.Data.Real.Sqrt
import Mathlib.Tactic

theorem my_monic_quadratic_formula (b c x : ℝ) :
    x ^ 2 + b * x + c = 0 ↔
      0 ≤ b ^ 2 - 4 * c ∧
        (x = (-b + Real.sqrt (b ^ 2 - 4 * c)) / 2 ∨
          x = (-b - Real.sqrt (b ^ 2 - 4 * c)) / 2) := by
  trans (b + 2 * x) ^ 2 = b ^ 2 - 4 * c
  . constructor
    . sorry
    . sorry
  . constructor
    . intro h
      constructor
      . sorry
      . refine Or.imp (fun hle => ?_) (fun hgt => ?_) (le_or_gt 0 (b + 2 * x))
        . sorry
        . sorry
    . rintro ⟨h, rfl | rfl⟩
      . sorry
      . sorry