adamski/shiroindev
1
0
Fork 0
Code Issues Pull Requests Releases Wiki Activity

added findvalues function and better handling with non polynomial expressions and irrational numbers

Browse Source
This commit is contained in:
urojony 2020-04-28 09:52:08 +02:00
parent d192eac748
commit ee82c6c942
8 changed files with 13240 additions and 682 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

3055
.ipynb_checkpoints/examples-checkpoint.ipynb
View File

File diff suppressed because it is too large Load Diff

7072
.ipynb_checkpoints/sandbox-checkpoint.ipynb
View File

File diff suppressed because it is too large Load Diff

BIN
__pycache__/shiroindev.cpython-36.pyc Normal file
View File

Binary file not shown.

BIN
__pycache__/shiroindev.cpython-37.pyc
View File

Binary file not shown.

918
examples.ipynb
View File

File diff suppressed because it is too large Load Diff

2731
sandbox.ipynb
View File

File diff suppressed because it is too large Load Diff

144
shiroindev.py
View File

@ -1,13 +1,13 @@
from __future__ import (absolute_import, division, from __future__ import (absolute_import, division,
print_function, unicode_literals) print_function, unicode_literals)
import warnings,operator import warnings,operator
warnings.filterwarnings("ignore") warnings.filterwarnings("ignore")
#Seed is needed to select the weights in linprog function. #Seed is needed to select the weights in linprog function.
#None means that the seed is random. #None means that the seed is random.
class Empty: class Vars:
pass pass
sVars=Empty() sVars=Vars()
sVars.print=print sVars.display=print
sVars.seed=None sVars.seed=None
sVars.translation={} sVars.translation={}
translationList=['numerator:','denominator:','status:', translationList=['numerator:','denominator:','status:',
@ -24,9 +24,10 @@ translationList=['numerator:','denominator:','status:',
#Initialize english-english dictionary. #Initialize english-english dictionary.
for phrase in translationList: for phrase in translationList:
sVars.translation[phrase]=phrase sVars.translation[phrase]=phrase
from scipy.optimize import linprog from scipy.optimize import linprog,fmin
import random import random
from sympy import S,cancel,fraction,Pow,expand,solve,latex,oo from sympy import S,cancel,fraction,Pow,expand,solve,latex,oo,Poly,lambdify
from collections import Counter
import re import re
def _remzero(coef,fun): def _remzero(coef,fun):
#coef, fun represents an expression. #coef, fun represents an expression.
@ -72,6 +73,28 @@ def ssolve(formula,variables):
return result return result
def sstr(formula): def sstr(formula):
return str(formula).replace('**','^').replace('*','').replace(' ','') return str(formula).replace('**','^').replace('*','').replace(' ','')
def reducegens(formula):
pol=Poly(formula)
newgens={}
ind={}
for gen in pol.gens:
base,pw=_powr(gen)
coef,_=pw.as_coeff_mul()
ml=pw/coef
if base**ml in newgens:
newgens[base**ml]=gcd(newgens[base**ml],coef)
else:
newgens[base**ml]=coef
ind[base**ml]=S('tmp'+str(len(ind)))
for gen in pol.gens:
base,pw=_powr(gen)
coef,_=pw.as_coeff_mul()
ml=pw/coef
pol=pol.replace(gen,ind[base**ml]**(coef/newgens[base**ml]))
newpol=Poly(pol.as_expr())
for gen in newgens:
newpol=newpol.replace(ind[gen],gen**newgens[gen])
return newpol
def Sm(formula): def Sm(formula):
#Adds multiplication signs and sympifies a formula. #Adds multiplication signs and sympifies a formula.
#For example, Sm('(2x+y)(7+5xz)') -> S('(2*x+y)*(7+5*x*z)') #For example, Sm('(2x+y)(7+5xz)') -> S('(2*x+y)*(7+5*x*z)')
@ -88,14 +111,14 @@ def _input2fraction(formula,variables,values):
subst=[] subst=[]
for x,y in zip(variables,values): for x,y in zip(variables,values):
if y!=1: if y!=1:
sVars.print(sVars.translation['Substitute']+' $'+str(x)+'\\to '+slatex(S(y)*S(x))+'$') sVars.display(sVars.translation['Substitute']+' $'+str(x)+'\\to '+slatex(S(y)*S(x))+'$')
subst+=[(x,x*y)] subst+=[(x,x*y)]
formula=formula.subs(subst) formula=formula.subs(subst)
numerator,denominator=fractioncancel(formula) numerator,denominator=fractioncancel(formula)
sVars.print(sVars.translation['numerator:']+' $'+slatex(numerator)+'$') sVars.display(sVars.translation['numerator:']+' $'+slatex(numerator)+'$')
sVars.print(sVars.translation['denominator:']+' $'+slatex(denominator)+'$') sVars.display(sVars.translation['denominator:']+' $'+slatex(denominator)+'$')
return (numerator,denominator) return (numerator,denominator)
def _formula2list(formula,variables): def _formula2list(formula):
#Splits a polynomial to a difference of two polynomials with positive #Splits a polynomial to a difference of two polynomials with positive
#coefficients and extracts coefficients and powers of both polynomials. #coefficients and extracts coefficients and powers of both polynomials.
#'variables' is used to set order of powers #'variables' is used to set order of powers
@ -103,30 +126,13 @@ def _formula2list(formula,variables):
#the program tries to prove that #the program tries to prove that
#0<=5x^2-4xy+8y^3 #0<=5x^2-4xy+8y^3
#4xy<=5x^2+8y^3 #4xy<=5x^2+8y^3
#lcoef=[4] #returns [4],[(1,1)], [5,8],[(2,0),(0,3)], (x,y)
#lfun=[[1,1]] formula=reducegens(formula)
#rcoef=[5,8] neg=(formula.abs()-formula)/2
#rfun=[[2,0],[0,3]] pos=(formula.abs()+formula)/2
lfun=[] neg=Poly(neg,gens=formula.gens)
lcoef=[] pos=Poly(pos,gens=formula.gens)
rfun=[] return neg.coeffs(),neg.monoms(),pos.coeffs(),pos.monoms(),Poly(formula).gens
rcoef=[]
varorder=dict(zip(variables,range(len(variables))))
for addend in formula.as_ordered_terms():
coef,facts=addend.as_coeff_mul()
powers=[0]*len(variables)
for var in variables:
powers[varorder[var]]=0
for fact in facts:
var,pw=_powr(fact)
powers[varorder[var]]=int(pw)
if(coef<0):
lcoef+=[-coef]
lfun+=[powers]
else:
rcoef+=[coef]
rfun+=[powers]
return(lcoef,lfun,rcoef,rfun)
def _list2proof(lcoef,lfun,rcoef,rfun,variables,itermax,linprogiter,_writ2=_writ2,theorem="From weighted AM-GM inequality:"): def _list2proof(lcoef,lfun,rcoef,rfun,variables,itermax,linprogiter,_writ2=_writ2,theorem="From weighted AM-GM inequality:"):
#Now the formula is splitted on two polynomials with positive coefficients. #Now the formula is splitted on two polynomials with positive coefficients.
#we will call them LHS and RHS and our inequality to prove would #we will call them LHS and RHS and our inequality to prove would
@ -157,13 +163,15 @@ def _list2proof(lcoef,lfun,rcoef,rfun,variables,itermax,linprogiter,_writ2=_writ
#If LHS is empty, then break. #If LHS is empty, then break.
localseed=sVars.seed localseed=sVars.seed
bufer=[] bufer=[]
lcoef,lfun=_remzero(lcoef,lfun)
rcoef,rfun=_remzero(rcoef,rfun)
itern=0 itern=0
if len(lcoef)==0: #if LHS is empty if len(lcoef)==0: #if LHS is empty
sVars.print(sVars.translation['status:']+' 0') sVars.display(sVars.translation['status:']+' 0')
status=0 status=0
elif len(rcoef)==0: elif len(rcoef)==0:
#if RHS is empty, but LHS is not #if RHS is empty, but LHS is not
sVars.print(sVars.translation['status:']+' 2') sVars.display(sVars.translation['status:']+' 2')
status=2 status=2
itermax=0 itermax=0
foundreal=0 foundreal=0
@ -200,9 +208,9 @@ def _list2proof(lcoef,lfun,rcoef,rfun,variables,itermax,linprogiter,_writ2=_writ
res=linprog(vecc,A_eq=A,b_eq=b,A_ub=A_ub,b_ub=b_ub,options={'maxiter':linprogiter}) res=linprog(vecc,A_eq=A,b_eq=b,A_ub=A_ub,b_ub=b_ub,options={'maxiter':linprogiter})
status=res.status status=res.status
if itern==1: if itern==1:
sVars.print(sVars.translation['status:']+' '+str(status)) sVars.display(sVars.translation['status:']+' '+str(status))
if status==0: if status==0:
sVars.print(sVars.translation[theorem]) sVars.display(sVars.translation[theorem])
if status==2: #if real solution of current inequality doesn't exist if status==2: #if real solution of current inequality doesn't exist
if foundreal==0: #if this is the first inequality, then break if foundreal==0: #if this is the first inequality, then break
break break
@ -214,7 +222,7 @@ def _list2proof(lcoef,lfun,rcoef,rfun,variables,itermax,linprogiter,_writ2=_writ
continue continue
if status==0:#if found a solution with real coefficients if status==0:#if found a solution with real coefficients
for ineq in bufer: for ineq in bufer:
sVars.print(ineq) sVars.display(ineq)
foundreal=1 foundreal=1
bufer=[] bufer=[]
oldlfun,oldrfun=lfun,rfun oldlfun,oldrfun=lfun,rfun
@ -246,25 +254,25 @@ def _list2proof(lcoef,lfun,rcoef,rfun,variables,itermax,linprogiter,_writ2=_writ
lcoef,lfun=_remzero(lcoef,lfun) lcoef,lfun=_remzero(lcoef,lfun)
rcoef,rfun=_remzero(rcoef,rfun) rcoef,rfun=_remzero(rcoef,rfun)
for ineq in bufer: for ineq in bufer:
sVars.print(ineq) sVars.display(ineq)
lhs='+'.join([_writ2(c,f,variables) for c,f in zip(lcoef,lfun)]) lhs='+'.join([_writ2(c,f,variables) for c,f in zip(lcoef,lfun)])
if lhs=='': if lhs=='':
lhs='0' lhs='0'
elif status==0: elif status==0:
sVars.print(sVars.translation[ sVars.display(sVars.translation[
"Program couldn't find a solution with integer coefficients. Try "+ "Program couldn't find a solution with integer coefficients. Try "+
"to multiple the formula by some integer and run this function again."]) "to multiple the formula by some integer and run this function again."])
elif(status==2): elif(status==2):
sVars.print(sVars.translation["Program couldn't find any proof."]) sVars.display(sVars.translation["Program couldn't find any proof."])
#return res.status #return res.status
elif status==1: elif status==1:
sVars.print(sVars.translation["Try to set higher linprogiter parameter."]) sVars.display(sVars.translation["Try to set higher linprogiter parameter."])
rhs='+'.join([_writ2(c,f,variables) for c,f in zip(rcoef,rfun)]) rhs='+'.join([_writ2(c,f,variables) for c,f in zip(rcoef,rfun)])
if rhs=='': if rhs=='':
rhs='0' rhs='0'
sVars.print('$$ '+slatex(lhs)+' \\le '+slatex(rhs)+' $$') sVars.display('$$ '+slatex(lhs)+' \\le '+slatex(rhs)+' $$')
if lhs=='0': if lhs=='0':
sVars.print(sVars.translation['The sum of all inequalities gives us a proof of the inequality.']) sVars.display(sVars.translation['The sum of all inequalities gives us a proof of the inequality.'])
return status return status
def _isiterable(obj): def _isiterable(obj):
try: try:
@ -290,13 +298,13 @@ def prove(formula,values=None,variables=None,niter=200,linprogiter=10000):
if values: values=_smakeiterable(values) if values: values=_smakeiterable(values)
else: values=[1]*len(variables) else: values=[1]*len(variables)
num,den=_input2fraction(formula,variables,values) num,den=_input2fraction(formula,variables,values)
st=_list2proof(*(_formula2list(num,variables)+(variables,niter,linprogiter))) st=_list2proof(*(_formula2list(num)+(niter,linprogiter)))
if st==2 and issymetric(num): if st==2 and issymetric(num):
fs=sorted([str(x) for x in num.free_symbols]) fs=sorted([str(x) for x in num.free_symbols])
sVars.print(sVars.translation["It looks like the formula is symmetric. "+ sVars.display(sVars.translation["It looks like the formula is symmetric. "+
"You can assume without loss of generality that "]+ "You can assume without loss of generality that "]+
' >= '.join([str(x) for x in fs])+'. '+sVars.translation['Try']) ' >= '.join([str(x) for x in fs])+'. '+sVars.translation['Try'])
sVars.print('prove(makesubs(S("'+str(num)+'"),'+ sVars.display('prove(makesubs(S("'+str(num)+'"),'+
str([(str(x),'oo') for x in variables[1:]])+')') str([(str(x),'oo') for x in variables[1:]])+')')
return st return st
def powerprove(formula,values=None,variables=None,niter=200,linprogiter=10000): def powerprove(formula,values=None,variables=None,niter=200,linprogiter=10000):
@ -309,10 +317,11 @@ def powerprove(formula,values=None,variables=None,niter=200,linprogiter=10000):
else: values=[1]*len(variables) else: values=[1]*len(variables)
num,den=_input2fraction(formula,variables,values) num,den=_input2fraction(formula,variables,values)
subst2=[] subst2=[]
statusses=[]
for j in range(len(variables)): for j in range(len(variables)):
subst2+=[(variables[j],1+variables[j])] subst2+=[(variables[j],1+variables[j])]
for i in range(1<<len(variables)): #tricky substitutions to improve speed for i in range(1<<len(variables)): #tricky substitutions to improve speed
sVars.print('\n\\hline\n') sVars.display('\n\\hline\n')
subst1=[] subst1=[]
substout=[] substout=[]
for j in range(len(variables)): for j in range(len(variables)):
@ -321,11 +330,12 @@ def powerprove(formula,values=None,variables=None,niter=200,linprogiter=10000):
substout+=[str(variables[j])+'\\to 1/(1+'+str(variables[j])+')'] substout+=[str(variables[j])+'\\to 1/(1+'+str(variables[j])+')']
else: else:
substout+=[str(variables[j])+'\\to 1+'+str(variables[j])] substout+=[str(variables[j])+'\\to 1+'+str(variables[j])]
sVars.print(sVars.translation['Substitute']+ ' $'+','.join(substout)+'$') sVars.display(sVars.translation['Substitute']+ ' $'+','.join(substout)+'$')
num1=fractioncancel(num.subs(subst1))[0] num1=fractioncancel(num.subs(subst1))[0]
num2=expand(num1.subs(subst2)) num2=expand(num1.subs(subst2))
sVars.print(sVars.translation["Numerator after substitutions:"]+' $'+slatex(num2)+'$') sVars.display(sVars.translation["Numerator after substitutions:"]+' $'+slatex(num2)+'$')
_list2proof(*(_formula2list(num2,variables)+(variables,niter,linprogiter))) statusses+=[_list2proof(*(_formula2list(num2)+(niter,linprogiter)))]
return Counter(statusses)
def makesubs(formula,intervals,values=None,variables=None,numden=False): def makesubs(formula,intervals,values=None,variables=None,numden=False):
#This function generates a new formula which satisfies this condition: #This function generates a new formula which satisfies this condition:
#for all positive variables new formula is nonnegative iff #for all positive variables new formula is nonnegative iff
@ -346,18 +356,18 @@ def makesubs(formula,intervals,values=None,variables=None,numden=False):
if {end1,end2}=={S('-oo'),S('oo')}: if {end1,end2}=={S('-oo'),S('oo')}:
formula=formula.subs(var,var-1/var) formula=formula.subs(var,var-1/var)
equations=[equation.subs(var,var-1/var) for equation in equations] equations=[equation.subs(var,var-1/var) for equation in equations]
sVars.print(sVars.translation['Substitute']+' $'+str(var)+'\\to '+var-1/var+'$') sVars.display(sVars.translation['Substitute']+' $'+str(var)+'\\to '+sstr(var-1/var)+'$')
elif end2==S('oo'): elif end2==S('oo'):
formula=formula.subs(var,end1+var) formula=formula.subs(var,end1+var)
equations=[equation.subs(var,end1+var) for equation in equations] equations=[equation.subs(var,end1+var) for equation in equations]
sVars.print(sVars.translation['Substitute']+' $'+str(var)+'\\to '+sstr(end1+var)+'$') sVars.display(sVars.translation['Substitute']+' $'+str(var)+'\\to '+sstr(end1+var)+'$')
elif end2==S('-oo'): elif end2==S('-oo'):
formula=formula.subs(var,end1-var) formula=formula.subs(var,end1-var)
equations=[equation.subs(var,end1-var) for equation in equations] equations=[equation.subs(var,end1-var) for equation in equations]
sVars.print(sVars.translation['Substitute']+" $"+str(var)+'\\to '+sstr(end1-var)+'$') sVars.display(sVars.translation['Substitute']+" $"+str(var)+'\\to '+sstr(end1-var)+'$')
else: else:
formula=formula.subs(var,end2+(end1-end2)/var) formula=formula.subs(var,end2+(end1-end2)/var)
sVars.print(sVars.translation['Substitute']+" $"+str(var)+'\\to '+sstr(end2+(end1-end2)/(1+var))+'$') sVars.display(sVars.translation['Substitute']+" $"+str(var)+'\\to '+sstr(end2+(end1-end2)/(1+var))+'$')
equations=[equation.subs(var,end2+(end1-end2)/var) for equation in equations] equations=[equation.subs(var,end2+(end1-end2)/var) for equation in equations]
num,den=fractioncancel(formula) num,den=fractioncancel(formula)
for var,interval in zip(variables,intervals): for var,interval in zip(variables,intervals):
@ -370,7 +380,7 @@ def makesubs(formula,intervals,values=None,variables=None,numden=False):
if len(values): if len(values):
values=values[0] values=values[0]
num,den=expand(num),expand(den) num,den=expand(num),expand(den)
#sVars.print(sVars.translation["Formula after substitution:"],"$$",slatex(num/den),'$$') #sVars.display(sVars.translation["Formula after substitution:"],"$$",slatex(num/den),'$$')
if values and numden: if values and numden:
return num,den,values return num,den,values
elif values: elif values:
@ -395,7 +405,7 @@ def _formula2listf(formula):
else: else:
rcoef+=[coef] rcoef+=[coef]
rfun+=[facts[0].args] rfun+=[facts[0].args]
return(lcoef,lfun,rcoef,rfun) return(lcoef,lfun,rcoef,rfun,None)
def provef(formula,niter=200,linprogiter=10000): def provef(formula,niter=200,linprogiter=10000):
#this function is similar to prove, formula is a linear combination of #this function is similar to prove, formula is a linear combination of
#values of f:R^k->R instead of a polynomial. provef checks if a formula #values of f:R^k->R instead of a polynomial. provef checks if a formula
@ -403,7 +413,7 @@ def provef(formula,niter=200,linprogiter=10000):
#provides a proof of nonnegativity. #provides a proof of nonnegativity.
formula=S(formula) formula=S(formula)
num,den=_input2fraction(formula,[],[]) num,den=_input2fraction(formula,[],[])
_list2proof(*(_formula2listf(num)+(None,niter,linprogiter,_writ,'From Jensen inequality:'))) return _list2proof(*(_formula2listf(num)+(niter,linprogiter,_writ,'From Jensen inequality:')))
def issymetric(formula): #checks if formula is symmetric def issymetric(formula): #checks if formula is symmetric
#and has at least two variables #and has at least two variables
if len(formula.free_symbols)<2: if len(formula.free_symbols)<2:
@ -447,3 +457,19 @@ def symmetrize(formula,oper=operator.add,variables=None,init=None):
for i in range(1,len(variables)): for i in range(1,len(variables)):
formula=cyclize(formula,oper,variables[:i+1]) formula=cyclize(formula,oper,variables[:i+1])
return formula return formula
def findvalues(formula,values=None,variables=None):
formula=S(formula)
num,den=fractioncancel(formula)
if variables==None:
variables=sorted(num.free_symbols,key=str)
num=num.subs(zip(variables,list(map(lambda x:x**2,variables))))
num=Poly(num)
newformula=S((num.abs()+num)/(num.abs()-num))
f=lambdify(variables,newformula)
f2=lambda x:f(*x)
if values==None:
values=[1.0]*len(variables)
else:
values=S(values)
tup=tuple(fmin(f2,values))
return tuple([x*x for x in tup])

BIN
shiroindev.pyc Normal file
View File

Binary file not shown.