Towards Automating Permutation Proofs in Rocq: A Reflexive Approach with Iterative Deepening Search

The concept of permutations of a list is intuitive, yet readily formalized, and is useful for specifying and reasoning about the properties and behavior of a variety of data structures and algorithms. The Rocq (formerly Coq) proof assistant Standard Library provides an inductive definition of permutations as compositions of adjacent transpositions of elements of a list.¹¹1https://rocq-prover.org/doc/V8.20.0/stdlib/Coq.Sorting.Permutation.html The library additionally provides quite a large set of derived properties for reasoning about permutations. However, proving non-trivial permutation relationships between lists, especially in the context of transitivity and premises involving permutations of sublists, quickly turns into a tedious exercise of finding the right swapping order and transitive substitutions to solve the goal.

In this paper, we present the implementation of a fully automated tactic for proving complex goals involving permutations of lists (of arbitrary element type) described as the concatenation of their constituent portions, where some or all of those portions may be universally quantified variables (as opposed to concrete values of the element type). Figure 1 provides an example of a goal state that can be solved by the tactic.

Our approach uses proof by reflection (see Section 2) and is implemented entirely within the Rocq system itself. We first generate an environment mapping natural number labels to distinct pieces of all lists formed by concatenation operations. For every list in the proof context, a tree of natural numbers is constructed, such that substituting for the numbers based on the mapping environment results in (i.e. reflects into) the original list. Then, we implement a unification procedure on the sets of labels collected from the leaves, which takes into account substitutions representing permutation facts that occur as hypotheses in the context. The algorithm performs an iterative deepening search process to explore possible substitutions in order to unify the values between the two label sets in question. Finally, we prove that if the unification procedure succeeds, it means that the original two lists (corresponding to the trees of numbers, under the mapping environment) are permutations according to the standard library formulation.

In what follows, we review a few examples of permutation-based reasoning in existing Rocq developments (including the particular context that motivated the tactic described in this paper) and discuss related and prior work that inspired our tactic. We then present details of the implementation and conclude with a discussion of future directions.

Sorting is perhaps the most obvious algorithmic process for which the property of the output “having the same elements as” the input is crucial. Indeed, the initial textbook on the Rocq system [2] presents the specification of a sorting program as a motivating example. Rather than using the current standard library definition of Permutation, it introduces a relation on lists that is based on counting the number of times any element appears in both lists. As noted there, this definition is convenient for reasoning about properties, but actually “does not provide a way to determine whether two [concrete] lists are permutations of each other.”

The Verified Functional Algorithms volume [1] of the Software Foundations series presents additional algorithms and data structures for which proving correctness depends on reasoning about whether two collections have the same contents. In this development, the standard library’s inductive formalization of Permutation is adopted and used not only for sorting algorithms, but also for verifying properties of abstraction relations and representation invariants on data structures such as priority queues. As the formalization of these classical data structures is fairly straightforward, it is only mildly tedious to work with the existing standard library lemmas to manually guide proofs involving permutation relationships.

In a more substantial development, [10] developed a formalization of k-d trees in Rocq, utilizing the standard library definition of Permutation for specifying correctness properties of procedures that involve sorting and partitioning input and intermediate data points. That work noted that lack of automation for reasoning about Permutations resulted in significantly complex and tedious proof effort. The goal in Figure 1, for example, is adapted from one of the proof states in that development. Proving this goal using only the standard library facilities requires a long set of lemma invocations to reorder list components, interspersed with appeals to transitivity properties on sub-portions of the lists.

Reasoning about permutations also appears to be an important part of formalized Rocq libraries related to rewriting theory, termination, and program transformation [6, 3, 7]. Contejean [6] notes that most of the formal proofs “actually concern the permutations of the lists…” and “…the proofs are quite long since there are many subcases.”

