package coq-validsdp

ValidSDP is a library for the Coq formal proof assistant. It provides reflexive tactics to prove multivariate inequalities involving real-valued variables and rational constants, using SDP solvers as untrusted back-ends and verified checkers based on libValidSDP.

Once installed, you can import the following modules: From Coq Require Import Reals. From ValidSDP Require Import validsdp.