# Brooks’ theorem with forbidden colors

Carl Johan Casselgren111Department of Mathematics, Linköping University,
SE-581 83 Linköping, Sweden. E-mail address<EMAIL_ADDRESS>Research supported by a grant from the Swedish Research council VR
(2017-05077).

###### Abstract

We consider extensions of Brooks’ classic theorem on vertex coloring where
some colors cannot be used on certain vertices. In particular we prove that if
$G$ is a connected graph with maximum degree $\Delta(G)\geq 4$ that is not a
complete graph and $P\subseteq V(G)$ is a set of vertices where either

(i) at most $\Delta(G)-2$ colors are forbidden for every vertex in $P$, and
any two vertices of $P$ are at distance at least $4$, or

(ii) at most $\Delta(G)-3$ colors are forbidden for every vertex in $P$, and
any two vertices of $P$ are at distance at least $3$,

then there is a proper $\Delta(G)$-coloring of $G$ respecting these
constraints. In fact, we shall prove that these results hold in the more
general setting of list colorings. These results are sharp.

_Keywords: Graph coloring, List coloring, Brooks’ theorem_

##  1 Introduction

Brooks’ classic theorem on graph coloring states that if $G$ is a connected
graph, not isomorphic to a complete graph or an odd cycle, then $G$ is
properly $\Delta(G)$-colorable, where $\Delta(G)$ as usual denotes the maximum
degree of $G$. This theorem has been strengthened in many different ways, see
e.g. the recent survey [8]. In particular, a list coloring version of Brooks’
theorem was obtained already in the seminal paper on list coloring by Erdős et
al [10], and also independently by Vizing [12].

A precoloring (or partial coloring) of a graph $G$ is a proper coloring of
some subset $V^{\prime}\subseteq V(G)$. Given a precoloring $\varphi$ of $G$,
we are usually interested in finding an extension of $\varphi$, that is, a
proper coloring of $G$ that agrees with the partial coloring $\varphi$. If
there is such a coloring (using the same number of colors as $\varphi$), then
$\varphi$ is extendable.

A precoloring extension version of Brooks’ theorem was obtained by Albertson
et al [2] and, independently, by Axenovich [3]: if $P$ is an independent set,
$\Delta(G)\geq 3$ and the minimum distance between any two vertices in $P$ is
$8$, then any proper coloring of $P$ can be extended to a proper
$\Delta(G)$-coloring of $G$, unless $G$ contains a copy of $K_{\Delta(G)+1}$,
where $K_{n}$ as usual denotes a complete graph on $n$ vertices. In general,
the condition on the distance is tight, but Voigt obtained improvements for
the case when $G$ is $2$-connected [13, 14].

In this short note we consider the similar problem of constructing proper
$\Delta(G)$-colorings avoiding certain colors; that is, given a subset
$P\subseteq V(G)$ of the vertices of a graph $G$ where every vertex of $P$ is
assigned a set of forbidden colors from $\\{1,\dots,\Delta(G)\\}$, we are
interested in finding a proper $\Delta(G)$-coloring of $G$ respecting these
constraints. These type of questions go back to a paper by Häggkvist [11] and
although they arise naturally in problems where a coloring is constructed
sequentially, it seems that they so far primarily have been studied in the
setting of edge colorings, see e.g. [5, 6, 7, 9] and references therein. In
particular, a variant of Vizing’s edge coloring theorem with forbidden colors
was obtained in [9]. Note that it is not possible to prove a variant of
König’s edge coloring theorem with forbidden colors (even if only one
forbidden color is assigned to edges in a matching), as the coloring of the
graph in Figure 1 shows; here $K^{(i)}_{n,n}-e$ denotes a copy of the complete
bipartite graph $K_{n,n}$ where an arbitrary edge has been removed (which is
dashed in the figure). Since color $1$ cannot be used on any of the edges at
the top of the figure, it cannot be used on any edge incident with the bottom
vertex $u$ either. Hence, there is no proper $\Delta(G)$-edge coloring
respecting the forbidden colors.

Note that here we can make the distance between the colored edges arbitrarily
large by adding more copies of $K_{n,n}-e$ along with connecting edges between
different copies of $K_{n,n}-e$.

$u$$1$$1$$1$$K^{(1)}_{n,n}-e$$K^{(2)}_{n,n}-e$$K^{(n)}_{n,n}-e$$\dots$$\dots$
Figure 1: A bipartite graph $G$ with no proper $\Delta(G)$-edge coloring
respecting the forbidden colors.

Let us note that the general problem of coloring a given graph properly
subject to the condition that some colors cannot be used on certain vertices
is certainly NP-complete since the general vertex (list) coloring problem is.

Here we prove that if $G$ is a graph with $\Delta(G)\geq 4$, not containing a
copy of $K_{\Delta(G)+1}$, and $P\subseteq V(G)$ an independent set where

  * (i)

at most $\Delta(G)-2$ colors are forbidden for every vertex in $P$, and any
two vertices of $P$ are at distance at least $4$, or

  * (ii)

at most $\Delta(G)-3$ colors are forbidden for every vertex in $P$, and any
two vertices of $P$ are at distance at least $3$,

then there is a proper $\Delta(G)$-coloring of $G$ respecting these
constraints. It remains an open problem whether (i) holds in the case when
$\Delta(G)=3$.

Comparing this to the aforementioned results on precoloring extension [1, 2],
we see that allowing just the slight extra flexibility of having one or two
extra colors on the vertices in $P$ implies that the distance condition can be
relaxed significantly.

Moreover, as for the results on precoloring extension in [1, 2], we shall
prove that these results hold in the more general setting of list coloring of
graphs. This is proved in the next section, where we also give examples
showing that they are sharp. In Section 3 we briefly consider the related
question of avoiding a given partial coloring $\varphi$, i.e. the problem of
finding a coloring $f$ of a graph which differs from $\varphi$ on every vertex
that is colored under $\varphi$, and give some observations and remarks on
this problem.

##  2 Main Result

Before proving our main result, let us introduce some terminology. The block-
cutpoint graph of a graph $G$ has a vertex for each block of $G$ and a vertex
for each cut-vertex of $G$, where a cut-vertex $v$ is adjacent to a block $B$
if $v\in V(B)$. A leaf block in a graph $G$ is a block of $G$ that contains at
most one cut-vertex. We shall use standard graph theory notation; in
particular, $d_{G}(v)$ denotes the degree of a vertex $v$ in $G$ and an
induced subgraph of $G$ is denoted by $G[S]$, where $S$ is a set of vertices
or a set of edges.

Given a graph $G$, assign to each vertex $v$ of $G$ a set $L(v)$ of colors
(positive integers). Such an assignment $L$ is called a _list assignment_ for
$G$ and the sets $L(v)$ are referred to as _lists_ or _color lists_. If all
lists have equal size $k$, then $L$ is called a _$k$ -list assignment_.
Usually, one is interested in finding a proper vertex coloring $\varphi$ of
$G$, such that $\varphi(v)\in L(v)$ for all $v\in V(G)$. If such a coloring
$\varphi$ exists then $G$ is _$L$ -colorable_ and $\varphi$ is called an _$L$
-coloring_; if $L$ is clear from the context, then we just call $\varphi$ a
list coloring and say that $G$ is list colorable when the coloring exists.
Furthermore, $G$ is called _$k$ -choosable_ if it is $L$-colorable for every
$k$-list assignment $L$. The least number $k$ such that $G$ is $k$-choosable
is called the _list-chromatic number_ (or choice number) of $G$ and is denoted
by $\chi_{l}(G)$.

As mentioned above, Brooks’ theorem holds in the setting of list coloring;
that is, if $G$ is a connected graph which is not isomorphic to an odd cycle
or a complete graph, then $\chi_{l}(G)\leq\Delta(G)$. As in the aforementioned
papers on precoloring extension, we shall use the following stronger theorem
proved in [4, 10]. A Gallai tree is a connected graph in which every block is
a complete graph or an odd cycle. A graph $G$ is degree-choosable if it has an
$L$-coloring whenever $L$ is a list assignment such that $|L(v)|\geq d_{G}(v)$
for all $v\in V(G)$; such a list assignment of $G$ is called supervalent.

######  Theorem 2.1.

If $L$ is a supervalent list assignment for a connected graph $G$ and there is
no $L$-coloring of $G$, then

(a) $|L(v)|=d_{G}(v)$ for every $v\in V(G)$;

(b) $G$ is a Gallai tree;

(c) $L(v)=\cup_{B\in\mathcal{B}(v)}L_{B}$ for all $v\in V(G)$, where
$\mathcal{B}(v)$ is the set of blocks containing $v$, and for each block $B$,
$L_{B}$ is a set of $\chi(B)-1$ colors.

Note that this implies (as remarked in [2]) that each block $B$ is an
$|L_{B}|$-regular graph, and that all vertices of a single block that are not
cut-vertices of $G$ have the same list. Furthermore, we shall need the
following.

######  Corollary 2.2.

Suppose that $T$ is a Gallai tree, $L$ a supervalent list assignment
satisfying conditions (a), (b), and (c) of Theorem 2.1, and that there is a
leaf block $B_{L}$ of $T$ with $\Delta(T)\geq 3$ vertices
$u_{1},\dots,u_{\Delta(T)-1},v$, where $v$ is a cut-vertex of $T$ of degree
$\Delta(T)$. Assume further that $u_{0}$ is a vertex of degree $\Delta(T)-1$,
not contained in $B_{L}$, and that there are colors $c_{1},c_{2},c_{3}$ such
that

  * •

