Skip to Content.
Sympa Menu

coq-club - [Coq-Club] Dirty feature request

coq-club AT inria.fr

Subject: The Coq mailing list

List archive

[Coq-Club] Dirty feature request


chronological Thread 
  • 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.



Archive powered by MhonArc 2.6.16.

Top of Page