The Coq mailing list

[Julien Narboux <Julien.Narboux AT inria.fr>]

Hi Johannes,

Not really design pattern, but just a few lessons I have learned (but it 
is just my opinion) :

 - have a very very very detailed paper proof before starting the 
formal proof
 - name your intros : "intros A B C" instead of simply "intros" or at 
least do not use names which are generated automatically
 - do not hesitate to introduce a lot of lemmas, even 'strange' facts 
which seem to be very specific to your current proof, often appear 
several times
 - writing a small tactic specialized into a small problem can save time
 - automatic tactics should have a well defined scope (you should be 
able to tell when it is supposed to success of fail)
 - do not make proofs that rely on the previous modification of the 
goal by an automatic tactic: If the tactic is improved to solve more 
goals it will break your proof

 I hope it helps,

Julien



Johannes Waldmann a écrit :
> Dear all,
>
> I'm looking for some general reading on "Coq Design Patterns",
> i.e. established good practices (and alternatives)
> for efficient, flexible, readable construction of theories.
>
> (complemented, of course, by a list of "Coq code smells",
> i. e. a list of things to avoid ...)
>
> http://en.wikipedia.org/wiki/Design_pattern_(computer_science)
> http://en.wikipedia.org/wiki/Code_smell
>
> Any hints appreciated. - Thanks, Johannes Waldmann.
>
> --------------------------------------------------------
> Bug reports: http://coq.inria.fr/bin/coq-bugs
> Archives: http://pauillac.inria.fr/pipermail/coq-club
>           http://pauillac.inria.fr/bin/wilma/coq-club
> Info: http://pauillac.inria.fr/mailman/listinfo/coq-club