The Coq mailing list

[Adam Chlipala <adamc AT csail.mit.edu>]

On 10/16/2013 04:08 AM, t x wrote:
> Thus, my question:
>
>   is "the one rule of dependent type matching"
>
> a) a derivation from dependent theory alone?
> b) a derivation from inductive types alone?
> c) a derivation that only arises from dependent type theory + 
> inductive types?
>
> I believe it's (c), since "a" alone does not provide inductive types / 
> multiple constructors -- thus nothing to match on; and "b" alone ends 
> up being STLC.

You're right.

> Now, assuming it's (c), where can I read up on the mathematical 
> foundations of this? [I've looked through chapters in Coq d'Art, but 
> it's not clear if it's defined in the book.]

If by "mathematical foundations," you mean e.g. how to prove logical 
soundness at the meta level, then you'll need research papers and PhD 
dissertations and so forth.  If you just mean how to understand the 
behavior of the Coq type checker, then the CPDT section whose title 
you've cited should be exhaustive.