Short proof of Menger's Theorem in Coq (Proof Pearl)
Résumé
Menger's theorem is one of the cornerstones of graph theory, and Hall's Marriage Theorem, a straightforward consequence of Menger's Theorem, is one of the most applied graph-theoretic results. Following Göring's "Short proof of Menger's Theorem" we give formal proofs of Menger's theorem and of some of its consequences, including Hall's Marriage Theorem and Kőnig's Theorem, in the proof assistant Coq. Our proofs make use of the mathematical components library and a library for reasoning about paths in finite graphs developed previously.
Loading...