is -- check a mathematical property
of an expression
Introductionis(x, prop) checks whether the expression
x has the mathematical property prop.
is(y rel z) checks whether the relation
rel holds for the expressions y and
z.
is(x in set) checks whether x
is an element of the set.
Call(s)is(x, prop)
is(y rel z)
is(x in set)
Parametersx, y, z |
- | arithmetical expressions |
prop |
- | a property |
rel |
- | one of =,
<, >, <=, >=, <> |
set |
- | a property representing a set of numbers (e.g.,
Type::PosInt) or a set
returned by solve; such
a set can be an element of Dom::Interval, Dom::ImageSet, piecewise, or one of C_, R_, Q_, Z_. |
Returns
Related
Functionsassume, bool, getprop, property::implies, unassume
Detailsassume allows to attach basic
properties (``assumptions'') such as `x is a real number'
or `x is an odd integer' to an identifier x,
say. Arithmetical expressions involving x may inherit such
properties. E.g., `1 + x^2 is positive' if `x
is a real number'. The function is is the basic tool for
querying mathematical properties.
See the property library for a
description of all available properties.
is queries the properties of the given expressions via
getprop. Then it
checks whether the property prop or the relation y
rel z can be derived from the properties of x,
y, and z. If this is the case, then
is returns TRUE. If is derives the
logical negation of the property prop or the relation
y rel z, respectively, then it returns FALSE. Otherwise, is
returns UNKNOWN.is returns UNKNOWN, although the queried
property holds mathematically. Cf. example 4.bool to check a relation y rel
z. However, there are two main differences between bool and is:
bool produces an
error if it cannot decide whether the relation holds or not;
is(y rel z) returns UNKNOWN in this case.bool does not take
properties into account.bool(y rel z)
returns TRUE, then so
does is(y rel z). However, is is
more powerful than bool,
even when no properties are involved. Cf. example 3. On the other hand, is is usually much
slower than bool.Be careful when using is in a condition
of an if statement or a
for, while, or repeat loop: these constructs cannot
handle the value UNKNOWN. Use either is(...) =
TRUE or a case
statement. Cf. example 5.
is needs to check whether a constant symbolic
expression is zero, then it may employ a heuristic numerical zero test
based on floating point evaluation. Despite internal numerical
stabilization, this zero test may return the wrong answer in
exceptional pathological cases; in such a case, is may
return a wrong result as well.
Example
1The identifier x is assumed to be an
integer:
>> assume(x, Type::Integer): is(x, Type::Integer), is(x > 0), is(x^2 >= 0)
TRUE, UNKNOWN, TRUE
The identifier x is assumed to be a
positive real number:
>> assume(x > 0): is(x > 1), is(x >= 0), is(x < 0)
UNKNOWN, TRUE, FALSE
>> unassume(x):
Example
2is can derive certain facts even when no
properties were assumed explicitly:
>> is(x > x + 1), is(abs(x) >= 0)
FALSE, TRUE
>> is(Re(exp(x)), Type::Real)
TRUE
Example
3For relations between numbers, is yields
the same answers as bool:
>> bool(1 > 0), is(1 > 0)
TRUE, TRUE
However, on constant symbolic expressions,
is can realize more than bool:
>> is(sin(5) > 1/2), is(PI^3 + 2 < 33), is(exp(1) > exp(0.9))
FALSE, FALSE, TRUE
>> bool(sin(5) > 1/2)
Error: Can't evaluate to boolean [_less]
>> is(sqrt(2) > 1.4), is(PI > 3.1415)
TRUE, TRUE
>> bool(sqrt(2) > 1.4)
Error: Can't evaluate to boolean [_less]
>> is(E, Type::Real), is(PI, Type::PosInt)
TRUE, FALSE
Example
4Here are some examples where the queried property can be
derived mathematically. However, the current implementation of
is is not yet strong enough to derive the property:
>> assume(x, Type::Real): is(abs(x) >= x)
UNKNOWN
>> assume(x, Type::Interval(0, PI)): is(sin(x) >= 0)
UNKNOWN
>> unassume(x):
Example
5Care must be taken when using is in
if statements or for, repeat, while loops:
>> myabs := proc(x)
begin
if is(x >= 0) then
x
elif is(x < 0) then
-x
else
procname(x)
end_if
end_proc:
>> assume(x < 0): myabs(1), myabs(-2), myabs(x)
1, 2, -x
When the call of is returns UNKNOWN, an error occurs because
if expects TRUE or FALSE:
>> unassume(x): myabs(x)
Error: Can't evaluate to boolean [if];
during evaluation of 'myabs'
The easiest way to achieve the desired functionality is
a comparison of the result of is with TRUE:
>> myabs := proc(x)
begin
if is(x >= 0) = TRUE then
x
elif is(x < 0) = TRUE then
-x
else
procname(x)
end_if
end_proc:
>> myabs(x)
myabs(x)
>> delete myabs:
Example
6is can handle sets returned by solve. These include intervals of
type Dom::Interval and
R_ = solvelib::BasicSet(Dom::Real):
>> assume(x >= 0): assume(x <= 1, _and): is(x in Dom::Interval([0, 1])), is(x in R_)
TRUE, TRUE
The following solve command returns the solution as
an infinite parameterized set of type Dom::ImageSet:
>> unassume(x): solutionset := solve(sin(x) = 0, x)
{ X3*PI | X3 in Z_ }
>> domtype(solutionset)
Dom::ImageSet
is can be used to check whether an
expression is contained in this set:
>> is(20*PI in solutionset), is(PI/2 in solutionset)
TRUE, FALSE
>> delete solutionset: