The Coq mailing list

[Mohit Tekriwal <tmohit AT umich.edu>]

Hi Laurence,

Thanks again for the pointer. I have been able to use the Rstruct file to navigate between mathcomp and Coquelicot real analysis. I have also been looking at the complex numbers. I am trying to use an earlier development of Jordan canonical forms which uses algebraically closed field types for a project on numerical analysis.  I noticed there are compatibility files (Cstruct.v and Canalysis.v) for complex numbers as well which blends well with the Coquelicot analysis for the transcendence project. I tried to compile the files but I am facing compatibility issues with the latest version of Coq/mathcomp. The files have been developed using earlier versions of Coq, mathcomp and Coquelicot. However, I am using Coq 8.12.0, mathcomp 1.12.0, Coquelicot 3.3.0.

 I wanted to know if the files from transcendence project have been already been adapted with the new versions of Coq/mathcomp, or do they require porting ? 

Looking forward to your reply.

Thanking you,

Mohit Tekriwal

On May 6, 2021, at 1:43 AM, Laurence Rideau <Laurence.Rideau AT inria.fr> wrote:

Hello, some years ago , we proved with Sophie Bernard the transcendence of e and pi using mathcomp (for the algebraic part ) and Coquelicot (for analysis), the code  can be found here:

http://www-sop.inria.fr/members/Laurence.Rideau/transcendence.tar.gz

It has been publied in

Formal Proofs of Transcendence for e and pi as an Application of Multivariate and Symmetric Polynomials Certified Programs and Proofs (CPP'16) (2016), ACM. (open archive version)

On the other hand, as Christian said , using mathcomp analysis could a more modern way to formalise this kind of mathematics.

Best

Laurence

On 05/05/2021 16:56, Mohit Tekriwal wrote:

Hello,

I wanted to know if there is any work on interaction between Coquelicot and mathcomp libraries. I know that mathcomp has a rich  formalization of linear algebra. Coquelicot on the other hand has a rich formalization of reals and other analysis of real valued functions like limits, derivatives, integrals etc. If I were to define a real valued matrix in mathcomp and be able to leverage the Coquelicot formalization of reals for analysis, 
how would I go about doing that ? Are there any existing work, I can refer to ?

Thanking you,
Mohit Tekriwal,
PhD candidate, 
University of Michigan.