is
-- check a mathematical property
of an expressionis(
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.
is(x, prop)
is(y rel z)
is(x in set)
x, 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_ . |
assume
, bool
, getprop
, property::implies
, unassume
assume
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.The 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):
is
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
For 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
Here 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):
Care 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:
is
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: