equality - 什么是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's equality的概念:

Leibniz characterized the notion of equality as follows: Given any x and y, x = y if and only if, given any predicate P, P(x) if and only if P(y).

In this law, "P(x) if and only if P(y)" can be weakened to "P(x) if P(y)"; the modified law is equivalent to the original, since a statement that applies to "any x and y" applies just as well to "any y and 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