The Coq mailing list

[Matthieu Sozeau <mattam AT mattam.org>]

Hi, [return _] should do it, I believe it's in the manual too.
-- Matthieu

Le lun. 15 juin 2015 à 11:24, Ralf Jung <jung AT mpi-sws.org> a écrit :

Dear Coq-Club,

Is there any way to tell "Program" not to mess with certain matches?

Whenever a definition is performed using "Program", all the matches in
this definition will end up being dependent matches that introduce an
additional equation within the match arms. That's often very useful, but
sometimes totally unnecessary - and combined with "destruct" not working
well on dependent matches, it can really get into the way.

I attached a (contrived, simple) example demonstrating this: In the
second definition, there's no reason for the match to become dependent.
However, there are some proofs that I have to fill out, so I'd still
like to use "Program". Currently, what I have to do is
* either put the match into a non-Program definition, and write
  Program definitions for the arms (or the context) insofar as
  there are proof terms that have to be constructed there. This
  results in fairly pointless splitting of definitions, and
  it introduces additional delta-steps that some tactics stumble
  over.
* or use "refine". This results in a rather weird-looking definition,
  and if what I define is a *type* involving "forall", refine
  doesn't even work: "refine (forall (t:T), _)" says this is not
  supported. This came up for me when I was defining a complicated
  proposition.

So, I wonder - is there something I can do with the match, e.g. some
kind of marker I could apply somehow, that tells "Program" not to mess
with it? That would be very useful.

Kind regards,
Ralf