README

OVERVIEW

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

You need Rocq version 9.0.0

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