The Coq mailing list

[Adam Chlipala <adamc AT hcoop.net>]

Nikhil Swamy wrote:
> However, I wonder if there is some more standard idiomatic way of
> handling a situation like this. Ideally something that doesn't require
> me having to pollute my definitions with this counter instrumentation.
>   

Well, did you try proving a lemma analogous to the one I gave, but for 
the other "stuck" case from the original proof?  If that works, it 
avoids changing the definition of the relation.

> Also, you will notice that my proof script is not very readable at all
> :( I end up doing a lot of things manually, e.g, at various points
> when I use eauto I'm left with uninstantiated existential variables,
> so I often have to provide explicit parameters to eapply. Any tips for
> how to avoid this and/or to make my proof more readable would be
> great!
>   

At that point, you can run [Show Proof] to see where those evars came 
from.  I bet you could avoid most such problems by changing your 
relation definition, or defining another version that you prove 
equivalent.  I recommend removing the quantification over [a] values for 
any sub-judgments.  Instead, just require a [Fun] proof for every 
sub-judgment.  You can prove a lemma that any [NoFun] proof can be 
converted to a [Fun] proof.