normalize-rules.egi

--
-- Normalization-rule behavior that the samples depend on:
-- the rule-suppression quote '( ), negative sqrt powers, and the
-- w rules generated by declare ideal (lib/math/normalize.egi).
--

declare symbol x, θ, θ₂

--
-- The rule-suppression quote '( ): builds the expression with the
-- rule-free structural arithmetic (declare rule rewriting off inside).
--

-- generators survive construction instead of collapsing under auto rules
assertEqual "quoted pythagorean generator"
  (show '((sin θ)^2 + (cos θ)^2 - 1)) "('sin θ)^2 + ('cos θ)^2 - 1"
assertEqual "quoted w generator" (show '(w^2 + w + 1)) "w^2 + w + 1"
-- ... while the unquoted forms are rewritten as usual
assertEqual "plain pythagorean" ((sin θ)^2 + (cos θ)^2 - 1) 0
assertEqual "plain w" (w^2 + w + 1) 0

-- structural normalization still happens inside (merge, expand)
assertEqual "merge inside quote" (show '(2 * x + x)) "3 * x"
assertEqual "expand inside quote" (show '((x + 1)^2)) "x^2 + 2 * x + 1"

-- existing quote meanings are unchanged
assertEqual "function quote" (show ('sqrt x)) "'sqrt x"
assertEqual "operator-section quote" (show ('(^) x 3)) "'^ x 3"
assertEqual "apply simplification untouched" (sqrt 8) (2 * sqrt 2)

--
-- The w rules come from `declare ideal [w^2 + w + 1]`: the single
-- generated rule w^2 -> -1 - w subsumes the old hand-written pair.
--

assertEqual "w^2" (w^2) (-1 - w)
assertEqual "w^3" (w^3) 1
assertEqual "w^5" (w^5) (w^2)
assertEqual "1 + w + w^2" (1 + w + w^2) 0

--
-- Negative powers of sqrt atoms (arising from the Laurent folding of
-- single-term denominators) reduce like positive ones: |n| >= 2
-- splits off the radicand, leaving a remainder exponent in {-1,0,1}.
-- This is what lets thurston.egi's S shed its sqrt factors.
--

def β := `(1 + θ₂ - θ₂^2)
def v := 1 / (sqrt β * x)

assertEqual "sqrt^-2" (show (v * v)) "`(- θ₂^2 + θ₂ + 1)^-1 x^-2"
assertEqual "sqrt^-4" (show (v^2 * v^2)) "`(- θ₂^2 + θ₂ + 1)^-2 x^-4"
assertEqual "sqrt^-3"
  (show (v * v * v))
  "('sqrt `(- θ₂^2 + θ₂ + 1))^-1 * `(- θ₂^2 + θ₂ + 1)^-1 * x^-3"
assertEqual "sqrt^16" ((sqrt β)^16) (β^8)
assertEqual "integer radicand ^-2" ((sqrt 2)^(-2)) (1 / 2)
assertEqual "negative power value preserved" ((v * v * v) * (sqrt β * x)^3) 1

--
-- Depth-2 sqrt denesting (declare apply sqrt, root.egi):
-- sqrt(a + b sqrt c) with a^2 - b^2 c a perfect square opens up.
--

assertEqual "denest 9 - 4 sqrt 5" (sqrt (9 - 4 * sqrt 5)) (sqrt 5 - 2)
assertEqual "denest 7 + 4 sqrt 3" (sqrt (7 + 4 * sqrt 3)) (2 + sqrt 3)
assertEqual "denest rational halves" (sqrt (2 + sqrt 3)) ((sqrt 6 + sqrt 2) / 2)
assertEqual "non-denestable stays"
  (show (sqrt (5 - 2 * sqrt 5))) "'sqrt (-2 * 'sqrt 5 + 5)"
assertEqual "denested square recovers" ((sqrt (9 - 4 * sqrt 5))^2) (9 - 4 * sqrt 5)

--
-- exp structural rules (Math/Rewrite.hs, casRewriteExp): power
-- reduction and product merging; the value rules (exp 0 / exp 1 /
-- exp (n i pi)) stay in the library.
--

assertEqual "exp power" ((exp x)^3) (exp (3 * x))
assertEqual "exp negative power" ((exp x)^(-2)) (exp (-2 * x))
assertEqual "exp merge" (exp x * exp θ) (exp (x + θ))
assertEqual "exp cancel" (exp x * exp (- x)) 1
-- the old declare-rule merge dropped the numeric coefficient
-- (2 y e^x e^y came out as y e^(x+y)); the port fixes it
assertEqual "exp merge keeps the coefficient"
  (show (2 * exp x * θ * exp θ)) "2 * ('exp (θ + x)) * θ"

--
-- Principal-branch normalization of constant radicands
-- (lib/math/common/interval.egi + root.egi): negative constants are
-- certified by interval arithmetic and become i * sqrt(-x).
--

assertEqual "certified sign, positive" (signOfConst (5 - 2 * sqrt 5)) "pos"
assertEqual "certified sign, negative" (signOfConst (-5 + 2 * sqrt 5)) "neg"
assertEqual "negative constant radicand extracts i"
  (show (sqrt (-5 - 2 * sqrt 5))) "('sqrt (2 * 'sqrt 5 + 5)) * i"
assertEqual "principal pair product"
  (sqrt (-5 - 2 * sqrt 5) * sqrt (-5 + 2 * sqrt 5)) (- sqrt 5)