The Coq mailing list

[Frank Staals <f.staals AT student.tue.nl>]

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.

Obviously I would have to prove these lemmas. But assume that I have the tactics 'prove_hd' and 'prove_tl' that can prove the above lemmas fully automatically for any s,x and xs.

So an example of this which is already in Coq is the generation of a new inductive type: Coq automatically generates the induction principle.

I can imagine that the above is not directly possible on the already existing definition of Stream (because what I am asking should basically be a property of everything of type Stream). So I would also be content with having to define a new 'RichStream' type which has these properties. Such that I would have to define my stream using:

CoFixpoint s: RichStream A := x :: xs.

instead.

Would something like this be possible ?

Regards,  

-- 

- Frank