eq_rect是什么，它在Coq中的定义在哪里？

Question

据我所了解，eq_rect和等式密切相关。奇怪的是，我在手册上找不到它的定义。

它来自哪里？它的意思是什么？

- Siddharth Bhat

Answer 1

如果您使用Locate eq_rect，您会发现eq_rect位于Coq.Init.Logic中，但是如果您查看该文件，其中没有eq_rect。那么，这是怎么回事呢？

当您定义归纳类型时，在许多情况下，Coq会自动为您生成3个归纳原理，并将_rect，_rec，_ind附加到类型名称后面。

要理解eq_rect的含义，您需要知道它的类型。

Check eq_rect.

开始：

eq_rect
     : forall (A : Type) (x : A) (P : A -> Type),
       P x -> forall y : A, x = y -> P y

你需要理解莱布尼茨等式的概念：

莱布尼茨将等式的概念描述如下： 对于任意的 x 和 y，当且仅当对于任意的谓词 P，P(x) 等价于 P(y)，则有 x = y。

在这个定律中，"P(x) 等价于 P(y)" 可以被弱化为 "P(x) 如果 P(y)"；这个修改后的定律与原始定律等价，因为一个适用于 "任意的 x 和 y" 的语句同样适用于 "任意的 y 和 x"。

简单来说，上述引文表明，如果 x 和 y 相等，则它们对于每个谓词的“行为”都是相同的。

为了更清晰地看到Leibniz等式与eq_rect直接对应，我们可以将eq_rect的参数顺序重新排列为以下等效表述：

eq_rect_reorder
     : forall (A : Type) (P : A -> Type) (x y : A), 
         x = y -> P x -> P y

- Anton Trunov

---

谢谢！另外两个生成的术语是什么？我假设 _ind 是归纳原理。_rec 是什么？ - Siddharth Bhat

这些原则具有相同的形式，它们之间的区别在于谓词 P 的类型：对于 eq_rect，它是 A -> Type，对于 eq_ind，它是 A -> Prop，而对于 eq_rec，它是 A -> Set。实际上，eq_rec 只是 eq_rect 的一个特例，您可以使用 Print eq_rec 进行检查。 - Anton Trunov

请注意，您还可以使用类似于 Scheme eq_rect := Minimality for eq Sort Type、Scheme eq_rec := Minimality for eq Sort Set、Scheme eq_ind := Minimality for eq Sort Prop 的方式生成这些原则。还有一些依赖版本，您可以将 Minimality 替换为 Induction，并获得诸如 forall (A : Type) (x : A) (P : forall a : A, x = a -> Type), P x eq_refl -> forall (y : A) (e : x = y), P y e 这样的方案。我相信 Coq 会自动选择在 Prop 中归纳的 Minimality，而在落入 Set 和 Type 中的归纳中选择 Induction。 - Jason Gross