A Mechanized First-Order Theory of Algebraic Data Types with Pattern Matching

Algebraic data types form the backbone of functional programming languages; with recursion and exhaustive pattern matching, they enable elegant, concise, and type-safe functions over all kinds of list- and tree-like data. Reasoning about such functions requires only simple induction, and many proof assistants (e.g. Rocq, Lean, Isabelle) make heavy use of functional programming and induction. For instance, Rocq and Lean are implementations of the Calculus of Inductive Constructions (CIC), which extends the Calculus of Constructions with inductive types. But even SMT-based tools which target simpler first-order logic without induction still want to allow reasoning about ADTs, pattern matching, and/or recursive functions at the source level (see §2) – e.g. Dafny [28], VeriFast [22] and Frama-C [24] for C, Gobra [43] for Go, and Creusot [17] for Rust. In fact, these facilities are so useful that many intermediate verification languages upon which these deductive verifiers are built also include such features – both Why3 [10] (the back-end of Frama-C and Cruseot) and Viper [34] (the back-end of Gobra) have support for ADTs; Why3 additionally includes pattern matching and recursion. These SMT-based tools must axiomatize recursive types into first-order formulas. The exact set of axioms may vary; they typically include assertions of injectivity, disjointness, inversion, and non-circularity.

Similarly, while complex, nested, and simultaneous pattern matches are very useful at the source level, they must be compiled to simpler patterns in the underlying logic. In Rocq, this compilation is performed by the front-end, so the user sees the compiled version when printing a term. In SMT-based tools, this compilation occurs when ADTs are axiomatized; the resulting compiled matches can be replaced with let-bindings and case analysis. ML and Haskell compilers must also eliminate pattern matching; many schemes have been studied and implemented [32, 27, 26]. The underlying algorithms are broadly similar in all these cases, though the correctness proofs depend on the setting – eager, lazy, or purely logical.

It is vital that these compilation steps are sound or else a verifier could “prove” something false. This is especially important because ADTs and their semantics are central to many verifiers, enabling many useful constructs (pattern matching, recursive functions, inductive predicates) while relying on subtle checks to provide guarantees of well-foundedness (e.g. strict positivity, termination checking, pattern matching exhaustiveness). Despite the centrality of these features, existing verifier formalizations often omit them. Neither Featherweight VeriFast [23], a formalization of a core subset of VeriFast, nor a proof-producing version of Viper [16] include ADTs, though the underlying tools do. Meanwhile, the MetaRocq formalization of CIC within Rocq [39] includes only simple patterns, assuming that Rocq’s front-end has already done the pattern matching compilation.

A key difficulty is in specifying the semantics against which to prove such compilation steps correct. Cohen and Johnson-Freyd [14] addressed this by giving a Rocq formalization of the semantics of the Why3 logic (we will refer to this semantics as Why3Sem), which includes (mutually recursive) ADTs and pattern matching. Using Why3Sem, we take a key step towards filling this formalization gap by giving a mechanized proof of the Why3 pattern matching compiler and ADT axiomatization. Many of our results and methods are not specific to Why3 and would extend to other similar systems provided they had an appropriate formal semantics. In particular, we make the following contributions:

1. 1.

   We give the first verified implementation of a sophisticated, general-purpose pattern matching compiler (based on the technique of Maranget [32]).

2. 2.

   We use this compiler to implement exhaustiveness checking for Why3Sem, prove several results about the correctness and robustness of such matching (which extend proofs in the literature), and discover an exhaustiveness-related bug in Why3.

3. 3.

   We use this to give the first mechanized proved-sound first-order axiomatization of ADTs.

The problem of compiling pattern matches to simpler constructs like decision trees is well-studied (§10), particularly for ML and Haskell compilers. Why3’s pattern matching compiler is based on pattern matrix decomposition and is very similar to the techniques of Le Fessant and Maranget [27] and Maranget [32], which form the basis of the algorithm used in the OCaml compiler. We describe Why3’s algorithm in detail, discuss its termination (§4), prove its soundness (§5), detail how it is used to implement exhaustiveness checking (§6), and describe an exhaustiveness bug we discovered in Why3 (§7). Though we implement the exact algorithm found in Why3, the technique is quite general and many of our proofs could be reused in other contexts.

