equality - 在 Coq 中将不同的相等类型定义为归纳类型

Question

我试图在 Coq 中定义不同类型的等式。在大学类(class)中，我的教授给了我们四种不同类型的规则，如下(我只提供了规则的链接):

绅士:https://ibb.co/imQOCF

莱布尼茨:https://ibb.co/n0uBzv

马丁-洛夫:https://ibb.co/fALZKv

路径归纳:https://ibb.co/esZuKv

这四种类型之间的差异取决于类型 C。

我试图证明它们之间的同构。不幸的是，我在将第一个和第二个声明为归纳类型时遇到了一些麻烦，因为我找不到指定类型 C 的方法。我有第三个和第四个的定义，并且我已经证明了它们之间的同构。

提前致谢。

Answer 1

你不能完全使用归纳类型来获得完全体现前两个原则的东西而不获得其他两个。这样做的原因是 Coq 归纳数据类型自动支持强依赖消除，这意味着允许结果类型引用被消除的元素。这就是您在给定的最后两组规则中看到的:类型 C允许引用证明p那两点a和 b是平等的。任何合理的归纳定义的相等类型都将自动支持规则 3 和 4，从而支持较弱的规则 1 和 2。例如，下面是如何使用 Coq 的标准相等来获得 1 和 2。

Section Gentzen.

Variables (A : Type) (C : A -> A -> Type).

Definition e_id_g {a b : A} (p : a = b) (c : C a a) : C a b :=
  match p with eq_refl => fun c => c end c.

Definition c_id_g (a : A) (c : C a a) : e_id_g (eq_refl a) c = c :=
  eq_refl.

End Gentzen.

Section Leibniz.

Variables (A : Type) (C : A -> A -> Type).

Definition e_id_l {a b : A} (p : a = b) (c : forall x, C x x) : C a b :=
  match p with eq_refl => c a end.

Definition c_id_l (a : A) (c : forall x, C x x) :
                  e_id_l (eq_refl a) c = c a :=
  eq_refl.

End Leibniz.

可以给出一个不同的定义，它只支持规则 1 和 2，但不支持规则 3 和 4，通过使用 Church 相等编码:

Definition eq {A} (a b : A) : Prop :=
  forall P : A -> Prop, P a -> P b.

Definition refl {A} (a : A) : eq a a :=
  fun P x => x.

这里的想法——与 lambda 演算中数据类型的类似编码一样——是将类型定义为其(非依赖)消元或折叠的类型。这个定义有时被称为莱布尼茨等式，并且确实提供了与您在 1 和 2 中得到的基本相同的证明规则，如下面的脚本所示。

Section Gentzen.

Variables (A : Type) (C : A -> A -> Prop).

Definition e_id_g {a b : A} (p : eq a b) (c : C a a) : C a b :=
  p (C a) c.

Definition c_id_g (a : A) (c : C a a) : e_id_g (refl a) c = c :=
  eq_refl.

End Gentzen.

Section Leibniz.

Variables (A : Type) (C : A -> A -> Prop).

Definition e_id_l {a b : A} (p : eq a b) (c : forall x, C x x) : C a b :=
  p (C a) (c a).

Definition c_id_l (a : A) (c : forall x, C x x) :
                  e_id_l (refl a) c = c a :=
  eq_refl.

End Leibniz.

(这些原则实际上有点不同:它们仅限于 Prop ，这是由于 Coq 基本理论中与不可预测性相关的限制。但这是一个正交问题。)

如果不主张额外的公理，就不可能获得这种新的平等编码的原则 3 和原则 4。证明这一点需要对 forall P, P a -> P b 类型的元素进行案例分析。 ，并认为所有这些元素的形式都是 refl应用于某事。但是，这是一种函数，在 Coq 的基础理论中没有办法对它们进行案例分析。请注意，这个论点超出了 Coq 的理论:将 3 和 4 对这种新类型有效作为额外公理的断言并不矛盾；如果没有这些公理，就不可能证明这一点。