我试图在 Coq 中定义不同类型的等式。在大学课程中，我的教授给了我们四种不同类型的规则，如下（我只提供规则的链接）：
这四种类型的区别在于C型。
我试图证明它们之间的同构。不幸的是，我在将第一个和第二个声明为归纳类型时遇到了一些麻烦，因为我找不到指定类型 C 的方法。我有第三个和第四个的定义，并且我已经证明了它们之间的同构。
提前致谢。
【问题讨论】：
标签： equality coq coq-tactic
如果不了解其他两个原则，您就不能完全使用归纳类型来获得完全体现前两个原则的东西。原因是 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 演算中数据类型的类似编码一样 - 是将类型定义为其（非依赖）消除器或折叠的类型。这个定义有时被称为 Leibniz 等式，并且确实提供了与您在 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 的基本理论与称为 impredicativity 的东西有关。但这是一个正交问题。）
如果不断言额外的公理，就不可能为这种新的相等编码获得原则 3 和 4。证明这一点需要对forall P, P a -> P b 类型的元素进行案例分析，并论证所有这些元素的形式为refl 应用于某些东西。但是，这是一种函数，在 Coq 的基础理论中没有办法对它们进行案例分析。请注意，这个论点超出了 Coq 的理论：断言 3 和 4 对于这种新类型是有效的作为额外公理并不矛盾；如果没有这些公理，就不可能证明这一点。
【讨论】：
refl 上进行模式匹配，因为它不是构造函数，而且我不确定如何继续使用 Proof 环境。我认为我的问题是关于 Coq 标准平等的使用。