$c_{1}\notin L(u_{i})$, for $i=0,\dots,\Delta(T)-1$, and

  * •

$c_{2},c_{3}\in L(u_{i})$, for $i=0,\dots,\Delta(T)-1$.

Set $U=\\{u_{0},u_{1},\dots,u_{\Delta(T)-1}\\}$ and define the list
assignments $L^{\prime}$ and $L^{\prime\prime}$ for $T$ by setting

  * •

$L^{\prime\prime}(v)=L^{\prime}(v)=L(v)$ if $v\in V(T)\setminus U$, and

  * •

$L^{\prime}(v)=L(v)\cup\\{c_{1}\\}\setminus\\{c_{2}\\}$ and
$L^{\prime\prime}(v)=L(v)\cup\\{c_{1}\\}\setminus\\{c_{3}\\}$ if $v\in U$.

If $T$ is not $L^{\prime}$-colorable, then it is $L^{\prime\prime}$-colorable.

The proof of this corollary is a rather straightforward application of Theorem
2.1; we briefly sketch an argument.

The conditions imply that there must be a block $B_{2}\neq B_{L}$ containing
$v$, and since $B_{L}$ is a leaf block with $\Delta(T)$ vertices, $B_{2}\cong
K_{2}$, that is, $B_{2}=vx$, say. Moreover, since $T$ is neither
$L$-colorable, nor $L^{\prime}$\- or $L^{\prime\prime}$-colorable,
$L_{B_{2}}=\\{c_{1}\\}$, $L^{\prime}_{B_{2}}=\\{c_{2}\\}$, and
$L^{\prime\prime}_{B_{2}}=\\{c_{3}\\}$, where we use the notation from Theorem
2.1. Thus there must be a block $B_{3}$ in $T$ containing $x$, such that
$c_{2}\in L_{B_{3}}$ and $c_{1}\in L^{\prime}_{B_{3}}$.

Now, since $L$ and $L^{\prime}$ only differs on the lists for the vertices in
$U$, $B_{3}\cong K_{2}$, and, more generally, there is path from $v$ to
$u_{0}$ in $T$, all edges of which lie in blocks that are isomorphic to
$K_{2}$. Furthermore, since $T$ is not $L$\- or $L^{\prime}$-colorable, every
block $B_{i}$ of this path satisfies that $L_{B_{i}}=\\{c_{1}\\}$ or
$L_{B_{i}}=\\{c_{2}\\}$. Now, since $T$ is a Gallai tree, this is the only
path from $v$ to $u_{0}$ in $T$. Using this property, it is now easy to check
that this implies that $T$ must be $L^{\prime\prime}$-colorable.

The following is the main result of this paper.

######  Theorem 2.3.

Let $G$ be a connected graph with maximum degree $\Delta(G)\geq 4$ which is
not complete and $P\subseteq V(G)$ a subset of vertices. If $L$ is a list
assignment for $G$ such that $|L(v)|\geq\Delta(G)$ if $v\in V(G)\setminus P$,
then $G$ is $L$-colorable if either

  * (i)

$|L(v)|\geq 2$ and any two vertices of $P$ are at distance at least $4$, or

  * (ii)

$|L(v)|\geq 3$ and any two vertices of $P$ are at distance at least $3$.

Before proving the theorem, let us demonstrate that it is sharp both with
respect to list sizes and the distance conditions. For the case $\Delta(G)=3$,
we do not know whether a result as in (i) holds, but the example below shows
that distance $4$ would be best possible.

That the list size cannot be improved in part (i) follows by taking two copies
$K^{(1)}_{\Delta-1}$ and $K^{(2)}_{\Delta-1}$ of $K_{\Delta-1}$, where all
vertices have the list $\\{1,\dots,\Delta\\}$ and making exactly one vertex of
$K^{(1)}_{\Delta-1}$ adjacent to exactly one vertex of $K^{(2)}_{\Delta-1}$.
All other vertices of $K^{(1)}_{\Delta-1}$ are adjacent to a vertex $u$ with
the list $\\{1\\}$ and all vertices of $K^{(2)}_{\Delta-1}$ are adjacent to a
vertex $v\neq u$ with the list $\\{1\\}$. Clearly, this graph is not list
colorable.

$\dots$$\\{1,\dots,\Delta\\}$$K_{\Delta}$$\dots$$\\{1,\dots,\Delta\\}$$K_{\Delta}$$\vdots$$\\{1,\dots,\Delta\\}$$K_{\Delta}$$\\{1,2\\}$$\\{1,2\\}$$\\{1,2\\}$
Figure 2: A graph with a list assignment and no list coloring.

That the distance condition in part (i) is best possible follows from the fact
that the $\Delta$-regular graph in Figure 2 is not list colorable. Here all
vertices that are contained in copies of $K_{\Delta}$ are assigned the list
$\\{1,\dots,\Delta\\}$, while the vertices not contained in the copies of
$K_{\Delta}$ are assigned the list $\\{1,2\\}$. Since at least two of the
vertices not contained in the copies of $K_{\Delta}$ must be colored by the
same color, this graph is not list colorable. Hence, the distance condition in
part (i) cannot be improved. Moreover, this example also shows that the list
size in part (ii) is sharp.

That the distance condition in part (ii) is best possible can be seen by
taking a copy of $K_{\Delta-1}$ along with two vertices $u$ and $v$ that are
joined to every vertex of $K_{\Delta-1}$ by an edge. Assign the list
$\\{1,2,3\\}$ to $u$ and the list $\\{4,5,6\\}$ to $v$ and the list
$\\{1,2,\dots,\Delta\\}$ to all vertices of $K_{\Delta-1}$. Then this graph is
not list colorable.

Let us now turn to the proof of Theorem 2.3. We shall need the following
lemma. Recall that an acyclic subgraph of a digraph is a subgraph with no
directed cycle.

######  Lemma 2.4.

If $D$ is a digraph and $S\subseteq V(D)$ a set of vertices $v$ satisfying
that the outdegree is strictly larger than the indegree of $v$, then there is
an ayclic subgraph $D^{\prime}$ of $D$ such that every vertex of $S$ has
outdegree $1$ in $D^{\prime}$.

Since every vertex of $S$ has strictly larger outdegree than indegree, this is
straightforward; we leave the details to the reader.

###### Proof of Theorem 2.3.

Since (in both cases) $P$ is independent and $|L(v)|\geq 2$ if $v\in P$, there
is an $L$-coloring $\varphi^{\prime}$ of the vertices in $P$. Define a new
list assignment $L^{\prime}$ for $H=G-P$ by, for $v\in V(H)$, setting

$L^{\prime}(v)=L(v)\setminus\\{\varphi^{\prime}(u):\text{$u$ is adjacent to
$v$}\\}.$

Since $|L(v)|\geq\Delta(G)$ if $v\in V(G)\setminus P$, it follows from Theorem
2.1 that any component of $H$ that is not $L^{\prime}$-colorable is a Gallai
tree. Moreover, since any vertex in $G$ is adjacent to at most one vertex of
$P$, every component of $H$ that is not $L$-colorable has minimum degree
$\Delta(G)-1$, and all vertices of such a component has degree $\Delta(G)$ in
$G$.

Suppose that some component $T$ of $H$ together with the restriction of
$L^{\prime}$ to $T$ is not list colorable, and thus satisfies the conditions
in Theorem 2.1. We call such a component $\varphi^{\prime}$-bad (or just bad).
Suppose further that some vertex $p\in P$ is adjacent to exactly $\Delta(G)-1$
vertices of a leaf block $B_{1}\cong K_{\Delta(G)}$ in $T$ and has no other
neighbor in $T$. By recoloring $p$ with another color of its list we get a new
coloring $\varphi^{\prime\prime}$ of $P$ so that $T$ is not
$\varphi^{\prime\prime}$-bad. Similarly, if $p\in P$ has only one neighbor in
$T$, then by recoloring $p$ we obtain a coloring $\varphi^{\prime\prime}$ such
that $T$ is not $\varphi^{\prime\prime}$-bad. Our proofs of both part (i) and
(ii) relies heavily on this simple observation.

Without loss of generality, we shall assume that every component of $H$
satisfies the conditions (a) and (b) of Theorem 2.1 (with $L^{\prime}$ in
place of $L$); otherwise, we just consider a suitable subgraph of $H$, since
components not satisfying these conditions cannot be bad.

After these initial observations, let us now prove part (i) of the theorem.
Since $G$ is not complete, and any two vertices of $P$ are at distance at
least $4$, no component of $H$ is isomorphic to a complete graph, and no two
vertices of $P$ are adjacent to vertices of the same block in $H$, and thus no
vertex of $P$ is adjacent to vertices of two different leaf blocks. This
implies that every component of $H$ contains at least two leaf blocks.
Moreover, if $T$ is such a component, then every leaf block $B_{L}$ of $T$ is
isomorphic to $K_{\Delta(G)}$, $\Delta(G)-1$ vertices of $B_{L}$ are adjacent
to the same vertex of $P$, and the cut-vertex of $B_{L}$ is not adjacent to
any vertex of $P$.

