assumptions.py

from sage.structure.sage_object import SageObject
from sage.rings.all import ZZ, QQ, RR, CC
from sage.symbolic.ring import is_SymbolicVariable
_assumptions = []

class GenericDeclaration(SageObject):

    def __init__(self, var, assumption):
        """
        This class represents generic assumptions, such as a variable being
        an integer or a function being increasing. It passes such
        information to maxima's declare (wrapped in a context so it is able
        to forget).

        INPUT:


        -  ``var`` - the variable about which assumptions are
           being made

        -  ``assumption`` - a Maxima feature, either user
           defined or in the list given by maxima('features')


        EXAMPLES::

            sage: from sage.symbolic.assumptions import GenericDeclaration
            sage: decl = GenericDeclaration(x, 'integer')
            sage: decl.assume()
            sage: sin(x*pi)
            sin(pi*x)
            sage: sin(x*pi).simplify()
            0
            sage: decl.forget()
            sage: sin(x*pi)
            sin(pi*x)

        Here is the list of acceptable features.

        ::

            sage: maxima('features')
            [integer,noninteger,even,odd,rational,irrational,real,imaginary,complex,analytic,increasing,decreasing,oddfun,evenfun,posfun,constant,commutative,lassociative,rassociative,symmetric,antisymmetric,integervalued]
        """
        self._var = var
        self._assumption = assumption
        self._context = None

    def __repr__(self):
        """
        EXAMPLES::

            sage: from sage.symbolic.assumptions import GenericDeclaration
            sage: GenericDeclaration(x, 'foo')
            x is foo
        """
        return "%s is %s" % (self._var, self._assumption)

    def __cmp__(self, other):
        """
        TESTS::

            sage: from sage.symbolic.assumptions import GenericDeclaration as GDecl
            sage: var('y')
            y
            sage: GDecl(x, 'integer') == GDecl(x, 'integer')
            True
            sage: GDecl(x, 'integer') == GDecl(x, 'rational')
            False
            sage: GDecl(x, 'integer') == GDecl(y, 'integer')
            False
        """
        if isinstance(self, GenericDeclaration) and isinstance(other, GenericDeclaration):
            return cmp( (self._var, self._assumption),
                        (other._var, other._assumption) )
        else:
            return cmp(type(self), type(other))

    def has(self, arg):
        """
        Check if this assumption contains the argument ``arg``.

        EXAMPLES::

            sage: from sage.symbolic.assumptions import GenericDeclaration as GDecl
            sage: var('y')
            y
            sage: d = GDecl(x, 'integer')
            sage: d.has(x)
            True
            sage: d.has(y)
            False
        """
        return (arg - self._var).is_trivial_zero()

    def assume(self):
        """
        TEST::

            sage: from sage.symbolic.assumptions import GenericDeclaration
            sage: decl = GenericDeclaration(x, 'even')
            sage: decl.assume()
            sage: cos(x*pi).simplify()
            1
            sage: decl2 = GenericDeclaration(x, 'odd')
            sage: decl2.assume()
            Traceback (most recent call last):
            ...
            ValueError: Assumption is inconsistent
            sage: decl.forget()
        """
        from sage.calculus.calculus import maxima
        if self._context is None:
            # We get the list here because features may be added with time.
            valid_features = list(maxima("features"))
            if self._assumption not in [repr(x).strip() for x in list(valid_features)]:
                raise ValueError, "%s not a valid assumption, must be one of %s" % (self._assumption, valid_features)
            cur = maxima.get("context")
            self._context = maxima.newcontext('context' + maxima._next_var_name())
            try:
                maxima.eval("declare(%s, %s)" % (repr(self._var), self._assumption))
