Ezra elias kilty Cooper (Jan 10 2021 at 05:03): Ezra elias kilty Cooper (Jan 10 2021 at 05:03):After working with Coq for a few years, I've just started doing some dependently-typed programming in Coq for the first time. I'm finding it very painful! None of my usual techniques for doing equality proofs by induction work, or they seem to take a lot of extra work. For example, I wanted to prove forall (u : Vector.t A n) v w, u ++ (v ++ w) = (u ++ v) ++ w for size-indexed vectors.
First I found that I had to state the lemma using something like JMeq, which seemed no big deal. Then I found that I couldn't actually use propositions stated this way, such as the IH, to rewrite subterms of the goal, because the two terms have different types.
I spent some time reading about related issues in Adam Chlipala's book (CPDT) but wasn't quite finding the essence of the techniques to use.
Eventually, I spotted some code in the CoLoR library that did what I want <https://github.com/fblanqui/color/blob/master/Util/Vector/VecUtil.v>, by always casting the right-hand vector in every equality. This allowed me to prove some lemmas like the associativity, but seems to require a lot of extra work.
Is it fundamentally hard to work with structures like this, where the objects in a rewrite often have equivalent, but distinct types?
Is it just fundamentally hard to do dependently-typed programming in Coq, or am I going about it all wrong?
Guillaume Melquiond (Jan 10 2021 at 08:04):Your life will be significantly easier if you stop using Vector.t and use a different definition of vectors instead, e.g., the tuple type from MathComp. (You can define it yourself if you want; it is quite easy.) This type looks like tuple A n := { val: list A; HL: eqb (length l) n = true }. What makes this type so much easier to use is that you can drop at any time from the dependently typed world to the simply typed one. Indeed, the property val t1 = val t2 -> t1 = t2 always holds (without any axiom, thanks to the uniqueness of boolean identity proofs). For example, if at some point, you need the associativity of vector concatenation, just drop to the list world and use the associativity of list concatenation instead. That is a one-liner.
Enrico Tassi (Jan 10 2021 at 08:20):You can read more about this tuple type in section 7.1 of this book: https://zenodo.org/record/4282710#.X_q4aGso-yU
Bas Spitters (Jan 10 2021 at 09:40):Try using Equations...
Ezra elias kilty Cooper (Jan 10 2021 at 23:31):Guillaume, thank you for the recommendation. It sounds like my troubles with Vector.t are not unique. Enrico, thanks for the book reco, I'll check it out.
Ezra elias kilty Cooper (Jan 10 2021 at 23:32):Bas: does Equations help with using Vector.t? I have seen an Equations library that allows writing a function as a set of equations, but I'm not sure how it would help with things like showing associativity of vector-append.
Karl Palmskog (Jan 10 2021 at 23:42):all kinds of dependent pattern matching is easier with Equations, I believe this is what Bas means: https://github.com/mattam82/Coq-Equations
Matthieu Sozeau (Jan 11 2021 at 17:06):Equations does not automagically solve the problem that the inductive definition of size-indexed lists is painful to use if you start appending them etc... then you'll have to use a dependent equality type one way or the other. That's not limited to Coq, only systems which have a more relaxed conversion relation allowing to identify, e.g. n + (m + p) with (n + m) + p can handle this with less "pain". What you're really working with is the type sigma n : nat, vector A n in this case, and the equality for this is naturally v = v' <-> sigma p : v.len = v'.len, v.vector = coerce p v'.vector with a cast. You can show this is equivalent to vec_to_list v = vec_to_list v', but it's way simpler to just use tuple in the first place.
Ezra elias kilty Cooper (Jan 12 2021 at 04:04):That's a great summary, Matthieu, thanks. I'll steer towards tuple.
Last updated: Oct 08 2024 at 14:01 UTC