Now, suppose $\varphi^{\prime}$ is a coloring of $P$ so that some component
$T$ of $H$ is $\varphi^{\prime}$-bad. We shall prove that by recoloring some
vertices $P^{\prime}\subseteq P$ satisfying that if $p\in P^{\prime}$ then $p$
has $\Delta(G)-1$ neighbors in a leaf block, we can obtain an $L$-coloring
$\psi$ of $P$ so that no component of $H$ is $\psi$-bad. Indeed, in the
following we shall describe a recoloring procedure.

To this end, we shall prove the following claim. Let $P_{1}$ be the set of all
vertices of $P$ that have at least one neighbor in a leaf block of $H$, and
let $V_{1}$ be the set of all vertices in $H$ that are not contained in a
leaf-block and has a neighbor in $P_{1}$.

######  Claim 1.

If $T$ is a component in $H$, then the number of leaf-blocks in $T$ is greater
than the number of vertices in $T$ that are in $V_{1}$.

###### Proof.

Let us first note that no block of $H$ contains two vertices of $V_{1}$, as
follows from the definition of $V_{1}$. Suppose now that $v$ is a vertex of
$V_{1}$. Consider the block-cutpoint graph $W$ of $T$. Since $v$ has degree at
least four in $G$, and no other vertex of a block containing $v$ has a
neighbor in $V_{1}$, it follows that $v$ either is a cut-vertex of degree at
least $3$ in $W$, or that there is a block vertex of degree at least $3$ in
$W$, whose corresponding block in $T$ contains $v$. Moreover, since every
block of $T$ contains at most one vertex from $V_{1}$, we get that for each
vertex of $V_{1}$, there is a unique vertex of degree at least $3$ in $W$.
Now, since $W$ is a tree, it contains more leafs than vertices of degree at
least three. Hence, the number of leaf blocks of $T$ is greater than
$|V_{1}\cap V(T)|$. ∎

We now define a directed graph $D$ in the following way. Each component $T$ in
$H$ is represented by a vertex $t$, and there is a directed edge from a vertex
$t$ to another vertex $t^{\prime}$ if there is a vertex $p$ adjacent to
$\Delta(G)-1$ vertices of a leaf block in $T$ that is also adjacent to a
vertex of $T^{\prime}$. Moreover, for every leaf-block of a component $T$ of
$H$ for which the adjacent vertex $p\in P$ is not adjacent to any other vertex
in $H$, we add a new vertex $x_{p}$ and an arc $(t,x_{p})$; thus $x_{p}$ has
indegree $1$ and outdegree $0$ in the digraph $D$. Furthermore, every directed
edge of $D$ corresponds to a vertex in $P$.

By Claim 1 every vertex of $D$ corresponding to a component of $H$ has larger
outdegree than indegree, so it follows from Lemma 2.4 that there is an acyclic
directed subgraph $D^{\prime}$ of $D$ such that every vertex corresponding to
a component of $H$ has outdegree $1$; denote these vertices by $S$.

Since $D^{\prime}$ is acyclic there is a linear order $\prec$ of the vertices
of $S$ such that if $(t,t^{\prime})$ is a directed edge of $D^{\prime}$, then
$t\prec t^{\prime}$.

Suppose $S=\\{t_{1},\dots,t_{n}\\}$, where $t_{1}\prec t_{2}\prec\dots\prec
t_{n}$. We now traverse the vertices $t_{1},t_{2},\dots$ according to $\prec$
in the following way. Suppose $(t_{1},x)\in A(D^{\prime})$ (where $x$ might be
in $S$).

  * •

If $t_{1}$ corresponds to a $\varphi^{\prime}$-bad component and $(t_{1},x)\in
A(D^{\prime})$, then we recolor the vertex $p_{1}$ corresponding to the arc
$(t_{1},x)\in A(D^{\prime})$ to obtain a new coloring $\varphi_{1}$ of $P$.
Note that by the construction of $D^{\prime}$ and the order $\prec$, the only
component of $H$ that might be $\varphi_{1}$-bad but not
$\varphi^{\prime}$-bad is a component of $H$ corresponding to $x$, if there is
such a component. Moreover, after this recoloring, $T_{1}$ is not
$\varphi_{1}$-bad.

  * •

If $t_{1}$ is not bad, then we just set $\varphi_{1}=\varphi^{\prime}$ and
continue with the next vertex according to the order $\prec$.

We continue this process for all vertices of $S$ according to the linear order
$\prec$ and define $L$-colorings $\varphi_{1},\varphi_{2},\dots$. Then every
vertex in $S$ is considered once, and the process terminates after a finite
number of steps.

Now, since $t_{i}\prec t_{j}$ precisely when there is no directed path from
$t_{j}$ to $t_{i}$ in $D^{\prime}$, it follows that no component $T_{i}$
corresponding to a vertex $t_{i}\in S$ can be $\varphi_{j}$-bad for $j\geq i$.
Hence, after this process terminates when all vertices of $S$ have been
considered, we obtain a proper $L$-coloring $\varphi_{n}$ where no component
of $H$ is $\varphi_{n}$-bad. This proves part (i).

Let us now prove part (ii). We shall construct a subgraph $F^{\prime\prime}$
of $G$ for coloring the vertices of $P$ from their lists $L$.

Consider the bipartite multigraph $J$ with parts $P$ and $\mathcal{B}$, where
$\mathcal{B}$ contains a vertex for every leaf-block of $H$, and where a
vertex $p$ of $P$ is joined by an edge to a vertex $b\in\mathcal{B}$ for each
edge between $p$ and the block corresponding to $b$ in $H$. In $J$, every
vertex of $P$ has degree at most $\Delta(G)$, and every vertex of
$\mathcal{B}$ has degree at least $\Delta(G)-1$ and at most $\Delta(G)$. Thus,
by König’s edge coloring theorem, there is a proper $\Delta(G)$-edge coloring
of $J$.

We denote by $J^{\prime}$ the subgraph of $J$ induced by the edges colored
$1,2,3,4$. Then $\Delta(J^{\prime})\leq 4$ and every vertex of $\mathcal{B}$
has degree at least $3$ in $J^{\prime}$. Note further that if some vertex
$b\in\mathcal{B}$ has degree $3$ in $J^{\prime}$, then $b$ corresponds to a
leaf block of $H$ that is contained in a component with at least two leaf
blocks.

From $J^{\prime}$ we form a new graph $J^{\prime\prime}$ with vertex set
$V(J^{\prime})$ by for every component $T$ of $H$, where every leaf-block of
$T$ corresponds to a vertex of degree $3$ in $J^{\prime}$, arbitrarily
selecting two vertices $b_{1}$ and $b_{2}$, corresponding to different leaf-
blocks of $T$, and redistributing the edges incident with $b_{1}$ and $b_{2}$
so that one edge incident with $b_{2}$ is “moved to” $b_{1}$; thus $b_{1}$
gets degree four in $J^{\prime\prime}$ and $b_{2}$ gets degree two. Note that
this does not change the degrees of vertices in $P$.

Now, by arbitrarily adding edges between pairs of vertices of odd degree in
$J^{\prime\prime}$, we obtain a graph $K$ where all vertices have even degree
at most $4$. Thus every component of $K$ is Eulerian and by taking every
second edge in an Eulerian circuit of every component of $K$ we obtain a
subgraph $F_{K}$ where every vertex has degree $0,1$ or $2$. Denote the
restriction of this subgraph to $J^{\prime\prime}$ by $F_{J}$, and let $F$ be
the subgraph of $J^{\prime}$ corresponding to $F_{J}$. Then every vertex of
$F$ has degree at most two and, moreover, every component of $H$ has a leaf
block that corresponds to a vertex of degree $2$ in $F$.

Next, let $\mathcal{B}_{2}$ be the set of vertices in $\mathcal{B}$ that have
degree $2$ in $F$ and consider the vertex-induced subgraph
$F[\mathcal{B}_{2}\cup P]$. We define $\mathcal{B}_{d}$ to be the subset of
$\mathcal{B}_{2}$ containing all vertices that are incident to two different
vertices of $P$ in $F[\mathcal{B}_{2}\cup P]$. Let $F^{\prime}$ be the
subgraph of $F$ induced by $\mathcal{B}_{d}\cup P$.

Now, in $F[\mathcal{B}_{2}\cup P]$ every vertex of
$\mathcal{B}_{2}\setminus\mathcal{B}_{d}$ is incident with two edges with the
same endpoint in $P$, so every vertex of $P$ with a neighbor in
$\mathcal{B}_{2}\setminus\mathcal{B}_{d}$, has no other neighbor in
$F[\mathcal{B}_{2}\cup P]$. Set
$\mathcal{B}_{1}=\mathcal{B}_{2}\setminus\mathcal{B}_{d}$, and denote by
$\mathcal{B}^{\prime}_{1}$ the set of vertices in $\mathcal{B}_{1}$ that
correspond to leaf blocks in $H$ with at least two different neighbors in $P$
in $G$. Let $P^{\prime}$ be the set of vertices in $P$ that are adjacent to
vertices of $\mathcal{B}^{\prime}_{1}$ in $F$.

From $F^{\prime}$ we form a new graph $F^{\prime\prime}$ with
$V(F^{\prime\prime})=P$ and where the edge set is constructed iteratively in
the following way:

  * •

firstly, two vertices of $P$ are adjacent if they have a common neighbor in
$F^{\prime}$;

  * •