#            except TypeError, mess:
#                if 'inconsistent' in str(mess): # note Maxima doesn't tell you if declarations are redundant
#                    raise ValueError, "Assumption is inconsistent"
            except RuntimeError, mess:
                if 'inconsistent' in str(mess): # note Maxima doesn't tell you if declarations are redundant
                    raise ValueError, "Assumption is inconsistent"
                else:
                    raise
            maxima.set("context", cur)

        if not self in _assumptions:
            maxima.activate(self._context)
            _assumptions.append(self)

    def forget(self):
        """
        TEST::

            sage: from sage.symbolic.assumptions import GenericDeclaration
            sage: decl = GenericDeclaration(x, 'odd')
            sage: decl.assume()
            sage: cos(pi*x)
            cos(pi*x)
            sage: cos(pi*x).simplify()
            -1
            sage: decl.forget()
            sage: cos(x*pi).simplify()
            cos(pi*x)
        """
        from sage.calculus.calculus import maxima
        if self._context is not None:
            try:
                _assumptions.remove(self)
            except ValueError:
                return
            maxima.deactivate(self._context)
        else: # trying to forget a declaration explicitly rather than implicitly
            for x in _assumptions:
                if repr(self) == repr(x): # so by implication x is also a GenericDeclaration
                    x.forget()
                    break
            return

    def contradicts(self, soln):
        """
        Returns ``True`` if this assumption is violated by the given
        variable assignment(s).

        INPUT:

        - ``soln`` - Either a dictionary with variables as keys or a symbolic
            relation with a variable on the left hand side.

        EXAMPLES::

            sage: from sage.symbolic.assumptions import GenericDeclaration
            sage: GenericDeclaration(x, 'integer').contradicts(x==4)
            False
            sage: GenericDeclaration(x, 'integer').contradicts(x==4.0)
            False
            sage: GenericDeclaration(x, 'integer').contradicts(x==4.5)
            True
            sage: GenericDeclaration(x, 'integer').contradicts(x==sqrt(17))
            True
            sage: GenericDeclaration(x, 'noninteger').contradicts(x==sqrt(17))
            False
            sage: GenericDeclaration(x, 'noninteger').contradicts(x==17)
            True
            sage: GenericDeclaration(x, 'even').contradicts(x==3)
            True
            sage: GenericDeclaration(x, 'complex').contradicts(x==3)
            False
            sage: GenericDeclaration(x, 'imaginary').contradicts(x==3)
            True
            sage: GenericDeclaration(x, 'imaginary').contradicts(x==I)
            False

            sage: var('y,z')
            (y, z)
            sage: GenericDeclaration(x, 'imaginary').contradicts(x==y+z)
            False

            sage: GenericDeclaration(x, 'rational').contradicts(y==pi)
            False
            sage: GenericDeclaration(x, 'rational').contradicts(x==pi)
            True
            sage: GenericDeclaration(x, 'irrational').contradicts(x!=pi)
            False
            sage: GenericDeclaration(x, 'rational').contradicts({x: pi, y: pi})
            True
            sage: GenericDeclaration(x, 'rational').contradicts({z: pi, y: pi})
            False
       """
        if isinstance(soln, dict):
            value = soln.get(self._var)
            if value is None:
                return False
        elif soln.lhs() == self._var:
            value = soln.rhs()
        else:
            return False
        try:
            CC(value)
        except TypeError:
            return False
        if self._assumption == 'integer':
            return value not in ZZ
        elif self._assumption == 'noninteger':
            return value in ZZ
        elif self._assumption == 'even':
            return value not in ZZ or ZZ(value) % 2 != 0
        elif self._assumption == 'odd':
            return value not in ZZ or ZZ(value) % 2 != 1
        elif self._assumption == 'rational':
            return value not in QQ
        elif self._assumption == 'irrational':
            return value in QQ
        elif self._assumption == 'real':
            return value not in RR
        elif self._assumption == 'imaginary':
            return value not in CC or CC(value).real() != 0
        elif self._assumption == 'complex':
            return value not in CC

def preprocess_assumptions(args):
    """
    Turns a list of the form (var1, var2, ..., 'property') into a
    sequence of declarations (var1 is property), (var2 is property),
    ...

    EXAMPLES::

        sage: from sage.symbolic.assumptions import preprocess_assumptions
        sage: preprocess_assumptions([x, 'integer', x > 4])
        [x is integer, x > 4]
        sage: var('x,y')
        (x, y)
        sage: preprocess_assumptions([x, y, 'integer', x > 4, y, 'even'])
        [x is integer, y is integer, x > 4, y is even]
    """
    args = list(args)
    last = None
    for i, x in reversed(list(enumerate(args))):
        if isinstance(x, str):
            del args[i]
            last = x
        elif ((not hasattr(x, 'assume') or is_SymbolicVariable(x))
              and last is not None):
            args[i] = GenericDeclaration(x, last)
        else:
            last = None
    return args

