The Coq mailing list

[Greg Morrisett <greg AT eecs.harvard.edu>]

An interesting idea, assuming you can use short hashes and avoid
conflicts (else, when you want to specify an hypothesis, it could
be painful to type in a long name.) 

What I really want is a tool to take a set of dirty scripts and 
turn them into an Adam Chlipala-style tactic which avoids the use
of names (except locally) and instead is driven by ltac pattern
matching as much as possible.  I find myself manually abstracting
in this fashion to build robust proofs (where ideally, each proof
is essentially "induction x ; crush", and crush is the abstracted
tactic.)  

-Greg

On Oct 25, 2010, at 8:32 AM, AUGER Cedric wrote:

> 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.