September 13, 2014 - Tagged as: coq, en.
I never managed to write anything with dependent types in Coq, without using tactics. Pattern matching is never giving enough information in cases to allow me to generate the term I want. Certified Programming with Dependent Types book describes “Convoy pattern”, which is a way to write dependently typed terms in Coq without using tactics. I later learned that standard inversion tactic also uses something like a convoy pattern, except it’s not as fine grained as what a user would write by hand.
Unfortunately, even after learning about convoy pattern, I’m still not satisfied with what I get when I write dependently typed definitions without using tactics. The reason is that convoy pattern is incredibly ugly and hard to read and understand. Even if I embrace the ugliness, most of the time I have no idea how to use the pattern so that 1) it’s not horribly verbose 2) does what I want.
I had a small verification idea: I was going to implement Pascal’s triangle as a co-inductive type and implement operations on it. Later I was hoping to prove that p(n, k) = p(n-1, k-1) + p(n-1, k) where k is column and p is row.
I struggled for this for a long time. The problem was that I was not comfortable with tactics and I couldn’t define dependently typed terms using fixpoints or definitions. Now that I’m comfortable enough with tactics, I finally managed to implement what I want.
Here are a few things that I also mentioned in my mail to Coq-club:
snoc has a redundant argument which could be eliminated by using OCaml lists for vectors. First argument of sum-pairs is redundant because it’s just vector’s length so we could use Vector.t’s field instead. Similarly, I think pascal_aux’s first argument may also be removed etc. (see generated OCaml from the Github link above)If you look at the Coq code, you’ll realize that I couldn’t prove even the simplest fact about my definition. This is the problem with tactic-generated terms. The reason I can’t prove anything is that simpl just doesn’t work anymore, and there are no workarounds. The terms are so huge and complex, nothing is provable anymore.
I got very good responses about alternatives and problems in Coq-club mailing list. One of them was the suggestion of giving functions types that 1) show the properties I’m trying to show in separate theorems 2) still subject to erasure.
This approach has an obvious problem. There won’t be a program/proof distinction anymore. As a programmer I don’t like this at all. Also, making sure that proof terms will be erased is hard.(see rest of the discussion from the mailing list link above) I don’t think I’ll follow this idea.
Another alternative is just using Agda. I have my problems with Agda which I’m deferring to another post for now. Some of my excuses may actually not be Agda’s problem but rather they may be Coq’s advantage. In any case, I probably won’t be using Agda.
So now I’m stuck with Coq – I can’t define anything without using tactics, but when I use tactics for definitions(instead of proofs) then I can’t prove anything.