coq-proba
coq-proba copied to clipboard
A Probability Theory Library for the Coq Theorem Prover
Building
For dependencies see the coq-proba.opam file. The following configuration is known to work (listed by opam package name and version)
- coq 8.15.2
- coq-bignums 8.15.0
- coq-coquelicot 3.2.0
- coq-flocq 4.1.0
- coq-interval 4.5.2
- coq-mathcomp-ssreflect 1.15.0
- coq-stdpp 1.8.0
We have not tested compilation under other configurations.
You can install dependencies by running make build-dep
. Proof scripts should
then build by simply typing make
.
HTML Outline of Files
The file readme.html contains an outline of the paper by section with
links to important lemmas and definitions that are mentioned in the
paper. The CoqDoc html that it links to should be distributed as part
of the supplementary material distribution, but it may have been deleted
if you issued a command line "make clean". To rebuild it, please run
make html
.
Plaintext Guide to Files
All source files are in the subdirectory theories/, so all the paths we will quote are with respect to that.
-
basic/ -- Some miscellaneous files that do not really belong anywhere else: extensions to the ssreflect bigop library, tactics for converting between ssreflect nats and standard library nats, etc.
-
prob/ -- Basic library of results for discrete probability theory.
-
measure/ -- Basic measure theory (lebesgue integral and measure, Fubini's theorem, etc.)
-
monad/ -- Definitions of probabilistic choice monads.