The Coq mailing list

[Adam Chlipala <adamc AT hcoop.net>]

Kouskoulas, Yanni A. wrote:
> I find that when using refine, the context that I have access to lacks 
> assumptions that I think should be available.

[refine] operates with a literal treatment of the CIC typing rules.  You 
can see from the CIC section of the manual that no assumptions relating 
discriminees and pattern variables are added for you; you need to use 
the dependent [match] annotations to get those, and there is no 
annotation pattern that always brings you the extra assumptions you 
expect without altering the "computational part" of your match.  This 
can seem a baffling design decision at first, but a completely general 
mechanism would need to solve undecidable problems.

So, you have a few options:
- Use tactics, like you're already doing (not so nice)
- Learn about and apply dependent [match] annotations (The only source 
I'm aware of for tips of the trade on this subject is the [still 
incomplete!] textbook I'm writing: http://adam.chlipala.net/cpdt/)
- Use Program or some other convenience layer built on top of CIC