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?

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.

You can read more about this tuple type in section 7.1 of this book: https://zenodo.org/record/4282710#.X_q4aGso-yU

Try using Equations...

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.

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.

all kinds of dependent pattern matching is easier with Equations, I believe this is what Bas means: https://github.com/mattam82/Coq-Equations

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.

That's a great summary, Matthieu, thanks. I'll steer towards `tuple`

.

Last updated: Jan 28 2023 at 06:30 UTC