People:
Andreas Abel, Alois Brunel, Mathieu Boespflug, Guillaume Burel, Denis Cousineau, Maxime Denes, Gilles Dowek, Germain Faure, Olivier Hermant, Clément Houtmann, Claude Kirchner, Chantal Keller, Alberto Naibo, Cody Roux.
Working groups
- CoqInE: Coq -> Dedukti
- HOL2DK: HOL light -> Dedukti
- Terminaison checker
- NbE algorithms
- Sequent calculus/LL
CoqInE: Coq -> Dedukti
People: Mathieu, Guillaume, Maxime
We carried on the implementation of CoqInE, the translator of Coq
proofs into Dedukti proofs. Our work focused on the translation of
fixpoints. Until then, a fixpoint F x := C[F] was translated by a
rewrite rule F x --> C[F], which is of course non-terminating in
general.
To make the rule terminate, it should be applied only if x begins with
a constructor. A previous solution was to have one rule for each
constructor, for instance:
F O --> C[F]{O/x}
F (S y) --> C[F]{S y/x}
However, dependant inductive types make this solution fail sometimes,
as shown by the following counterexample:
F (A : Set) (a : A) (g : A -> A) (r : a = g a) := C[F]
cannot be translated by a rule
F A a g (refl A a) --> C[F]{refl A a/r}
since refl A a is of type a = a and not a = g a.
The first solution we thought of was to change the semantic of Dedukti
and to add special rewrite rules that can only be applied on terms
that are not free variables. Not only was this solution unsatisfactory
since it changed Dedukti's kernel behavior, but it was not enough,
because on the right hand side, F can be applied to a term that is not
a free variable, but that does not begin with a constructor.
We finally found a very simple solution that does not require to
change Dedukti's kernel: the idea is to decompose each constructor
into two parts, a first one which says that we have a constructor of
some inductive type, and a second one which say which constructor. For
instance, for the natural number, we obtain:
nat_constr : nat' -> nat.
O : nat'.
S : nat -> nat'.
Then, natural numbers are translated as:
||O|| = nat_constr O
||S x|| = nat_constr (S ||x||)
To translate fixpoints, we only need to know that the term begins with
a constructor, without having to know which one. Thus, fixpoints can
be translated by
F (I_constr p y) --> C[F]{I_constr y/x}
if the recursive argument x is of inductive type I p. Then, the
example with the equality above becomes:
F A a g (eq_constr A a (g a) y) --> C[F]{eq_constr A a (g a) y/r}
and is typable.
After having implemented this solution, we are able to translated all
the prelude of Coq. It remains to find how to translate universes (for
the moment, we put everything in UType and use dotType : UType).
HOL2DK: HOL light -> Dedukti
People: Chantal, Paul
In her master thesis, Chantal Keller translates HOL-light proofs to Coq
proofs the following way:
- Some piece of code added to HOL "listens" to the kernel and records
a proof tree.
- The proof tree is exported as a coq datatype theorem p where p
is the conclusion of the theorem. In the logical frameworks
terminology, this is called a deep embedding.
- A generic proof written in coq translates well-formed "deep" proofs
into "shallow" ones. In other words, it allows for the translation of
terms of type theorem p into terms of type
|p| where |p| is the reification of
p at the level of Coq propositions.
During the seminar, we focused on:
- Defining a lambda-pi modulo theory allowing for shallow embedding of
HOL proofs.
- Reusing part of the HOL -> Coq translation code in order to export
HOL proofs into dedukti proofs using this later theory.
After looking for a theory, we designed one akin to that presented in
http://www.logosphere.org/papers/holnuprlinlf.pdf, a paper proposing
a shallow embedding of HOL in twelf, the existence of which we were not
aware of at the beginning of the seminar. The main difference with our
approach is that the later paper follows the phillosophy of HOL-light,
which defines everything in terms of equality, whereas we treat logical
connectives as native ones, allowing for more intuitionnistic proofs.
The other main difference is that twelf allows for some kind of weak
polymorphism which is sufficient to encode HOL polymorphism whereas
dedukti doesn't. We have decided to test two approaches to
handle with polymorphism in HOL: adding quantifiers to close theorems or
renaming all free variables as a whole program transformation.
The second approach is currently being tested but may be replaced by the
first one which sounds less dirty.
Since dedukti doesn't allow for implicit parameters (no type inference
at all), we have to synthetize types of sub-proofs during the
translation, a feature that was not needed thus not supported by the
previous work of Chantal. Modification of the code is work in progress,
some basic proofs are already successfully translated and typechecked.
We expect full typechecking of HOL std library soon.
Terminaison checker
People: Cody, Andreas, Mathieu
NbE algorithms
People: Cody, Andreas, Mathieu
Sequent calculus/LL
People: Aloïs, Clément, Guillaume, Olivier
The initial aim of the workgroup is to have a direct proof of the statement "super-consistency implies cut-elimination" for (classical) sequent calculus, that does not go through:
- an encoding of classical sequent calculus into intuitionistic sequent calculus (a variant of Goedel not-not tranlation adapted by Dowek and Werner to deduction modulo)
- a use of the cut-elimination theorem for Natural Deduction through an encoding and a decoding
The first approach retained was to extend the notion of simplified Reducibility Candidates for (natural deduction) sequents coming from a paper of Dowek, Hermant to the sequent calculus case. Many approaches have been tried, that all have failed (any definition seems to have a drawback at some point).
The second approach was to adapt and simplify the symmetric reducibility candidates, e.g. the ones introduced by Urban, or the ones used in Linear Logic (see for instance the works of Okada or Brunel). This approach seems to work and is under current investigations, but the link with the other Natural Deduction candidates becomes unclear and still have to be explored.
Tempête de cerveaux
Cody: la reecriture de Coqine (et son
extension) ainsi que l'implementation d'un verificateur de terminaison,
pour lequel il reste cependant des problemes theoriques
D'un point de vue plus pratique, j'aimerais qu'il y ait une
implementation d'un systeme de messages d'erreurs de typage dans
Dedukti...
Chantal: importation de preuves HOL-light en Dedukti
Denis : en écho aux deux messages précédents (Coq en dedukti et HOL light en Coq/Dedukti), il serait sans doute intéressant de confronter ces deux traductions afin de comprendre comment faciliter le futur travail d'encodage de preuves d'autres assistants en fournissant une sorte de framework contenant tout le travail commun à ce genre de traductions.
A ce propos, Damien Doligez m'a fait part de son intérêt pour utiliser dedukti comme (un) backend (parmi d'autres) de son prouveur automatique Zenon.
Olivier "Normalisation par Evaluation" - theorie et/ou pratique.
