Does there exist any work on creating a Real Number/Probability Theory Framework in COQ?

Question

COQ is an interactive theorem prover that uses the calculus of inductive constructions, i.e. it relies heavily on inductive types. Using those, discrete structures like natural numbers, rational numbers, graphs, grammars, semantics etc. are very concisely represented.

However, since I grew to like the proof assistant, I was wondering whether there are libraries for uncountable structures, like real numbers, complex numbers, probability bounds and such. I am of course aware that one cannot define these structures inductively (at least not as far as I know), but they can be defined axiomatically, using for instance the axiomatic approach.

Is there any work that provides basic properties, or even probabilistic bounds like Chernoff bound or union bound as a library?

Answer 1

The standard library of Coq has a section about real numbers. These are the classical real numbers, using the Dedekind completion. There are also results about complex numbers, I suppose there are several libraries, I happen to know this one. Note that there is also a lot of results for constructive real and complex numbers, C-CoRN is the reference.

Side note: you could also define (computable) real numbers inductively with some of the constructive axiomatics, for example using rational numbers from the Cauchy sequences or some constructive version of the least-upper-bound property. I am not sure how much inductive that this.

I know there are some people working on probabilities with Coq. Unfortunately I am not sure how advanced their works are. My guess is that there is likely no such specific result about Chernoff bound or union bound. (But it's just a guess)

Answer 2

Check this out! http://coq.io/opam/coq-markov.8.5.0.html. A library for Markov's inequality built on mathematical probability theory.