September 17, 2013 - Tagged as: en, coq.
Adam Chilpala’s Certified Programming with Dependent Types has a great discussion on writing automated proofs and readability of proofs. Highly recommended. Chapter 16(page 319 on current revision).
I think one key thing to realize about interactive theorem proving is that there is no perfect, or maybe even good, solution to the problem of proof representation. Tactics help, but without automation tactic based proofs are just too fragile(every change in definitions implies changes in proofs) and verbose. But automated proofs are very hard to read, and it’s very hard to modify automated proofs for changes. CPDT book has a great example of this. Let’s think of this proof(I’ll skip the definitions, just think some simple arithmetic expressions language just like you could find in any elementary programming language theory book)
Theorem eval_times : forall k e,
eval (times k e) = k * eval e.
Proof.
induction e as [| ? IHe1 ? IHe 2]; [
trivial
| simpl; rewrite IHe1; rewrite IHe2; rewrite mult_plus_distr_l; trivial ].
Qed.And now let’s say you added one more constructor to arithmetic expression syntax. How to change this proof to adopt the changes? I don’t think there’s a way to do that without first writing the version without automation. And that brings us back to my first post.
I think the reason why I think too much about this stuff instead of writing some proofs is that I look for elegance and simplicity in my programs. And only if necessary I try to make my programs efficient(fast, small, whatever). After some simple trivial proofs that I did for learning I never found my proofs satisfactory. They are either very very long and repetitive or very hard to understand and modify. It’s very hard to find a sweet-spot in proofs that is not very repetitive and long and still possible to read and understand.
You can always apply methods you learned to make your programs easier to read and modify, like moving some code to a new function with a useful name and formal parameters etc. but in the case of proofs it’s also very hard to find what pieces are considered worthy to be a lemma and what would be useful name for it.
My ideas about proof automation is changed from “no way I use them” to “okay they can be very useful for eliminating repetition without adding obscurity to the proof” in one day. I’ll continue writing Coq proofs for while and probably add new posts on this topic later.