我如何阅读Coq对proj1_sig的定义？

Question

在Coq中,sig定义为

Inductive sig (A:Type) (P:A -> Prop) : Type :=
    exist : forall x:A, P x -> sig P.

我读到的是

"sig P是一种类型,其中P是取A并返回Prop的函数.定义类型,使得如果P x成立,则类型A的元素x的类型为sig P."

proj1_sig 被定义为

Definition proj1_sig (e:sig P) := match e with
                                    | exist _ a b => a
                                    end.

我不知道该怎么做.有人可以提供更直观的理解吗？

Answer 1

非依赖对 sig

定义类型,使得x类型的元素的类型A为sig Pif P x.

这不完全正确:我们不能说x : sig A P.e类型的居民sig A P本质上是一对元素x : A和P x持有的证据(这被称为依赖对).x并P x使用数据构造函数"包装"在一起exist.

为了看到这一点,让我们首先考虑非依赖对类型prod,其定义如下:

Inductive prod (A B : Type) : Type :=  pair : A -> B -> A * B

prod居民是成对的,如pair 1 true(或使用符号(1, true)),两个组成部分的类型彼此独立.

因为A -> B在Coq中只是语法糖forall _ : A, B(在此定义),所以prod可以将其定义为desugared

Inductive prod (A B : Type) : Type :=  pair : forall _ : A, B -> prod A B

或许,上面的定义可以帮助看到sig A P(依赖)对的元素.

我们可以从实现和类型中获得什么 proj1_sig

从实现中我们可以看到proj1_sig e解包该对并返回第一个组件,即.x扔掉证据P x.

该Coq.Init.Specif模块包含以下注释:

(sig A P)或更具暗示性地{x:A | P x}表示A满足谓词的类型元素的子集P.

如果我们看一下的类型 proj1_sig

Check proj1_sig.

proj1_sig : forall (A : Type) (P : A -> Prop), {x : A | P x} -> A

我们将看到,它proj1_sig为我们提供了一种A从子集中恢复超集元素的方法{x : A | P x}.

fst和之间的模拟proj1_sig

此外,我们可以说在某种意义上proj1_sig类似于fst函数,它返回一对的第一个组件:

Check @fst.

fst : forall A B : Type, A * B -> A

有一个微不足道的财产fst:

Goal forall A B (a : A) (b : B),
  fst (a, b) = a.
Proof. reflexivity. Qed.

我们可以为以下内容制定类似的声明proj1_sig:

Goal forall A (P : A -> Prop) (x : A) (prf : P x),
  proj1_sig (exist P x prf) = x.
Proof. reflexivity. Qed.