The Coq mailing list

[Ömer Sinan Ağacan <omeragacan AT gmail.com>]

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