secondly, for all vertices $p^{\prime}$ of $P^{\prime}$ we do the following:
suppose $p^{\prime}$ is adjacent to $b$ in $F$. We add an edge between
$p^{\prime}$ and another arbitrary vertex $p^{\prime\prime}\in P$ that in $J$
is adjacent to $b$.

We note the following properties of $F^{\prime\prime}$.

  * (a)

Since every vertex of $F$ has degree at most $2$, the same holds for the
induced subgraph $F^{\prime\prime}[P\setminus P^{\prime}]$. Thus, by
construction, every component of $F^{\prime\prime}$ is unicyclic, i.e., has at
most one cycle.

  * (b)

Every component $T$ of $H$ that is isomorphic to $K_{\Delta(G)}$ satisfies
that two vertices in $P$ with neighbors in $T$ are adjacent in
$F^{\prime\prime}$.

  * (c)

If the vertices of a leaf block $B$ of $H$, which corresponds to a vertex in
$\mathcal{B}_{2}$, has at least two different vertices in $P$ as neighbors in
$G$, then there are two vertices $p,p^{\prime}\in P$, both with at least one
neighbor in $B$, that are adjacent in $F^{\prime\prime}$.

We now color the vertices of $P$ as follows. By (a), the core of
$F^{\prime\prime}$, obtained by successively removing vertices of degree $1$
from $F^{\prime\prime}$, has maximum degree at most $2$. Hence
$F^{\prime\prime}$ is properly colorable from the lists $L$ of vertices in
$P$. We take such a coloring $\varphi$ of $P$ with a minimum number of
$\varphi$-bad components in $H$.

Now, consider this coloring of the vertices of $P$ in the graph $G$. It
follows from Theorem 2.1 that if a component $T$ of $H$ is $\varphi$-bad, then
for every leaf-block $B$ of $T$, every vertex of $P$ that has a neighbor in
$B$ has the same color under $\varphi$. Now, since every component of $H$ has
a leaf block that corresponds to a vertex of $\mathcal{B}_{2}$, it follows
from (c) that there is a leaf-block $B_{L}$ in $T$ where $\Delta(G)-1$
vertices are adjacent to the same vertex $p$ in $P$; that is, $p$ has at most
one neighbor outside $B_{L}$.

Suppose $\varphi(p)=c_{1}$ and $L(p)=\\{c_{1},c_{2},c_{3}\\}$. Since $p$ has
at most one neighbor outside $B_{L}$, it follows that by recoloring $p$ by the
color $c_{2}$ we get a new $L$-coloring $\varphi^{\prime}$ of $P$ such that
either $T$ is $\varphi^{\prime}$-bad (and then the neighbor of $p$ not in
$B_{L}$ is in $T$), or $T$ is not $\varphi^{\prime}$-bad but some other
component is $\varphi^{\prime}$-bad but not $\varphi$-bad, since $\varphi$ is
an $L$-coloring with a minimum number of $\varphi$-bad components. Now, since
coloring $p$ by the color $c_{2}$ does not decrease the number of bad
components and $p$ has at most one neighbor outside $B_{L}$, we may color $p$
by the color $c_{3}$ to obtain a coloring $\varphi^{\prime\prime}$ with fewer
bad components. In the case when $p$ has a neighbor outside $T$, this follows
from our initial observation before the proof of part (i), and in the case
when $p$ has all neighbors in $T$, then it follows from Corollary 2.2. In both
cases, this contradicts the choice of $\varphi$ and thus completes the proof
of the theorem. ∎

It is natural to ask if it is possible to prove a version of Theorem 2.3 where
the set $P$ of vertices with shorter lists is allowed to be any independent
set.

######  Problem 2.5.

Let $G$ be a graph with maximum degree $\Delta=\Delta(G)\geq 4$, not
containing a copy of $K_{\Delta+1}$, and $P$ an independent set. Is there a
$k=k(\Delta)<\Delta$ such that if $L$ is a list assignment where

  * •

$|L(v)|=k$, if $v\in P$, and

  * •

$|L(v)|=\Delta$, if $v\in V(G)\setminus P$,

then $G$ is $L$-colorable?

Since $P$ is independent, it follows from Theorem 2.1 that any minimal
counterexample $G$ to this question must satisfy that all vertices of
$V(G)\setminus P$ has degree $\Delta(G)$.

In particular, we are interested in whether Problem 2.5 has a positive
solution in the case when then lists of $P$ have size $|L(v)|=\Delta(G)-1$; in
the next section we investigate this question further for the special case
when all lists are chosen from the set $\\{1,\dots,\Delta(G)\\}$.

##  3 Avoiding colorings

In this section we consider the problem of coloring a graph $G$ using colors
$1,\dots,\Delta(G)$, subject to the condition that some colors cannot be used
on certain vertices. Let us begin by noting the following reformulation of
Theorem 2.3, which is a generalization of Brooks’ theorem for ordinary graph
coloring for the case of $\Delta(G)\geq 4$.

######  Corollary 3.1.

Let $G$ be a connected graph with maximum degree $\Delta(G)\geq 4$ that is not
complete. Suppose that a set $P$ of vertices is assigned a list of forbidden
colors. If either

  * (i)

each vertex of $P$ has most $\Delta(G)-2$ forbidden colors and any two
vertices of $P$ are at distance at least $4$, or

  * (ii)

each vertex of $P$ has most $\Delta(G)-3$ forbidden colors and any two
vertices of $P$ are at distance at least $3$,

then there is a proper $\Delta(G)$-coloring of $G$ which respects the
forbidden colors.

An interesting special case of Problem 2.5 is when the lists of $P$ have size
$|L(v)|=\Delta(G)-1$ and all lists use colors from $\\{1,\dots,\Delta(G)\\}$,
which would be a useful generalization of Brooks’ theorem along the lines of
Corollary 3.1. We note the following partial result towards such a general
theorem. Recall that a partial coloring $\varphi$ of $G$ is avoidable if there
is a proper coloring $f$ of $G$ such that $f(v)\neq\varphi(v)$ for any vertex
that is colored under $\varphi$.

######  Proposition 3.2.

Let $G$ be a connected graph with maximum degree $\Delta(G)\geq 4$ that is not
complete, and $\varphi$ a precoloring of a subset $P\subseteq V(G)$. If $P$ is
independent and every vertex in $V(G)\setminus P$ is either adjacent to at
least three vertices from $P$ or to no vertex from $P$, then $\varphi$ is
avoidable.

This proposition is a special case of a more general result proved below, so
we postpone its proof. Conversely, for the case when each vertex in
$V(G)\setminus P$ has a bounded number of neighbors in $P$, then we have the
following.

######  Proposition 3.3.

Let $G$ be a connected graph with maximum degree $\Delta(G)\geq 4$ that is not
complete, and $\varphi$ a precoloring of an independent subset $P\subseteq
V(G)$. Furthermore, suppose that every vertex in $V(G)\setminus P$ has at most
$d_{0}$ neighbors in $P$, and that every vertex in $P$ has neighbors in at
most $d_{1}$ components of $G-P$. If $d_{0}d_{1}<\Delta(G)-1$ and every
component of $G-P$ contains a leaf block with at least $d_{0}+1$ distinct
neighbors in $P$, then then there is a proper $\Delta(G)$-coloring of $G$ that
avoids $\varphi$.

###### Proof.

The proof is based on Theorem 2.1 and uses similar ideas as the proof of
Theorem 2.3, so we only sketch the argument. The basic idea is to find a
proper coloring $f$ of the vertices of $P$ that avoids $\varphi$, and such
that no component of $H=G-P$ together with the list assignment for the
vertices of $V(G)\setminus P$ obtained by setting

$L_{f}(v)=\\{1,\dots,\Delta(G)\\}\setminus\\{f(u):\text{$u$ is adjacent to
$v$}\\}$

for $v\in V(G)\setminus P$, satisfies the conditions in Theorem 2.1.
Consequently, there is a proper $\Delta(G)$-coloring of $G$ avoiding
$\varphi$.

If $T$ is a component of $H$ so that $V(T)$ is not $L_{f}$-colorable for some
coloring $f$ of $P$, then every leaf-block of $T$ is a complete graph $K$
where all vertices have degree $\Delta(G)$ in $G$, and which satisfies that
$L_{f}(u)=L_{f}(v)$ for any two vertices $u$ and $v$ of $K$ that are not cut-
vertices. Moreover, the cut-vertex $w$ of $K$ satisfies that
$L_{f}(u)\subseteq L_{f}(w)$, where $u\in V(K)$. Hence, it suffices to prove
that there is a coloring $f$ of $P$ so that every component of $G-P$ has a
leaf block that does not satisfy this condition.

To this end, we define a ”conflict graph” $D$ with vertex set $P$ in the
following way. Suppose that $K$ is a leaf block in $H$ that is isomorphic to
$K_{k}$, for some integer $k$, and where the vertices in $K$ altogether have
at least $d_{0}+1$ distinct neighbors in $P$. We arbitrarily pick $d_{0}+1$
vertices in $P$, each of which has a neighbor in $K$, and form a clique on
those $d_{0}+1$ vertices.

