We show how to translate the Calculus of Inductive Constructions (CIC) as implemented by Coq into the -calculus modulo, a proposed common backend proof format for heterogeneous proof assistants. Veri cation of large developments will rely increasingly on a combination of heterogeneous provers, each being adapted to a particular aspect of the speci cation to realize. The question of the validity of the whole proof quickly arises. A way to recover con dence over all parts of the proofs is to translate them into a unique, simple but strong enough, formalism, in which they are all checked. A good candidate for such a formalism is the -calculus modulo, a simple yet extensible logical framework that conserves good properties of proofs, as presented in a companion paper [3]. A proof checker based on it, called Dedukti, has been developed by the rst author. It was shown that many proof systems, if not all, can be encoded into the -calculus modulo, including HOL [7], pure type systems [4], resolution proofs for rst-order logic, etc. In this paper, we present how to translate proofs of the Coq proof assistant into this formalism. This translation has been implemented in a tool called CoqInE1, making it possible to use Dedukti to check Coq's developments. The core formalism implemented by Coq, the Calculus of inductive Constructions (CIC), is an immensely expressive type theory. As implemented by Coq, it embeds all other systems of the -cube [1], includes local and global de nitions, full dependent inductive datatype de nitions, guarded xpoint de nitions and pattern matching, large eliminations, as well as a cumulative hierarchy of universes, to name but a few features. None of these features are native to the -calculus modulo in its bare form, which we call the -calculus. Encoding speci cations and proofs from such a powerful formalism is therefore a good benchmark as to the adaptability and versatility of the -calculus modulo, and its convenience as a common proof format for all manner of systems. The calculus of inductive constructions (CIC) is an extension of the calculus of constructions (CC), which is a type system for the -calculus with dependent types. [4] provides a sound 1Available at https://github.com/gburel/coqine.
2.1
and conservative encoding of all pure type systems, including CC, into the -calculus modulo
(see also in [
In this paper, we use Dedukti's syntax for the -calculus modulo, where x : A -> B
denotes the dependent product, x : A => B denotes the abstraction ( la Church) and
[ ] l --> r. is the rule rewriting l to r, being the typing context of the free variables
of l. Following [
es : Us -> Type. dots1 : Us2. [] es2 dots1 --> Us1.
The rst is called a universe constant, for which we also have an associated decoding function
("s). For each axiom s1 : s2 in fProp : Type; Set : Typeg, [
[
CIC extends CC such that it becomes possible to de ne inductive types. In our translation, each time an inductive type is de ned, we add new declarations and rewrite rules corresponding to the type. To give an intuition, let us rst present how a concrete example, namely the vector indexed type, is translated.
Indexed vectors are de ned in Coq by: Inductive vector (A : Type) : nat -> Type :=
where nat is itself an inductive type with constructors O and S. The translation consists rst in declaring two corresponding types in -calculus modulo: vector : A : Utype -> (eset nat) -> Utype. pre__vector : A : Utype -> (eset nat) -> Utype.
The pre__vector will be used to tag constructors. This will be useful for xpoints (see next section). First, we give constants for each constructor, building a pre__vector:
CoqInE: Translating CIC into -modulo As we can see above in the case of the constructors of nat, constructors are guarded by a constant vector__constr allowing to pass from pre__vectors to vectors: vector__constr : A : Utype -> n : eset nat ->
etype (pre__vector A n) -> etype (vector A n).
Thus, the translation as a term of a constructor applied to its arguments will use this guard: jVnil Aj = vector__constr jAj (nat__constr O) (Vnil j j A ) jVcons A a n vj = vector__constr j j (nat__constr S (jnj)) (Vcons jAj jaj jnj jvj).
A If a constructor is only partially applied, we use -expand it during translation. For the sake of readability, we now hide __constr guards using italics : O represents nat__constr O, Vnil
To translate pattern matching, we also add a case constant: vector__case : A : Utype ->
P : (n : eset nat -> vector A n -> Utype) -> fVnil : etype (P O (Vnil A)) -> fVcons : ( a : A -> n : eset nat -> v : etype (vector A n) ->
P (S n) (Vcons A a n v) ) -> n : eset nat -> m : etype (vector A n) ->
etype (P n m). together with two rewrite rules, one for each constructor: [A : Utype, P : ...] vector__case A P fVnil fVcons O (Vnil A) --> fVnil. [...] vector__case A P fVnil fVcons (S n) (Vcons A a n v) --> fVcons a n v.
We now turn to the general case. Following the notations of Coq's manual [
When the type t of the inductive type is of the form x1 : t1: : : : xn : tn: s, we also de ne a guarding constant: I__constr : x1:jjt1jj -> -> xn:jjtnjj -> es (pre__I x1 xn) -> es (I x1 xn).
For each constructor c : x1 : t1: : : : xp : tp: y1 : s1: : : : yl : sl: Ix1 : : : xp u1 : : : un p we declare a constant: c : x1 : jjt1jj -> es (pre__I x1 -> xp : jjtpjj -> y1 : jjs1jj -> xp ju1j jun pj).
-> yl : jjsljj -> The translation as a term of a constructor applied to its arguments will therefore be: jc p1 : : : pp r1 : : : rlj = I constr jp1j : : : jppj jv1j : : : jvn pj (c jp1j : : : jppj jr1j : : : jrlj) where vi = uifp1=x1; : : : ; pp=xp; r1=y1; : : : ; rl=ylg.
To translate pattern matching, we also add a case constant: -> xn : jjtnjj -> where P is the return type, and we have fc for each constructor, representing the corresponding branch of the matching. We then add a rewrite rule for each constructor: [...] I__case x1 ... xp P ... fc ... ju1j ... jun pj
(I__constr x1 ... xp ju1j ... jun pj (c x1 ... xp y1 ... yl) --> fc y1 ... yl. 2.3
For each xed point in a term, we add a new constant with an associated rewrite rule. Since rewrite rules are de ned globally, this constant must take as parameters the context of the xed point, that is, all bounded varables above the position of the xed point.
Given a xed point Fixfiff1=k1 : A1 := t1 : : : fn=kn : An := tng in a context x1 : B1, . . . , xm : Bm, assuming Ai is yi1 : Ai1: : : : yiki : Aiki : A0i where Aiki is an inductive type Iiwi1 : : : wili of sort s, we obtain the following declarations: f1 : x1 : jjB1jj -> ... -> xm : jjBmjj -> jjA1jj. [x1 : jjB1jj, ..., xm : jjBmjj, y11 : jjA11jj, ..., yk1-1 : jjA1k1 1jj, z1 : es (pre__I1 jw11j ... jw1l1 j)] f1 x1 ... xm y11 ... y1k1-1 (I1__constr jw11j ... jw1l1 j z1) wl1 --> jt1j y11 ... y1k1-1 (I1__constr jw11j ... j 1 j z1). . .
. fn : x1 : jjB1jj -> ... -> xm : jjBmjj -> jjAnjj. [x1 : jjB1jj, ..., xm : jjBmjj, yn1 : jjA1njj, ..., ynkn-1 : jjAknn 1jj, zn : es (pre__In jwn1j ... jwnln j)] fn x1 ... xm yn1 ... ynkn-1 (In__constr jwn1j ... jwnln j zn)
--> jtnj yn1 ... ynkn-1 (In__constr jwn1j ... jwnln j zn).
The Ii__constr prevents the reduction of the xed point unless a constructor is present as its kith parameter, which is exactly its semantics. Then, Fixfiff1=k1 : A1 := t1 : : : fn=kn : An := tng is translated as fi x1 . . . xm where the xi are the actual variables of the context of the xed point. Because of dependent types, it is not possible to have a rewrite rule for the unfolding of the xed point for each constructors of the inductive type. Indeed, the arguments wij of the inductive type Ii can depend on yik, and this can be incompatible with the type of the constructors. For instance, if we had a xed point Fixf ff : A : Set: x y : A: p : x =A y: P := tg, the following rewrite rule would be ill-typed: f : A : Uset -> x : eset A -> y : eset A -> p : eprop (eq A x y) -> jjP jj. [A:Uset, x:eset A, y:eset A] f A x y jeq ref l A xj --> jtj A x y jeq ref l A xj. because jeq ref l A xj has type eprop (eq A x x) and not eprop (eq A x y). This is the reason why we choose to translate constructors with the guarding constant I__constr.
Another solution would have been to duplicate the argument on which structural induction is based, one copy serving to match a constructor, the other being used to typecheck the body of the xed point. Concretely, on the example above, this would give: f : A : Uset -> x : eset A -> y : eset A -> p : eprop (eq A x y) -> jjP jj. [...] f A x y p -> f' A x y p A x y p. f' : A : Uset -> x : eset A -> y : eset A -> p : eprop (eq A x y) ->
A' : Uset -> x' : eset A' -> y' : eset A' -> p' : eprop (eq A' x' y') -> jjP jj. [...] f' A x y p A' x' x' (eq_refl A' x') --> jtj.
We plan to implement this second solution in a future version of CoqInE, since it avoids doubling the size of ground terms (i.e. terms build using only constructors).
Note that Dedukti does not check that the rewrite system terminates, in particular the
rules corresponding to the xed points. Indeed, the philosophy behind Dedukti is to have
di erent tools for each purpose. The termination of the system corresponding to a xed point
should, however, be checkable using a tool based on size-based termination [
Coq features a powerful system of modules, with functors and re ned structures. However, Dedukti understands only a notion of namespaces, lacking anything close to a full edged module system.
To be able to translate functors, our choice is to parameterize each de nition of a structure by all the parameters of the argument module. Then, for functor application, we need to apply all arguments of the applied module in each de nitions. Concretely, if we have the following de nitions in Coq:
Module P := N(M). we obtain the following modules in Dedukti: In module M.dk: a : Utype. [] a --> dotprop. b : Uprop. [] b --> dotpitp dotprop (p : etype dotprop => p). In module N.dk: x : fp_a : Utype -> fp_b : etype fp_a -> etype fp_a. [fp_a : Utype, fp_b : etype fp_a] x fp_a fp_b --> fp_b. In module P.dk: x : etype M.a. [] x --> N.x M.a M.b. 2.5
Since in CIC there are in fact an in nity of universes, we cannot declare constants Us, es, etc. for each of them. A rst solution would be to restrict oneself to the universes actually used in the module we are translating. This number is nite and typically very small 2. However, this solution is not modular, since there are de nitions that are polymorphic with respect to the universes. Typically, the list type takes as rst parameter an argument of type Type for all universes, so that it can be seen as a family of inductive types. If a module uses list on a higher universe than those that were used when list was de ned, we would have to duplicate its de nition.
A better solution would be to have sorts parameterized by universe levels. Although technically possible, it should be proved that this provides a sound and conservative encoding of CIC. Currently, we bypass this issue by translating all universes by Type, and having dottype : Utype. Of course, this is not sound, since Girard's paradox can be reproduced.
Another issue concerns subtyping of sorts. Indeed, in CIC, if t : T ype(i) then t : T ype(j) for
all j i. Rewrite rules could be used to encode subtyping, for instance Utype i --> Utype j,
but only if they are applied at positive positions. Since subtyping is contravariant, at negative
positions, the dual rule Utype j --> Utype i should be used. Nevertheless, such a mechanism
of polarized rewrite rules [
CoqInE takes a Coq compiled le (.vo) and translates it into a Dedukti input le (.dk). Concretely speaking, a Coq compiled le contains a copy of the Coq kernel's in-memory representation of a module marshalled to disk. Since the marshalling facility is provided by the OCaml compiler, the format of the content in a .vo le is dependent both on the version of the compiler that compiled Coq, and also the version of Coq itself. Reading a Coq compiled le is a simple matter of unmarshalling the data, as implemented in the OCaml standard library.
The advantage of this scheme is that it avoids having to write a parser to read Coq proofs. Moreover, this ensures that the translation is performed on exactly the same terms that are used in Coq: on the contrary, an export of Coq's terms into another format could be unsound. And last but not least, it makes it easy to reuse part of Coq's code, because the data structures used to represent a Coq module are identical. In fact, CoqInE started as a fork of Chicken, a stripped down version of the Coq kernel. However, this has to following drawbacks: the same version of OCaml as the one used to compile Coq has to be used to compile CoqInE; The close coupling between the data structures of CoqInE and those of the Coq implementation means that CoqInE is tributary to Coq's implementation: core data structures change frequently between Coq releases (as happened between versions 8.2 and 8.3 for instance) and these changes need to be ported to CoqInE's codebase every time. A better scheme would be to harness an export facility to a generic and stable format. Coq can already export proof snippets in XML. Unfortunately, however, this facility does not currently scale up to all the content of a full module.
2For instance, it is possible to type all of the Coq 8.2 standard library using only 4 levels of universes.
CoqInE is able to translate 256 modules of the standard library of Coq out of 304 (84%). The main features that are missing to translate the whole library are the following: coinductive types are not supported for the moment. A mechanism for handling lazy terms would be needed to get them. We cannot rely on abstracting terms to avoid their reduction, because Dedukti reduces terms under abstractions when it checks their convertibility. Also, translation of modules is not complete, in particular we do not translate re ned structures (S with p := p').
We could not check all of these translations using Dedukti. Indeed, although the translation is linear, some of them are too big. For instance, the Coq.Lists.List module, whose .vo le has length 260KB, is translated into a Dedukti le of length 1.2MB, which is in turn translated into a Haskell le of size 12MB. Of course, GHC is not able to run or compile this le. A simple solution to overcome this issue would be to cut big modules into smaller les. A more stable solution consists in making Dedukti no longer produce Haskell code, but code that can be compiled just-in-time. Dedukti is currently rewritten to allow this.
Another limitation of Dedukti is the absence of higher-order matching. Higher-order
patterns can appear for instance in the rules for I__case when the real arguments of the inductive
type I are higher order. For instance, if we de ne the inductive type
Inductive I : (Prop -> Prop) -> Prop := c : I (fun t => t).
we obtain the following rewrite rule:
[...] I__case P fc (t : Uprop => t) (I__constr (t : Uprop => t) c) --> fc.
which contains higher-order patterns. However, these higher-order patterns are not useful for
the matching, since the important pattern is the constructor c. Therefore, the possibility to
declare that a pattern should be used for the typing of the rule but not for the matching
has been added recently to Dedukti. Nevertheless, these so-called dot patterns (see [
As noted in Section 2.5, one last remaining point is the encoding of universes.