A formal proof of the Sands-Sauer-Woodrow theorem using the Rocq prover and mathcomp/ssreflect

TL;DR

This paper provides a formal proof of the Sands-Sauer-Woodrow theorem using the Rocq proof assistant and MathComp/SSReflect, formalizing graph properties and establishing a stronger version of the theorem.

Contribution

It formalizes the SSW theorem in a proof assistant and introduces a stronger version with weaker assumptions, recovering the original as a corollary.

Findings

Formal proof of the SSW theorem in Rocq proof assistant.

Development of a dedicated library for binary relations as classical sets.

Establishment of a stronger version of the theorem with weaker assumptions.

Abstract

We present a formal proof of the Sands-Sauer-Woodrow (SSW) theorem using the Rocq proof assistant and the MathComp/SSReflect library. The SSW theorem states that in a directed graph whose edges are colored with two colors and that contains no monochromatic infinite outward path, there exists an independent set S of vertices such that every vertex outside S can reach S by a monochromatic path. We formalize the graph using two binary relations Eb and Er , representing the blue and red edges respectively, and we develop a dedicated library for binary relations represented as classical sets. Beyond formalizing the original SSW theorem, we establish a strictly stronger version in which the assumption ''no monochromatic infinite outward path'' is replaced by the weaker condition that the asymmetric parts of the transitive closures of Eb and Er admit no infinite outward paths. The original SSW theorem is then recovered as a corollary via a lemma showing that an infinite path for the asymmetric part of the transitive closure of a relation implies an infinite path for the relation.