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.
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, andP : 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!
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.