Skip to Content.
Sympa Menu

coq-club - Re: [Coq-Club] more generous context when typing branches of [match]?

coq-club AT inria.fr

Subject: The Coq mailing list

List archive

Re: [Coq-Club] more generous context when typing branches of [match]?


chronological Thread 
  • 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....)



Archive powered by MhonArc 2.6.16.

Top of Page