在 Coq 中将不同的相等类型定义为归纳类型
Defining different equality types as inductive types in Coq
我试图在 Coq 中定义不同类型的等式。在一次大学课程中，我的教授给了我们四种不同类型的规则，如下（我只提供规则的链接）：
- 根岑：https://ibb.co/imQOCF
- 莱布尼茨：https://ibb.co/n0uBzv
- 马丁-洛夫：https://ibb.co/fALZKv
- 路径归纳：https://ibb.co/esZuKv
这四种类型的区别在于类型C。
我想证明它们之间的同构。不幸的是，我在将第一个和第二个声明为归纳类型时遇到了一些麻烦，因为我找不到指定类型 C 的方法。我有第三个和第四个的定义，并且我已经证明了它们之间的同构。
提前致谢。
您不能完全使用归纳类型来获得完全前两个原则而不得到其他两个原则的东西。原因是 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.
通过使用平等的 Church 编码，可以给出仅支持规则 1 和 2，而不支持规则 3 和 4 的不同定义：
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 对于这种新类型有效作为附加公理并不矛盾；没有这些公理就不可能证明这一点。
我试图在 Coq 中定义不同类型的等式。在一次大学课程中，我的教授给了我们四种不同类型的规则，如下（我只提供规则的链接）：
- 根岑：https://ibb.co/imQOCF
- 莱布尼茨：https://ibb.co/n0uBzv
- 马丁-洛夫：https://ibb.co/fALZKv
- 路径归纳：https://ibb.co/esZuKv
这四种类型的区别在于类型C。
我想证明它们之间的同构。不幸的是，我在将第一个和第二个声明为归纳类型时遇到了一些麻烦，因为我找不到指定类型 C 的方法。我有第三个和第四个的定义，并且我已经证明了它们之间的同构。
提前致谢。
您不能完全使用归纳类型来获得完全前两个原则而不得到其他两个原则的东西。原因是 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.
通过使用平等的 Church 编码，可以给出仅支持规则 1 和 2，而不支持规则 3 和 4 的不同定义：
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 对于这种新类型有效作为附加公理并不矛盾；没有这些公理就不可能证明这一点。