As is standard [27, 32], we view the (simultaneous) pattern match as a matrix $P$ (Figure 2 shows an example); we will refer to the last column in the matrix as “actions” (in our case, terms or formulas). Patterns consist of variables, wildcards, constructors, disjunctions, and as-patterns; we will show later that we can assume the first column contains only wildcards and constructors. We then define two decompositions (Figure 3): specialization for constructor $c$ ($S(c,P)$) and the default matrix ($D(P)$). Specialization gives the remaining matrix if the term in the first column is an instance of constructor $c$; it removes all non-$c$ constructors from the matrix, replaces $c$ with its $k$ arguments, and replaces a wildcard with $k$ wildcards. The default matrix gives the result assuming that $t$ does not match any of the constructors appearing in the first column.

With these decompositions, we can define the compile algorithm (Figure 4). We demonstrate compile on the example of Figure 2, which includes both nested and simultaneous matching. The first column contains both constructors; the specialized matrices are:

$l_1$’s constructor is unknown, so applying Step 3c results in the following partial match:

We focus on the first case. $P_1$ again contains both constructors; the specialization matrices are $P_3:=S(\text{nil},P_1)=\left(\begin{array}{c}{x}_1\end{array}\right)$ and . Expanding gives:

Each case can be simplified easily. The first compile evaluates to $x_1$ by Step 2, while the second evaluates to $x_4$ by repeated applications of Step 3a. The $P_2$ case is broadly similar; we omit the details but show the full compiled pattern match:

This example also demonstrates how the algorithm checks exhaustiveness. Suppose we had not included the last case in the original pattern match $(x_4)$. Then, $P_1$ (i.e. $S(\text{nil},P)$) is , and the first match again results in compile($l_2,P_1$). Here we are again in Step 3c, but we find that $S(\text{cons},P_1)$ is empty, triggering Step 1 and causing the compilation to fail.

Now we fill in implementation details missing from Figure 4. The simplify transformation removes all non-constructor, non-wildcard patterns from the first column. It expands disjunctions and replaces variables at the outer level with let-bindings in the action column (it does not expand within constructors). Note that $\overline{p}$ represents the rest of the columns in the matrix, $t_1$ is the first matched term, and $++$ again represents concatenation (i.e. gluing matrices together):

Our implementation, consistent with Why3, computes simplify, $D$, and all $S$ matrices in a single pass, but we prove equivalence with a version that allows us to reason separately and assume the matrix is simplified when considering $S$ and $D$.

Why3 implements the check in Step 3c that all ADT constructors appear in the first column in 2 ways: either the caller provides a function to retrieve the list of constructors for an ADT or compile relies on metadata from the constructor function symbols. The former requires more information but is useful for reporting unmatched cases (which we do not consider). We prove the two equivalent in any well-typed context.

The first difficulty with formalizing compile is proving termination – the function recurses on non-structurally-smaller matrices $S(c,P)$ and $D(P)$. A termination argument is very tricky, as the matrix both expands (in simplify and in the wildcard case for $S(c,P)$) and contracts (in $D(P)$ and the constructor case of $S(c,P)$). Thus, several natural candidates for decreasing measures (e.g. the total size of the patterns in the matrix) fail. To build intuition, we first consider the case when there are no disjunctions. Here, we can almost use the total matrix size as a measure. The only complication is that the $S(c,P)$ case would not decrease unless the constructor size decreases by enough to offset the additional $k$ wildcards. However, this wildcard increase can be statically bounded, so we could set the constructor size appropriately. Therefore, a version of compile that first expanded all disjunctions terminates. We lift this to the general case by considering the total size of the fully expanded matrix (which is never actually computed), parameterized by the constructor increase.

More formally, we give the definition of the full expansion of a pattern matrix ($E^M(P)$) in Figure 5. The difficult case is for constructor patterns: we must expand the entire row of arguments, which involves concatenating all the resulting expansions of each pattern in the row. We then define a size function $|\cdot {|}_n$ on patterns, pattern-lists, and pattern-matrices, where $n$ is a parameter describing the extra fuel added to the constructor case: ${|c(ps)|}_n=n+{\sum }_{p\in ps}{|p|}_n$. To give a suitable upper bound, we let $m$ be the largest number of arguments that any constructor in the matrix $P$ takes. In the worst case, every row in the matrix but one starts with a wildcard, causing $m$ new wildcards to appear per row. Thus, the total amount of measure added is bounded by $\mathrm{len}(P^{\prime })\ast m$, where $\mathrm{len}(P^{\prime })$ is the number of rows of the current matrix $P^{\prime }$. Since $P^{\prime }$ is created via calls to simplify, we can upper bound $\mathrm{len}(P^{\prime })$ by $\mathrm{len}(E^M(P))$. We let $b(P)=\mathrm{len}(E^M(P))\ast m$. The full termination metric is then ${|E^M(P)|}_{b(P)+1}$. Proving that compile terminates according to this measure involves 4 key steps:

