Applying manipulations to comparisons

[MasonProtter]

So one thing that I think is pretty natural in a CAS to want to do things like

julia> ex = @term (0 == x^2 - 4);

julia> normalize(@term ex + 4)
@term 4 == x^2 

julia> normalize(sqrt(ans))
@term ±2 == x

and

julia> ex = @term (-5x <= 1);

julia> normalize(@term ex/(-5))
@term x => 1/5

Mathematica recently implemented special functions for manipulating comparisons like the above (AddSides, MultiplySides, ApplySides, etc.). Should this package prefer to manipulate comparisons with something like ApplySides or should it be done more or less magically as sketched above?

[HarrisonGrodin]

This seems like a great feature to have. The less magic, the better, since Rewrite aims to work with generic rules. It seems like the following should solve everything but the ±, actually:

@term RULES [
    (a == b) + x => (a + x) == (b + x)
    (a >= b) + x => (a + x) >= (b + x)
    (a <= b) + x => (a + x) >= (b + x)
]

If you add that to the rule set you're using, normalizing (0 == x^2 - 4) + 4 should give 4 + 0 == x^2 - 4 + 4, which normalizes to 4 == x^2.

It's also possible that we could use broadcasting syntax (e.g. (0 == x^2 - 4) .+ 4) as syntactic sugar for applying a function call to a bunch of arguments, but that would just be more of a bonus for later (and/or implementation details).

---

Dealing with multiple solutions is tough. I might argue that sqrt(ans) in your first example should just result in 2 == x, since the sqrt function in Julia is pure and returns the positive square root. However, actually handling multiple solutions is a bigger question that will need a good answer in the coming months. I'm hoping to work on some basic solver logic soon, but that depends on a good deal of infrastructure in Rewrite which is currently indev.

[MasonProtter]

Yes, I realized as soon as I posted that sqrt is canonically considered to be the principal square root. ^(1/2) should give two solutions though I’d argue (at least once the machinery is developed in time).

Multiplication on both sides of <= by a variable x needs to include a factor of sgn(x).

I really like the idea of using .+ instead of just + because it forces one to be aware of what they’re doing when manipulating an equation but it’s also much less cumbersome than something like AddSides. Could have different broadcast types for different types of comparison relations.