login  home  contents  what's new  discussion  bug reports     help  links  subscribe  changes  refresh  edit

An "assume" system based on equational reasoning.

assume(x,T) returns a kernel T(x) intended to be interpreted as forall(x:T).

fricas
domainOfComp:=empty()$Table(Symbol,BasicOperator)

\label{eq1} \mbox{\rm table} \left({}\right)(1)
Type: Table(Symbol,BasicOperator)
fricas
assume(x:Expression Integer,t:Symbol):Expression Integer ==
  -- cache operators
  if not key?(t,domainOfComp) then domainOfComp.t := operator t
  (domainOfComp.t) x
Function declaration assume : (Expression(Integer),Symbol) -> Expression(Integer) has been added to workspace.
Type: Void

Default assumptions about constants.

fricas
markConstants(x:Expression Integer):Expression Integer ==
  if (s:=isPlus(x)) case List Expression Integer then
    return reduce(+,[markConstants i for i in s::List Expression Integer])
  if (s:=isTimes(x)) case List Expression Integer then
    return reduce(*,[markConstants i for i in s::List Expression Integer])
  if (r:=retractIfCan(x)@Union(Integer,"failed")) case Integer then
    if r<0 then return assume(x,'integer)
    if r>0 then return assume(x,'positiveInteger)
    return assume(x, 'nonNegativeInteger)
  return x
Function declaration markConstants : Expression(Integer) -> Expression(Integer) has been added to workspace.
Type: Void

Inference rules.

fricas
normalForm := rule
  -- subtypes
  assume(assume(x,'integer),'integer) == assume(x,'integer)
  assume(assume(x,'integer),'nonNegativeInteger) == assume(x,'nonNegativeInteger)
  assume(assume(x,'integer),'positiveInteger) == assume(x,'positiveInteger)
  assume(assume(x,'integer),'nonZero) == assume(x,'nonZero)
  --
  assume(assume(x,'nonNegativeInteger),'integer) == assume(x,'nonNegativeInteger)
  assume(assume(x,'nonNegativeInteger),'nonNegativeInteger) == assume(x,'nonNegativeInteger)
  assume(assume(x,'nonNegativeInteger),'positiveInteger) == assume(x,'positiveInteger)
  assume(assume(x,'nonNegativeInteger),'nonZero) == assume(x,'positiveInteger)
  --
  assume(assume(x,'positiveInteger),'integer) == assume(x,'positiveInteger)
  assume(assume(x,'positiveInteger),'nonNegativeInteger) == assume(x,'positiveInteger)
  assume(assume(x,'positiveInteger),'positiveInteger) == assume(x,'positiveInteger)
  assume(assume(x,'positiveInteger),'nonZero) == assume(x,'positive)
  --
  assume(assume(x,'nonZero),'integer) == assume(x,'nonZero)
  assume(assume(x,'nonZero),'nonNegativeInteger) == assume(x,'positiveInteger)
  assume(assume(x,'nonZero),'positiveInteger) == assume(x,'positiveInteger)
  assume(assume(x,'nonZero),'nonZero) == assume(x,'nonZero)
  -- operations
  assume(x,'integer) + assume(y,'integer) == assume(x+y,'integer)
  assume(x,'integer) + assume(y,'nonNegativeInteger) == assume(x+y,'integer)
  assume(x,'integer) + assume(y,'positiveInteger) == assume(x+y,'integer)
  assume(x,'integer) + assume(y,'nonZero) == assume(x+y,'integer)
  assume(x,'nonNegativeInteger) + assume(y,'nonNegativeInteger) == assume(x+y,'nonNegativeInteger)
  assume(x,'nonNegativeInteger) + assume(y,'positiveInteger) == assume(x+y,'positiveInteger)
  assume(x,'nonNegativeInteger) + assume(y,'nonZero) == assume(x+y, 'integer)
  assume(x,'positiveInteger) + assume(y,'positiveInteger) == assume(x+y,'positiveInteger)
  assume(x,'positiveInteger) + assume(y,'nonNegativeInteger) == assume(x+y,'positiveInteger)
  assume(x,'positiveInteger) + assume(y,'nonZero) == assume(x+y,'integer)
  assume(x,'nonZero) + assume(y,'nonZero) == assume(x+y,'integer)
  --
  assume(x,'integer) * assume(y,'integer) == assume(x*y,'integer)
  assume(x,'integer) * assume(y,'nonNegativeInteger) == assume(x*y,'integer)
  assume(x,'integer) * assume(y,'positiveInteger) == assume(x*y,'integer)
  assume(x,'integer) * assume(y,'nonZero) == assume(x*y,'integer)
  assume(x,'nonNegativeInteger) * assume(y,'nonNegativeInteger) == assume(x*y,'nonNegativeInteger)
  assume(x,'nonNegativeInteger) * assume(y,'positiveInteger) == assume(x*y,'nonNegativeInteger)
  assume(x,'nonNegativeInteger) * assume(y,'nonZero) == assume(x*y, 'integer)
  assume(x,'positiveInteger) * assume(y,'positiveInteger) == assume(x*y,'positiveInteger)
  assume(x,'positiveInteger) * assume(y,'nonNegativeInteger) == assume(x*y,'nonNegativeInteger)
  assume(x,'positiveInteger) * assume(y,'nonZero) == assume(x*y,'nonZero)
  assume(x,'nonZero) * assume(y,'nonZero) == assume(x*y,'nonZero)
fricas
Compiling function assume with type (Expression(Integer),Symbol) -> 
      Expression(Integer)

\label{eq2}\begin{array}{@{}l}
\displaystyle
\left\{{{integer \left({integer \left({x}\right)}\right)}\mbox{\rm = =}{{{\tt'}assume}\left({x , \: integer}\right)}}, \: \right.
\
\
\displaystyle
\left.{{nonNegativeInteger \left({integer \left({x}\right)}\right)}\mbox{\rm = =}{{{\tt'}assume}\left({x , \: nonNegativeInteger}\right)}}, \right.
\
\
\displaystyle
\left.\: \right.
\
\
\displaystyle
\left.{{positiveInteger \left({integer \left({x}\right)}\right)}\mbox{\rm = =}{{{\tt'}assume}\left({x , \: positiveInteger}\right)}}, \right.
\
\
\displaystyle
\left.\:{{nonZero \left({integer \left({x}\right)}\right)}\mbox{\rm = =}{{{\tt'}assume}\left({x , \: nonZero}\right)}}, \: \right.
\
\
\displaystyle
\left.{{integer \left({nonNegativeInteger \left({x}\right)}\right)}\mbox{\rm = =}{{{\tt'}assume}\left({x , \: nonNegativeInteger}\right)}}, \right.
\
\
\displaystyle
\left.\: \right.
\
\
\displaystyle
\left.{{nonNegativeInteger \left({nonNegativeInteger \left({x}\right)}\right)}\mbox{\rm = =}{{{\tt'}assume}\left({x , \: nonNegativeInteger}\right)}}, \right.
\
\
\displaystyle
\left.\: \right.
\
\
\displaystyle
\left.{{positiveInteger \left({nonNegativeInteger \left({x}\right)}\right)}\mbox{\rm = =}{{{\tt'}assume}\left({x , \: positiveInteger}\right)}}, \right.
\
\
\displaystyle
\left.\: \right.
\
\
\displaystyle
\left.{{nonZero \left({nonNegativeInteger \left({x}\right)}\right)}\mbox{\rm = =}{{{\tt'}assume}\left({x , \: positiveInteger}\right)}}, \right.
\
\
\displaystyle
\left.\: \right.
\
\
\displaystyle
\left.{{integer \left({positiveInteger \left({x}\right)}\right)}\mbox{\rm = =}{{{\tt'}assume}\left({x , \: positiveInteger}\right)}}, \right.
\
\
\displaystyle
\left.\: \right.
\
\
\displaystyle
\left.{{nonNegativeInteger \left({positiveInteger \left({x}\right)}\right)}\mbox{\rm = =}{{{\tt'}assume}\left({x , \: positiveInteger}\right)}}, \right.
\
\
\displaystyle
\left.\: \right.
\
\
\displaystyle
\left.{{positiveInteger \left({positiveInteger \left({x}\right)}\right)}\mbox{\rm = =}{{{\tt'}assume}\left({x , \: positiveInteger}\right)}}, \right.
\
\
\displaystyle
\left.\:{{nonZero \left({positiveInteger \left({x}\right)}\right)}\mbox{\rm = =}{{{\tt'}assume}\left({x , \: positive}\right)}}, \: \right.
\
\
\displaystyle
\left.{{integer \left({nonZero \left({x}\right)}\right)}\mbox{\rm = =}{{{\tt'}assume}\left({x , \: nonZero}\right)}}, \: \right.
\
\
\displaystyle
\left.{{nonNegativeInteger \left({nonZero \left({x}\right)}\right)}\mbox{\rm = =}{{{\tt'}assume}\left({x , \: positiveInteger}\right)}}, \right.
\
\
\displaystyle
\left.\: \right.
\
\
\displaystyle
\left.{{positiveInteger \left({nonZero \left({x}\right)}\right)}\mbox{\rm = =}{{{\tt'}assume}\left({x , \: positiveInteger}\right)}}, \right.
\
\
\displaystyle
\left.\:{{nonZero \left({nonZero \left({x}\right)}\right)}\mbox{\rm = =}{{{\tt'}assume}\left({x , \: nonZero}\right)}}, \: \right.
\
\
\displaystyle
\left.{{{integer \left({y}\right)}+{integer \left({x}\right)}+ \%B}\mbox{\rm = =}{{{{\tt'}assume}\left({{y + x}, \: integer}\right)}+ \%B}}, \right.
\
\
\displaystyle
\left.\: \right.
\
\
\displaystyle
\left.{{{nonNegativeInteger \left({y}\right)}+{integer \left({x}\right)}+ \%C}\mbox{\rm = =}{{{{\tt'}assume}\left({{y + x}, \: integer}\right)}+ \%C}}, \right.
\
\
\displaystyle
\left.\: \right.
\
\
\displaystyle
\left.{{{positiveInteger \left({y}\right)}+{integer \left({x}\right)}+ \%D}\mbox{\rm = =}{{{{\tt'}assume}\left({{y + x}, \: integer}\right)}+ \%D}}, \right.
\
\
\displaystyle
\left.\: \right.
\
\
\displaystyle
\left.{{{nonZero \left({y}\right)}+{integer \left({x}\right)}+ \%E}\mbox{\rm = =}{{{{\tt'}assume}\left({{y + x}, \: integer}\right)}+ \%E}}, \right.
\
\
\displaystyle
\left.\: \right.
\
\
\displaystyle
\left.{{{nonNegativeInteger \left({y}\right)}+{nonNegativeInteger \left({x}\right)}+ \%F}\mbox{\rm = =}{{{{\tt'}assume}\left({{y + x}, \: nonNegativeInteger}\right)}+ \%F}}, \right.
\
\
\displaystyle
\left.\: \right.
\
\
\displaystyle
\left.{{{positiveInteger \left({y}\right)}+{nonNegativeInteger \left({x}\right)}+ \%G}\mbox{\rm = =}{{{{\tt'}assume}\left({{y + x}, \: positiveInteger}\right)}+ \%G}}, \right.
\
\
\displaystyle
\left.\: \right.
\
\
\displaystyle
\left.{{{nonZero \left({y}\right)}+{nonNegativeInteger \left({x}\right)}+ \%H}\mbox{\rm = =}{{{{\tt'}assume}\left({{y + x}, \: integer}\right)}+ \%H}}, \right.
\
\
\displaystyle
\left.\: \right.
\
\
\displaystyle
\left.{{{positiveInteger \left({y}\right)}+{positiveInteger \left({x}\right)}+ \%I}\mbox{\rm = =}{{{{\tt'}assume}\left({{y + x}, \: positiveInteger}\right)}+ \%I}}, \right.
\
\
\displaystyle
\left.\: \right.
\
\
\displaystyle
\left.{{{positiveInteger \left({x}\right)}+{nonNegativeInteger \left({y}\right)}+ \%J}\mbox{\rm = =}{{{{\tt'}assume}\left({{y + x}, \: positiveInteger}\right)}+ \%J}}, \right.
\
\
\displaystyle
\left.\: \right.
\
\
\displaystyle
\left.{{{positiveInteger \left({x}\right)}+{nonZero \left({y}\right)}+ \%K}\mbox{\rm = =}{{{{\tt'}assume}\left({{y + x}, \: integer}\right)}+ \%K}}, \right.
\
\
\displaystyle
\left.\: \right.
\
\
\displaystyle
\left.{{{nonZero \left({y}\right)}+{nonZero \left({x}\right)}+ \%L}\mbox{\rm = =}{{{{\tt'}assume}\left({{y + x}, \: integer}\right)}+ \%L}}, \right.
\
\
\displaystyle
\left.\: \right.
\
\
\displaystyle
\left.{{\%M \ {integer \left({x}\right)}\ {integer \left({y}\right)}}\mbox{\rm = =}{\%M \ {{{\tt'}assume}\left({{x \  y}, \: integer}\right)}}}, \right.
\
\
\displaystyle
\left.\: \right.
\
\
\displaystyle
\left.{{\%N \ {integer \left({x}\right)}\ {nonNegativeInteger \left({y}\right)}}\mbox{\rm = =}{\%N \ {{{\tt'}assume}\left({{x \  y}, \: integer}\right)}}}, \right.
\
\
\displaystyle
\left.\: \right.
\
\
\displaystyle
\left.{{\%O \ {integer \left({x}\right)}\ {positiveInteger \left({y}\right)}}\mbox{\rm = =}{\%O \ {{{\tt'}assume}\left({{x \  y}, \: integer}\right)}}}, \right.
\
\
\displaystyle
\left.\: \right.
\
\
\displaystyle
\left.{{\%P \ {integer \left({x}\right)}\ {nonZero \left({y}\right)}}\mbox{\rm = =}{\%P \ {{{\tt'}assume}\left({{x \  y}, \: integer}\right)}}}, \right.
\
\
\displaystyle
\left.\: \right.
\
\
\displaystyle
\left.{{\%Q \ {nonNegativeInteger \left({x}\right)}\ {nonNegativeInteger \left({y}\right)}}\mbox{\rm = =}{\%Q \ {{{\tt'}assume}\left({{x \  y}, \: nonNegativeInteger}\right)}}}, \right.
\
\
\displaystyle
\left.\: \right.
\
\
\displaystyle
\left.{{\%R \ {nonNegativeInteger \left({x}\right)}\ {positiveInteger \left({y}\right)}}\mbox{\rm = =}{\%R \ {{{\tt'}assume}\left({{x \  y}, \: nonNegativeInteger}\right)}}}, \right.
\
\
\displaystyle
\left.\: \right.
\
\
\displaystyle
\left.{{\%S \ {nonNegativeInteger \left({x}\right)}\ {nonZero \left({y}\right)}}\mbox{\rm = =}{\%S \ {{{\tt'}assume}\left({{x \  y}, \: integer}\right)}}}, \right.
\
\
\displaystyle
\left.\: \right.
\
\
\displaystyle
\left.{{\%T \ {positiveInteger \left({x}\right)}\ {positiveInteger \left({y}\right)}}\mbox{\rm = =}{\%T \ {{{\tt'}assume}\left({{x \  y}, \: positiveInteger}\right)}}}, \right.
\
\
\displaystyle
\left.\: \right.
\
\
\displaystyle
\left.{{\%U \ {nonNegativeInteger \left({y}\right)}\ {positiveInteger \left({x}\right)}}\mbox{\rm = =}{\%U \ {{{\tt'}assume}\left({{x \  y}, \: nonNegativeInteger}\right)}}}, \right.
\
\
\displaystyle
\left.\: \right.
\
\
\displaystyle
\left.{{\%V \ {nonZero \left({y}\right)}\ {positiveInteger \left({x}\right)}}\mbox{\rm = =}{\%V \ {{{\tt'}assume}\left({{x \  y}, \: nonZero}\right)}}}, \right.
\
\
\displaystyle
\left.\: \right.
\
\
\displaystyle
\left.{{\%W \ {nonZero \left({x}\right)}\ {nonZero \left({y}\right)}}\mbox{\rm = =}{\%W \ {{{\tt'}assume}\left({{x \  y}, \: nonZero}\right)}}}\right\} (2)
Type: Ruleset(Integer,Integer,Expression(Integer))

Check if x is in t.

fricas
check(x:Expression Integer,t:Symbol):Boolean ==
  --output("check: ",x::OutputForm)$OutputPackage
  p := normalForm markConstants x
  e := equation(p, normalForm markConstants assume(p,t))
  --output e
  e
Function declaration check : (Expression(Integer),Symbol) -> Boolean has been added to workspace.
Type: Void

Simplification

fricas
-- conditions in rules need to be unary functions
int1 := (m:Expression Integer):Boolean+->check(m,'integer)
fricas
Compiling function markConstants with type Expression(Integer) -> 
      Expression(Integer)
fricas
Compiling function check with type (Expression(Integer),Symbol) -> 
      Boolean

\label{eq3}\mbox{theMap (...)}(3)
Type: (Expression(Integer) -> Boolean)
fricas
simplifyAssumming := rule
  -- trig rules
  sin((n|int1(n))*2*%pi) == 0
  cos((n|int1(n))*2*%pi) == 1

\label{eq4}\left\{{{\sin \left({2 \  n \  \pi}\right)}\mbox{\rm = =}0}, \:{{\cos \left({2 \  n \  \pi}\right)}\mbox{\rm = =}1}\right\}(4)
Type: Ruleset(Integer,Integer,Expression(Integer))

Tests

fricas
assume(x,'positiveInteger)

\label{eq5}positiveInteger \left({x}\right)(5)
Type: Expression(Integer)
fricas
normalForm %

\label{eq6}positiveInteger \left({x}\right)(6)
Type: Expression(Integer)
fricas
assume(x,'positiveInteger)+1

\label{eq7}{positiveInteger \left({x}\right)}+ 1(7)
Type: Expression(Integer)
fricas
normalForm markConstants %

\label{eq8}positiveInteger \left({x + 1}\right)(8)
Type: Expression(Integer)
fricas
assume(assume(x,'nonNegativeInteger),'positiveInteger)

\label{eq9}positiveInteger \left({nonNegativeInteger \left({x}\right)}\right)(9)
Type: Expression(Integer)
fricas
normalForm %

\label{eq10}positiveInteger \left({x}\right)(10)
Type: Expression(Integer)
fricas
check(assume(x,'positiveInteger),'positiveInteger)

\label{eq11} \mbox{\rm true} (11)
Type: Boolean
fricas
check(assume(x,'positiveInteger)+1,'positiveInteger)

\label{eq12} \mbox{\rm true} (12)
Type: Boolean
fricas
check(3,'positiveInteger)

\label{eq13} \mbox{\rm true} (13)
Type: Boolean
fricas
check(-3,'positiveInteger)

\label{eq14} \mbox{\rm false} (14)
Type: Boolean
fricas
check(0,'positiveInteger)

\label{eq15} \mbox{\rm false} (15)
Type: Boolean
fricas
--
assume(x,'nonNegativeInteger)

\label{eq16}nonNegativeInteger \left({x}\right)(16)
Type: Expression(Integer)
fricas
normalForm %

\label{eq17}nonNegativeInteger \left({x}\right)(17)
Type: Expression(Integer)
fricas
check(assume(x,'positiveInteger),'nonNegativeInteger)

\label{eq18} \mbox{\rm true} (18)
Type: Boolean
fricas
assume(x,'nonNegativeInteger)+1

\label{eq19}{nonNegativeInteger \left({x}\right)}+ 1(19)
Type: Expression(Integer)
fricas
normalForm markConstants %

\label{eq20}positiveInteger \left({x + 1}\right)(20)
Type: Expression(Integer)
fricas
assume(assume(x,'integer),'nonNegativeInteger)

\label{eq21}nonNegativeInteger \left({integer \left({x}\right)}\right)(21)
Type: Expression(Integer)
fricas
normalForm %

\label{eq22}nonNegativeInteger \left({x}\right)(22)
Type: Expression(Integer)
fricas
check(assume(x,'nonNegativeInteger),'nonNegativeInteger)

\label{eq23} \mbox{\rm true} (23)
Type: Boolean
fricas
check(assume(x,'nonNegativeInteger)+1,'nonNegativeInteger)

\label{eq24} \mbox{\rm true} (24)
Type: Boolean
fricas
check(3,'nonNegativeInteger)

\label{eq25} \mbox{\rm true} (25)
Type: Boolean
fricas
check(-3,'nonNegativeInteger)

\label{eq26} \mbox{\rm false} (26)
Type: Boolean
fricas
check(0,'nonNegativeInteger)

\label{eq27} \mbox{\rm true} (27)
Type: Boolean
fricas
--
assume(x,'integer)

\label{eq28}integer \left({x}\right)(28)
Type: Expression(Integer)
fricas
normalForm %

\label{eq29}integer \left({x}\right)(29)
Type: Expression(Integer)
fricas
check(assume(x,'positiveInteger),'integer)

\label{eq30} \mbox{\rm true} (30)
Type: Boolean
fricas
assume(x,'integer)+1

\label{eq31}{integer \left({x}\right)}+ 1(31)
Type: Expression(Integer)
fricas
normalForm markConstants %

\label{eq32}integer \left({x + 1}\right)(32)
Type: Expression(Integer)
fricas
assume(assume(x,'integer),'integer)

\label{eq33}integer \left({integer \left({x}\right)}\right)(33)
Type: Expression(Integer)
fricas
normalForm %

\label{eq34}integer \left({x}\right)(34)
Type: Expression(Integer)
fricas
check(assume(x,'integer),'integer)

\label{eq35} \mbox{\rm true} (35)
Type: Boolean
fricas
check(assume(x,'integer)+1,'integer)

\label{eq36} \mbox{\rm true} (36)
Type: Boolean
fricas
check(3,'integer)

\label{eq37} \mbox{\rm true} (37)
Type: Boolean
fricas
check(-3,'integer)

\label{eq38} \mbox{\rm true} (38)
Type: Boolean
fricas
check(0,'integer)

\label{eq39} \mbox{\rm true} (39)
Type: Boolean
fricas
--
simplifyAssumming sin(n*2*%pi)

\label{eq40}\sin \left({2 \  n \  \pi}\right)(40)
Type: Expression(Integer)
fricas
simplifyAssumming sin(assume(n,'integer)*2*%pi)

\label{eq41}0(41)
Type: Expression(Integer)

Dump domain cache

fricas
entries domainOfComp

\label{eq42}\left[ nonZero , \: positiveInteger , \: nonNegativeInteger , \: integer \right](42)
Type: List(BasicOperator)




  Subject:   Be Bold !!
  ( 13 subscribers )  
Please rate this page: