The Coq mailing list

[Adam Chlipala <adamc AT hcoop.net>]

Ian Lynagh wrote:
> Hi Adam,
>
> On Mon, Mar 02, 2009 at 06:44:35PM -0500, Adam Chlipala wrote:
>   
> > I've never heard of C-zar,
> >     
>
> http://coq.inria.fr/V8.2/doc/html/refman/Reference-Manual014.html
>   

Ah, OK, a new, less generic name for something old.  That's a good 
marketing move. :)

> Thanks for the proof, but unfortunately I don't consider Ltac proofs
> readable, which is why I'm trying to use C-zar.
>   

Well, your particular theorem is so obviously true that I think no 
mathematician would bother to spell out a proof in structural detail, so 
it's unclear to me why you want to do so here.  When I consider the 
practical motivations for proof-writing, my conclusion is that Ltac is 
usually a better choice than any of the "structured" proof languages out 
there.  Proof scripts that adapt to changes in theorem statements can 
save you a lot of time in the long run, and I believe that most proof 
scripts that go into structural detail end up _not_ being readable by 
others anyway, despite their authors' best intentions.  To me, the best 
way to write a proof script in a way that documents "why" the theorem is 
true is to break tricky steps out into their own lemmas, with every 
theorem and lemma still proved by Ltac automation.