The Coq mailing list

[Kevin Sullivan <sullivan.kevinj AT gmail.com>]

Abishek solved my immediate problem (Thanks!) and Greg has nicely stated the general problem. Seems like solving it would involve lifting patterns to pattern-valued expressions. The language of pattern-valued expressions would need to be rich enough to support the kinds of abstraction we care about (probably including definition unfolding), but tractable enough to reduce pattern _expression_ to patterns efficiently at compile-time. 

Thanks, guys.

Kevin

On Wed, Oct 8, 2014 at 3:14 PM, Greg Morrisett <greg AT eecs.harvard.edu> wrote:

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
>
>