quadratic-equation.egi

-- Quadratic Formula

declare symbol x, a, b, c

def quadraticFormula : MathExpr -> MathExpr -> (MathExpr, MathExpr) := qF

def qF (f: MathExpr) (x: MathExpr) : (MathExpr, MathExpr) :=
  match coefficients f x as list mathExpr with
    | [$a_0, $a_1, $a_2] -> qF' a_2 a_1 a_0

def qF' (a: MathExpr) (b: MathExpr) (c: MathExpr) : (MathExpr, MathExpr) :=
  match (a, b, c) as (mathExpr, mathExpr, mathExpr) with
    | (#1, #0, _) -> (sqrt (- c), - sqrt (- c))
    | (#1, _, _) ->
      (2)#((- (b / 2)) + $1, (- (b / 2)) + $2)
        (withSymbols [x, y]
          qF (substitute [(x, y - b / 2)] (x ^ 2 + b * x + c)) y)
    | (_, _, _) -> qF' 1 (b / a) (c / a)

assertEqual "x^2 + x + 1"
  (qF (x ^ 2 + x + 1) x)
  ((-1 + i * sqrt 3) / 2, (-1 - i * sqrt 3) / 2)

assertEqual "x^2 + b*x + c"
  (qF (x ^ 2 + b * x + c) x)
  ((- b + sqrt (b^2 - 4 * c)) / 2, (- b - sqrt (b^2 - 4 * c)) / 2)

assertEqual "a*x^2 + b*x + c"
  (qF (a * x ^ 2 + b * x + c) x)
  ((- b + sqrt (b^2 - 4 * a * c)) / (2 * a), (- b - sqrt (b^2 - 4 * a * c)) / (2 * a))

assertEqual "a*x^2 + 2*b*x + c"
  (qF (a * x ^ 2 + 2 * b * x + c) x)
  ((- b + sqrt (b^2 - a * c)) / a, (- b - sqrt (b^2 - a * c)) / a)