Dear Coq developers,
I suspect that this question is asked quite frequently, but I cannot find it easily.
Is there currently one library (or some libraries) that formalizes a bunch of undergraduate mathematical results?
A good example of the kind of things I would be interested in would be a library allowing to formalize answers to exercises given during first years of University (for instance those exercises https://www.concours-commun-inp.fr/_resource/annales%20oraux/MP/2024/banque%20finale%20avec%20corr%20session%202024_avril.pdf (this sadly is in French. I am quite convinced that equivalent list exists in English, but being French, finding this list was much easier for me)).
Faithfully yours,
Guillaume
There are multiple libraries with mathematical results. The most complete one is probably MathComp and MathComp Analysis. You can learn about Coq and MathComp in the MathComp Book.
Dear Pierre,
Thanks a lot for your answer.
Indeed, mathcomp looks to be the more complete library, and I had a look at it before even asking the question here.
Sadly, I feel that I am unable to know if a notion is defined in it or not.
Let me take an example, question 1 of exercise 1 of previously linked document.
Translated to English, it is:
Let E be the vectorial space of continuous functions from [0, 1] to R.
We define : ∀f ∈ E, ||f||_∞ = sup_{t∈[0,1]} |f(t)|
and ||f||_1 =\int_{0}^{1} |f(t)|dt.
1. Are norms || ||_∞ and || ||_1 equivalent? Justify.
Such a question requires a lot of notions, “vector space”, “closed intervals of reals”, “continuous functions”, “normed vector space”, “equivalent norms”.
- For vector space and continuous functions, I think I found it.
- But for “normed vector space” and “equivalent norms”, I found a module called
normedtype Module mathcomp.analysis.normedtype. Reading the header of this module was not enough for me to know if it contains the notion I am looking for.
What is the good strategy to know what is implemented in mathcomp?