We mechanise the Cook-Levin theorem, i.e. the NP-completeness of SAT, in the proof assistant Coq. We use the call-by-value lambda-calculus L as the model of computation to formalise time complexity, the class NP, and polynomial-time reductions. The latter two notions agree with the usual characterisations via Turing machines (TMs), as L and TMs are polynomial-time equivalent.
The use of L as the computational model, as opposed to TMs, significantly eases program verification and the derivation of resource bounds. However, for showing the NP-hardness of SAT, computations of L need to be encoded in SAT, which is complicated by L's more complex computational structure. Thus, the polynomial-time reduction chain to SAT employs TMs as an intermediate problem, for which we neatly factor out a known textbook reduction from TMs to SAT. Still, all reduction functions are implemented and analysed in L.
To the best of our knowledge, this is the first result in *computational* complexity theory that has been mechanised with respect to any concrete computational model.
We discuss what makes this area of computer science hard to mechanise and highlight the design choices which enable our mechanisations.