def assume(*args):
    """
    Make the given assumptions.

    INPUT:

    -  ``*args`` - assumptions

    EXAMPLES:

    Assumptions are typically used to ensure certain relations are
    evaluated as true that are not true in general.

    Here, we verify that for `x>0`, `\sqrt(x^2)=x`::

        sage: assume(x > 0)
        sage: bool(sqrt(x^2) == x)
        True

    This will be assumed in the current Sage session until forgotten::

        sage: forget()
        sage: bool(sqrt(x^2) == x)
        False


    Another major use case is in taking certain integrals and limits
    where the answers may depend on some sign condition::

        sage: var('x, n')
        (x, n)
        sage: assume(n+1>0)
        sage: integral(x^n,x)
        x^(n + 1)/(n + 1)
        sage: forget()

    ::

        sage: var('q, a, k')
        (q, a, k)
        sage: assume(q > 1)
        sage: sum(a*q^k, k, 0, oo)
        Traceback (most recent call last):
        ...
        ValueError: Sum is divergent.
        sage: forget()
        sage: assume(abs(q) < 1)
        sage: sum(a*q^k, k, 0, oo)
        -a/(q - 1)
        sage: forget()

    An integer constraint::

        sage: var('n, P, r, r2')
        (n, P, r, r2)
        sage: assume(n, 'integer')
        sage: c = P*e^(r*n)
        sage: d = P*(1+r2)^n
        sage: solve(c==d,r2)
        [r2 == e^r - 1]

    Simplifying certain well-known identities works as well::

        sage: sin(n*pi)
        sin(pi*n)
        sage: sin(n*pi).simplify()
        0
        sage: forget()
        sage: sin(n*pi).simplify()
        sin(pi*n)

    If you make inconsistent or meaningless assumptions,
    Sage will let you know::

        sage: assume(x<0)
        sage: assume(x>0)
        Traceback (most recent call last):
        ...
        ValueError: Assumption is inconsistent
        sage: assume(x<1)
        Traceback (most recent call last):
        ...
        ValueError: Assumption is redundant
        sage: assumptions()
        [x < 0]
        sage: forget()
        sage: assume(x,'even')
        sage: assume(x,'odd')
        Traceback (most recent call last):
        ...
        ValueError: Assumption is inconsistent
        sage: forget()

    You can also use assumptions to evaluate simple
    truth values::

        sage: x, y, z = var('x, y, z')
        sage: assume(x>=y,y>=z,z>=x)
        sage: bool(x==z)
        True
        sage: bool(z<x)
        False
        sage: bool(z>y)
        False
        sage: bool(y==z)
        True
        sage: forget()
        sage: assume(x>=1,x<=1)
        sage: bool(x==1)
        True
        sage: bool(x>1)
        False
        sage: forget()

    TESTS:

    Test that you can do two non-relational
    declarations at once (fixing Trac ticket 7084)::

        sage: var('m,n')
        (m, n)
        sage: assume(n, 'integer'); assume(m, 'integer')
        sage: sin(n*pi).simplify()
        0
        sage: sin(m*pi).simplify()
        0
        sage: forget()
        sage: sin(n*pi).simplify()
        sin(pi*n)
        sage: sin(m*pi).simplify()
        sin(pi*m)
    """
    for x in preprocess_assumptions(args):
        if isinstance(x, (tuple, list)):
            assume(*x)
        else:
            try:
                x.assume()
            except KeyError:
                raise TypeError, "assume not defined for objects of type '%s'"%type(x)

