@shzan 

Well, I wouldn't be as paternalistic as Carl... What I have shown is the source of this problem in Maple's internal code by means of a technique called debugging. The good thing is that your example exposes this bug. It will be reported and hopefully fixed in some future version of Maple.

@Rouben Rostamian  

Precisely, in the first linked thread I have given a link to an earlier thread were I have discussed with Edgardo about changing of Maple's behavior so that dummies in sums (but mutatis mutandis also for integrals, etc) were treated as locals. Sadly, all my posts to that thread were removed. I do not know whether it was because of censorship or plain incompetence of the administrator of this site. Nevertheless, I keep a copy of the original thread, so that I could send it to you by private email, if it were of interest.

@Carl Love 

I would say that this is a (design) bug:

> type(eval(f(x), x= -1), constant);
                                      true
> type(eval(diff(f(x), x), x= -1), constant);
                                     false
> type(D(f)(-1), constant);
                                      true

@Andriy 

Yes in 2013 he said Maple IDE. In 2011 he said Standard GUI, 2D language. And what was he using before? By the way, do you know who was behind the introduction of Java to the Maple system? And then the Standard GUI, and the 2D language, etc.

@Andriy 

Who knows? Here Laurent said that he uses 2D input all the time.

@tomleslie 

I have forgotten to tell something about why 42 expressions in my sample. It happens that for the expression 43 (of length value 143323) is entered into an apparently endless loop (internally calling a huge number of times to ithprime). As you may understand, in a programmatic situation, this is a very serious problem. With all of its defects, I have not seen simplify producing a similar bad behavior.

@tomleslie 

I would like also very much to know about pragmatic solutions! This is an issue of my concern for years, but I have not got good enough answers, even from persons with CS background. Note that this is an old issue in symbolic computation, older than Maple itself actually. And specifically about Maple, the mere fact that there are so many commands around for testing equivalence is an indication that nobody is satisfied. 

It happens that the programmatic situation is much relevant for me at present, so that I share your concerns. But precisely because of that, I think that a "scientific" survey is much needed. Otherwise, comments or advices are largely subjective.

Nevertheless, I have run a comparison between evalb((simplify@@2)(ex)=0) vs is(ex=0) on a sample of 42 medium to large expressions equivalent to zero. I have got 33 true true, 6 true false and 3 false false. I have used simplify@@2 because the idempotency issue seem to hit the class of expressions in my sample, though for many of them a single simplify would be enough. Then, my "unscientific" conclusion is that simplify@@2 is a bit better...

By the way, numerical checks of false has its own list of problems. For instance, two functions of a variable z may differ only within a region of the complex plane. So a numerical check of their equivalence with values that happen to lie outside that region may lead to a wrong conclusion. And this problem is compounded with each additional variable/parameter.

@tomleslie 

Many issues again that deserve further discussion. Specifically about is, you may be interested in reading this thread.

@ecterrab 

On my side, to the Mapleprimes site manager. I am amazed at how bad this site is being backed up.

@tomleslie 

Again, it all depends on the class of expressions (among other issues). Note that Alec's post linked In the previous thread, deals exactly with an is vs verify case. The main difference may be stated as verify is extensible by the user while is is not (apparently, beyond patching non-documented code). So, if is works for you, OK, but if not, it may be a problem.

By the way, to make things even better, note of the new command MathematicalFunctions:-Is in Maple 2015, not yet properly documented...

@Carl Love 

Yes, for a simple case like verify(x*(1-x),x-x^2,simplify) it is directly equivalent:

> kernelopts(opaquemodules=false):
> stopat(VerifyTools:-VerifyTab[simplify]):
> verify(x*(1-x),x-x^2,simplify);
VerifyTools:-VerifyTab[simplify]:
   1*  if type(x,'algebraic') and type(y,'algebraic') then
         ...
       elif type(x,'relation') and type(y,'relation') then
         ...
       elif type(x,'list') and type(y,'list') then
         ...
       else
         ...
       end if
DBG> into
VerifyTools:-VerifyTab[simplify]:
   2     evalb(simplify(x-y,args[3 .. -1]) = 0)
DBG> args
x*(1-x),
-x^2+x

And certainly the case of false has to be checked as simplify(A-B) may not return 0, even when A=B mathematically, for some classes of expressions large/complex enough. One path to that effect, a subject of a recent thread that you may remember, is simplify not being idempotent.

Nevertheless, about is(...) vs verify(...,simplify) returning false, I wonder about the source of that difference in skepticism (have  you made a comparative survey?).

@Carl Love 

I think that the GUI should show the current Digits setting in the status bar or an equivalent place as a reminder. Idem for the values of the some other relevant environment variables, etc. Something that I have requested many years ago.

@Kitonum 

This difference is a well known issue arising from differences in the order of the computation, poorly documented though. In the computation of an integral by int(f(x),x=a..b), the range a..b is used to generate internally an assumption for the name x representing the dummy integration variable. Similar process occurs for each dummy in a multiple integral computed by a single call of the form int(f(x,y,z), [z=..., y=..., x=...]). But, in a statement with nested calls to int like int(int(int(f(x,y,z), z=...), y=...), x=...), each of these calls is computed after the normal evaluation rules. So that the two inner calls to int are evaluated before the argument x=... is evaluated, less converted to an assumption for those inner integrals. Meaning that this assumption has to be added by hand explicitly, like you did for Int3.

@acer 

I do not think that you have to resolve that dichotomy. Or actually, that there is a dichotomy to be decided on the one side or the other. Within the O(10^6) users that Maplesoft claims to have, there are surely most diverse usage patterns and needs. And the same user may have diverse usage patterns or needs at different times. So, a single rigid system design is not good. Meaning that a bettter aproach is being flexible and modular, so that a user could configure and adapt the system to his/her needs. May be performance on top for somebody like you, or consistency/mathematical correctness on top for somebody like me, and the diverse variations that may be found fit.

@tomleslie 

Again, many issues. First, again, there are many equivalence checking posibilities within the framework of verify, with different strength and scope. Besides the basic verify(...,equal), you can see ?verify,expand , ?verify,evalc , etc. Structured verifications are possible, see ?verify,structured and  custom verifications can be added, see e.g. Alec's post here.

Now, typically, larger equivalence checking strength comes at a larger computational cost. Meaning that evalb is both the weakest and the cheapest, being purely built in the kernel. So, in a design where performance is the top priority, evalb is the natural choice. Note, nevertheless, that there are several other intermediate level tools at hand of the user like testeq, is and signum.