**March 6, 2014** - Tagged as: en, coq, plt, multi-stage programming.

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:

- I’m looking to improve proofs. I have a lot more to implement for the rest of the program until deadline, so I may not be able to refactor current proofs very much, but at one point I want to simplify the proofs and use more advanced tactics.
- Currently only
`inversion`

,`destruct`

,`induction`

,`rewrite`

,`assumption`

,`assert`

,`constructor`

,`auro`

,`simpl`

,`intro`

/`intros`

,`apply`

,`right`

/`left`

,`exists`

,`unfold`

,`subst`

,`reflexivity`

,`remember`

and`generalize`

tactics are used. - Language definition is almost the same as in papers. There is one difference, we implemented substitutions as a function. In reality, substitution in multi-staged lambda-calculus is not a function. I believe this doesn’t effect correctness of theorems. At one point I’ll refactor the code and define substitution as a relation.
- I used
`Case`

,`SCase`

,`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 …