在Coq中将不同的相等类型定义为归纳类型 [英] Defining different equality types as inductive types in Coq
问题描述
我试图在Coq中定义不同类型的平等。在大学课程中，我的教授为我们提供了四种不同类型的规则，如下所示（我仅提供规则的链接）：
I am trying to define in Coq different types of equalities. During an university course my professor gave us the rules of four different types, as follows (I provide just the links to the rules):
- Gentzen： https://ibb.co/imQOCF
- Leibniz： https://ibb.co/n0uBzv
- Martin-Lof： https://ibb.co/fALZKv
- 路径归纳：< a href = https://ibb.co/esZuKv rel = nofollow noreferrer> https://ibb.co/esZuKv
- Gentzen : https://ibb.co/imQOCF
- Leibniz : https://ibb.co/n0uBzv
- Martin-Lof : https://ibb.co/fALZKv
- Path Induction : https://ibb.co/esZuKv
这四种类型之间的差异取决于类型C。
The difference among these four types relies on the type C.
我试图证明它们之间的同构。不幸的是，我在将第一个和第二个类型定义为归纳类型时遇到了一些麻烦，因为我找不到找到指定类型C的方法。我为第三个和第四个定义了，并且我已经证明了它们之间的同构。
I am trying to prove the isomorphism among them. Unfortunately I have some troubles in declaring as inductive types the first and the second, because I cannot find a way to specify the type C. I have a definition for the third and the fourth, and I already proved the isomorphism between them.
预先感谢。
推荐答案
您不能完全使用归纳类型以获得完全体现前两个原理的东西，而没有获得其他两个原理。原因是Coq归纳数据类型自动支持强依赖性消除，这意味着结果类型允许引用要消除的元素。这是在您提供的最后两组规则中看到的：类型 C 允许引用证明 p 两个点 a 和 b 相等。任何合理的归纳定义的相等类型都将自动支持较弱的规则3和4，并因此支持规则1和2。例如，这就是在Coq的标准相等性下获得1和2的方式。
You cannot quite use inductive types to obtain something that embodies exactly the first two principles without getting the other two. The reason for that is that Coq inductive data types automatically support strong dependent elimination, which means that the result type is allowed to refer to the element being eliminated. This is what you see in the last two sets of rules you gave: the type C is allowed to refer to a proof p that two points a and b are equal. Any reasonable inductively defined equality type will automatically support rules 3 and 4, and thus 1 and 2, which are weaker. For instance, here's how you get 1 and 2 with Coq's standard equality.
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编码：
It is possible to give a different definition that supports just rules 1 and 2, but not 3 and 4, by using a Church encoding of equality:
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中获得的证明规则基本相同的证明规则，如以下脚本所示。
The idea here -- as in similar encodings for data types in the lambda calculus -- is to define a type as the type of its (non-dependent) eliminator, or fold. This definition is sometimes known as Leibniz equality, and indeed provides essentially the same proof rules as you got in 1 and 2, as the following script shows.
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 有关的限制。但这是一个正交的问题。）
(These principles are actually a bit different: they are restricted to Prop, due to restrictions in Coq's basic theory related to something called impredicativity. But this is an orthogonal issue.)
如果不主张额外的公理，就不可能获得这种新的相等编码的原理3和4。要证明这一点，就需要对类型为 forall P，P a->的元素进行案例分析。 P b ，并争辩说所有这些元素的形式都是 refl 应用于某种事物。但是，这是一种功能，Coq的基本理论中无法对这些功能进行案例分析。请注意，该论点超出了Coq的理论范围：将3和4对此新类型有效是一个额外的公理，这并不矛盾。没有这些公理就不可能证明如此。
Without asserting extra axioms, it is impossible to obtain principles 3 and 4 for this new encoding of equality. Proving this would require doing a case analysis on elements of the type forall P, P a -> P b, and arguing that all these elements are of the form refl applied to something. However, this is a type of functions, and there is no way in Coq's basic theory to perform case analysis on those. Note that this argument lays outside of Coq's theory: it is not contradictory to assert as an extra axiom that 3 and 4 are valid for this new type; it is just impossible to prove so without these axioms.
这篇关于在Coq中将不同的相等类型定义为归纳类型的文章就介绍到这了，希望我们推荐的答案对大家有所帮助，也希望大家多多支持IT屋！
