The Coq mailing list

[Adam Chlipala <adam AT chlipala.net>]

Frank Staals wrote:
> Hey everyone,
>
> Is there a way to automatically bind/attach a lemma to a definition ? 
> I will try to explain what I mean with that with a concrete example: 
> Suppose I have a stream defintion s:
>
> CoFixpoint s : Stream A := x :: xs.
>
> Now I want coq to automatically generate the following lemmas:
>
> Lemma s_hd : A := hd s = x.
> Lemma s_tl : Stream A : tl s = xs.

These last two lines don't make sense as Coq [Lemma] commands, but 
that's probably just a typo.

In general, what you ask about is possible but not easy, using a mix of 
two metaprogramming methods:
1) The traditional "dynamically-typed" approach, where you write 
syntax-manipulating code in an OCaml plugin.  This probably requires at 
least a few days familiarizing yourself with the Coq code base (which 
means, at best, reading .mli files, not some separate documentation [and 
you also need to figure out the structure of the code base on your own, 
to know which .mli files to read]).
2) Proof by reflection, which can be implemented entirely in normal Coq 
code, but can be trickier (though easier to know when you have 
implemented correctly, thanks to expressive Gallina type-checking).  
Especially when a metaprogram analyzes an inductive type definition, it 
is usually convenient to pair reflection with some amount of OCaml 
plugin code, to reify some plugin-specific class of syntax.  For a quick 
introduction to proof by reflection in Coq, you can see Chapter 10 of 
CPDT (http://adam.chlipala.net/cpdt/).

This tech report might also be of interest:
    http://adam.chlipala.net/papers/AutoSyntaxTR/
It describes an old system for generating standard theorems 
automatically about inductive definitions of syntax trees with de Bruijn 
indices.

Perhaps the most useful summary answer is that you would have to go down 
a significant rabbit hole to implement what you want.  Whether this is 
worthwhile depends on your interests, how often you want to use this 
functionality, and how big the examples are.