The Coq mailing list

[Enrico Tassi <enrico.tassi AT inria.fr>]

On Wed, Oct 08, 2014 at 03:49:32PM -0400, Kevin Sullivan wrote:
> 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),

It cannot work in all cases, but something you may consider is writing
your own (computable) comparison function that gives you a boolean and
match on that.  Computation unfolds definitions for you.  More concretely,

  if cmp_nat n foo then 1
  else 0

The whole Mathematical Components library is built on the idea, usually
called small scale reflection, that everything that is computable is
expressed as a computable function.  In other words general pattern
matching is very complex, but pattern matching over naturals is way
simpler and can be coded taking into account definition unfolding,
fixpoint computation and the like.

Best,
-- 
Enrico Tassi