First part of my first non-trivial(e.g. something other than a Software Foundations exercise) Coq program is finally done. I learned Coq from Software Foundations, but I didn’t finish to book. I still know only very basic tactics, which I think is one of the reasons why my proofs are so long. You can see the source here.
Some random notes about implementation:
generalizetactics are used.
SSCase… constructs from SFlib extensively.
Now I’m going to implement lambda-calculus with row-polymorphic records. I expect this to be at least 2x harder, since polymorphism is involved. Let’s see how it goes …