在 Coq 中证明 Martin-Lof 等式与路径归纳之间的同构

Question

我正在研究 Coq，并试图证明 Martin-Lof 的等式和路径归纳的等式之间的同构。

我对这两个等式的定义如下。

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 中定义的事物使用更简单的递归原则（尽管可以通过一些命令来更改该行为）。