1. 1.

   We show that simplification does not change full expansion: $E^M($simplify$(P))=E{}^M(P)$.

2. 2.

   We show the default case decreases: $\forall n$, . This is not too hard to show, as either constructors or wildcards are removed when constructing $D$.

3. 3.

   For the specialization case, we show that if constructor $c$ appears in the first column of $P$ and takes $k$ arguments, ${|E^M(S(c,P))|}_n+n\le {|E^M(P)|}_n+\mathrm{len}(E^M(P))\ast k$. This proof is complex, as we must reason about the nested expansions for constructors.

4. 4.

   Finally, since ($b(P)+1$) depends on $P$, we show monotonicity: if $n\le m$, ${|P|}_n\le {|P|}_m$. We also show that $b$ does not decrease: $b(D(P))\le b(P)$ and $b(S(c,P))\le b(P)$.

We combine these results to prove that compile terminates. However, none of this was specific to compile – we effectively proved that any algorithm based on pattern matrix decomposition terminates via this metric. More sophisticated algorithms [32, 27] follow the same basic structure but with additional optimizations (e.g, not always examining the first column, swapping columns, data structure sharing, etc); this termination metric should suffice in these settings with almost identical proof.

We implement compile in Rocq using Equations [40] and this size metric. Our function is parametric in the action type, constructor-finding method, and a flag governing Step 3b (see §7), returning an option that is None if the match is non-exhaustive.

We want to prove the semantic correctness of compile. To state this theorem, we first define the semantics of matching against a pattern matrix (${⟦al,P⟧}_v^M$), which builds on pattern- and row-matching (Figure 1).

Namely, ${⟦al,P⟧}_v^M$ (Figure 6) iterates through each row until it finds a match (with ${⟦\cdot ⟧}^R$), then evaluates the matched action under the valuation $v$ extended with the new bindings (this reduces to match_rep for a single-column matrix). We define ${⟦ts⟧}_v^T$ to be the (heterogeneous) list generated by ${⟦t⟧}_v^t$ for each $t$ in $ts$ (recall that ${⟦t⟧}_v^t$ is the interpretation for terms under valuation $v$). Then the correctness theorem is:

In other words, if compile succeeds and produces term $t$, then the pattern match succeeds and results in a term semantically equivalent to $t$. The proof involves many pieces.

First, we prove that simplify preserves the semantics. Note that a row beginning with a disjunction becomes multiple rows in the simplified matrix; we must prove that the semantics of the resulting matrix is equivalent to that of the original row. Additionally, since simplify transforms variable patterns into let-bindings, this changes a simultaneous binding into an iterated one, causing problems if variable names overlap. For example, given match y, z with | x, y $\to$ f x y end, the result should be equivalent to f y z. However, simplify gives let y = z in (let x = y in f y x), equivalent to f z z. To avoid this, we require the condition on variable names in Theorem 1. Then we prove:

Next, we reason about the matrices $D(P)$ and $S(c,P)$, assuming that the input matrix is simplified and well-typed. First, we define the notion “term $t$ is semantically equivalent to $c(al)$” (i.e. ${⟦t⟧}_v^t={⟦c⟧}^{\lambda }(al)$) for constructor $c$ in ADT $a$; we call this predicate tm_semantic_constr. Then we prove that, given any term $t$ of ADT type $a$, we can find the constructor $c$ and arguments $al$ such that tm_semantic_constr $t$ $c$ $al$; this is a direct consequence of find_constr_rep (§2). We prove that, if term $t$ is semantically equal to $c(al)$, matching $t$ against pattern $c(ps)$ is the same as matching $al$ against $ps$:

The proof is straightforward, relying on the definition of ${⟦\cdot ⟧}^p$ and the injectivity and disjointness of constructor interpretations (§2). Similarly, we then prove that if tm_semantic_constr holds of a different constructor, then the term does not match:

Along with some additional lemmas about concatenation of pattern-rows, we now have all the pieces to prove the $D$ and $S$ cases. Recall that $D(P)$ is intended to represent the remaining pattern match if the term $t$ does not match any constructor in the first column of $P$. We prove this property in 2 parts: either $t$ has ADT type and matches a constructor that does not appear in the first column or $t$ does not have ADT type:

The proofs are simple; the first follows by Lemma 4, while the second uses the fact that there can be no constructors in the first column by typing. Next, recall that $S(c,P)$ is intended to represent the remaining pattern match if the term $t$ matches constructor $c$. Unlike $D$, the remaining match is not just the rest of the rows; rather, we must first match the arguments of the $c$-patterns. The formal statement is:

We reason by induction on $P$. In the case where the first row starts with $c(ps)$, we split the pattern-row concatenation, using Lemma 3 to reason about the $c(ps)$ match. The case where the first row starts with $c^{\prime }(ps)$ ($c\ne c^{\prime })$ is similar; we use Lemma 4. Lastly, in the wildcard case, we prove that matching a row against all wildcards gives Some $\mathrm{\varnothing }$. With this, we have all the pieces we need for the proof of Theorem 1. The full proof is quite complex; we give a sketch of an interesting case.

An exhaustiveness check follows as an immediate corollary of Theorem 1.

In other words, if there is an interpretation such that the match is semantically non-exhaustive, then compile will correctly fail (return None). However, this is a fairly weak specification: compile could always return None and satisfy Theorem 1 (and hence Corollary 8).

It is worthwhile to compare and contrast this with existing pen-and-paper proofs of a virtually identical scheme to prove non-exhaustiveness by Maranget [31]. Maranget discusses two versions of exhaustiveness checking: for ML-like call-by-value languages and for Haskell-like lazy languages. The theorems can be summarized as, “the exhaustiveness check on pattern matrix $P$ of types $tys$ returns “non-exhaustive” iff there is a value list $vs$ of type $tys$ such that $vs$ does not match $P$” (where matching is defined as a syntactic relation on value-vectors). The difference is that lazy values also include an unknown value $\mathrm{\Omega }$ and the exhaustiveness check must be generalized by a disambiguating predicate.

By contrast, our setting is purely logical, not evaluation-based. Why3’s logic does not have any notion of values, and terms can include free variables or uninterpreted symbols. This means that unlike the syntactic match relation in Maranget’s theorems (defined over values), we can only reason about matching semantics under a particular interpretation and valuation. However, once an interpretation/valuation are fixed (and we reason semantically rather than syntactically), the setting becomes similar to the call-by-value one. But there is still a crucial difference: uninterpreted symbols can be interpreted as any constructor; such ambiguity is not present for values.

Similarly, lazy matching is distinct from our setting. Here, Maranget’s proofs require a monotonicity property so that a failing match will continue to fail as values are partially evaluated. This relies on an ordering relation on values such that $\mathrm{\Omega }$ is smaller than all others. Once again, our setting has no such ordering, partial evaluation, or monotonicity, but if we reason semantically and quantify over interpretations, we can recover similar concepts. For example, we can re-interpret the ordering relation as denoting the existence of an interpretation that produces semantic equality (e.g. $v\le w\iff \exists I,{⟦v⟧}_I^t={⟦w⟧}_I^t$). This satisfies similar properties – non-constructor terms are “smaller” than all constructors while different constructors are incomparable – but it would be very inconvenient to reason about. Therefore, we can view our proofs as broadly similar to (both of) Maranget’s but significantly simpler when reasoning in a purely logical setting where the meaning of terms is given by a particular interpretation rather than by (full or partial) evaluation.

It would be possible to state and prove the reverse direction of Maranget’s theorem translated to our setting: if compile returns None, there is an interpretation $I$ and term list $ts$ that does not match (${⟦{⟦ts⟧}_I^T,P⟧}_I^M=$ None). Equivalently, if matching succeeds for all interpretations and for all terms of the correct type, then compile returns Some. We do not formally prove such a result (soundness is sufficient for our applications), though we do need a weaker version – if the pattern match is simple (consisting only of wildcards and constructors applied to variables) and “obviously” exhaustive (either all constructors in an ADT are present or there is a wildcard), then compile always succeeds. Note that many programs in practice fall into this category (e.g. many standard functions on lists and trees).