As far as existing work towards automating reasoning about permutations, there are only a few perfunctory developments that we are aware of. Braibant and Pous [5] describe a general-purpose Rocq plugin for rewriting modulo associativity and commutativity with some limited application to lists and permutations. The Rocq Reference Manual provides an example of writing a tactic to prove that a list is a permutation of a second list, based on an alternate inductive definition of the concept, but it only works on lists with concrete individual elements.

An online GitHub repository [8] provides a tactic that transforms Permutation goals into solving multiplicity calculation (an alternate, deprecated definition of the notion of permutations based on multisets in the Rocq standard library). In its current form, this tactic is limited to reasoning about lists of natural numbers, although in theory it could be generalized to any type with decidable equality and would appear to be able to solve goals with the same level of complexity as the tactic described in this paper. The requirement of decidable equality for the domain of the list elements, however, introduces the need for “a more complex apparatus,” which is unnecessary for our tactic. [8] relies on the omega (now lia) tactic, a decision procedure for linear integer arithmetic, to trivially solve equations over the group of natural numbers with addition once the permutation statements have all been transformed into multiplicity equations. Preliminary comparisons on goals involving lists of nat indicate that our tactic produces much smaller proof terms, reflected in the size of compiled script files. It is unclear how the time to check the larger proof terms compares to the computation time for our reflection-based tactic. Further analysis and comparison of space and time efficiency of these two approaches remains as an item for future work.

Our tactic utilizes the technique of proof by reflection [4, 2], in which explicit reasoning steps (i.e. on a permutation goal) are transformed into some implicit computation that is carried out by the proof assistant. A theorem is then separately established that shows that the result on the computational values is reflected as a property on the original terms (i.e. that a pair of lists satisfies the Permutation predicate). We also adapt some inspirations from prior approaches [9, 2] such as building binary trees of nat values, flattening, and using the Ltac metalanguage to program a reification tactic, all described in the next section.

In Section 3.1, we step through the overall approach of our tactic, perm_solver, on the goal state of Figure 1, to give a general idea of how it operates. Section 3.2 describes the computational “unification” algorithm, followed by an overview in Section 3.3 of the metaprogramming tactics implemented to reify list objects and apply the reflective technique.

To date, we have utilized our perm_solver tactic to rewrite proofs from the k-d tree verification proofs of [10]. The results appear to be significant, with some 707 lines ($\sim 20\%$) reduced out of 3277 lines of definitions and proof scripts – some of this due to refactoring of the scripts supported by the incorporation of perm_solver. It thus seems promising that the tactic would help speed up proof developments that use the Permutation definition. In future work, we would like to validate its utility on a broader scale – seeking out existing developments for which it could be adopted and/or promoting its use along with the standard library’s notion of Permutation where appropriate.

In the short term, we anticipate porting the implementation to Rocq’s Ltac2, in line with recommended practice. Along with that, it would be interesting to incorporate support for proving goals related to Permutation, such as the List.In predicate or length properties.

The unification algorithm as presented is certainly not complete. Since it is depth-limited, it is straightforward to formulate contrived examples where it fails to successfully unify lists when it should (i.e., a situation where the minimum number of substitutions needed exceeds the maximum depth). In practice however, so far, we have found that the iterative deepening approach works fine, even in pathological cases where there are a large number of Permutation assumptions in the proof context. We have not profiled the algorithm, but we did investigate the use of Rocq’s binary representation of numbers and the incorporation of sorting lists into a canonical form. Since the reified lists of numeric labels are usually short, neither of these optimizations was worth the effort – we found that implementing them did not produce noticeable improvement in speed; and the sorting perhaps even introduced additional overhead. Use of Rocq’s positive type speeds up comparison of numeric values, but does not affect the recursion depth of any of the key functions which dominate the run time. It would be ideal to discover a more sophisticated, efficient, and/or complete decision procedure for the unification process. At a very minimum, future improvement might focus on a pre-processing step to clear unrelated permutation facts/substitutions from the environment before the main work of the tactic.