如何阅读Coq对proj1_sig的定义？ [英] How can I read Coq's definition of proj1_sig?

问题描述

在Coq中， sig 定义为

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

我读为

A sig P是一种类型，其中P是一个接受A并返回Prop的函数。定义该类型，使得如果P x成立，则类型A的元素x就是sig P类型。

"A sig P is a type, where P is a function taking an A and returning a Prop. The type is defined such that an element x of type A is of type sig P if P x holds."

proj1_sig 定义为

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

我不确定该怎么做。有人可以提供更直观的理解吗？

I'm not sure what to make of that. Could somebody provide a more intuitive understanding?

推荐答案

非依赖对与 sig

Non-dependent pairs vs. sig

定义类型，使得元素 x 类型为 A P x 成立，则code>的类型为 sig P 。

这并不完全正确：我们不能说 x：信号AP 。 sig AP 类型的居民 e 本质上是元素<$ c的对 $ c> x：A 和 P x 成立的证明（称为依赖对）。 x 和 P x 通过数据构造器存在。

That is not entirely correct : we can't say x : sig A P. An inhabitant e of type sig A P is essentially a pair of an element x : A and a proof that P x holds (this is called a dependent pair). x and P x are "wrapped" together using the data constructor exist.

要查看此信息，我们首先考虑定义的非依赖对类型 prod

To see this let us first consider the non-dependent pair type prod, which is defined as follows:

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

prod 的居民是对，例如 pair 1 true （或使用符号（1，true）），其中

prod's inhabitants are pairs, like pair 1 true (or, using notations, (1, true)), where the types of both components are independent of each other.

由于 A->，所以这两个组成部分的类型相互独立。 Coq中的B 只是语法<_c $ c> forall _的语法糖：A，B （已定义此处），可以将 prod 的定义修改为

Since A -> B in Coq is just syntactic sugar for forall _ : A, B (defined here), the definition of prod can be desugared into

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

上面的定义也许可以帮助我们了解的元素sig AP 是（依赖的）对。

The above definition, perhaps, can help to see that elements of sig A P are (dependent) pairs.

从实现中我们可以看到 proj1_sig e 解开了对，而
返回了 first 组件，即。 x ，丢掉了 P x 的证明。

From the implementation we can see that proj1_sig e unpacks the pair and returns the first component, viz. x, throwing away the proof of P x.

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

The Coq.Init.Specif module contains the following comment:

（sig AP）或更具暗示性的 {x：A | P x} 表示满足谓词 P A 类型元素的子集>。

(sig A P), or more suggestively {x:A | P x}, denotes the subset of elements of the type A which satisfy the predicate P.

如果我们查看 proj1_sig

Check proj1_sig.

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

我们会看到 proj1_sig 给了我们从子集 {x：A |中恢复超集 A 的元素的一种方法P x} 。

we will see that proj1_sig gives us a way of recovering an element of a superset A from its subset {x : A | P x}.

另外，我们可以说在某种意义上 proj1_sig 类似于 fst 函数，该函数返回一对的第一个组件：

Also, we can say that in some sense proj1_sig is analogous to the fst function, which returns the first component of a pair:

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 编写类似的语句：

We can formulate a similar statement for proj1_sig:

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

这篇关于如何阅读Coq对proj1_sig的定义？的文章就介绍到这了，希望我们推荐的答案对大家有所帮助，也希望大家多多支持IT屋！