While Why3 includes exhaustiveness checking, Why3Sem previously omitted it. We fix this by adding a check to the Why3Sem type system, requiring that for any term or formula $\text{match }t\text{ with }ps\text{ end}$, $\text{compile}[t]ps$ is Some (where $ps$ becomes a single-column matrix). Since compile produces a pattern match in Step 3c, we must prove that this match itself passes the exhaustiveness checker. We prove this by showing that compile produces simple, obviously exhaustive patterns.

The larger difficulty is to show that the existing functions over Why3 terms that preserve typing also preserve the exhaustiveness check. Writing such a theorem is surprisingly difficult; such functions modify the term list (e.g. for substitution and rewriting), the term and pattern types (for type substitution), the action type (when axiomatizing recursive functions), and the variables in the pattern matrix (for $\alpha$-conversion). In the end, we need a generic robustness theorem to show that exhaustiveness checking still succeeds under such changes. Of course the conditions cannot be too permissive: changing the pattern matrix arbitrarily clearly does not preserve exhaustiveness; neither does changing the types so that a constructor match no longer succeeds. In the end, the latter turns out to be the trickier condition to formalize, as we need to ensure that an ADT type cannot be transformed into a non-ADT type. We encode this as an asymmetric relation ty_rel. We finally require that the two pattern matrices have the same “shape” – they are equal up to changing variable names.

We will state such a robustness theorem shortly, but unfortunately it does not hold of Why3’s compile. If we allow the term list to change arbitrarily, a check that succeeds due to Step 3b may then fail. For example, given match [1] with | [x] $\to$ x end and the equality H: [1] = y, if one rewrites with H, the resulting term fails the exhaustiveness checker and Why3 crashes with a fatal error. While rewriting in such a “backwards” manner is unlikely in practice, this non-robustness also rules out potential optimizations like constant subexpression elimination. This is a bug in Why3 which we reported.³³3https://gitlab.inria.fr/why3/why3/-/issues/903

One possible fix is to remove Step 3b of compile. This is the common approach to exhaustiveness checking (e.g. in Rocq and OCaml). But Why3 uses this step to compile simultaneous matching, implemented via tuples. Instead, we parameterize compile by a flag simpl_constr indicating whether Step 3b is used. In our Rocq development, we prove the soundness of compile for both versions. For exhaustiveness checking, we set simpl_constr to false, so that a robustness theorem (Theorem 9) holds; for compilation, simpl_constr should be true to make the resulting patterns as simple as possible for the eventual SMT queries. We discuss the connection between the two versions of compile in §8.4. Here, we give the full robustness theorem.

The proof is similar to Theorem 1; we prove the cases for simplify, $S$, $D$, and compile.

We have endeavored to keep our proved-correct implementations of compile_match and eliminate_algebraic as close as possible to their Why3 counterparts. These have proven useful in practice, both in Why3 itself and in tools like EasyCrypt [7] which supports ADTs, pattern matching, and recursive functions by compiling to Why3. While compile and compile_match are virtually identical to the Why3 implementation, our version of eliminate_algebraic differs from the Why3 version slightly (it is stateless and requires all types in a mutual block to be axiomatized or kept) but produces similar output.

Furthermore, we note that our proofs could extend to other solvers and settings. As we discussed in §8, we could follow a nearly identical approach for other ADT axiomatizations. Our pattern matching compiler is quite general: it already allows arbitrary term-like action types, the termination proofs would be useful for any matrix-decomposition-based method, and the proofs of soundness could be refactored to remove dependence on Why3Sem (though it is crucial that the semantics for pattern matching behaves like match_rep). We note also that our proofs do not rely on axioms beyond those already present in Why3Sem (classical logic, functional extensionality, and indefinite description); other than UIP, these axioms are only needed to define Why3Sem and thus our proofs would suffice in intutitionistic settings.

We have presented a sophisticated, real-world pattern matching compiler and exhaustiveness checker along with a first-order axiomatization of ADTs, the first such implementations mechanized and proved sound in a proof assistant. These features and compilation steps are critical in enabling powerful assertion languages that allow users to express elegant, functional specifications amenable to logical reasoning. Proved-correct implementations make it possible to retain these advantages while ensuring that the verifier is foundationally sound. Additionally, since our transformations are computable functions within a proof assistant, they could be directly connected to higher level language semantics (e.g. CompCert) or verifiers (e.g. VST) to improve automation without compromising soundness guarantees.