Ohio University Verification Toolsuite
coq 8.9.0 mathcomp algebra 1.7.0 mathcomp fingroup 1.7.0 mathcomp ssreflect 1.7.0
To build OUVerT, clone it and do:
make
make install
The latter command installs the OUVerT files in your local .opam directory.
To use OUVerT files in another development, simply import them with OUVerT.filename, as in:
Require Import OUVerT.dyadic.
Following are the primary files in the development:
- axioms.v: Axiomatizes Pinsker's and Gibb's inequalities
- bigops.v: Computable Ssreflect-style bigops
- chernoff.v: Chernoff inequalities
- dist.v: Distributions over finite types
- dyadic.v: Dyadic rational numbers
- expfacts.v: Facts about
e^x - learning.v: Basic results in learning theory
- listlemmas.v: Basic results on lists
- maplemmas.v: Basic results on map
- numerics.v: Lemmas relating
Q,R, and dyadicsD - strings.v:
Showabletypes - vector.v: A sparse vector library