Coq中命题真/假和布尔真/假之间的区别[重复]

Question

布尔值true/false 的定义及其与命题类型True/False 的联系在Coq.Bool.Bool 中进行了描述：

Inductive bool : Set := true : bool | false : bool

Definition Is_true (b:bool) :=
  match b with
    | true => True
    | false => False
  end.

对于bool 类型，我或多或少了解它们的用途和功能，但Prop 类型并非如此。 This question 很好地说明了我的困惑。如那里所述，以下不是有效的定义：

Definition inv (a: Prop): Prop :=
match a with
| False => True
| True => False
end.

导致“Pattern "True" is redundant in this clause.”。另一方面，与 bool 类型相同的定义编译得很好：

Definition inv (a: bool): bool :=
  match a with
  | false => true
  | true => false
  end.

Ptival's answer 很好地解释了为什么在模式匹配意义上会发生这种情况：“False 不是数据构造函数 [...]”。事实上，通过检查 True 和 False 可以清楚地看到这一点：

Print True.
Print False.

Inductive True : Prop :=  I : True
Inductive False : Prop := 

然而，在这种情况下，我的问题变成了：为什么？如果它们与true/false 不一样，那么它们是什么？具体来说：

• 从命题 True 和 False 创建布尔值 true 和 false 的目的是什么，而不是将它们合并为一个原始构造？
• 如果Prop 版本True/False 与bool 版本true/false 的含义不同，那么它们的实际含义是什么以及它们应该代表什么与它们的布尔变量相比？

Answer 1

让我回答您的不同问题。 首先，在模式匹配中

Definition inv (a: Prop): Prop :=
  match a with
  | False => True
  | True => False
  end.

Coq 告诉您它是多余的，因为它将 False 和 True 解释为将被绑定的变量。事实上，True 和 False 无法匹配，因此它假定您的意思是命名变量 True 或 False。 这段代码相当于

Definition inv (a: Prop): Prop :=
  match a with
  | x => True
  | y => False
  end.

那么你就会明白为什么y 会是多余的：你说匹配任何值到True 和任何值到False。

---

我认为您最大的困惑是认为True 和False 应该在某种程度上与true 和false 具有相同的含义。简短的回答是：除了名称之外，根本没有任何关系。

实际上True 和False 比true 和false 更接近bool：它们是（数据）类型。 True 是只包含一个元素的类型，False 是空类型，没有居民。

Inductive True : Prop :=
| I : True.

Inductive False : Prop :=.

（诚然，False 的定义可能有点奇怪，但它确实表示它是一个没有构造函数的类型。）

相比之下，bool 是一个包含两个元素的类型：true 和 false。 所以你可以拥有h : True，它是True 的证明，但不是x : true，因为true 不是一种类型，而是一段数据。

可以观察数据（模式匹配），但不能观察数据类型。

我真的要坚持true 和false 不是True 和False 的变体。 true 和 false 只是一点点，除了你如何使用它们之外没有任何意义。另一方面，True 和 False 具有非常精确的含义。 True 是可证明的微不足道的命题，False 是永远不可证明的命题，h : False 表示矛盾。

False 的消除原理展示了如何使用它：

False_rect : ∀ P : Type, False → P

它说你可以从False 的证明中推导出任何东西。