The Coq mailing list

[Greg Morrisett <greg AT eecs.harvard.edu>]

This is an instance of a more general problem with datatypes/inductive
definitions that arises in the ML/Haskell/Coq/etc. community:  pattern
matching does not promote abstraction.

I’ve always wanted to have more control over this in the form of 
an abstract pattern declaration (with attendant proofs that the
patterns are exhaustive and non-overlapping.)  

-Greg


On Oct 8, 2014, at 2:26 PM, Kevin Sullivan 
<sullivan.kevinj AT gmail.com>
 wrote:

> Yeah. Simple unfolding of symbolic names in patterns would be nice, though, 
> for the reasons I mentioned. On the other hand, I guess it'd arguably be a 
> hack that breaks design symmetry. Maybe it'd cause other problems, too. 
> Thanks, --k
> 
> On Wed, Oct 8, 2014 at 2:07 PM, Adam Chlipala 
> <adamc AT csail.mit.edu>
>  wrote:
> Just like in ML and Haskell, those positions don't make sense with 
> arbitrary expressions.  You need patterns there, and it would add 
> nontrivial complexity to the Gallina design to introduce more first-class 
> treatment of patterns.  [Definition] introduces new expression constructs.
> 
> 
> On 10/08/2014 02:05 PM, Kevin Sullivan wrote:
>> I'm wondering what's the technical reason that Coq doesn't unfold 
>> expressions in pattern position?
>> 
>> (* THIS WORKS *)
>> 
>> Definition bar (n:nat): nat := match n with 1 => 1 | _ => 0 end.
>> 
>> (* THIS DOESN'T *)
>> 
>> Definition foo: nat := 1.
>> Definition bar (n:nat): nat := match n with foo => 1 | _ => 0 end.
>> 
>> (* 
>> The only difference is the use of a symbol rather than a "manifest 
>> constant" in the second case.
>> When using nats to represent objects of another kind, I'd prefer to match 
>> on symbolic names rather than on their concrete representations as nats -- 
>> for  abstraction, information hiding,             readability. Of course 
>> the question generalizes beyond nats.
>> *)
>> 
>> Kevin 
> 
>