The Coq mailing list

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

Erik Ernst wrote:
> Den 22/09/2011 kl. 14.14 skrev Adam Chlipala:
>
>   
> > Erik Ernst wrote:
> >     
> > > thanks for the quick answer!  In fact, this is exactly what I meant when I 
> > > said that the dilemma can be avoided.  However, this means that the type of P 
> > > will be (R N1 N2) in all branches, which creates a number of problems in the 
> > > other branches (just shown as 'magic ..' above).
> > >
> > > Can't we have the more specific typing of P in each branch (that we do get 
> > > with 'match N1,N2,P return..') without getting into the dilemma?
> > >       
> > I'm not sure what you mean.  The type of [P] _is_ maximally refined above, as 
> > far as I understand.
> >     
> In fact, I get error messages like 'The term "P" has type "R (natS N1') (natS N2')" in the last branch above when doing 'match N1,N2,P return..' and error messages like 'The term "P" has type "R N1 N2" when doing 'match N1,N2 return..'.  
>
> I interpreted that to mean that P was typed as indicated, which would 
> presumably mean that the extra knowledge about N1 and N2 would only appear in 
> the type of P when it is included in the pattern match, otherwise it always 
> gets the type (R N1 N2).
>
> I've experimented a little more with this and attached two example files 
> showing the two situations.

The code I suggested has none of the problems you mention.  I'm a bit 
confused because your new example program demonstrates issues with two 
ways of writing the pattern match, neither of which is the way that I 
suggested.

The rules in question here, for dependent pattern matching, are 
extremely simple, and basically 10 minutes of studying the typing rule 
can save you from ever being surprised again about the types of 
variables.  The CPDT book explains all this, along with some useful 
design patterns for fitting the dependency structures of particular 
programs into the framework that Coq understands.