coq-club AT inria.fr
Subject: The Coq mailing list
List archive
- From: Matthieu Sozeau <mattam AT mattam.org>
- To: coq-club AT inria.fr
- Subject: Re: [Coq-Club] "Program" and match
- Date: Mon, 15 Jun 2015 12:47:36 +0000
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
- [Coq-Club] "Program" and match, Ralf Jung, 06/15/2015
- Re: [Coq-Club] "Program" and match, Matthieu Sozeau, 06/15/2015
- Re: [Coq-Club] "Program" and match, Arnaud Spiwack, 06/15/2015
- Re: [Coq-Club] "Program" and match, Ralf Jung, 06/15/2015
Archive powered by MHonArc 2.6.18.