coq-club AT inria.fr
Subject: The Coq mailing list
List archive
- From: Adam Chlipala <adam AT chlipala.net>
- To: Adam Megacz <megacz AT cs.berkeley.edu>
- Cc: coq-club AT inria.fr
- Subject: Re: [Coq-Club] more generous context when typing branches of [match]?
- Date: Wed, 24 Mar 2010 08:16:20 -0400
Adam Megacz wrote:
It seems that in Coq's rule for typing [match], the hypotheses for the
well-typedness of the branches have a more restrictive context than I'd
like (perhaps for a good reason!).
Yes. It's not clear what else to do instead. Updating types of variables "in place" is undecidable in the general case, since higher-order unification reduces to it. "Adding equalities" could be done in general, but Coq typing right now includes no notion of "equalities in the context." I recommend reading CPDT to learn the most useful design patterns for dependent pattern matching:
http://adam.chlipala.net/cpdt/
In your particular example, however you slice it, you seem to be expecting Coq to apply the identity [n + 1 - 1 = n] automatically. This equality doesn't hold definitionally, so it would take a significant change to Coq's implementation and metatheory to accommodate it. (Not that folks haven't been looking at that kind of thing already....)
- [Coq-Club] more generous context when typing branches of [match]?, Adam Megacz
- Re: [Coq-Club] more generous context when typing branches of [match]?, Damien Pous
- Re: [Coq-Club] more generous context when typing branches of [match]?, Adam Chlipala
- Re: [Coq-Club] more generous context when typing branches of [match]?,
Matthew Brecknell
- [Coq-Club] Re: more generous context when typing branches of [match]?, Adam Megacz
Archive powered by MhonArc 2.6.16.