How to use HoTT path induction in Coq?

Question

In Coq I have

Definition f (s:Unit) : tt=tt := match s with tt => idpath end.
Definition g (p:tt=tt) : Unit := match p with idpath => tt end.

and I would like to prove forall (p:tt=tt), (f o g) p = p.

I want to do it using the path induction described in 1.12.1 in HoTT's book.

It is clear that for the case in which p is idpath, we can prove

assert( (f o g) idpath = idpath).
simpl.
reflexivity.

But how do I use path induction in Coq to package together the whole proof?

The whole proof until now: (What to put instead of admit?)

Require Import HoTT.
Definition f (s:Unit) : tt=tt := match s with tt => idpath end.
Definition g (p:tt=tt) : Unit := match p with idpath => tt end.
Theorem myTheorem : forall (p:tt=tt), (f o g) p = p.
  assert( (f o g) idpath = idpath).
  simpl.
  reflexivity.
admit.

Answer 1

I realize this question is super old and has long been solved but I do want to note that HoTT path induction is done slightly differently than Arthur's answer prescribes. I think this is helpful to see for two reasons: (i) the way HoTT sets things up is a bit less complicated and (ii) it is more in line with how path induction is actually used in HoTT and so it will be easier to translate into their library. Both of these points are mostly for people like me who come upon this question years later.

First, the symbol equality symbol is redefined in HoTT to denote the path space, which is defined as being the inductive type with one generator refl x for each point in a type A.

So in HoTT we have

Inductive paths {A : UU} (x : A) := A -> UU
   | refl : paths a a.

Based path induction is then just the function paths_rect which is automatically generated by the Coq system. Path induction can then be defined as an instance of Based Path induction, as is done in The HoTT Book.

This can all be seen in the UniMath file "Preamble" in the Foundations directory.

Answer 2

The analog of path induction in Coq is the match construct. Here is how we can use it to define (based) path induction as described in the HoTT book.

Set Implicit Arguments.

Definition J {A} {x : A} (P : forall y, x = y -> Type)
                 (H : P x eq_refl) : forall y p, P y p :=
  fun y p => match p with eq_refl => H end.

The type of this definition says that, whenever we want to prove P y p, where

• y : A,
• p : x = y, and
• P : forall y, x = y -> Type,

it suffices to show that P x eq_refl holds. We can use J to show that your g function is constant. (I have rephrased the definitions to match the ones given by the Coq standard library.)

Definition f (s : unit) : tt = tt := match s with tt => eq_refl end.
Definition g (p : tt = tt) : unit := match p return unit with eq_refl => tt end.

Definition g_tt p : g p = tt :=
  J (fun y q => match q return unit with eq_refl => tt end = tt)
    eq_refl p.

The tricky part of this proof is finding out what the P parameter of J should be, which is also the case of other proofs that proceed by path induction. Here, I had to unfold the definition of g, because it requires an argument of type tt = tt, whereas the q used above has type tt = y. In any case, you can see that P tt p is definitionally equal to g p = tt, which is what we want to prove.

We can play trick to show that p = eq_refl for any p : tt = tt. Combined with the previous result, it will give exactly what you want.

Definition result (p : tt = tt) : p = eq_refl :=
  J (fun y q =>
       unit_rect (fun z => tt = z -> Prop)
                 (fun u => u = eq_refl)
                 y q)
    eq_refl p.

Once again, the crux is the P parameter. We make use of the induction principle for unit, which says that we can define something of type T x (for T : unit -> Type and x : tt) whenever we can find an element of T tt. Recall that the result of this application of J should have type

P tt p

which in this case is just

unit_rect (fun z => tt = z -> Prop)
          (fun u => u = eq_refl)
          tt p
= (p = eq_refl)

by the computation rules for unit_rect.

Unfortunately, this sort of proof is difficult to replicate with Coq's tactic language, because it often has trouble inferring what P should be. It is often easier to figure out what this value should be yourself and write down the proof term explicitly.

I don't quite understand why, but Coq is also much better at figuring out this annotation if you write down the proof term with match. Compare:

Definition result' (p : tt = tt) : p = eq_refl :=
  match p with eq_refl => eq_refl end.

Although this looks much simpler, you will see that the actual term inferred by Coq is much more complicated when you try to print it. Try it!

Edit

Ah, I just realized that you were trying to use the HoTT version of Coq. I don't have that version installed, but I think it shouldn't be too hard to adapt my solution to it.