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)  (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)  (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
 (3)
Type: (Expression(Integer) -> Boolean)
fricas
simplifyAssumming := rule
-- trig rules
sin((n|int1(n))*2*%pi) == 0
cos((n|int1(n))*2*%pi) == 1
 (4)
Type: Ruleset(Integer,Integer,Expression(Integer))

Tests

fricas
assume(x,'positiveInteger)
 (5)
Type: Expression(Integer)
fricas
normalForm %
 (6)
Type: Expression(Integer)
fricas
assume(x,'positiveInteger)+1
 (7)
Type: Expression(Integer)
fricas
normalForm markConstants %
 (8)
Type: Expression(Integer)
fricas
assume(assume(x,'nonNegativeInteger),'positiveInteger)
 (9)
Type: Expression(Integer)
fricas
normalForm %
 (10)
Type: Expression(Integer)
fricas
check(assume(x,'positiveInteger),'positiveInteger)
 (11)
Type: Boolean
fricas
check(assume(x,'positiveInteger)+1,'positiveInteger)
 (12)
Type: Boolean
fricas
check(3,'positiveInteger)
 (13)
Type: Boolean
fricas
check(-3,'positiveInteger)
 (14)
Type: Boolean
fricas
check(0,'positiveInteger)
 (15)
Type: Boolean
fricas
--
assume(x,'nonNegativeInteger)
 (16)
Type: Expression(Integer)
fricas
normalForm %
 (17)
Type: Expression(Integer)
fricas
check(assume(x,'positiveInteger),'nonNegativeInteger)
 (18)
Type: Boolean
fricas
assume(x,'nonNegativeInteger)+1
 (19)
Type: Expression(Integer)
fricas
normalForm markConstants %
 (20)
Type: Expression(Integer)
fricas
assume(assume(x,'integer),'nonNegativeInteger)
 (21)
Type: Expression(Integer)
fricas
normalForm %
 (22)
Type: Expression(Integer)
fricas
check(assume(x,'nonNegativeInteger),'nonNegativeInteger)
 (23)
Type: Boolean
fricas
check(assume(x,'nonNegativeInteger)+1,'nonNegativeInteger)
 (24)
Type: Boolean
fricas
check(3,'nonNegativeInteger)
 (25)
Type: Boolean
fricas
check(-3,'nonNegativeInteger)
 (26)
Type: Boolean
fricas
check(0,'nonNegativeInteger)
 (27)
Type: Boolean
fricas
--
assume(x,'integer)
 (28)
Type: Expression(Integer)
fricas
normalForm %
 (29)
Type: Expression(Integer)
fricas
check(assume(x,'positiveInteger),'integer)
 (30)
Type: Boolean
fricas
assume(x,'integer)+1
 (31)
Type: Expression(Integer)
fricas
normalForm markConstants %
 (32)
Type: Expression(Integer)
fricas
assume(assume(x,'integer),'integer)
 (33)
Type: Expression(Integer)
fricas
normalForm %
 (34)
Type: Expression(Integer)
fricas
check(assume(x,'integer),'integer)
 (35)
Type: Boolean
fricas
check(assume(x,'integer)+1,'integer)
 (36)
Type: Boolean
fricas
check(3,'integer)
 (37)
Type: Boolean
fricas
check(-3,'integer)
 (38)
Type: Boolean
fricas
check(0,'integer)
 (39)
Type: Boolean
fricas
--
simplifyAssumming sin(n*2*%pi)
 (40)
Type: Expression(Integer)
fricas
simplifyAssumming sin(assume(n,'integer)*2*%pi)
 (41)
Type: Expression(Integer)

Dump domain cache

fricas
entries domainOfComp
 (42)
Type: List(BasicOperator?)

 Subject:   Be Bold !! ( 15 subscribers )