The Coq mailing list

[Jesper Bengtson <jebe AT itu.dk>]

Dear all.

A while ago I sent a letter to the list regarding Ltac's use of the 
constr-command. I got a few replies, thank you all for those, but nothing 
that actually solved the problem. It seems to me that whenever constr:xxx is 
used, xxx has to be type-checked. In a way, this makes perfect sense, but I 
get huge performance problems when creating inductively defined datatypes by 
using recursive Ltac-procedures. The problem is that even though if terms 
have been type-checked in previous calls, wrapping these terms in a new 
constructor requires that the whole term is type-checked, including 
re-checking the ones that have already been done.

It seems that anyone doing proofs by reflection would run into this problem. 
The examples I have found in the literature are mostly quite small, and 
therefor manageable. One of the larger examples I found was some very 
interesting work by Das Barman and Bertot from 04, and they also seem to use 
an equivalent of Ltac to construct their terms. Did this work scale to larger 
examples?

To sum up, it seems that Ltac does not scale when constructing datatypes. Is 
there any other way to go around this, possibly building a term lazily and 
performing type-checking at the end? As it is now I'm a bit stuck.

Best regards, and I hope you have all had a happy and relaxing easter.

/Jesper