And "assume" system based on equational reasoning.
fricas
domains:=empty()$Table(Symbol,BasicOperator)
Type: Table(Symbol,
BasicOperator
?)
fricas
assume(x:Expression Integer,t:Symbol):Expression Integer ==
if not key?(t,domains) then domains.t := operator t
(domains.t) x
Function declaration assume : (Expression(Integer),Symbol) ->
Expression(Integer) has been added to workspace.
Type: Void
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
fricas
prove := rule
-- subtypes
assume(assume(x,'integer),'integer) == assume(x,'integer)
assume(assume(x,'nonNegativeInteger),'integer) == assume(x,'integer)
assume(assume(x,'positiveInteger),'integer) == assume(x,'integer)
assume(assume(x,'nonNegativeInteger),'nonNegativeInteger) == assume(x,'nonNegativeinteger)
assume(assume(x,'positiveInteger),'nonNegativeInteger) == assume(x,'nonNegativeInteger)
-- 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,'nonNegativeInteger) + assume(y,'nonNegativeInteger) == assume(x+y,'nonNegativeInteger)
assume(x,'nonNegativeInteger) + assume(y,'positiveInteger) == assume(x+y,'nonNegativeInteger)
assume(x,'positiveInteger)+assume(y,'positiveInteger) == assume(x+y,'positiveInteger)
assume(x,'positiveInteger)+assume(y,'nonNegativeInteger) == assume(x+y,'positiveInteger)
fricas
Compiling function assume with type (Expression(Integer),Symbol) ->
Expression(Integer)
Type: Ruleset(Integer,Integer,Expression(Integer))
fricas
check(x:Expression Integer,t:Symbol):Boolean ==
--k:=retractIfCan(prove markConstants x)@Union(Kernel Expression Integer,"failed")
--if k case Kernel Expression Integer then is?(k,t) else false
prove markConstants x = assume(x,t)
Function declaration check : (Expression(Integer),Symbol) -> Boolean
has been added to workspace.
Type: Void
fricas
assume(x,'positiveInteger)
Type: Expression(Integer)
fricas
prove %
Type: Expression(Integer)
fricas
assume(assume(x,'positiveInteger),'integer)
Type: Expression(Integer)
fricas
prove %
Type: Expression(Integer)
fricas
check(assume(x,'positiveInteger),'positiveInteger)
fricas
Compiling function markConstants with type Expression(Integer) ->
Expression(Integer)
fricas
Compiling function check with type (Expression(Integer),Symbol) ->
Boolean
Type: Boolean
fricas
check(assume(x,'positiveInteger)+1,'positiveInteger)
Type: Boolean
fricas
check(3,'positiveInteger)
Type: Boolean
fricas
domains
Type: Table(Symbol,
BasicOperator
?)