coq-club AT inria.fr
Subject: The Coq mailing list
List archive
- From: AUGER Cedric <Cedric.Auger AT lri.fr>
- Cc: Coq Club <coq-club AT inria.fr>
- Subject: [Coq-Club] Dirty feature request
- Date: Mon, 25 Oct 2010 14:32:43 +0200
Hi all,
when we do "dirty" developpements in Coq,
we use tactics like "intros.", "inversion H7.", "destruct x."
without giving names.
Coq generates names automatically, using a counter, and
checking non collision; so that if you change the order of tactics,
change your inductive types, give name to some hypothesis,
clear of some hypothesis, ...,
all the proof script will be broken due to shifting the names
(H3 becomes H0, H4 becomes H1, ...).
As these tactics exist, we want the user to be able to do
"dirty" proofs, to help him, couldn't the name generation use
a hash of the type of the hypothesis, so that messing with
the previous operations won't "shift" the name of hypothesis
(as far as two hypothesis don't have same type)?
Of course, such a feature may (slightly) slow the generation of
hypothesis, and imply a command like "Set NameGeneration Hash.",
to keep backward compatibility, when this command doesn't appear.
I am not sure my message is clear and such a feature hasn't already
been discussed; if so, let it me know.
- [Coq-Club] Well-founded induction over finite sets, David Pereira
- Re: [Coq-Club] Well-founded induction over finite sets, Stéphane Lescuyer
- [Coq-Club] Dirty feature request, AUGER Cedric
- Re: [Coq-Club] Dirty feature request, Greg Morrisett
- Re: [Coq-Club] Dirty feature request,
Randy Pollack
- Re: [Coq-Club] Dirty feature request, AUGER Cedric
- Re: [Coq-Club] Dirty feature request, Jeff Vaughan
Archive powered by MhonArc 2.6.16.