HoTT in Coq

It seems like I would be missing the point of HoTT if I didn’t learn how to use it in a proof assistant. And it also seemed like it would make things more fun! So I decided to get and learn the HoTT’s computational implementation in Coq.

The installation went relatively smoothly, except that I had to patch one of the configuration files before it would compile (which has since been patched in the official version). I also got Proof General to use it with Emacs. I was impressed by how easy this was to install, even after reading that it was easy to install.

Once everything was working, I poked around and looked at all the theory files. There were some things I recognized, but also a lot of things that were foreign. I found these video tutorials for Coq by Andrej Bauer, which were very helpful. I tried following along, but I didn’t get very far because the firstorder command didn’t work in the HoTT version! But they were still very helpful for showing the way around Coq.

By this time, I was itching to get started proving things with Coq. So first, I tried looking for some of the theorems and definitions from the book in the theory files that came with my version of Coq. I quickly found that the relevant files were Overture.v and PathGroupoids.v. Somewhat confusingly, it looks like Notation is used for definitions, and Definition is used for lemmas. Well ok, whatever works. Once I got a feel for the notation, I tried writing out the type for some of the lemmas, and checking to see if I got it right.

Definition ap_pp {A B : Type} (f : A -> B) {x y z: A} (p : x = y) (q : y = z) :
  ap f (p @ q) = (ap f p) @ (ap f q). 

Yay, it works! Now to prove it. (I’ll talk more about ap next time.) Looking at the proofs in the PathGroupoids.v file, it looked like the eliminator could be invoked with destruct. So now everything thing was replaced with identity paths, good good. It looked pretty trivial after this… and after using reflexivity, everything was proved! These two commands got me surprisingly far, and helped cement how induction worked in my head.

I was curious to see what would happen for the example from last time. First let’s set things up…

Definition why_not_pp_p {A : Type} {x : A} (p : x = x):
  p @ p = p.

*****************************
1 subgoals, subgoal 1 (ID 158)

 A : Type
 x : A
 p : x = x
 ============================
  p @ p = p

Now let’s try destroying p!

Proof.
> destruct p.

******************************
Toplevel input, characters 0-10:
Error: Cannot instantiate metavariable P of type
"forall a : A, x0 = a -> Type" with abstraction
"fun (x0 : A) (p : x0 = x0) => p @ p = p" of incompatible type
"forall x0 : A, x0 = x0 -> Type".

Good! Looks like me and Coq caught the same error. So everything works as expected.

Playing with Coq is actually pretty fun, and it is a very convenient way of writing out (and verifying) my proofs to some of the exercises! Also, if I have a hard time understanding a new concept, writing it out in Coq helps clarify things for me – usually since it forces me to make sure all the types match up, which is usually where my confusion lies.