The documentation for Zeroequiv does say
> If the expression contains functions which are
> not solutions to first order differential
> equations... there may be incorrect results.
Abs(x) doesn't qualify. In fact, Macsyma doesn't do much
with Abs, Signum, etc. For example, although abs(x)*abs(x)
simplifies to x^2, cos(abs(x)) doesn't simplify to cos(x),
signum(atan(x)) doesn't simplify to signum(x), etc.
Still, Zeroequiv does need work....
On the one hand, it is not as trivial as you might think. For
example, the following all correctly give False, though they're
numerically small over a large part of their domain:
atan(10^200*x*x)-%pi/2
atan(10^200/x^2)
exp(10*cos(x)-10)
sin(x)^1000
On the other hand, Zeroequiv gives Dontknow in some surprising
cases:
x-atan(x)
This function is well-behaved and numerically nonzero for
abs(x)>1.0e-8.
Worse, the following give True:
sin(1/1000) !!! (no variable)
sin(asin(x)+1/1000)-x
sin(x+1/1000)-sin(x)
And it gets an internal error (stack overflow) with
atan(x)^1000
Still, Zeroequiv is better than simple Ratsimp in many cases. In
particular, neither Ratsimp nor Radcan gets sin(x)^2+cos(x)^2-1 or
even tan(x)-1/cot(x). In general, if there are trig functions
involved, you need to do something like
Ratsimp(Trigexpand(Trigsimp(x)))
or
Logcontract(Radcan(ev(x,exponentialize,logarc)))
Both zeroequiv and this last simplification get
atan2(2*x,1-x^2)/2-atan(x), for example.
By the way, I often use Taylor for checking for identical zero.
Try Taylor(...,x,0,10) on the expression above, for example.
In fact, it's very good at finding some non-zero identities.
Try it on sin(x)^2+cos(x)^2. Careful, though, with large
exponents, e.g. atan(x)^1000.
-s