The ValidSDP library for the Coq proof assistant provides a reflexive tactic for proving inequalities on multivariate polynomials involving real-valued variables and rational constants.
The library is hosted on GitHub. It was developed by Erik Martin-Dorel and Pierre Roux.
You can browse the ValidSDP theories online:
The ValidSDP library depends on the following tools and libraries:
READMEfile in the archive.
You can download a tarball (tar.gz, 592 KiB) containing benchmarks for OCaml/OSDP, Coq/ValidSDP-0.3, PVS/Bernstein, SAGE/[Monniaux and Corbineau 2011], NLCertify, HOL Light/Formal_ineqs.
A new version of these benchmarks (compatible with the latest version of ValidSDP) is available in the ValidSDP Git repository (folder "benchs", branch "master").
This work has been presented at the 6th ACM SIGPLAN Conference on Certified Programs and Proofs CPP 2017 (slides – demo.v) and a report appears in the proceedings of CPP 2017: A Reflexive Tactic for Polynomial Positivity using Numerical Solvers and Floating-Point Computations (DOI). Author version available in open archive.