2
$\begingroup$

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).

$\endgroup$
1
  • $\begingroup$ Putting this in a comment since Metamath is not likely to be the sort of system you'd be interested in, but the Metamath Proof Explorer proof of associativity appears to be here. $\endgroup$
    – Mark S.
    May 18, 2020 at 10:20

1 Answer 1

2
$\begingroup$

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.

$\endgroup$
3
  • $\begingroup$ Nice! Do you have any recommendations for where to learn more about this? $\endgroup$ May 18, 2020 at 9:18
  • 1
    $\begingroup$ Before learning HoTT in Coq, I'd definitely try to get used to using it for more generic math. I've heard that Software Foundations is a pretty good introduction. The Coq documentation is dense but thorough. $\endgroup$
    – SCappella
    May 18, 2020 at 9:32
  • $\begingroup$ A good resource for HoTT formalization: github.com/EgbertRijke/HoTT-Intro $\endgroup$ May 18, 2020 at 10:43

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Not the answer you're looking for? Browse other questions tagged or ask your own question.