尝试理解索引类型族的概念

Question

定义如下：

Inductive eq (A : Type) (x : A) : A → Prop := eq refl : (eq x) x

Parameter a b : A.

当我考虑其中一个实例 eq a b 时，我读到了类型 A -> Prop 的 (eq a)。

那么，我的问题是，(eq a) b如何确定a和b对应的是同一个对象呢？

令我感到奇怪的是，我们没有关于 (eq a) 实际做什么的信息。

Answer 1

Eq a 是一个谓词，只有当它的参数等于 b 时才被定义（只有居民 eq_refl），其中相等意味着 "up to unification by the typechecker"。所以 Coq 必须认为 a 与 b 相同，否则 Eq a b 等价于 False。

Answer 2

为了补充 John 的回答，人们似乎很欣赏我在这里给出的关于我如何直观地看待索引类型族的非正式描述：

我还要补充一点，类型 (eq a) b（与 eq a b 相同）和具有此类型的术语之间存在区别。

例如，您可以定义：

Definition a_weird_type : Type := eq 0 42.

因为这样的类型只是一种说法，没有证据。但是，您不应该定义类型为 a_weird_type 的 a_weird_term，因为您永远无法说服系统 0 和 42 实际上是相等的。

请注意，虽然还有一点检查，因此您不能定义：

Definition a_weirder_type : Type := eq 42 true. (* Coq will reject this *)

因为eq类型隐式携带了它比较的元素的类型，类型系统将确保两个元素具有该类型：

Check (@eq nat 42 true).
(*                ^^^^ this should have type nat *)

Check (@eq bool 42 true).
(*              ^^ this should have type bool *)

Check (@eq nat 23 42).
(* fine, but not provable *)

尝试理解索引类型族的概念

Try to understand concept of Indexed type family

coq

type-families