Skip to content

roglo/puiseuxth

Folders and files

NameName
Last commit message
Last commit date

Latest commit

 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 

Repository files navigation

OVERVIEW

* Formal proof of Puiseux's theorem
* Computation of roots of polynomials of Puiseux's series

You need coq version 8.14.1

PROOF

If you are only interested on the proof, you can just do:
   cd coq; make

and ignore the rest of this README.

EVERYTHING

Otherwise, everything can be done by typing at top:
       make

Faster compilation with option -j of make. E.g. "make -j4"

If this command "make" does not work, try reading the sections PROOF
(coq proof) and PROGRAM (ocaml program) below. They are independent.

PROGRAM

You need ocaml, its library num, camlp5, library mfpr (dev) to compile
(under Debian, it is the package libmpfr-def). Do:
        cd cpoly; make; cd ..
        cd ocaml; make; cd ..

This creates the executable named "puiseux".
Also building of a library function computing float complex roots of
any polynomial. See in directory 'cpoly' for details.

LIBRARY

The directory 'cpoly' contains an ocaml translation of CPOLY.F, a
well-known Fortran function that computes the float complex roots
of any polynomial

PROOF

Do:
        cd coq; make

EXAMPLES OF THE PROGRAM

Warning: your terminal must be utf-8.

-- Robert J. Walker, "Algebraic Curves"
./puiseux '(-x3+x4)-2x2y-xy2+2xy4+y5'
./puiseux 'x4-x3y+3x2y3-3xy5+y7'
./puiseux '2x5-x3y+2x2y2-xy3+2y5'
./puiseux '(x2+4x3+6x4)-4x4y+(-2x-4x2-2x3)y2+y4'

-- Xavier Caruso
./puiseux -y X 't2X6+6t2X5+(8t3-2t2+t)X3+(7t4-t2-2t)X2+(8t3-3t)X-t8+t3'

-- Franz Winkler
./puiseux 'y5-4y4+4y3+2x2y2-xy2+2x2y+2xy+x4+x3'
./puiseux 'y2-x3+2x2-x'

-- Adrien Poteaux
./puiseux -y X '(Y3-X)((Y-1)^2-X)(Y-2-X2)-X2Y5'

-- Nicholas J. Willis, "Newton-Puiseux Algorithm" thesis
./puiseux '2x5-x3y+2x2y2-xy3+2y5'
./puiseux 'y4-(2x3+2x2)y2+(x6+2x5+x4)'
./puiseux 'y4-2x3y2-2x2y2+x6+2x5+x4'
./puiseux ' -x3+x4-2x2y-xy2+2xy4+y5'
./puiseux 'x2+xy+y2+x+y'                #1
./puiseux 'x2+xy+y2+y'
./puiseux 'x2+xy+y2+x'
./puiseux 'x2+4xy+y2'
./puiseux 'x2+xy+y2'                    #5
./puiseux 'x2+2xy+y2'
./puiseux 'x3+x2y+xy2+y3+x2+xy+y2+x+y'
./puiseux 'x3+x2y+xy2+y3+x2+xy+y2+y'
./puiseux 'x3+x2y+xy2+y3+x2+xy+y2+x'
./puiseux 'x3+x2y+xy2+y3+x2'            #10
./puiseux 'x3+x2y+xy2+y3+y2'
./puiseux 'x3+x2y+xy2+y3+x2+xy'
./puiseux 'x3+x2y+xy2+y3+xy+y2'
./puiseux 'x3+x2y+xy2+y3+xy'
./puiseux 'x3+x2y+xy2+y3+xy+y'          #15
./puiseux 'x3+x2y+xy2+y3+xy+x'
./puiseux 'yx2-y3'
./puiseux 'x3+x2y+xy2+y3'
./puiseux 'yx2-2xy2+y3'
./puiseux 'x3-3yx2+3xy2-y3'             #20
./puiseux 'x3+x2y+xy2+y3+x2+4xy+y2'
./puiseux 'x3+x2y+xy2+y3+x2+xy+y2'
./puiseux 'x3+x2y+xy2+y3+x2+2xy+y2'
./puiseux 'x3+x2y+xy2+y3+x2+4xy+4y2'
./puiseux 'x4+x3y+x2y2+xy3+y4+x+y'      #25
./puiseux 'x4+x3y+x2y2+xy3+y4+x2+y'
./puiseux 'x4+x3y+x2y2+xy3+y4+x+y2'
./puiseux 'x4+x3y+x2y2+xy3+y4+x3+y'
./puiseux 'x4+x3y+x2y2+xy3+y4+y3+x'
./puiseux 'x4+x3y+x2y2+xy3+y4+y3+x2'    #30

About

Formal proof in Coq of Puiseux's Theorem.

Resources

License

Stars

Watchers

Forks

Releases

No releases published

Packages

No packages published

Languages