The Coq mailing list

[Jason Gross <jasongross9 AT gmail.com>]

You can only do a syntactic match when you're building a proof in Ltac, not within a gallina function.  Gallina (the non-Ltac Coq language) doesn't have any notion of syntactic equality, and you can't access the definitional equality.  As a rule of thumb, gallina functions need to respect equality; if substituting (propositional) equals for equals changes the behavior of the function, then you can't do it in Gallina.  You could try Mtac (I've never tried it), which, I think, does some tricks with delaying computation until you run the code.  But I don't think you can prove much about Mtac code.  Alternatively, you could reify the types you use so that you only consider a subset of Type with decidable equality.

-Jason

On Sun, Jun 16, 2013 at 8:02 AM, Michiel Helvensteijn <mhelvens AT gmail.com> wrote:

On Sun, Jun 16, 2013 at 3:22 AM, Jason Gross <jasongross9 AT gmail.com> wrote:

> Type does not have decidable equality, and you cannot productively
> destruct/match on a thing of type Type.

That makes sense.

> Additionally, the match you use is
> in Ltac; it matches on a syntactic level, unlike the non-ltac match.

And that, I guess, is why I expected it to work anyway. ;-) A
syntactic match is exactly what I'm after (modulo delta/beta/zeta
reduction). I'm basically trying to create some syntactic sugar. And
isn't syntactic equality decidable?

> You will probably want to reify your types so that you can distinguish
> function types from other types.

Indeed. But I won't need that until I write the recursive definition
later, right? For the moment, I'm trying to solve one problem at a
time: that of matching the 'T' of 'primitive' to the 'T' of
'delta_op'.

> Appologies if this is not enough information; I'm typing from my cellphone
> at the moment and thus being concise.

No problem. Though if you can find some time later, I would appreciate
an example of how to do this properly. It seems like it should be
possible.

Thanks!

--
www.mhelvens.net