The Coq mailing list

[Michael Soegtrop <MSoegtrop AT Michael-Soegtrop.de>]

Hi Thalia,

a very nice course outline!

What might be missing (not sure if it is hidden in one of your points) 
is eauto style (includign typeclass eauto) proof automation and 
designing lemmas such that the branching factor in such brute force 
proof search is small. I am personally out of this proof style these 
days since I concentrate on numerics where such an automation style 
doesn't really work, but it did serve me well for a few years for more 
symbolic proofs.

I try to divide lemmas into those which are more for forward reasoning, 
that is have specific premises and generic goals and those which are 
more for backward reasoning, that is have specific goals and generic 
premises. Often one has a lot of freedom in stating a lemma so that it 
goes more in the one or the other direction. I frequently have the same 
lemma stated differently for the one or other direction. If a lemma 
doesn't fit either case, I use gating tactics to make sure it is only 
applied in cases where it is likely to be useful.

One can also talk about lemma database design and proof search 
statistics, e.g. how mixing forward and backward search and delimiting 
the branch factor influences proof search time.

When I was still using this style, I had on average of about 3 lemmas 
tried per one lemma successfully used over large developments, and this 
also included rather deep proofs (say 100 levels), where one would 
expect that proof search time is exponential.

Best regards,

Michael