coq-club AT inria.fr

Subject: The Coq mailing list

List archive

Re: [Coq-Club] Interacting between Coquelicot and mathcomp

From: Mohit Tekriwal <tmohit AT umich.edu>
To: coq-club AT inria.fr
Cc: Jean-Baptiste Jeannin <jeannin AT umich.edu>
Subject: Re: [Coq-Club] Interacting between Coquelicot and mathcomp
Date: Thu, 6 May 2021 07:49:34 +0530
Authentication-results: mail2-smtp-roc.national.inria.fr; spf=None smtp.pra=tmohit AT umich.edu; spf=Pass smtp.mailfrom=tmohit AT umich.edu; spf=None smtp.helo=postmaster AT mail-pf1-f169.google.com
Ironport-hdrordr: A9a23:Fepl1a5Vt20pfrUoQQPXwY2BI+orLtY04lQ7vn1ZYxpTb8CeioSFmfwAz3bP+VEscVsnns2NP7TFfGPE+fdOkOwsFJqBfC2jgmunK4l+8ZDvqgeKcRHW2+ZB2c5bE5RWJ9H9AFNzh8S/wCTQKada/PCp66at7N2w815MSRhtcLxp6A10YzzrdHFeYCljKd4HGIGH5sxBzgDQG0g/SsigHHEKU6ziirTw5fHbSCccBxg96BSf5AnYkYLSKBST0hcAXz4n+95LzUH+jwf76q+/2svb9jbg1nTe55kTpd35ytErPqGxo/USQw+Dti+YIKBoW7iPp1kO0YWSwWdvtNnJrzEEE61ImgvsV1DwmzfWny/9zTgp63jtoGXo+0fLvM3jSDo2T8pHiI5JGyG013Yd
Ironport-phdr: A9a23:y5mIxR0ojkm009gSsmDO/wMyDhhPgJ3EezUN459isYplN5qZl7zcNUDSrc9gkEXOFd2Cra4d2qyM6PCrADdcqb+681k6OKRWUBEEjchE1ycBO+WiTXPBEfjxciYhF95DXlI2t1uyMExSBdqsLwaK+i764jEdAAjwOhRoLerpBIHSk9631+ev8JHPfglEnjWwba52IRmsswncuMobjYR/Jqs/xRbCv2dFdflRyW50P1yYggzy5t23/J5t8iRQv+wu+stdWqjkfKo2UKJVAi0+P286+MPkux/DTRCS5nQHSWUZjgBIAwne4x7kWJr6rzb3ufB82CmeOs32UKw0VDG/5KplVBPklCEKPCMi/WrJlsJ/kr5UoBO5pxx+3YHUZp2VNOFjda/ZZN8WWHZNUtpUWyFHH4iybZYAD/AZMOlEoIbzulsAohmwCwejB+3vxCFGiHjt0K0myuQhFB3K3Aw8E94QtnnfsdX7NL0VUeCw1KTGyjLDb/NX2Tfh9YPGbA4uofKWXbJxf8ve000vHB7Cg1WMrIzlODOV1uURs2WA8upgUOOvhHInqw1rvDeg29osh5DPi4kIxV/K6T93z5wpJd2kVkF7e9ikHYNMuyybN4V7Q98vTnxmtionybAIuZ+2cigIxZoo2xLSZP+KfYiK7x/nVeufLjR1iXF4dL+/iBu/7Eetx+3gWsS71ltBsyRLkt7Jtn8X1hzT7NCKSvR8/ke92TaPyhvc5vtYLkAzkKrWLYMqzL0olpcLr0jPAiv7lF/1gaKWbEko5PWk5/j9brn7p5KRM5d4hh/xP6gymsGyBPo0PhQTU2We4+uwyKHv8VP8TbhOjPA7nazUvI3GKskfoqO0BhFZ3po95xuxCjqqzsgUkmMdI19Adh+Ki4jkNlDILfvlF/mwmU6sny1ux/3ePr3uHJHNLn/bnbfkZ7l96kpcxBMrzdBR+p5YE78BLO/yV0L1rtDYARg5Mwu7w+bjFtpxzJ8RWWWKAqOBMaPSt0GH5v43LuWSeIMYvCzxJvsl6vL0k3M1hEMRcbO00ZYWbH20BvFmLF+YYXrojNcBC2AKvg8mQez2jV2CVj5TZ3euX68n+zE7DYOmApvDRoy3nrOOwTq7EoVMZm9aElCMDWvod4KcVvgQbyKSO9ZtnSAAVbi8UIAszgqutQ//y7p/NOXY4CwYtZT51Nh0/eLfjx8y9SYnR/iahmqKViR/mn4Cbz4wxqF250JnmXmZ1q0tpvtYFMAb2/5KSAYlPJqUm/B/DNDzRirce9aCSBCrTsjwUmJ5dc4439JbOxU1IN6llB2WmnPyW9c9p/mwHJUxt5nk8T3xKsJ6o17D3aglykEoG45BbDP3wKF48AfXCsjClEDLz86CReEnxCfIsVy74y+LtUBcXhR3VM3tQHUebUuQoNjktBqqZ4/rMqwuN0568eDHMrFDAvX0iFRNRLHuNMmMOwqM

Thanks Christian !

> On May 5, 2021, at 10:57 PM, Christian Doczkal <christian.doczkal AT inria.fr>
> wrote:
>
> Hi,
>
> I don't know about Coquelicot, but note that there is also math-
> comp/analysis (https://github.com/math-comp/analysis/), which may well
> have most of the things you mention and is designed to be used together
> with mathcomp.
>
> Best,
> Christian
>
> On Wed, 2021-05-05 at 20:26 +0530, 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.
>

[Coq-Club] Interacting between Coquelicot and mathcomp, Mohit Tekriwal, 05/05/2021
- Re: [Coq-Club] Interacting between Coquelicot and mathcomp, Christian Doczkal, 05/05/2021
  - Re: [Coq-Club] Interacting between Coquelicot and mathcomp, Mohit Tekriwal, 05/06/2021
- Re: [Coq-Club] Interacting between Coquelicot and mathcomp, Laurence Rideau, 05/05/2021