Now, by assumption every component of $G-P$ contains such a leaf block as
described in the preceding paragraph, so by repeating this process for one
such leaf block of every component of $H$, we obtain the conflict graph $D$.
The maximum degree of this graph is at most $d_{1}d_{0}$, since every vertex
of $P$ has neighbors in at most $d_{1}$ components of $H$. Thus, by the list
coloring version of Brooks’ theorem, there is a proper $\Delta(G)$-coloring
$f$ of $D$ that avoids $\varphi$.

Now, by the construction of $D$ every component of $H$ has a leaf block with
neighbors in $P$ of $d_{0}+1$ different colors under $f$. Since every vertex
of $V(G)\setminus P$ has at most $d_{0}$ neighbors in $P$, this implies that
no component of $H$ together with the list assignment

$L_{f}(v)=\\{1,\dots,\Delta(G)\\}\setminus\\{f(u):\text{$u$ is adjacent to
$v$}\\}$

satisfies the conditions in Theorem 2.1 and, consequently, there is a proper
$\Delta(G)$-coloring of $G$ that avoids $\varphi$. ∎

More generally, we might ask what can be said in the case when $P$ is not
required to be an independent set? A $\Delta(G)$-coloring of $G$ where every
vertex is assigned the same color is not avoidable if $\chi(G)=\Delta(G)$. We
note the following reformulation of a result for edge colorings from [7].

######  Proposition 3.4.

If $\varphi$ is a partial $k$-coloring of a connected graph $G$ that is not
complete, where every color appears on at most $\Delta(G)-k$ vertices, then
there is a proper $\Delta(G)$-coloring of $G$ that avoids $\varphi$.

The proof is virtually identical to the corresponding result for edge
colorings in [7], so we omit it. Note, in particular, that Proposition 3.4
implies that every partial coloring with at most $\Delta(G)-1$ colored
vertices is avoidable, which is sharp by the example of the join of $K_{d}$
with two vertices $u$ and $v$, where $u$ and all vertices of $K_{d}$ are
colored $1$.

For the case when the vertices in $P$ induce a subgraph of small maximum
degree, we have the following.

######  Proposition 3.5.

Let $G$ be a connected graph with maximum degree $\Delta(G)\geq 3$ that is not
complete, and $\varphi$ a precoloring of a subset $P\subseteq V(G)$, where
every vertex in $V(G)\setminus P$ either has at least $d$ neighbors in $P$ or
no neighbors in $P$. If $\Delta(G[P])<d-2$, then there is a proper coloring of
$G$ avoiding $\varphi$.

###### Proof.

Again, the argument is similar to the one in the proof of Theorem 2.3, so we
only sketch the proof.

Since $\Delta(G[P])<d-2$, there is a proper $(d-1)$-coloring $f$ of $G[P]$
that avoids $\varphi$. Now, consider the lists induced for the vertices of
$V(G)\setminus P$ obtained by setting

$L_{f}(v)=\\{1,\dots,\Delta(G)\\}\setminus\\{f(u):\text{$u$ is adjacent to
$v$}\\}$

for $v\in V(G)\setminus P$.

Since every vertex of $V(G)\setminus P$ has at least $d$ neighbors in $P$ or
no neighbor in $P$, no component $T$ of the graph $G-P$ along with the
restriction of $L_{f}$ to $T$ satisfies the conditions in Theorem 2.1. Hence,
there is an $L_{f}$-coloring of $G-P$. This $L$-coloring taken together with
$f$ is the required coloring. ∎

Note that Proposition 3.2 is a special case of Proposition 3.5.

Next, we consider the special case that the partial coloring to be avoided is
proper. It is straightforward that for the case $\Delta(G)\leq 2$, there are
unavoidable partial proper colorings of even cycles and paths, while any
partial proper $3$-coloring of an odd cycle is avoidable. For the case
$\Delta(G)=3$, the examples after Theorem 2.3 show that there are unavoidable
partial proper $3$-colorings of graphs with maximum degree three. For the case
$\Delta(G)=4$, Figure 3 depicts a graph with an unavoidable partial proper
coloring. For $\Delta(G)\geq 5$ we do not know any such examples, and in
general we would like to suggest the following.

$1$$2$$2$$1$$1$$2$$2$$1$$1$$2$$2$$1$ Figure 3: A graph with a partial proper
coloring that is not avoidable.

######  Problem 3.6.

Is there a constant $\Delta_{0}$ such that if $\Delta(G)\geq\Delta_{0}$ and
$G$ does not contain a copy of $K_{\Delta(G)+1}$, then any partial proper
$\Delta(G)$-coloring of $G$ is avoidable?

We note that every proper coloring of a graph is avoidable by permuting
colors; thus any extendable partial coloring is avoidable.

Finally, let us briefly consider corresponding questions for $k$-colorings of
$k$-chromatic graphs; that is, if $G$ is a $k$-colorable graph and every
vertex is assigned a forbidden color, can we find a proper coloring that
avoids the forbidden colors?

Since for any $k$, there are well-known examples of uniquely $k$-colorable
graphs, we need at least $k+1$ colors for such a coloring. Moreover, since
there are examples of planar graphs with $4$-list assignments with colors from
the set $\\{1,\dots,5\\}$, that are not list colorable (see e.g. [1]), it is
in general not possible to avoid a $(k+1)$-coloring of a $k$-colorable graph
using $k+1$ colors. Furthermore, in the example from [1], the missing colors
in fact form a proper coloring of the planar graph, so it follows that not
every proper $5$-coloring of a planar graph is avoidable.

On the other hand, if we require that the set of vertices with a forbidden
color form an independent set, then any partial $(k+1)$-coloring of a
$k$-chromatic graph is trivially avoidable.

######  Proposition 3.7.

If $G$ is a $k$-colorable graph, and $\varphi$ a partial $(k+1)$-coloring of
an independent set in $G$, then there is a proper $(k+1)$-coloring of $G$
avoiding $\varphi$.

###### Proof.

Let $f$ be any proper $k$-coloring of $G$. For any vertex $v$ that has the
same color under $f$ and $\varphi$ we recolor $v$ by the color $k+1$; the
resulting coloring is proper and avoids $\varphi$. ∎

## References

  * [1] M.O. Albertson, You Can’t Paint yourself into a corner, J. Combin. Theory Ser. B 78 (1998), 189–194.
  * [2] M.O. Albertson, A.V. Kostochka, D.B. West, Precoloring extensions of Brooks’ theorem, SIAM J. Discriete Math. 18 (2005), 542–553.
  * [3] M. Axenovich A note on graph coloring extensions and list-colorings, Electron. J. Combin. 10 (2003), note 1.
  * [4] O.V. Borodin, Criterion of chromaticity of a degree prescription, Abstracts of IV All-Union Conference on Theoretical Cybernetics (Novisibirsk), 1977, 127–128 (in Russian).
  * [5] C.J. Casselgren, L.A. Pham, Restricted extension of sparse partial edge colorings of complete graphs. Electron. J. Combin. 28 (2021).
  * [6] C.J. Casselgren, On avoiding some families of arrays. Discr. Math. 312 (2012), 963–972.
  * [7] C.J. Casselgren, P. Johansson, K. Markström, Avoiding and Extending Partial Edge Colorings of Hypercubes, Graphs and Combin. 38 (2022).
  * [8] D.W. Cranston, L. Rabern, Brooks’ Theorem and Beyond, J. Graph Theory 80 (2015), 199–225.
  * [9] K. Edwards, A. Girao, J. van den Heuvel, R.J. Kang, G.J. Puleo, J.-S. Sereni, Extension from Precoloured Sets of Edges, Electron J. of Combin. 25 (2018), P3.1, 28 pp.
  * [10] P. Erdős, A.L. Rubin, H. Taylor, Choosability in graphs, Proceedings of the West Coast Conference on Combinatorics, Graph Theory and Computing, Utilitas Math, Winnipeg, MB, Canada, 1980, 126–157.
  * [11] R. Häggkvist, A note on Latin squares with restricted support. Discr. Math. 75 (1989), 253–254.
  * [12] V.G. Vizing, Vextex coloring with given colors, Metody Diskretn. Anal. 29 (1976), 3–10 (in Russian).
  * [13] M. Voigt, Precoloring extension for $2$-connected Graphs with maximum degree three, Discrete Math. 309 (2009), 4926–4930.
  * [14] M. Voigt, Precoloring extension for 2-connected graphs. SIAM J. Discrete Math. 21 (2007), 258–263.


# CoqPyt: Proof Navigation in Python in the Era of LLMs

Pedro Carrott<EMAIL_ADDRESS>0000-0003-4316-928X Imperial
College LondonLondonUK ,  Nuno Saavedra<EMAIL_ADDRESS>0000-0003-4148-5991 INESC-ID/IST, University of LisbonLisbonPortugal ,  Kyle
Thompson  0000-0002-2868-7612<EMAIL_ADDRESS>University of California San
DiegoSan DiegoUSA ,  Sorin Lerner  0000-0003-3957-0628<EMAIL_ADDRESS>University of California San DiegoSan DiegoUSA ,  João F. Ferreira
0000-0002-6612-9013<EMAIL_ADDRESS>INESC-ID/IST, University of
LisbonLisbonPortugal and  Emily First  0000-0002-2896-2928<EMAIL_ADDRESS>University of California San DiegoSan DiegoUSA

(2024)

###### Abstract.

