Krajono

A Matita to Dedukti translator

What is Krajono?

Krajono (which means pencil in Esperanto) translates the proofs of Matita to the Dedukti logical framework. The translation is based on the works of Cousineau and Dowek [1] for pure type systems, Boespflug and Burel [2] for inductive types, and Assaf [3] for the infinite universe hierarchies and cumulativity.

References:

1. D. Cousineau and G. Dowek, Embedding pure type systems in the lambda-Pi calculus modulo, TLCA 2007
2. M. Boespflug and G. Burel, Coqine: Translating the calculus of inductive constructions into the lambda-Pi calculus modulo, PXTP 2012
3. A. Assaf, A calculus of constructions with explicit subtyping, submitted to the post- proceedings of TYPES 2014

Code and license

The current prototype is implemented as a fork of matitac (based on the 2014/11/24 svn snapshot). The code is distributed under the CeCILL free software license (the French equivalent of the GNU GPL). It can be downloaded here or directly from the Inria Forge project page.

Usage

Krajono is a fork of Matita that adds an option to export proofs to Dedukti. You compile it just like you compile matita. See Matita’s (complicated) compilation process for further info. Good luck! ;-)

To use Krajono, call matitac with the -extract_dedukti option on your matita (.ma) file:

matitac -extract_dedukti lib/arithmetics/nat.ma

Because of the way Matita caches developments, this option forces the recompilation of the file. At the end, the translation produces one dedukti (.dk) file for each matita file that contains at least one object. It produces nothing for empty (e.g. wrapper) files. It also produces a file univs.dk that contains the definitions of the universes used by these files. All the files depend on the cic.dk file in the present directory.

The included Makefile can be used to translate (make translate) and check (make check) parts of the Matita library. Currently, the arithmetics library is translated and successfully checked with little modification. Additionally, there are two scripts parse_matita_output.py and parse_dedukti_output.py that can collect various data from the output of the translation and verification passes of the build process and display them in a clean and concise way that can serve to compile benchmarks.

Known problems

• Floating universes: Because of the way universes work, it is not possible to correctly translate files independently of each other. Therefore it is recommended to write a wrapper file that includes all the files you want to translate (no need to include their dependencies) and call matitac only on this wrapper file. For example, to translate all of the arithmetics library, the wrapper file would look like this:

  include "arithmetics/div_and_mod.ma".
  include "arithmetics/log.ma".
  include "arithmetics/chinese_reminder.ma".
  include "arithmetics/pidgeon_hole.ma".
  include "arithmetics/nth_prime.ma".
  include "arithmetics/factorial.ma".
  include "arithmetics/nat.ma".
  include "arithmetics/lstar.ma".
  include "arithmetics/sqrt.ma".
  include "arithmetics/permutation.ma".
  include "arithmetics/bounded_quantifiers.ma".
  include "arithmetics/fermat_little_theorem.ma".
  include "arithmetics/nat_commented.ma".
  include "arithmetics/gcd.ma".
  include "arithmetics/congruence.ma".
  include "arithmetics/minimization.ma".
  include "arithmetics/sigma_pi.ma".
  include "arithmetics/binomial.ma".
  include "arithmetics/exp.ma".
  include "arithmetics/bigops.ma".
  include "arithmetics/ord.ma".
  include "arithmetics/iteration.ma".
  include "arithmetics/primes.ma".
  include "arithmetics/chebyshev/all.ma".

• Constructor names: Krajono currently does not distinguish between constructors with the same name, even if they belong to different inductive types. It is recommended to avoid such constructor names.

• Prop irrelevance: Krajono does not handle prop irrelevance. It is recommended to avoid proofs using it if possible, and to turn the concerned theorems into axioms otherwise (such as for lemma K).

Contact

Krajono is developed and maintained by Ali Assaf. For information, feedback, bugs, and everything else, please contact him at at ali.assaf@inria.fr.