The Coq mailing list

[Jason Gross <jasongross9 AT gmail.com>]

In terms of directions to study: CPDT is, among other things, a guide to being productive in Coq using tactics and writing your own tactic scripts.  There is also Adam's tactics quick reference, and the index of all of the tactics.

-Jason

On Sat, Mar 8, 2014 at 4:14 PM, Ömer Sinan Ağacan <omeragacan AT gmail.com> wrote:

Hi all,

I'm a starter and I studied large part of Software Foundations book.
Recently I finished my first non-trivial proofs, progress and
preservation for simply-typed multi-staged lambda calculus. You can
see the program here:
https://github.com/osa1/StagedLambda/blob/master/Lc.v

I'm not happy with this proofs, though. Because they were very
tiresome to write, and they're now very hard to read and they're just
too long. You can spot some repeated lines but I just couldn't find a
way to eliminate that. There are probably lots of other problems too.

Since I learned Coq from SF book, I only know very basic tactics. I
was wondering if it's possible to improve my proofs using some more
advanced tactics and what would that advanced tactics be. Can anyone
point me some directions to study and improve my proofs?

Thanks..

---
Ömer Sinan Ağacan
http://osa1.net