equations.egi

--
--
-- Equations
--
--

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

--
-- Quadratic Equations
--
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) :=
  ( ((- b) + sqrt (b ^ 2 - 4 * a * c)) / 2 * a
  , ((- b) - sqrt (b ^ 2 - 4 * a * c)) / 2 * a )

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

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

def cF' (a: MathExpr) (b: MathExpr) (c: MathExpr) (d: MathExpr) : (MathExpr, MathExpr, MathExpr) :=
  match (a, b, c, d) as (mathExpr, mathExpr, mathExpr, mathExpr) 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)