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

Question

根据我的阅读，eq_rect平等似乎有着深深的联系。奇怪的是，我无法在手册上找到它的定义。

它来自哪里，它的状态是什么？

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

并且您需要了解莱布尼兹平等的概念：

莱布尼兹（Leibniz）将平等的概念描述如下：给定任意x和y，x = y当且仅当给定谓词P，P(x)当且仅当P(y)。

在该法律中，“ P(x)可以且仅当P(y)”可以弱化为“ P(x)如果P(y)”；修改后的法律等同于原始法律，因为适用于“ any xand y” 的陈述也适用于“ any yand x”。

较不正式地讲，上面的引文说，如果x和y相等，则每个谓词的“行为”是相同的。

为了更清楚地看到莱布尼兹的等式直接对应于，eq_rect我们可以将参数的顺序重新排列eq_rect为以下等效公式：

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