Trocq [5] is both the name of a calculus, describing a parametricity framework, and of a Coq plugin [6] that provides tactics for performing representation changes in goals, as well as vernacular commands for specifying the expected translations. More precisely, from an initial goal of type , the tactic simultaneously computes using the Trocq calculus [5] a translation and a justification . If successful, the user is thus left with proving .

The plugin orchestrates this double synthesis, by assembling existing building blocks known to the tactic, in the course of a linear traversal of the input term . These building blocks are of two natures. First, the actual rules of the parametricity framework [5] govern the synthesis rule attached to each term construction of \(CC_{\omega }\). The other nature of building blocks is the collection of registered pairs of user-defined constants. These pairs come equipped with a witness of their relatedness at some level, a data registered via the command. When the linear traversal of the input term hits a constant, it queries the database registering these user-defined relations, looking for the corresponding constant and witness to be used in the synthesis.

The Trocq plugin is implemented in Elpi [9]: a dialect of \(\lambda \) Prolog which can be used as a meta-language for Coq, through the Coq-Elpi [20] plugin. The latter encodes Coq terms in higher-order abstract syntax (HOAS) which provides native support for bound variables, complemented by a comprehensive API (typechecking, elaboration, interacting with the global environment, etc).

1 Example

Let us translate the induction principle associated with type , the unary representation of \(\mathbb {N}\), to type , the binary one. Types  and  are equivalent and we use the command to register such pairs of related types:

figure m

Proof  coerces to a relation of type , and we also register proofs that it relates the respective zero and successor constants of these types:

figure p

We can now use tactic  to prove a useful induction principle on type :

figure s

Inspecting the proof term actually reveals that univalence was not needed in the proof of . The example directory of the artifact provides more examples, for weaker relations than equivalences, and beyond representation independence.

2 Architecture of the plugin

A Trocq parametricity sequent \(\varDelta \vdash _t M\ @\ A\,\sim \,M'\ \because \ M_R\) expresses that terms M and \(M'\) are related at type A with witness \(M_R\) in context \(\varDelta \). Unlike standard, unequivocal parametricity translations, each construct of \(CC_{\omega }\) gives rise to a family of possible synthesis rules, indexed by annotations on M and A.

Encoding \(CC_{{\omega }^{+}}\). To implement the annotation calculus \(CC_{{\omega }^{+}}\), we just annotate Coq’s sort with a pair (n, m) using convertible synonyms , where . The two thrown-away arguments code for the annotation. In the course of the synthesis, arguments of certain occurrences of are left as holes and filled by a constraint solving algorithm.

Synthesis. The logic programming paradigm on which Elpi is based, is ideal to implement algorithms expressed as inference rules, as each rule can be associated to an instance of a predicate. The linear traversal of the input term at the core of the Trocq plugin is operated by the predicate , of arity 4, where stands for the parametricity sequent \(\varDelta \vdash _t x\ @\ T\,\sim \,x'\ \because \ x_R\) for a certain context \(\varDelta \). In this sequent, x and T are input values (initially, the source goal and the annotated sort \(\Box ^{(0,1)}\)), and the synthesized term \(x'\) and witness \(x_R\) are outputs. Each construct of \(CC_{\omega }\) leads to one instance of the predicate. As an example, let us inspect the instance of the predicate for dependent products, which implements the rule TrocqPi of the Trocq calculus. For the sake of readability, we removed lines related to logs, pretty-printing, and fresh universe instance generation. The head of the predicate is:

figure ab

which matches an input term \(\varPi x : A.\,B\) and our Coq encoding of its annotated type \(\Box ^{(M_1, M_2)}\). Then, following the hypotheses in the inference rule, the predicate computes the prescribed annotation \((C_A, C_B) = \mathcal {D}_\varPi (C)\), and does two recursive calls on A and B with classes \(C_A\) and \(C_B\):

figure ac

The last step (omitted in the above snippet) is to build the output proof \(p_\varPi ^{C}\ A_R\ B_R\). As the axioms (univalence, functional extensionality) that might be involved in some proofs are not assumed globally, they are used as an additional argument albeit only in the building blocks that require them. Therefore, we check whether the requested rule requires the addition of an axiom to the list of arguments (in the case of the dependent product, function extensionality). If this axiom is not present in the context at the time of calling this part of the code, the tactic rightfully fails, because the translation is impossible.

Exploiting symmetries. Trocq provides several distinct rules per language construct (such as \(\varPi \)) and per relation structure among the 36 items in the hierarchy: for a same construct, these rules differ by the annotations required on the input of the rule, and by the structure of the relation relating the input term and the synthesized one. For each such rule, a Coq function provides the corresponding rule building block. Making the most of symmetries, the 495 rule building blocks are generated by meta-programming from only 9 manually defined ones.

Handling of constants. Finally, the traversal of the input term collects constraints on the annotations, as multiple valid solutions might exists: for instance, an implication might be obtained from weakening an equivalence. The algorithm strives to minimize the requirements on the user-defined building blocks, which also amounts to minimizing the dependency on axioms. This inference procedure is formalized as a finite domain constraint solving problem, and implemented using Constraint Handling Rules (CHR) language [10], as available in Elpi.

3 Related work

In the context of type theory, Barthe and Pons [3] already noticed that the computational content of type isomorphisms can serve proof transfer. The first implementation report of a tool based on this idea appeared soon after [16]. Implemented in a meta-language and based on proof rewriting, this heuristic translation produced a candidate proof term from an existing proof term, with no formal guarantee, not even that of being well-typed. Generalized rewriting [17], which generalizes setoid rewriting to preorders, is also a variant of proof transfer, albeit within the same type. As such, it allows in particular rewriting under binders. The restriction to homogeneous relations however excludes more general instances of proof transfer, e.g., , datatype representation change and quasi-PERs (QPER, or zig-zag complete relations) [13], essentially heterogeneous.

The other proof transfer methods we are aware of all address the case of heterogeneous relations. Incidentally, they can thus also be used for the homogeneous case, and thus for generalized rewriting, although this special case is seldom emphasized. The Coq Effective Algebra Library (CoqEAL) [7, 8] and the Isabelle/HOL transfer package [11, 12, 14, 15], pioneered the use of parametricity-based methods for proof transfer, motivated by the refinement of proof-oriented data-structures to computation-oriented counterparts. Together with a subsequent generalization of the CoqEAL approach [21], these tools address the case of a transfer between a subtype of a certain type A and a quotient of a certain type B, i.e., the case of a trivial QPER in which the zig-zag morphism is a surjection from A to B.

Modern approaches to proof transfer rely on univalence, either as an axiom, in the case of univalent parametricity [19] or as a computing primitive [2]. Key ingredients of univalent parametricity were already present in earlier seemingly unpublished work [1], implemented using an ancestor of the MetaCoq library [18].

The columns of Table 1 lists these tools in chronological order, and indicates when the features listed as lines are available (), not available () or only partially available (). Transfer along heterogeneous relations, and while the oldest tool operates via a monolithic translation of an input proof term, others rather prove an internal implication lemma. Anticipation [19] refers to the need to define a dedicated structure for the signature to be transported. Binders (\(\forall \)) can prevent transfer, as well as dependent types, which require univalence.

Table 1. Comparison of proof transfer automation devices
Full size table