The Coq mailing list

[Adam Chlipala <adamc AT hcoop.net>]

Wouter Swierstra wrote:
> > On the issue of proofs, I think the proof scripts in both your (Adam 
> > Koprowski's) code and the code of the mysterious "muad" are manual 
> > enough that I would refuse to accept them in a serious development. 
> > ;-)  I say that every certified function should have a single proof 
> > script associated with it, and that proof script should be a single 
> > tactic, with no intermediate periods.  That style (which I used in my 
> > implementation posted earlier) is easy to use when you commit to 
> > following it, and it has many advantages in brevity of code and 
> > resilience to changes in specs and implementations.
>
> That's a very interesting point. I certainly agree that proof scripts 
> can extremely brittle (especially if their poorly engineered) - but 
> aren't you just moving the problem somewhere else? You have a lot more 
> experience with this than I do, but why are Ltacs any easier to 
> maintain than proof scripts?

The idea is that you write very general automation tactics, which are 
easy to eye-ball and convince yourself of their correctness and of the 
cases when they apply.  "Video game"-style proof scripts tend to involve 
many levels of nesting, local name introduction, etc., which make them 
harder to understand, for someone who has taken the time to learn Ltac.

Another answer to your question is this: Ltac-automated proofs usually 
don't _need_ maintenance, because they keep working even after you 
change the theorem.  This is almost never true of manual proofs.