14 Executable pebble game
The formal pebble game on a graph \(G\) (definition 13.26) cannot be computed, since it uses mathlib’s lists of finite sets (formalization note 13.15). In this section we define the computable pebble game on \(G\), which uses lists sorted by a linear order on \(V\) instead. With it we define procedures that decide, for \(\ell {\lt} 2k\), whether a finite graph is \((k, \ell )\)-sparse or \((k, \ell )\)-tight, and whether it is Laman. These procedures can be run in Lean, and a command-line program uses the computable pebble game to decide whether a graph read from a file is Laman.
In section 14.1 we define the sorted lists, and in section 14.2 the computable pebble game. It needs no new correctness argument: its verdict accepts \(G\) if and only if \(G\) is \((k, \ell )\)-sparse (theorem 14.7). We define the three decision procedures in section 14.3, and describe three ways to run them in section 14.4. We list the examples on which they are run in section 14.5, and describe the command-line program in section 14.6. As for the formal pebble game, we prove no bound on the running time of the computable one (section 13).
14.1 Sorted lists
The formal pebble game uses mathlib’s lists in two places. The pebble search follows the arcs of \(D\) along the lists \(N^+_D(a)\) of out-neighbours (definition 13.9), and the pebble game on \(G\) runs on a list of the edges of \(G\) (definition 13.14). We replace both with lists sorted by a linear order on \(V\).
Let \(V\) be a set with a linear order, and let \(D\) be a partial orientation on \(V\) (definition 13.1). For \(v \in V\), the sorted out-neighbour list of \(v\) in \(D\) is the list of the out-neighbours of \(v\) in \(D\), the vertices \(u\) with \((v, u) \in D\), in increasing order.
Let \(V\) and \(D\) be as in definition 14.1, and let \(u, v \in V\). Then \(u\) is an entry of the sorted out-neighbour list of \(v\) in \(D\) if and only if \((v, u) \in D\).
Sorting a finite set lists each of its elements, and nothing else.
So the sorted out-neighbour lists are lists \(N^+_D(a)\) as in section 13.3.
Let \(V\) be a set with a linear order, and let \(G\) be a simple graph on \(V\) with finitely many edges. The sorted edge list of \(G\) is the list of the pairs \((\min e, \max e)\), for the edges \(e\) of \(G\), in lexicographic order. Here \(\min e\) and \(\max e\) are the smaller and the larger end of \(e\).
Let \(V\) and \(G\) be as in definition 14.3, and let \(u, v \in V\). Then \((u, v)\) is an entry of the sorted edge list of \(G\) if and only if \(u \le v\) and \(uv \in E(G)\).
Sorting a finite set lists each of its elements, and nothing else. So the entries are the pairs \((\min e, \max e)\) for \(e \in E(G)\). Such a pair \((u, v)\) has \(u \le v\) and \(e = uv\). Conversely, if \(u \le v\) and \(uv \in E(G)\), then \((u, v) = (\min uv, \max uv)\).
14.2 The computable pebble game
With the sorted lists, the pebble game on a list (definition 13.14) gives a pebble game on \(G\) that can be computed.
Let \(V\) be a finite set with a linear order, let \(G\) be a simple graph on \(V\), and let \(k\) and \(\ell \) be non-negative integers with \(\ell {\lt} 2k\). The computable pebble game on \(G\) runs the pebble game on the sorted edge list of \(G\) (definition 14.3) from the empty orientation, with the sorted out-neighbour lists (definition 14.1) as the lists \(N^+_D(a)\). It returns the verdict on \(G\) (definition 13.25) that is an acceptance, given by \(D\), if the game returns a partial orientation \(D\), and a rejection, given by \(V'\), if the game returns a failure witness whose set is \(V'\).
The computable pebble game is formalized as the forms of the pebble game that take the lists as an argument (formalization note 13.15), applied to the sorted lists. Sorting a finite set by a linear order needs no choice, so the sorted lists, and with them the game, can be computed. Only a definition that can be computed can be run by #eval or native_decide. A verdict consists of a partial orientation or a set of vertices together with proofs, and proofs are erased in compiled code. So the compiled program computes only the pebble game.
The verdict is well defined, as for the formal pebble game (the paragraph after definition 13.26). The sorted edge list lists the pairs \((u, v)\) with \(u {\lt} v\) and \(uv \in E(G)\), in increasing order (lemma 14.4). So it lists each edge of \(G\) once, and theorem 13.24 applies to it. By its part (1), a returned \(D\) has \(\underline{D} = E(G)\), and \(D\) is \((k, \ell )\)-reachable, as is every orientation that the game reaches. By its part (2), whose proof uses lemma 13.22 and \(\ell {\lt} 2k\), a returned \(V'\) is a blocking witness for \(G\).
Let \(V\) be a finite set with a linear order, let \(G\) be a simple graph on \(V\), and let \(k\) and \(\ell \) be non-negative integers with \(\ell {\lt} 2k\). Then \(G\) is \((k, \ell )\)-sparse if and only if the verdict that the computable pebble game on \(G\) returns accepts \(G\).
The computable pebble game returns an acceptance when the pebble game on the sorted edge list returns a partial orientation, and a rejection when it returns a failure witness (definition 14.5). So its verdict accepts \(G\) if and only if this game returns a partial orientation. The entries of the sorted out-neighbour list of a vertex are its out-neighbours (lemma 14.2). The sorted edge list lists each edge of \(G\) once (lemma 14.4). So theorem 13.24 applies, and the game returns a partial orientation if and only if \(G\) is \((k, \ell )\)-sparse.
14.3 Deciding sparsity, tightness and the Laman property
A decision procedure for a proposition \(P\) returns either a proof of \(P\) or a proof of its negation. In Lean it is an instance of Decidable \(P\), and a command or a tactic that decides \(P\) uses the one registered for \(P\) (section 14.4). We register decision procedures for three properties of a finite graph with a linear order on its vertices. The one for \((k, \ell )\)-sparsity runs the computable pebble game. Those for \((k, \ell )\)-tightness and the Laman property add a count of the edges.
Let \(V\) be a finite set with a linear order, let \(G\) be a simple graph on \(V\), and let \(k\) and \(\ell \) be non-negative integers with \(\ell {\lt} 2k\). The decision procedure for the \((k, \ell )\)-sparsity of \(G\) runs the computable pebble game on \(G\) (definition 14.5). If the verdict accepts \(G\), it returns a proof that \(G\) is \((k, \ell )\)-sparse, and otherwise a proof that \(G\) is not, both by theorem 14.7.
The procedure takes the hypothesis \(\ell {\lt} 2k\) as a registered fact, so that a command or a tactic finds the procedure without being given a proof. The fact \(3 {\lt} 2 \cdot 2\) is registered, so at \((k, \ell ) = (2, 3)\) the procedures of this subsection apply with no hypothesis given.
As \(V\) is finite, whether \(G\) is \((k, \ell )\)-sparse can also be decided by checking the inequality of definition 3.1 for each of the \(2^{|V|}\) subsets of \(V\). A procedure of this kind decides the same proposition, but on a sparse graph it checks all \(2^{|V|}\) subsets. We register only the procedure of definition 14.8 for sparsity, and build the procedures for tightness and the Laman property on it. So a command or a tactic that decides one of these properties runs the pebble game.
Let \(V\), \(G\), \(k\) and \(\ell \) be as in definition 14.8. The decision procedure for the \((k, \ell )\)-tightness of \(G\) decides whether \(G\) is \((k, \ell )\)-sparse by definition 14.8, and whether \(|E(G)| + \ell = k|V|\) by computing both sides. It returns a proof that \(G\) is \((k, \ell )\)-tight if both hold, and otherwise a proof that \(G\) is not (definition 3.3).
Let \(V\) be a finite set with a linear order, and let \(G\) be a simple graph on \(V\). The decision procedure for the Laman property of \(G\) is the decision procedure for the \((2, 3)\)-tightness of \(G\) (definition 14.11), since \(3 {\lt} 2 \cdot 2\) and a graph is Laman if and only if it is \((2, 3)\)-tight (definition 4.1).
14.4 Runtime and backends
A decision procedure registered for a proposition \(P\), such as “\(G\) is Laman” for a given graph \(G\), can be run in three ways.
The command #eval decide \(P\) runs the procedure in Lean’s interpreter, and prints its answer, true or false. The examples of section 14.5 are run in this way.
The command-line program lake exe pebble-game of section 14.6 runs the computable pebble game, compiled to native code.
The tactic native_decide proves \(P\) by running the compiled procedure. The proof rests on an axiom, added for it, that states the program’s answer. So it trusts Lean’s compiler, and mathlib does not accept such proofs. It proves that the graph obtained from \(K_4\) by deleting an edge is Laman, and that \(K_4\) is not.
The tactic decide would instead prove \(P\) by evaluating the procedure by reduction, trusting only Lean’s type checker. It does not evaluate these procedures. The processing of an edge (definition 13.12) and the search of definition 12.2 are defined by well-founded recursion, which decide does not unfold. With the option +kernel, decide leaves the reduction to the type checker itself, which does unfold that recursion but does not evaluate the sort that builds the sorted lists of section 14.1. It proves that the graph on two vertices with its one edge is Laman, but not that the graph obtained from \(K_4\) by deleting an edge is. A Lean file in the repository, scripts/DFSTiming.lean, checks these facts, and those about native_decide above. It is not a module of Lean’s module system: in a module, the type checker sees the body of a definition from another module only if that module exports it, and there decide +kernel does not prove even that the graph on two vertices with its one edge is Laman.
14.5 Worked examples
We run the decision procedures with #eval on four graphs, each on the vertices \(\{ 0, \ldots , n - 1\} \) for some \(n\). The file that does so, PebbleGame/Examples.lean in the Lean library, records the expected answer beside each evaluation, and the procedures return it.
The graph on \(\{ 0, 1, 2, 3\} \) obtained from \(K_4\) by deleting the edge \(23\) has \(4\) vertices and \(5 = 2 \cdot 4 - 3\) edges, and it is Laman (theorem 5.14). The procedure for the Laman property answers true.
The Moser spindle on \(\{ 0, \ldots , 6\} \) consists of the triangles \(012\) and \(034\), a vertex \(5\) adjacent to \(1\) and \(2\), a vertex \(6\) adjacent to \(3\) and \(4\), and the edge \(56\). It has \(7\) vertices and \(11 = 2 \cdot 7 - 3\) edges, and the procedure for the Laman property answers true.
The complete graph \(K_4\) on \(\{ 0, 1, 2, 3\} \) has \(6\) edges, more than \(2 \cdot 4 - 3 = 5\), so it is not \((2, 3)\)-sparse. The procedures for sparsity and for the Laman property answer false. So the computable pebble game rejects \(K_4\) (theorem 14.7), and its blocking witness is \(\{ 0, 1, 2, 3\} \). Indeed a blocking witness has at least two vertices (definition 13.13), and a set \(X\) of two or three vertices spans \(2|X| - 3\) edges of \(K_4\).
The path on \(\{ 0, \ldots , 4\} \) with the edges \(01\), \(12\), \(23\) and \(34\) is \((2, 3)\)-sparse, since a set of \(s \ge 2\) of its vertices spans at most \(s - 1 \le 2s - 3\) edges. It has \(4\) edges, fewer than \(2 \cdot 5 - 3 = 7\), so it is not \((2, 3)\)-tight and not Laman. The procedure for sparsity answers true, and those for tightness and the Laman property answer false.
14.6 CLI binary
The command lake exe pebble-game file runs a program that reads a graph from a file and decides whether it is Laman. The first line of the file is \(n\) \(m\), the numbers of vertices and of edges. Each of the next \(m\) lines is \(u\) \(v\), for an edge between the vertices \(u\) and \(v\), where \(0 \le u, v {\lt} n\). Numbers on a line are separated by spaces or tabs, a line may end in a carriage return, and blank lines and lines that start with # are skipped. If the file does not have this form, the program prints an error message.
The program takes for \(G\) the simple graph on \(\{ 0, \ldots , n - 1\} \) whose edges are the pairs read, leaving out a pair with \(u = v\). It runs the computable pebble game on \(G\) with \((k, \ell ) = (2, 3)\), and prints the following.
If the verdict is an acceptance, given by \(D\): the line LAMAN if \(|E(G)| + 3 = 2n\), and SPARSE_NOT_TIGHT otherwise; then a line ARCS \(u\) \(v\) for each arc \((u, v)\) of \(D\), in lexicographic order.
If the verdict is a rejection, given by \(V'\): the line NOT_SPARSE, then the line BLOCKING \(|V'|\), then a line VERTEX \(w\) for each \(w \in V'\), in increasing order.
By theorem 14.7 and definition 4.1, the first line is LAMAN if \(G\) is Laman, SPARSE_NOT_TIGHT if \(G\) is \((2, 3)\)-sparse but not Laman, and NOT_SPARSE if \(G\) is not \((2, 3)\)-sparse. The reading of the file and the printing are not verified. The directory examples/ holds the four graphs of section 14.5 as input files, each with its expected output in a comment at the top.