The Coq mailing list

["Serge D. Mechveliani" <mechvel AT botik.ru>]

Dear Coq people,

I have questions about algebraic library applications for Coq.

The `Contributions' section on the Coq homepage shows 

  Contribution: Algebra
  Authors  * L. Pottier  ...

Does there exist a in-formal description of this library?
-- a paper, a documentation manual -- with explanations.

Has it definition and computing in a  ResidueRing  (by an ideal) ?
If yes, then -- for what (commutative) Ring and Ideald has it?


Concerning 
  Proof of Buchberger's algorithm 
  Authors  * Lau'ry
           * Henrik Persson
:
does there exist a in-formal description of this library?
-- a paper, a documentation manual -- with explanations.

* Is it for the coefficient ring R being any Field?
* Can the user set  R = (Rational [x]) / (x^2 + 3)
  (the field generated by  squareRoot(-3))
  and then, apply GroebnerBasis for polynomials in  R[x,y,z] ?

Do there exist packages in Coq for  factoring polynomials  over
various coefficient rings?  (with proofs ?).

Generally, I am trying to find out: 
what is the current state of the practical verified programming 
(in Coq) in symbolic algebra?  

For example, there exist several rich algebra libraries (say,
Axiom, Maple, Mathematica, Sage). Has Coq a similar application 
library, which has both fast algorithms (practically working in 
Coq) and proofs?
The method library of Axiom is rather large. 
How much part of the above libraries method set is covered by 
the Coq contributions? (which part is with formal proofs?).

Please, copy the response to  
mechvel AT botik.ru
(I am not in the list).

Thank you in advance for explanation,

------
Sergei