Theorem Prover for complexity theoretic reductions

Question

Can complexity theoretic reductions that lead to proofs of say NP completeness be formalized using an existing theorem prover such as Coq?

If so, can you provide an outline of how to formalize a simple reduction argument? I’d also appreciate pointers to the literature.

• Yuval Filmus: The belief is that all mathematical arguments can be formalized in Coq. NP-hardness reductions are mathematical arguments. The only conclusion is...

Answer 1

This is certainly possible, and the language of higher order functions makes this quite nice. If you're doing a Turing/Cook reduction, you can basically just write a function that takes an oracle as a parameter.

For example, to show that Graph Coloring is NP-hard, you could write something like this (pardon my terrible Coq-like pseudocode)

Theorem reduction: 
 (forall (k:Nat) (g:Graph), Decidable (Coloring g))
 -> (forall (f:BoolFormula), Decidable (Model f))

What gets tricky is proving that your reductions are polynomial-time. There are ways to do this, such as with a time-tracking monad. This example verifies the time complexity of a sorting algorithm, and gives some hints as to how to model this. Basically, for whatever operation you're counting as $O(1),ドル you require that it be performed in the monad, as well as calls to your oracle. Then you write a proof of some polynomial bound on the number of operations performed in the monad (which can keep track of them by encapsulating state).