The Coq mailing list

[Adam Chlipala <adamc AT hcoop.net>]

Robin Green wrote:
> On Fri, 20 Feb 2009 08:39:06 -0500
> Adam Chlipala 
> <adamc AT hcoop.net>
>  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.
> >     
>
> But any proof can be turned into a tactic, whose definition is simply
> the original proof - but that would achieve nothing. What is the formal
> definition of what you mean? ;-)
>   

I don't think it's necessary to give a formal definition; folks tend to 
get the idea.  Proof scripts should almost never follow the structure of 
the proof, since that makes them brittle to necessary structural 
changes.  This rules out solving every goal by [exact], since this would 
involve giving proof terms that follow proof structure.