Proof assistants enable users to develop machine-checked proofs regarding
software-related properties. Unfortunately, the interactive nature of these
proof assistants imposes most of the proof burden on the user, making formal
verification a complex, and time-consuming endeavor. Recent automation
techniques based on neural methods address this issue, but require good
programmatic support for collecting data and interacting with proof
assistants. This paper presents CoqPyt, a Python tool for interacting with the
Coq proof assistant. CoqPyt improves on other Coq-related tools by providing
novel features, such as the extraction of rich premise data. We expect our
work to aid development of tools and techniques, especially LLM-based,
designed for proof synthesis and repair. A video describing and demonstrating
CoqPyt is available at: https://youtu.be/fk74o0rePM8.

Coq, Data extraction, Theorem proving, Retrieval augmentation

††conference: Companion Proceedings of the 32nd ACM International Conference
on the Foundations of Software Engineering; July 15–19, 2024; Ipojuca
(Pernambuco), Brazil††booktitle: Companion Proceedings of the 32nd ACM
International Conference on the Foundations of Software Engineering (FSE
Companion ’24), July 15–19, 2024, Ipojuca (Pernambuco), Brazil††copyright:
rightsretained††journalyear: 2024††doi: 10.1145/3663529.3663814††isbn:
979-8-4007-0658-5/24/07††ccs: Software and its engineering Software notations
and tools††ccs: Software and its engineering Development frameworks and
environments

##  1\. Introduction

Formal software verification is an incredibly effective method for developing
high quality software, as it ensures that a software program adheres to a
predefined formal specification. For example, a study compared industrial
standard compilers (e.g., GCC and LLVM) to CompCert, a C compiler verified
using the Coq proof assistant (coq, 25), and CompCert was the only one for
which no bugs were found (Yang11a, 30). Unfortunately, even though formal
software verification provides valuable guarantees, its development is still
too costly. CompCert took 100,000 lines of Coq code and 6 person-years to
formally verify (leroy2016compcert, 13). For this reason, it is important to
find methods that decrease the cost of formal verification.

One recent approach to address this is the use of neural methods to automate
proof synthesis. _Neural theorem provers_ , given a partial proof and the
_proof state_ , use neural networks to predict the next likely _proof steps_.
A proof assistant is then used to evaluate the candidate proof steps,
returning either new proof states or errors. Neural theorem provers iterate on
this procedure, performing _proof search_ to traverse the space of possible
proofs. A complementary task is automated proof repair (ringer2021proof, 20),
which is necessary to perform when specifications or dependencies change and
result in broken proofs. To train these neural models and implement proof
search, sufficient programmatic support is thus required for collecting
training examples and driving the theorem prover.

In this paper, our target proof assistant is Coq due to its popularity for
building verified software systems. Existing tools, such as Coq Serapy
(sanchez2020generating, 22) and PyCoq (pycoq, 9), provide programmatic support
for interacting with Coq in Python, and all current neural theorem provers for
Coq utilize them. These tools implement Python bindings for Coq SerAPI
(GallegoArias2016SerAPI, 7), which is a library for machine-to-machine
interaction with Coq. However, with the announcement that Coq SerAPI will be
deprecated and replaced with Coq LSP (coq-lsp, 26), a language server for Coq,
the need arises for a new tool to continue supporting existing features.
Fortunately, this also creates a great opportunity to support new features
that prior tools did not.

In the emerging era of large language models (LLMs), additional functionality
is desirable in tools for interfacing with Coq in Python in order to promote
LLM-based approaches for Coq proof synthesis and repair. Namely, the ability
to collect rich contextual data is not supported by any of the existing
programmatic tools for controlling Coq. LLM-based neural theorem provers for
Lean and Isabelle proof assistants rely on _retrieval augmentation_ , wherein
they retrieve premises, such as lemmas and definitions, that are relevant to
the proof goal, and condition the next tactic generation on those premises
(yang2023leandojo, 29, 17). For the approach to be effective, they collect
fine-grained annotations of which premises are used in proofs as well as which
premises are accessible from a proof. However, existing tools for Coq do not
collect that type of premise data.

Figure 1. UML diagram for a simplified view of the domain of CoqPyt. The
selected attributes and methods are all public.

We introduce CoqPyt, a tool that enables interaction with Coq in Python using
Coq LSP as the backend. CoqPyt continues to support existing capabilities
essential to training data collection and proof search, but goes beyond state-
of-the-art tools for Coq by supporting the ability to collect rich contextual
data, among other novel features. Our tool supports the newest versions of Coq
(8.17 to 8.19), which will facilitate mining software repositories for new,
enriched training and evaluation data. We foresee that our work will help
promote future research into neural proof synthesis and repair for Coq,
especially as LLM capabilities continue to evolve. CoqPyt is open-source and
available at: https://github.com/sr-lab/coqpyt.

##  2\. CoqPyt

CoqPyt is a Python tool that enables developers and researchers to interact
programmatically with Coq. It also allows users to extract textual and
structural information from Coq files. We now describe the structure and main
functionalities of CoqPyt, providing an illustrative example on how to
interact with the tool.

###  2.1. The Coq Proof Assistant

Coq provides an interactive environment with a rich type system suitable for
theorem proving. A theorem in Coq is a type definition, which can be proven by
constructing a _proof term_ with the stated theorem type. Since writing a
proof term directly is difficult, Coq allows users to write a _proof script_
consisting of a sequence of high-level _tactics_ (e.g., induction or
reflexivity). Each tactic guides Coq in a search for the desired proof term,
refining the state until no new obligations hold. After a tactic application,
Coq displays the current _proof state_ , which includes the goals to prove and
the local context. When executed, a complete proof script generates the proof
term.

###  2.2. Coq Language Server Protocol

To interact with Coq files, we use Coq LSP (coq-lsp, 26), a language server
that provides Coq-related features. Coq LSP was developed to replace Coq
SerAPI (GallegoArias2016SerAPI, 7), a well-known tool in the Coq community
that implements a protocol for interacting specifically with Coq files. Unlike
Coq SerAPI, Coq LSP follows a standardized protocol for interacting with text
documents known as Language Server Protocol (LSP) (lsp, 16). LSP servers, such
as Coq LSP, provide useful language features, such as auto complete. Client
applications, such as IDEs, can use these features by running their own LSP
client.

Besides the usual LSP features, Coq LSP provides Coq-specific functionality,
namely requesting the proof state at any given point of a Coq file. Coq LSP
also allows users to request the abstract syntax tree (AST) of the entire
document, which corresponds to a list of steps in the file, each with its own
AST representation. A step can be a term definition (e.g., definitions and
theorems) or a proof step (e.g., mid-proof tactic application), determined by
the AST contents of each step. For erroneous Coq files, Coq LSP is able to
ignore erroneous steps and evaluate the remaining steps of the file, allowing
any subsequent non-erroneous steps to define new terms. Coq LSP also enables
project-wise imports by saving compiled .vo files, which may also benefit from
this error-ignoring approach, given that valid files may still import terms
from invalid files.

###  2.3. Interaction with Coq Files

CoqPyt implements a client for Coq LSP providing the interface shown in Figure
1. This client implementation is encapsulated within CoqFile, a class that
abstracts the state of an actual Coq file, hiding the interaction with Coq
LSP. For instance, the is_valid boolean flag indicates if the underlying Coq
file is valid and the save_vo method allows the user to compile the file.

A CoqFile object provides an exec method which allows users to take an
arbirary number of forward and backward steps through the file. The method
returns a list of Steps corresponding to the steps that were executed or
backtracked during the call. Each step contains its textual representation in
the file and the AST contents.

Given that steps may be term definitions, a FileContext object is kept within
the CoqFile, indexing by name all terms that have been defined until the last
executed step. Any term defined inside a module has its name prefixed by the
module path. Although notations are nameless terms, these are also stored in
the context, indexed by the string pattern used to define them. For each
defined term, a Term object is created containing its corresponding step, as
well as its term type. This type depends on whether the term is a theorem, a
notation, a tactic or any other definable Coq construct.

###  2.4. Proof Navigation

With CoqPyt, it is also possible to track the proof state throughout the file.
A CoqFile can be instantiated through the ProofFile subclass, which allows
users to manage the file’s proof context. As steps are taken, one can enter
(or leave) proof mode, which will activate (or deactivate) the in_proof
boolean flag. If there are any on-going goals, these can be accessed via the
current_goals attribute. Goals are represented as a GoalAnswer object, which
mimics the structure of goals in the Coq LSP response (coq-lsp, 26).

In addition to allowing users to manage a file’s proof context, ProofFile
instances also fetch all of the file’s imported terms. Thus, a ProofFile
captures terms in a file and in its dependencies. In practice, the ProofFile
context is initialized by instantiating a CoqFile for each library imported by
the file and extracting the context of each library to the new ProofFile
instance. Since creating a ProofFile requires instantiating multiple CoqFiles,
it is more expensive to create a ProofFile than a CoqFile.

A ProofFile holds information about all proofs found in the file until the
last executed step. Proofs with open goals are kept in the open_proofs
attribute. Multiple open proofs occur in files with nested proofs, as we need
to open inner proofs before closing outer proofs. Each proof is a ProofTerm, a
Term with a context attribute, listing all terms found in the current context
used to define the proof term. This contextual information is valuable for
neural-based models and is not accessible from prior Coq-related tools.

