Maple's coulditbe is useful. But unfortunately it does not return back to the user the conditions under which the proposition was found true. This could make it much more useful. It seems in way similar to Mathematica' Reduce but Reduce returns the conditions.
Is there a way to find the conditions which makes it true?
I use coulditbe alot. I use it to verify that the result of odetest (I call it the residue) is zero or not. Maytimes, odetest does not return zero. And using simplify, or evalb or is to check if the residue is zero, all fail. But many times, coulditbe returns true, meaning the residue is zero. But I do not know under what conditions. In Mathematica's Reduce, it tells me the conditions.
Here is one of hundreds of examples I have
restart;
ode:=(t^3+y(t)^2*sqrt(t^2+y(t)^2))-(t*y(t)*sqrt(t^2+y(t)^2))*diff(y(t),t)=0;
ic:=y(1)=1;
sol:=dsolve([ode,ic]);
the_residue:=odetest(sol,[ode,ic]);
You see, odetest says it could not verify the solution (the first entry above) but it did verify the solution against the initial conditions.
Using simplify, evalb and is all also could not verify it
simplify(the_residue[1]);
evalb(the_residue[1]=0);
is(the_residue[1]=0);
Now coulditbe does:
_EnvTry:='hard':
coulditbe(the_residue[1]=0);
So the solution is correct, but I do not know under what conditions. Using Mathematica's Reduce I can find this:
So now back in Maple, I can do this
simplify(the_residue[1]) assuming t>exp(-2*sqrt(2)/3);
0
Actually in this example, just using assume t>0 also gives zero. But I am using Mathematica's result for illustration.
You might ask, why do I need to know for what values of the independent variable is the residue zero?
Because in some cases, the residue is zero only at single point! So it does not make sense to say the solution is verified to be correct only at one single point of the domain, right?
it needs to be some finite range at least. Here is an example of an ode whose solution is correct only at x=0
ode:=diff(y(x),x)=3*x*(y(x)-1)^(1/3);
ic:=y(3)=-7;
sol:=dsolve([ode,ic]);
the_residue:=odetest(sol,[ode,ic]);
And simplify, evalb, is all fail to verifiy this, but coulditbe says true
simplify(the_residue[1]);
evalb(the_residue[1]=0);
is(the_residue[1]=0);
_EnvTry:='hard':
coulditbe(the_residue[1]=0);
So now, we ask, is this solution then correct or not? It turns out to be zero but only at origin x=0
plot(abs(the_residue[1]),x=-1..1)
If I knew that residue is zero only at single point, then I would say this solution is not correct, right?
And that is why I need to know under what conditions coulditbe retruned true.
I tried infolevel[coulditbe]:=5 but nothing more was displayed on the screen.
Mathematica's Reduce confirms that when x=0 the residue is zero.
So my question is simply this: Can one obtain the conditions used by coulditbe to determine when result is true?
It will be useful if Maple could in future version return the value/range which makes it true.
