The Coq mailing list

[Pierre Geneves <pgeneves AT us.ibm.com>]

Hello,

I have two different abstract syntaxes
G and G', along with a derivor D that maps each construct of G to a specific
construct of G' using rewriting rules. I am interested in identifying the
abstract syntax of D(G), which is a restriction of G'. Let's consider that
both G and G' are first order for now.

I guess that Coq can automatically infer
the output inductive type of D(G). I am looking for a convenient way to
trigger this computation and print the output. 

I have naively started by encoding G
as an inductive set definition. I have then tried to encode D as a fixpoint
that takes a term of G as a parameter and outputs its translation by D.
I have also tried to encode D as rewriting rules for using the "AutoRewrite"
tactic. My attempts so far force me to encode G' (ok, but kind of overkill).
They allow me to handle instances of G, but I haven't found a way to automatically
get D(G) yet. I realize that the answer could be obvious (a simple lemma
or definition?) but I don't find it. Also, there might be better ways for
encoding my problem...

Any hints, suggestions, or pointers?

Thank you!

Pierre