Coq:Prop与类型中的设置(n)

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

set和type版本还包含set和type定义的归纳原则(分别为rec和rect).这是我对Prop和Set之间差异的了解程度; Prop的诱导较弱.

我还读到,虽然Set是预测性的,但Prop是不可预测的,但这似乎是属性而不是定义的质量.

虽然Set和Prop之间的一些实际(道德？)差异是明确的,但Set和Prop之间的确切定义差异以及它们适合类型范围的位置尚不清楚(运行检查Prop和Set给出类型(*(设置)+ 1*)),我不确定如何解释这个...

Answer 1

Type : 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的这一章吗？