The Coq mailing list

[Abhishek Anand <abhishek.anand.iitg AT gmail.com>]

In my experience, the more automated a proof is, the more nameless it gets: the manual or automation steps don't care about what names get assigned to variables/hypotheses in the context and if some hypothesis has to be identified, it is done by shape matching, not by names.

That said, some people see some value in having complex automation tactics preserve the user-chosen names as much as possible and perhaps also choose names of new hypotheses in a predictable way, perhaps based on the existing names. The simplest example is perhaps:

destructing H: A /\ B could result in

Hl: A 

Hr: B

But doing this is complex in most cases, e.g. when a lemma is applied to multiple hypotheses to produce a new one.

Does anyone have experiences to share trying to design complex automation tactics that preserve the user chosen names as much as possible? Or is there some fundamental conflict between the degree of automation and the reliability of names of hypotheses?

(In general, I wish there was more science about the art of writing Coq proofs robust against "future changes": I see a lot of debates about it but not much hard evidence)

Thanks,

-- Abhishek

http://www.cs.cornell.edu/~aa755/