def forget(*args):
    """
    Forget the given assumption, or call with no arguments to forget
    all assumptions.

    Here an assumption is some sort of symbolic constraint.

    INPUT:


    -  ``*args`` - assumptions (default: forget all
       assumptions)


    EXAMPLES: We define and forget multiple assumptions::

        sage: var('x,y,z')
        (x, y, z)
        sage: assume(x>0, y>0, z == 1, y>0)
        sage: list(sorted(assumptions(), lambda x,y:cmp(str(x),str(y))))
        [x > 0, y > 0, z == 1]
        sage: forget(x>0, z==1)
        sage: assumptions()
        [y > 0]
        sage: assume(y, 'even', z, 'complex')
        sage: assumptions()
        [y > 0, y is even, z is complex]
        sage: cos(y*pi).simplify()
        1
        sage: forget(y,'even')
        sage: cos(y*pi).simplify()
        cos(pi*y)
        sage: assumptions()
        [y > 0, z is complex]
        sage: forget()
        sage: assumptions()
        []
    """
    if len(args) == 0:
        _forget_all()
        return
    for x in preprocess_assumptions(args):
        if isinstance(x, (tuple, list)):
            forget(*x)
        else:
            try:
                x.forget()
            except KeyError:
                raise TypeError, "forget not defined for objects of type '%s'"%type(x)

def assumptions(*args):
    """
    List all current symbolic assumptions.

    INPUT:

        - ``args`` - list of variables which can be empty.

    OUTPUT:

        - list of assumptions on variables. If args is empty it returns all
          assumptions

    EXAMPLES:

        sage: var('x,y,z,w')
        (x, y, z, w)
        sage: forget()
        sage: assume(x^2+y^2 > 0)
        sage: assumptions()
        [x^2 + y^2 > 0]
        sage: forget(x^2+y^2 > 0)
        sage: assumptions()
        []
        sage: assume(x > y)
        sage: assume(z > w)
        sage: list(sorted(assumptions(), lambda x,y:cmp(str(x),str(y))))
        [x > y, z > w]
        sage: forget()
        sage: assumptions()
        []

    It is also possible to query for assumptions on a variable independently::

        sage: x, y, z = var('x y z')
        sage: assume(x, 'integer')
        sage: assume(y > 0)
        sage: assume(y**2 + z**2 == 1)
        sage: assume(x < 0)
        sage: assumptions()
        [x is integer, y > 0, y^2 + z^2 == 1, x < 0]
        sage: assumptions(x)
        [x is integer, x < 0]
        sage: assumptions(x, y)
        [x is integer, x < 0, y > 0, y^2 + z^2 == 1]
        sage: assumptions(z)
        [y^2 + z^2 == 1]
    """
    if len(args) == 0:
        return list(_assumptions)

    result = []
    if len(args) == 1:
        result.extend([statement for statement in _assumptions
            if statement.has(args[0])])
    else:
        for v in args:
            result += [ statement for statement in list(_assumptions) \
                            if str(v) in str(statement) ]
    return result

def _forget_all():
    """
    Forget all symbolic assumptions.

    This is called by ``forget()``.

    EXAMPLES::

        sage: forget()
        sage: var('x,y')
        (x, y)
        sage: assume(x > 0, y < 0)
        sage: bool(x*y < 0)      # means definitely true
        True
        sage: bool(x*y > 0)      # might not be true
        False
        sage: forget()    # implicitly calls _forget_all
        sage: bool(x*y < 0)      # might not be true
        False
        sage: bool(x*y > 0)      # might not be true
        False

    TESTS:

    Check that Trac ticket 7315 is fixed::

        sage: var('m,n')
        (m, n)
        sage: assume(n, 'integer'); assume(m, 'integer')
        sage: sin(n*pi).simplify()
        0
        sage: sin(m*pi).simplify()
        0
        sage: forget()
        sage: sin(n*pi).simplify()
        sin(pi*n)
        sage: sin(m*pi).simplify()
        sin(pi*m)
    """
    from sage.calculus.calculus import maxima
    global _assumptions
    if len(_assumptions) == 0:
        return
    #maxima._eval_line('forget([%s]);'%(','.join([x._maxima_init_() for x in _assumptions])))
    for x in _assumptions[:]: # need to do this because x.forget() removes x from _assumptions
        x.forget()
    _assumptions = []