证明Martin-Lof的等式与Path Coction在Coq中的同构

Question

我正在研究Coq并试图证明Martin-Lof的等式与Path Induction的同构。

我定义了两个等式如下。

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. 

虽然尚不清楚，对应于您PathInduction.eq，并eq2对应于您MartinLof.eq。您可以通过询问勒柯克打印自己的递归原理的类型检查：

Check eq1_rect. 
Check eq2_rect. 

您可能注意到，我在Type而不是Prop定义的两个。我只是这样做，使Coq生成的递归原理更接近你所拥有的递归原则;默认情况下，Coq对Prop中定义的事物使用更简单的递归原则（尽管该行为可以通过几条命令进行更改）。