equations.egi

--
--
-- Equations
--
--

--def solve (eqs: [(MathValue, MathValue, MathValue)]) : [(MathValue, MathValue)] := solve' eqs []
--  where
--    solve1 (f: MathValue) (expr: MathValue) (x: MathValue) : MathValue := inverse expr f x
--
--    solve' (eqs: [(MathValue, MathValue, MathValue)]) (rets: [(MathValue, MathValue)]) : [(MathValue, MathValue)] :=
--      match eqs as list (mathValue, mathValue, mathValue) with
--        | [] -> rets
--        | ($f, $expr, $x) :: $rs ->
--          solve'
--            rs
--            (rets ++ [(x, solve1 (substitute rets f) (substitute rets expr) x)])

--
-- Quadratic Equations
--
def quadraticFormula : MathValue -> MathValue -> (MathValue, MathValue) := qF

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

def qF' (a: MathValue) (b: MathValue) (c: MathValue) : (MathValue, MathValue) :=
  ( ((- b) + sqrt (b ^ 2 - 4 * a * c)) / 2 * a
  , ((- b) - sqrt (b ^ 2 - 4 * a * c)) / 2 * a )

--
-- Cubic Equations
--
def cubicFormula : MathValue -> MathValue -> (MathValue, MathValue, MathValue) := cF

def cF (f: MathValue) (x: MathValue) : (MathValue, MathValue, MathValue) :=
  match coefficients f x as list mathValue with
    | $a_0 :: $a_1 :: $a_2 :: $a_3 :: [] -> cF' a_3 a_2 a_1 a_0

def cF' (a: MathValue) (b: MathValue) (c: MathValue) (d: MathValue) : (MathValue, MathValue, MathValue) :=
  match (a, b, c, d) as (mathValue, mathValue, mathValue, mathValue) with
    | (#1, #0, $p, $q) ->
      let (s1, s2) := (2)#(rt 3 $1, rt 3 $2) (qF' 1 (27 * q) ((-27) * p ^ 3))
       in ( (s1 + s2) / 3               -- r1
          , (w ^ 2 * s1 + w * s2) / 3   -- r2
          , (w * s1 + w ^ 2 * s2) / 3)  -- r3
    | (#1, _, _, _) ->
      let (s1, s2, s3) := withSymbols [x, y]
          cF (substitute [(x, y - b / 3)] (x ^ 3 + b * x ^ 2 + c * x + d)) y
       in (s1 - b / 3, s2 - b / 3, s3 - b / 3)
    | (_, _, _, _) -> cF' 1 (b / a) (c / a) (d / a)