I am studying Coq and trying to prove the isomorphism between Martin-Lof's equality and the Path Induction's one.
I defined the two equalities as follows.
Module MartinLof.
Axiom eq : forall A, A -> A -> Prop.
Axiom refl : forall A, forall x : A, eq A x x.
Axiom el : forall (A : Type) (C : forall x y : A, eq A x y -> Prop),
(forall x : A, C x x (refl A x)) ->
forall a b : A, forall p : eq A a b, C a b p.
End MartinLof.
Module PathInduction.
Axiom eq : forall A, A -> A -> Prop.
Axiom refl : forall A, forall x : A, eq A x x.
Axiom el : forall (A : Type) (x : A) (P : forall a : A, eq A x a -> Prop),
P x (refl A x) -> forall y : A, forall p : eq A x y, P y p.
End PathInduction.
And I defined the two functions involved in the isomorphism as follows.
Definition f {A} : forall x y: A, forall m: MartinLof.eq A x y, PathInduction.eq A x y.
Proof.
apply: (MartinLof.el A (fun a b p => PathInduction.eq A a b) _ x y m).
move=> x0.
exact: PathInduction.refl A x0.
Defined.
Definition g {A} : forall x y: A, forall p: PathInduction.eq A x y, MartinLof.eq A x y.
Proof.
apply: (PathInduction.el A x (fun a p => MartinLof.eq A x a) _ y p).
exact: MartinLof.refl A x.
Defined.
Now I am trying to define the following proof-terms, but I cannot move from the initial statement because I actually don't know what tactic to apply.
Definition pf1 {A}: forall x y: A, forall m: MartinLof.eq A x y,
eq m (g x y (f x y m)).
Definition pf2 {A} : forall x y: A, forall p: PathInduction.eq A x y,
eq p (f x y (g x y p)).
I through I could simplify the expression
(g x y (f x y m))
but I don't know how to do that. Does anyone know how I can go on on this proof?
Thanks in advance.
The problem is that your definition of the identity types is incomplete, because it does not specify how el interacts with refl. Here is a complete solution.
From mathcomp Require Import ssreflect.
Module MartinLof.
Axiom eq : forall A, A -> A -> Prop.
Axiom refl : forall A, forall x : A, eq A x x.
Axiom el : forall (A : Type) (C : forall x y : A, eq A x y -> Prop),
(forall x : A, C x x (refl A x)) ->
forall a b : A, forall p : eq A a b, C a b p.
Axiom el_refl : forall (A : Type) (C : forall x y : A, eq A x y -> Prop)
(CR : forall x : A, C x x (refl A x)),
forall x : A, el A C CR x x (refl A x) = CR x.
End MartinLof.
Module PathInduction.
Axiom eq : forall A, A -> A -> Prop.
Axiom refl : forall A, forall x : A, eq A x x.
Axiom el : forall (A : Type) (x : A) (P : forall a : A, eq A x a -> Prop),
P x (refl A x) -> forall y : A, forall p : eq A x y, P y p.
Axiom el_refl : forall (A : Type) (x : A) (P : forall y : A, eq A x y -> Prop)
(PR : P x (refl A x)),
el A x P PR x (refl A x) = PR.
End PathInduction.
Definition f {A} (x y: A) (m: MartinLof.eq A x y) : PathInduction.eq A x y.
Proof.
apply: (MartinLof.el A (fun a b p => PathInduction.eq A a b) _ x y m).
move=> x0.
exact: PathInduction.refl A x0.
Defined.
Definition g {A} (x y: A) (p: PathInduction.eq A x y) : MartinLof.eq A x y.
Proof.
apply: (PathInduction.el A x (fun a p => MartinLof.eq A x a) _ y p).
exact: MartinLof.refl A x.
Defined.
Definition pf1 {A} (x y: A) (m: MartinLof.eq A x y) : eq m (g x y (f x y m)).
Proof.
apply: (MartinLof.el A (fun x y p => p = g x y (f x y p))) => x0.
by rewrite /f MartinLof.el_refl /g PathInduction.el_refl.
Qed.
Definition pf2 {A} (x y: A) (m: PathInduction.eq A x y) : eq m (f x y (g x y m)).
Proof.
apply: (PathInduction.el A x (fun y p => p = f x y (g x y p))).
by rewrite /f /g PathInduction.el_refl MartinLof.el_refl.
Qed.
Alternatively, you could have just defined the two identity types as Coq inductive types, which would have given you the same principles without the need to state separate axioms; Coq's computation behavior already yields the equations you need. I have used pattern-matching syntax, but similar definitions are possible using the standard combinators eq1_rect and eq2_rect.
Inductive eq1 (A : Type) (x : A) : A -> Type :=
| eq1_refl : eq1 A x x.
Inductive eq2 (A : Type) : A -> A -> Type :=
| eq2_refl x : eq2 A x x.
Definition f {A} {x y : A} (p : eq1 A x y) : eq2 A x y :=
match p with eq1_refl _ _ => eq2_refl A x end.
Definition g {A} {x y : A} (p : eq2 A x y) : eq1 A x y :=
match p with eq2_refl _ z => eq1_refl A z end.
Definition fg {A} (x y : A) (p : eq2 A x y) : f (g p) = p :=
match p with eq2_refl _ _ => eq_refl end.
Definition gf {A} (x y : A) (p : eq1 A x y) : g (f p) = p :=
match p with eq1_refl _ _ => eq_refl end.
Although not immediately clear, eq1 corresponds to your PathInduction.eq, and eq2 corresponds to your MartinLof.eq. You can check this by asking Coq to print the types of their recursion principles:
Check eq1_rect.
Check eq2_rect.
You may notice that I have defined the two in Type instead of Prop. I just did this to make the recursion principles generated by Coq closer to the ones you had; by default, Coq uses simpler recursion principles for things defined in Prop (though that behavior can be changed with a few commands).