The Coq mailing list

[Emmanuel Polonowski <polonowski AT u-pec.fr>]

Dear Coq-club members,

I am pleased to announce that the release of DBGen 0.5.2 is now available at
http://www.lacl.fr/~polonowski/Develop/DBGen/dbgen.html .

DBGen is a tool designed to help the computer theoretist to formalize 
higher-order languages in the De Bruijn setting. From a Coq inductive 
definition annotated with special comments, it generates a Coq file with all 
the definitions and statements needed to work with De Bruijn encodings (up to 
the substitution lemma). It also provide a named syntax and a smart 
translation function.
DBGen handles mutually inductive definitions and multiple distinct index 
sets: definitions, statements and proofs will proceed along the user 
inductive syntax definition.

Input file is a simple Coq module with special annotations that describes the 
binding structure of the defined syntax (aka DBEB abstract syntax). For 
instance, source syntax for System F is written as follows:

Module SYS_F_terms.

  Inductive type : Type :=
  | tvar ((* index *) i : nat)
  | tconst (n : nat)
  | tarrow (A B : type)
  | tall ((* bind type in *) A : type).

  Inductive term : Type :=
  | var ((* index *) x : nat)
  | app (t1 t2 : term)
  | lam (A : type) ((* bind term in *) t : term)
  | tapp (t : term) (A : type)
  | gen ((* bind type in *) t : term).

End SYS_F_terms.

With this annotations, DBGen will produce a Coq module of the given name 
SYS_F_terms (around 2200 lines) that contains this definition (without the 
comments), the three lifting functions (term_lift_in_term : nat -> nat -> 
term -> term, type_lift_in_term : nat -> nat -> term -> term and 
type_lift_in_type : nat -> nat -> type -> type), the three substitution 
functions (term_subst_in_term : term -> nat -> term -> term, 
type_subst_in_term : type -> nat -> term -> term and type_subst_in_type : 
type -> nat -> type -> type) and a large collection of statements with their 
proofs, up to the three substitution lemmas.

Moreover, a tactic named dbgen_tac is built with all the simplification 
lemmas and is therefore able to simplify and decompose arbitrary terms that 
contains lifting and substitution functions invocation.

A user manual and a large set of examples are provided in the distribution.

The main changes in v0.5.2 are:
- Handles mixed constructors with (at most) one index parameter and other 
non-index parameters.
- Handles simultaneous definition of parameters of the same category (as in 
"app (t u : term)").
- Performs static checking of source syntax for: no multiple index in a 
constructor, only user defined binding categories.

See http://www.lacl.fr/~polonowski/Develop/DBGen/dbgen.html for more details. 
Comments and experimentations are very welcome !

Best regards,
Emmanuel Polonowski

--
Emmanuel Polonowski
Directeur de l'ESIAG-MIAGE
Université Paris-Est Créteil
www.lacl.fr/~polonowski