The Coq mailing list

[Danil Annenkov <danil.v.annenkov AT gmail.com>]

Hi Enrico,

I am not sure if anything as good as Nominal Isabell exists for Coq.

One can go quite far in defining alpha-equivalence using the nominal techniques but the real problem is how to define a type of terms quotient with alpha-equivalence.

This project: https://github.com/lewer/nominal-coq uses an approach to quotients (if I am not mistaken) described in Cyril Cohen's Pragmatic quotient types in coq (https://dl.acm.org/citation.cfm?id=2529335)

You also might want to take a look on A Generic Approach to Proofs about Substitution by Abhishek Anand and Vincent Rahli (http://www.nuprl.org/html/CFGVLFMTP2014/).

Another reference (but, again, not really a package) is Nominal Reasoning Techniques in Coq by Brian Aydemir, Aaron Bohannon, Stephanie Weirich (https://www.seas.upenn.edu/~sweirich/papers/nominal-coq/lfmtp06.pdf)

But this is more like an axiomatic approach to defining a nominal "interface" to your syntax and then justifying this interface by using locally nameless representation. So, again, no automatic generation of alpha conversion.

On Fri, Dec 6, 2019 at 12:55 PM Enrico Tassi <Enrico.Tassi AT inria.fr> wrote:

Dear Coq-Club,
  I was looking for some "nominal package" for Coq.
 

I could find Metalib (https://github.com/plclub/metalib) but, as far as
I could understand, it does not synthesize axioms for alpha conversion
(said otherwise it does not provide a syntax to write ADT with binders,
hence it can't synthesize for you much). If I'm wrong please correct
me.

Otherwise, is there another package giving some support for nominals?

Best regards,
--
Enrico Tassi

--

Best regards,

   Danil Annenkov