4

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.

Anton Trunov
  • 15,074
  • 2
  • 23
  • 43
madipi
  • 355
  • 2
  • 11

1 Answers1

3

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

Arthur Azevedo De Amorim
  • 23,012
  • 3
  • 33
  • 39
  • 1
    Sorry @Artur, just one more question. If I had to do the same, but using the Leibniz's equality instead of Path Induction, how could I define Leibniz's equality using inductive types? I am trying to do so, but I am in trouble since I don't know how to specify the difference in the dependent type. – madipi Aug 03 '17 at 17:45
  • It depends on what you mean by "Leibniz equality." Note that Coq's standard equality (`=`, which is infix syntax for `eq`) is actually an inductive proposition: its definition really just `eq1` given above. – Arthur Azevedo De Amorim Aug 03 '17 at 17:50
  • Yes I know, and if I am not wrong it is equivalent to the Leibniz one. The difference I meant was about the dependent type. In `eq1` the elimination type depends on a inhabitant `P x (refl A x)`. On the other hand with Leibniz the elimination type does not depend on the proof-term `refl A x`, but only on `P x x`. I mean, instead of having a proof of equality as second "parameter" there's just `x`. – madipi Aug 03 '17 at 18:01
  • But what exactly do you mean by "Leibniz equality"? The standard equality in Coq? Or something else? – Arthur Azevedo De Amorim Aug 03 '17 at 18:04
  • 1
    Something else. I actually find it difficult to explain. During lectures, my professor explained four types of equality: à la Gentzen (https://ibb.co/imQOCF), Leibniz (https://ibb.co/n0uBzv), Martin-Lof (https://ibb.co/fALZKv) and with Path Induction (https://ibb.co/esZuKv). The links point to the rules she gave us. The difference among these four types rely on the type C. I find it difficult to formalize the first and the second with inductive types because I cannot find a way to specify that type. – madipi Aug 03 '17 at 21:11
  • I see. I have an answer, but I think it is easier for you to post this as a different question. – Arthur Azevedo De Amorim Aug 03 '17 at 21:24
  • Yes, you're right. Here is the link to the new question: https://stackoverflow.com/questions/45495135/defining-different-equality-types-as-inductive-types-in-coq . I cannot thank you enough for your help! – madipi Aug 03 '17 at 21:54