A ProofTerm also contains an ordered list of ProofSteps, corresponding to all
steps taken until the proof is closed (or until the last executed step if the
proof is open). The ProofStep class enables a mapping from each proof step to
the intermediate proof goals it attempts to solve or simplify. A ProofStep is
thus constructed by augmenting the respective Step with the intermediate proof
goals before that step is taken. Similarly to ProofTerm, a ProofStep also has
a context attribute listing the terms used in the step.

###  2.5. Proof Modification

CoqPyt allows steps to be added to or deleted from the file. Allowing such
modifications on Coq files yields an interface well suited for proof
development. Invalid changes, such as adding inexisting tactics, may lead to
explicit errors or undefined behaviour, depending on the nature of the error.
For erroneous modifications, the file will revert to its original state,
ignoring the requested changes.

Through the add_step method, it is possible to define terms, introduce
theorems and apply tactics to solve proof obligations. Conversely, delete_step
enables the removal of steps, such as added tactics which do not alter the
proof goals as intended. Both methods allow editing in arbitrary parts of the
file: delete_step requires an index i to delete the i${}^{\text{th}}$ step in
the file; add_step requires the index of the step which precedes the new step.
To add a new step, its textual representation must also be provided.

Modifications may also be batched as transactions. A sequence of CoqChanges
can be provided to the change_steps method, which will perform all
modifications. A CoqChange can be either a CoqAdd or a CoqDelete, which serve
as data wrappers for the parameters of add_step and delete_step, respectively.
During the transaction, intermediate invalid states are allowed as long as the
final state is valid. For example, it is possible to add a Qed before adding
the actual proof steps, which cannot be done through successive add_step
calls. To directly modify a proof, ProofFile provides the methods append_step
and pop_step for single step modifications, as well as a change_proof method
for a transaction of ProofChanges.

###  2.6. Use Cases

The features that CoqPyt offers are particularly useful for proof search and
learning-based tasks, such as neural theorem proving. To get a sense of
CoqPyt’s interface for collecting data and conducting proof search, consider
the file test.v in Listing 1, where we have a Coq file that defines a property
about reversing a list. Listing 2 shows how we can leverage CoqPyt to collect
data from the file shown in Listing 1. We can see which terms are available to
the file via the pf.context attribute (line 3). For example, all the terms
from the imported package List.v are available to the proofs in the file.
Likewise, we show how to retrieve information from each proof step in the file
via the ProofStep attributes (line 6).

⬇

1Require Import List.

2Lemma rev_append: forall {a} (l1 l2: list a),

3 rev (l1 ++ l2) = rev l2 ++ rev l1.

4Proof.

5intros a l1 l2. induction l1; intros.

6 - simpl. rewrite app_nil_r. reflexivity.

7 - simpl. rewrite IHl1.

8Admitted.

Listing 1: Example Coq file test.v with a property of rev.

⬇

1with ProofFile("test.v") as pf:

2 pf.exec(len(pf.steps))

3 print(pf.context)

4 for proof in pf.proofs:

5 for step in proof.steps:

6 print(step.text, step.ast, step.context, step.goals)

Listing 2: Proof data available with CoqPyt.

Developing neural-based theorem provers requires the ability to attempt
possibly erroneous proofs during proof search. For example, suppose we wanted
to complete the proof rev_append from Listing 1. Listing 3 shows how we can
use the change_proof method to conduct proof attempts. We first obtain the
ProofTerm object of the proof rev_append (line 5). We then delete the
‘‘Admitted.’’ step from the proof of rev_append (line 7) and add the steps
associated with our new proof attempt (line 9). When we attempt to add the
erroneous steps from the proof attempt incorrect (line 11), an error is
returned and test.v will remain in its original state. In turn, when the valid
steps from the proof attempt correct are added (line 11), the changes are
applied to test.v.

⬇

1incorrect = [" reflexivity.", "\nQed."]

2correct = [" rewrite app_assoc."] + incorrect

3with ProofFile("test.v") as pf:

4 pf.exec(len(pf.steps))

5 unproven = pf.unproven_proofs[0]

6 for attempt in [incorrect, correct]:

7 changes = [ProofPop()] # Admitted

8 for s in attempt:

9 changes.append(ProofAppend(s))

10 try:

11 pf.change_proof(unproven, changes)

12 print("Proof succeeded!")

13 break

14 except InvalidChangeException:

15 print("Proof attempt not valid.")

Listing 3: Proof attempts with CoqPyt. Table 1. Evaluation of CoqPyt’s performance on CompCert. PCC stands for Pearson correlation coefficient. | Count | Execution time (s)
---|---|---
Metric/Feature |  |  |  |  | Add step | Delete step | Change steps (Add) | Change steps (Delete)
Proofs | Steps | Load file | Execute file | Beginning | On pointer | Beginning | On pointer | Beginning | On pointer | Beginning | On pointer
$\mu(\sigma^{2})$ | 32.3 (48.1) | 609.6 (828.1) | 6.6 (7.3) | 31.2 (63.8) | 1.1 (1.8) | 0.9 (1.5) | 1.0 (1.7) | 0.9 (1.6) | 1.5 (2.7) | 1.0 (1.7) | 1.1 (1.8) | 0.8 (1.5)
$\tilde{x}$ | 12.0 | 258.0 | 3.9 | 9.6 | 0.4 | 0.3 | 0.3 | 0.3 | 0.5 | 0.3 | 0.4 | 0.3
PCC (steps) | - | 1.00 | 0.59 | 0.72 | 0.90 | 0.92 | 0.94 | 0.92 | 0.87 | 0.92 | 0.90 | 0.91

##  3\. Related Work

Most neural theorem provers for Coq use either Coq Serapy
(sanchez2020generating, 22, 24), PyCoq (tactician, 2), or a custom Python
class (yang2019learning, 28, 5, 23, 4) to create training examples and perform
proof search. The neural theorem prover GamePad (Huang2019Gamepad, 8) instead
modifies Coq itself to record intermediate proof states. The CoqGym benchmark
dataset (yang2019learning, 28), collected using a Python class, is the state-
of-the-art benchmark for Coq. However, it was collected in 2019 and has only
been updated to support versions 8.10 and 8.12 of Coq, while the newest
version is 8.19. CoqPyt will render neural theorem provers useful for new Coq
developments since it can be used for mining software repositories for newer
Coq training data and for evaluation.

LeanDojo (yang2023leandojo, 29) and PISA (jiang2021lisa, 10) are learning
environments for Lean and Isabelle, allowing for data extraction and proof
search interaction. The neural theorem provers that use these environments are
LLM-based and use retrieval augmentation (Jiang2022Thor, 11, 17, 29). CoqPyt
would enable retrieval augmented LLM approaches in Coq.

Pretrained LLMs have been shown to have quantitative reasoning capabilities
(palm, 3, 27, 18), especially when they undergo continued training on math
data (Lewkowycz2022Minerva, 14, 1). To synthesize proofs, they can be fine-
tuned on proof data (first2023baldur, 6, 29, 10), few-shot prompted
(azerbayev2023llemma, 1, 12, 31), or even zero-shot prompted
(thakur2023languageagent, 24, 29). However, the question of test leakage
arises in any evaluation that uses pretrained LLMs. CoqPyt will allow for data
collection after the pretraining cutoff date.

During proof development, proof engineers are constantly performing proof
repair (ringer2020replica, 21). The first work in automating this task uses
symbolic tools for automated proof repair in Coq (ringer2021proof, 20), and
has since been applied to other proof systems (masci2022proof, 15). Baldur is
the first work to use neural methods (in particular, LLMs) to repair proofs,
but as part of its proof synthesis approach (first2023baldur, 6). With the
creation of a large-scale dataset of proof repair instances (reichel2023proof,
19), the creation of LLM methods to automate real-world proof repairs is
forthcoming.

##  4\. Evaluation

Table 2. Feature comparison between CoqPyt and similar tools (✓full support, $\sim$ partial support, ✗ no support).  Feature | CoqPyt | Coq LSP | Coq Serapy
---|---|---|---
Get proof state | ✓ | ✓ | ✓
Check file validity | ✓ | ✓ | ✓
Execute/Modify steps | ✓/✓ |  $\sim$/✗ |  ✓/$\sim$
Extract step context | ✓ | ✗ | ✗
Track modules/terms/proofs | ✓/✓/✓ | ✗/✓/✗ |  ✓/✗/$\sim$

#### Feature Evaluation

Table 2 compares the features of CoqPyt to similar tools. When compared to Coq
LSP, CoqPyt supports a more extensive range of features by using the data
supplied by Coq LSP and constructing additional components of Coq program
logic upon it. For instance, Coq LSP provides partial support for operating
with steps by enabling retrieval of the proof state at any position of the
file. However, it lacks implementation for navigating backward or forward from
a specific step, which is provided by CoqPyt. Compared to Coq Serapy, CoqPyt
offers complete support for an additional four features:  (1) modifying steps
– while Coq Serapy supports the addition or deletion of steps at the current
point of execution, it does not offer the capability to add or delete steps at
arbitrary positions within the file;  (2) extract step context – Coq Serapy
does not collect the terms used in each step;  (3) track terms – Coq Serapy
does not retain a record of the terms defined up to the current execution
point;  (4) track proofs – even though Coq Serapy supports commands such as
navigating to the next proof, it does not maintain a record of all the proofs
already defined in a file.

#### Performance Evaluation

