Coq：提案与类型（n）中的集合 [英] Coq: Prop versus Set in Type(n)

问题描述

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

I want to consider the following three (related?) Coq definitions.

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

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

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

这三种类型都给出归纳原理来证明命题成立。

All three types give induction principles to prove a proposition holds.

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之间差异的了解的程度；道具的归纳性较弱。

The set and type versions also contain induction principles for definitions over set and type (rec and rect respectively). This is the extent of my knowledge about the difference between Prop and Set; Prop has a weaker induction.

我还读到，道具是强制性的，而Set是谓性的，但这似乎是一种属性，而不是定义性。

I have also read that Prop is impredicative while Set is predicative, but this seems like a property rather than a defining quality.

尽管Set和Prop之间存在一些实际的（道德上的）区别，但Set和Prop之间的确切定义区别以及它们在类型宇宙中的适合位置尚不清楚（在Prop和Set上运行检查得到Type（*（Set）+ 1 *））），我不确定如何解释这一点。

While some practical (moral?) differences between Set and Prop are clear, the exact, defining differences between Set and Prop, as well as where they fit into the universe of types is unclear (running check on Prop and Set gives Type (* (Set) + 1*)), and I'm not exactly sure how to interpret this...

推荐答案

Type：类型不一致。

强制性 Set 中间不包含表示证明不相关，因此强制性的 Set 带有证明相关性，例如 true<>错误的，反驳了不应该采用直觉主义的中间立场。

Impredicative Set with excluded middle implies proof irrelevance, so impredicative Set with proof relevance, e.g. true <> false, refutes excluded middle, which intuitionism isn't supposed to do.

因此，我们在 Prop 和其他类型层次结构为我们提供了谓语。

Therefore we leave impredicativity in Prop and the rest of the type hierarchy gives us predicativity.

顺便说一句，

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

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

is provable. Don't ask me what's the benefit of Coq only automatically proving that other weaker induction principle...

此外，您是否阅读过 CPDT的这一章？

这篇关于Coq：提案与类型（n）中的集合的文章就介绍到这了，希望我们推荐的答案对大家有所帮助，也希望大家多多支持IT屋！