Homotopy Type Theory: How long is the computer-assisted proof that concatenation of paths is associative

Question

My question refers to Lemma $2.1.4\ (\text{iv})$ of the HoTT book. I chose this lemma because it is simple to understand yet tedious to prove by hand. I have never used a proof assistant before, so I'm curious to see how helpful it would be.

I am hoping that a computer-assisted proof looks like the second proof given in the book. That proof is simple and intuitive. However, I could not accept it without filling in all of the details, and doing so did not teach me anything.

Of course simpler proofs are possible, but that is not the point of the question. I am asking about writing the given proof in a proof assistant. I would like to see an example of how the code looks in Coq (or another program).

Answer 1

About 2-3 lines in Coq. The context of the statement (the type, the four elements and the three paths) is longer than the proof itself.

Lemma concat_assoc {A: Type} {x y z w: A} (p: x = y) (q: y = z) (r: z = w):
(p @ q) @ r = p @ (q @ r).
Proof.
  destruct p, q, r.
  reflexivity.
Defined.

Here, p @ q is a notation for path concatenation. All we're doing is using path induction on all three paths (though just q and r would suffice, depending on the exact definition of concatenation) and then using the reflexive path to connect the two sides of the equation.