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.
Input file is a simple Coq module with special annotations that
describe the binding structure of the defined syntax. For
instance, ordinary lambda-calculus is written as follows:
Module STLCterms.
Inductive term : Type :=
| var ((* index *) x : nat)
| app (t1 t2 : term)
| lam ((* bind term in *) t : term).
End STLCterms.
With this annotations, DBGen will produce a Coq module of the
given name
STLCterms that contains this definition
(without the comments), the lifting function
(
term_lift_in_term : nat -> nat -> term -> term),
the substitution function (
term_subst_in_term : term -> nat
-> term -> term) and a large collection of statements with
their proofs, up to the substitution lemma:
Lemma term_subst_in_term_term_subst_in_term_distrib :
forall (_arg : term) (_arg' _arg'' : term) (_n _m : nat),
_m <= _n ->
term_subst_in_term _arg' _n (term_subst_in_term _arg'' _m _arg) =
term_subst_in_term (term_subst_in_term _arg' (_n - _m) _arg'') _m (term_subst_in_term _arg' (S _n) _arg)
.
Moreover, a tactic named
dbgen_tac is built with
every simplification lemma and is therefore able to simplify and
decompose arbitrary terms that contains lifting and
substitution.
A complete example of how the generated module (definitions and
tactics) can be used is provided in the
test/Case_STLCletval/test.v file.
(february 26, 2013) Version 0.5.2 release.
(january 30, 2013) Version 0.4.2 release.
(january 22, 2013) Version 0.4.1 release.
(january 15, 2013) First public release.