Coq: 在 Type(n) 中 Prop 和 Set 的区别

Question

我希望考虑以下三个（相关的？）Coq定义。

Inductive nat1: Prop :=
  | z1 : nat1
  | s1 : nat1 -> nat1.

Inductive nat2 : Set := 
  | z2 : nat2
  | s2 : nat2 -> nat2.

Inductive nat3 : Type :=
  | z3 : nat3
  | s3 : nat3 -> nat3.

这三种类型都提供了归纳原理来证明一个命题成立。

nat1_ind
     : forall P : Prop, P -> (nat1 -> P -> P) -> nat1 -> P

nat2_ind
     : forall P : nat2 -> Prop,
       P z2 -> (forall n : nat2, P n -> P (s2 n)) -> forall n : nat2, P n

nat3_ind
     : forall P : nat3 -> Prop,
       P z3 -> (forall n : nat3, P n -> P (s3 n)) -> forall n : nat3, P n

集合版本和类型版本还包含用于集合和类型上定义的归纳原理（rec和rect）。这是我对Prop和Set之间区别的全部了解；Prop的归纳性较弱。

我也读到过Prop是不明示的，而Set是明示的，但这似乎更像是一种属性而不是定义上的差异。

虽然有些实际（道德？）差别在Set和Prop之间很明显，但是Set和Prop的确切、定义上的差别以及它们如何适应类型世界并不清楚（对Prop和Set进行检查得到了类型（*（Set）+1*），我也不确定如何解释这个……

- Jonathan Gallagher

---

一个小观察：nat1在Prop中并没有定义自然数 - 这个问题在这里讨论过。 - Anton Trunov

Answer 1

类型(Type)不一致。

带有排中律的非预测性集合(Set)意味着证明无关性，因此带有证明相关性的非预测性集合(Set)（例如true <> false）反驳了排中律，这与直觉主义并不相符。

因此，我们将非预测性保留在Prop中，而类型层次结构的其余部分则给出了预测性。

顺便说一下，

forall P : nat1 -> Prop, P z1 -> (forall n : nat1, P n -> P (s1 n)) -> forall n : nat1, P n

是可证明的。不要问我Coq自动证明其他弱归纳原则有什么好处...

此外，你读过CPDT的这一章吗？

- gen

---

谢谢您的回答。我正在寻找更多“低级”/证明论解释这些差异。例如，Type0的居民除了Set和Prop之外还有什么，唯一的区别是可预测性吗？我发现这篇文章可以给出一个很好的大致想法http://www.cs.ucsb.edu/~benh/290C_W15/papers/Calculus%20of%20Inductive%20Constructions.pdf。但我还有一些细节缺失。此外，在Hott中，他们谈论集合和纯命题，我想知道Coq中的Prop是否就是这个意思。 - Jonathan Gallagher

Answer 2

刚刚花了一个小时读了这个。这是因为Coq会假设两个相同Prop的证明对象相等。这是一个公理，被称为证明无关性。

https://coq.inria.fr/library/Coq.Logic.ProofIrrelevance.html

它只是认为在Prop（这里是P）上的谓词不需要传递某些证明作为其参数（或假设），因此将其删除。

考虑到这一点。由于每个nat1都是相同的，因此无论我们尝试证明某个属性P，我们都可以在某些nat1上进行抽象，同时使用公理将其重写为所需的形式。因此，Coq生成了“简化”的归纳原理版本。

要生成“完整”的版本，您可以使用

Scheme nat1_ind_full := Induction for nat1 Sort Prop.

参考 Prop和Type的不同归纳原理

- Hexadecimal Hyuga