Hi, I am a Software Engineer (mainly C++, Rust) currently started getting really interested in Formal Program Verification and interesting programming languages (like: Idris, Agda, ATS, HOL, Curry, Mercury and of course Coq etc…) and also proving Real Analysis theorems that I learned a while ago while I was studying at university a few years back but now by using a computer.
I myself really think that mathematical theorems should be organized in a manner like software libraries on computers and this is how I would like use them and work with right now while proving mathematical theorems.
Now, I want to ask: Is it really possible to use Coq alongside learning Real Analysis and Measure Theory and use it for proving important theorems in those fields? Real Analysis I already know quite well but I want to study it again using a book teaching it from the ground up that goes deeper into what I already learned and also I want to learn Measure Theory (I’ve already read about a quarter book on the subject).
Thanks, And if you have interesting links that deal with the subject please share with me.
Coq might not be the best tool for real analysis and measure theory and especially not if you’re new to it.
I would expect you would want to mostly reason synthetically with nonconstructive axioms. At the very least I expect you would want law of excluded middle.
Coq isn’t bad at classical math it’s just that nonconstructive axioms puts a dent into extracting your theorems to code. There’s ways to kind of work around this but it’s something to keep in mind.
There is usually no need to extract mathematical theorems so this is not an actual issue.
AFAIK, there are two main libraries developing real analysis in Coq:
Coquelicot based on Coq standard library, still maintained but doesn’t seem to be actively developed anymore, includes Riemann integral but not Lebesgue
Before diving into MC Analysis, I would recommend first being acquainted with MathComp, the best introduction to the library and its principles being the MathComp book
However, the fact that this is still an active research area today indeed seems to indicate that analysis is not such an easy field (well, it also means it’s an interesting subject ).
).