To evaluate CoqPyt’s performance, we used the project CompCert
(leroy2016compcert, 13) since it is a popular project with over 1,700 stars on
GitHub and 259 Coq files with considerable complexity. We ran the experiments
inside a Docker container on an Intel Xeon Silver 4210R CPU @ 2.40GHz. Table 1
summarizes our results. CoqPyt was able to run on 193 files, 58 files
contained Coq-related errors, 6 files generated out-of-memory errors, and 2
files crashed for unknown reasons. The column _Count_ describes metrics for
the number of steps and proofs of CompCert. We ran all the features in each
Coq file. For features that modify steps, we performed the modification in the
beginning of the file and at the current point of execution, after executing
the whole file. We performed each case 5 times for each feature. This approach
is driven by the understanding that the number of required operations for
these features increases as the distance to the point of execution rises. To
evaluate change_steps, we performed a single addition or deletion to make it
simpler to compare to the other features. The results for file execution are
dependent on a cache that saves our loading of Coq libraries. As more
libraries were cached, the time to execute the files decreased. By calculating
the Pearson correlation coefficient, we conclude that the execution time for
all features is positively correlated to the number of steps in a file. A
replication package is available at: https://zenodo.org/records/10292580.

##  5\. Conclusion

We developed CoqPyt, a Python tool for interacting with Coq. It offers
valuable features previously unavailable in similar Coq-related tools, namely
per-step context extraction and arbitrary file and proof modification. CoqPyt
does not yet explore the full potential of context extraction, as it does not
consider a small subset of Coq’s rich environment (e.g., module types and
section-local constructs) nor does it fetch context recursively, i.e., for
each term in a step context we ignore the context of the term itself.
Nonetheless, we have shown that CoqPyt provides rich features and reasonable
execution times, enabling an expressive interaction style with Coq. These
contributions are expected to ease the automation of machine-checked proof
synthesis and repair in the emerging era of LLMs.

## Acknowledgements

This work was partially funded by NSF, National Science Foundation grants
CCF-1955457 and CCF-2220892, and by FCT, Fundação para a Ciência e a
Tecnologia, under grant BD/04736/2023 and project UIDB/50021/2020
(DOI:10.54499/UIDB/50021/2020).

## References

  * (1) Zhangir Azerbayev et al.  “Llemma: An Open Language Model For Mathematics”, 2023  arXiv:2310.10631
  * (2) Lasse Blaauwbroek, Josef Urban and Herman Geuvers  “The Tactician”  In _Intelligent Computer Mathematics_ , CICM 2020  Springer, Cham, 2020, pp. 271–277  DOI: 10.1007/978-3-030-53518-6˙17
  * (3) Aakanksha Chowdhery  “PaLM: Scaling Language Modeling with Pathways”  In _CoRR_ abs/2204.02311, 2022  DOI: 10.48550/arXiv.2204.02311
  * (4) Emily First and Yuriy Brun  “Diversity-driven automated formal verification”  In _Proceedings of the 44th International Conference on Software Engineering_ , ICSE ’22  Pittsburgh, Pennsylvania: Association for Computing Machinery, 2022, pp. 749–761  DOI: 10.1145/3510003.3510138
  * (5) Emily First, Yuriy Brun and Arjun Guha  “TacTok: semantics-aware proof synthesis”  In _Proceedings of the ACM on Programming Languages_ 4.OOPSLA, 2020  DOI: 10.1145/3428299
  * (6) Emily First, Markus Rabe, Talia Ringer and Yuriy Brun  “Baldur: Whole-Proof Generation and Repair with Large Language Models”  In _Proceedings of the 31st ACM Joint European Software Engineering Conference and Symposium on the Foundations of Software Engineering_ , ESEC/FSE 2023  San Francisco, CA, USA: Association for Computing Machinery, 2023, pp. 1229–1241  DOI: 10.1145/3611643.3616243
  * (7) Emilio Jesús Gallego Arias  “SerAPI: Machine-Friendly, Data-Centric Serialization for Coq”, 2016  URL: https://hal-mines-paristech.archives-ouvertes.fr/hal-01384408
  * (8) Daniel Huang, Prafulla Dhariwal, Dawn Song and Ilya Sutskever  “GamePad: A Learning Environment for Theorem Proving”  In _ICLR_ , 2019  URL: https://openreview.net/forum?id=r1xwKoR9Y7
  * (9) IBM  “pycoq”, https://github.com/IBM/pycoq, 2021
  * (10) Albert Q. Jiang, Wenda Li, Jesse Michael Han and Yuhuai Wu  “LISA: Language models of ISAbelle proofs”  In _6th Conference on Artificial Intelligence and Theorem Proving_ , 2021
  * (11) Albert Qiaochu Jiang et al.  “Thor: Wielding Hammers to Integrate Language Models and Automated Theorem Provers”  In _Advances in Neural Information Processing Systems_ 35, NeurIPS 2022  Curran Associates, Inc., 2022, pp. 8360–8373
  * (12) Albert Qiaochu Jiang et al.  “Draft, Sketch, and Prove: Guiding Formal Theorem Provers with Informal Proofs”  In _The Eleventh International Conference on Learning Representations_ , 2023  URL: https://openreview.net/forum?id=SMa9EAovKMC
  * (13) Xavier Leroy et al.  “CompCert - A Formally Verified Optimizing Compiler”  In _ERTS 2016: Embedded Real Time Software and Systems, 8th European Congress_ , 2016  SEE  URL: https://inria.hal.science/hal-01238879
  * (14) Aitor Lewkowycz et al.  “Solving Quantitative Reasoning Problems with Language Models”  In _CoRR_ abs/2206.14858, 2022  DOI: 10.48550/arXiv.2206.14858
  * (15) Paolo Masci and Aaron Dutle  “Proof Mate: An Interactive Proof Helper for PVS (Tool Paper)”  In _NASA Formal Methods Symposium_ , 2022, pp. 809–815  Springer
  * (16) Microsoft  “Language Server Protocol”, https://microsoft.github.io/language-server-protocol, 2023
  * (17) Maciej Mikuła et al.  “Magnushammer: A Transformer-based Approach to Premise Selection”, 2023  arXiv:2303.04488
  * (18) OpenAI  “GPT-4 Technical Report”, 2023  arXiv:2303.08774
  * (19) Tom Reichel et al.  “Proof repair infrastructure for supervised models: Building a large proof repair dataset”  In _14th International Conference on Interactive Theorem Proving (ITP 2023)_ , 2023  Schloss-Dagstuhl-Leibniz Zentrum für Informatik  DOI: 10.4230/LIPIcs.ITP.2023.26
  * (20) Talia Ringer  “Proof Repair”, 2021
  * (21) Talia Ringer, Alex Sanchez-Stern, Dan Grossman and Sorin Lerner  “REPLica: REPL instrumentation for Coq analysis”  In _Proceedings of the 9th ACM SIGPLAN International Conference on Certified Programs and Proofs_ , CPP 2020  New Orleans, LA, USA: Association for Computing Machinery, 2020, pp. 99–113  DOI: 10.1145/3372885.3373823
  * (22) Alex Sanchez-Stern, Yousef Alhessi, Lawrence Saul and Sorin Lerner  “Generating correctness proofs with neural networks”  In _Proceedings of the 4th ACM SIGPLAN International Workshop on Machine Learning and Programming Languages_ , MAPL 2020  London, UK: Association for Computing Machinery, 2020, pp. 1–10  DOI: 10.1145/3394450.3397466
  * (23) Alex Sanchez-Stern et al.  “Passport: Improving Automated Formal Verification Using Identifiers”  In _ACM Transactions on Programming Languages and Systems_ 45.2, 2023  DOI: 10.1145/3593374
  * (24) Amitayush Thakur, Yeming Wen and Swarat Chaudhuri  “A Language-Agent Approach to Formal Theorem-Proving”, 2023  arXiv:2310.04353
  * (25) The Coq Development Team  “Coq – Release 8.19.1”, https://coq.inria.fr, 2024
  * (26) The Coq LSP Development Team  “Coq LSP – Release 0.1.8”, https://github.com/ejgallego/coq-lsp, 2024
  * (27) Hugo Touvron et al.  “Llama 2: Open Foundation and Fine-Tuned Chat Models”, 2023  arXiv:2307.09288
  * (28) Kaiyu Yang and Jia Deng  “Learning to prove theorems via interacting with proof assistants”  In _Proceedings of the 36th International Conference on Machine Learning_ 97 PMLR, 2019, pp. 6984–6994
  * (29) Kaiyu Yang et al.  “LeanDojo: Theorem Proving with Retrieval-Augmented Language Models”  In _Advances in Neural Information Processing Systems_ 36, NeurIPS 2023  Curran Associates, Inc., 2023, pp. 21573–21612
  * (30) Xuejun Yang, Yang Chen, Eric Eide and John Regehr  “Finding and understanding bugs in C compilers”  In _Proceedings of the 32nd ACM SIGPLAN Conference on Programming Language Design and Implementation_ , PLDI ’11  San Jose, California, USA: Association for Computing Machinery, 2011, pp. 283–294  DOI: 10.1145/1993498.1993532
  * (31) Shizhuo Dylan Zhang, Talia Ringer and Emily First  “Getting More out of Large Language Models for Proofs”  In _8th Conference on Artificial Intelligence and Theorem Proving_ , 2023  arXiv:2305.04369