Доказательство изоморфизма равенства Мартин-Лофа и индукции пути в Coq

Question

Я изучаю Coq и пытаюсь доказать изоморфизм между равенством Мартина-Лофа и равенством Пути.

Я определил два равенства следующим образом.

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.

И я определил две функции, участвующие в изоморфизме, следующим образом.

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.

Сейчас я пытаюсь определить следующие контрольные термины, но я не могу отойти от первоначального утверждения, потому что на самом деле не знаю, какую тактику применять.

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

Я через, я мог бы упростить выражение

(g x y (f x y m))

но я не знаю как это сделать. Кто-нибудь знает, как я могу продолжать это доказательство?

Заранее спасибо.

Answer 1

Проблема в том, что ваше определение типов идентичности является неполным, потому что оно не определяет, как el взаимодействует с refl, Вот полное решение.

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.

В качестве альтернативы, вы могли бы просто определить два типа идентичности как индуктивные типы Coq, которые дали бы вам те же принципы без необходимости формулировать отдельные аксиомы; Вычислительное поведение Coq уже приводит к нужным вам уравнениям. Я использовал синтаксис сопоставления с образцом, но подобные определения возможны при использовании стандартных комбинаторов eq1_rect а также 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.

Хотя не сразу понятно, eq1 соответствует вашему PathInduction.eq, а также eq2 соответствует вашему MartinLof.eq, Вы можете проверить это, попросив Coq напечатать типы их рекурсивных принципов:

Check eq1_rect.
Check eq2_rect.

Вы можете заметить, что я определил два в Type вместо Prop, Я просто сделал это, чтобы сделать принципы рекурсии, сгенерированные Coq, ближе к тем, которые у вас были; по умолчанию Coq использует более простые принципы рекурсии для вещей, определенных в Prop (хотя это поведение можно изменить с помощью нескольких команд).