The Coq mailing list

["Soegtrop, Michael" <michael.soegtrop AT intel.com>]

Dear Amin,

thanks a lot for your very detailed answer! It contains a lot of interesting 
ideas/hints/pointers. But it also brings up a few more questions:

1.) Partly this seems to be a problem of simplification of fixpoints. The 
type terms generated by the fixpoint are huge and ugly, but when I do a 
compute on them, they become very small and nice. One thing I couldn't find 
in Gallina is a function to do reductions on a term. I know it should never 
make a logical difference, but especially with large developments, it could 
make a significant performance difference, if I could do reductions of terms 
at Gallina level. I also think that it would solve the problem here (except 
for the nesting depht problem).

2.) Is the Type Class mechanism considered to be part of Gallina or outside 
of it at the vernacular / tactics level? In the first case, does the 
implementation of Type Class instance search with eauto mean that the Type 
Class feature breaks the parametricity feature of Gallina?

3.) Is the instance search an easily decidable problem?

Best regards,

Michael