为什么逻辑连接词和布尔值在 Coq 中是分开的？
Why are logical connectives and booleans separate in Coq?
我有 JavaScript/Ruby 编程背景并且习惯了 true/false 的工作方式（在 JS 中）：
!true
// false
!false
// true
然后您可以将这些 true/false 值与 && 一起使用，例如
var a = true, b = false;
a && !b;
因此 and 和 not（以及其他 logical/boolean 运算符）是单个系统的一部分； "logical" 系统和 "boolean" 系统似乎是一回事。
然而，在 Coq 中，逻辑和布尔值是两个不同的东西。为什么是这样？下面的 quote/link 演示了如何将它们联系起来需要一个定理。
We've already seen several places where analogous structures can be found in Coq's computational (Type) and logical (Prop) worlds. Here is one more: the boolean operators andb and orb are clearly analogs of the logical connectives ∧ and ∨. This analogy can be made more precise by the following theorems, which show how to translate knowledge about andb and orb's behaviors on certain inputs into propositional facts about those inputs.
Theorem andb_prop : ∀b c,
andb b c = true → b = true ∧ c = true.
http://www.seas.upenn.edu/~cis500/current/sf/Logic.html#lab211
本质上，Coq 两者都有，因为它们对不同的事物有用：布尔值对应于可以机械检查的事实（即，使用算法），而命题可以表达更多的概念。
严格来说，逻辑世界和布尔世界在 Coq 中并不是分开的：布尔世界是逻辑世界的一个子集。换句话说，您可以将每个语句表示为布尔计算，都可以将其视为一个逻辑命题（即 Prop 类型的东西）：如果 b : bool 表示一个语句，我们可以断言该语句b = true 为真，属于 Prop.
类型
Coq 中的逻辑比布尔值更多的原因是前面语句的逆命题不成立：并非所有逻辑事实都可以被视为布尔计算。换句话说，Ruby 和 JavaScript 等普通编程语言中的布尔值并不是 Coq 中同时包含 bool 和 Prop 的情况，因为 Props 可以表达这些语言中的布尔值所不能表达的东西。
为了说明这一点，请考虑以下 Coq 谓词：
Definition commutative {T} (op : T -> T -> T) : Prop :=
forall x y, op x y = op y x.
顾名思义，这个谓词断言运算符 op 是可交换的。编程语言中的许多运算符都是可交换的：例如，对整数进行乘法和加法运算。实际上，在 Coq 中我们可以证明以下陈述（我相信这些是《软件基础》一书中的示例）：
Lemma plus_comm : commutative plus. Proof. (* ... *) Qed.
Lemma mult_comm : commutative mult. Proof. (* ... *) Qed.
现在，想想如何用更传统的语言翻译像 commutative 这样的谓词。如果这看起来很困难，那并非偶然：可以证明我们不能用这些语言编写返回布尔值的程序来测试操作是否可交换。您当然可以编写 单元测试 来检查这个事实是否适用于特定输入，例如：
2 + 3 == 3 + 2
4 * 5 == 5 * 4
但是，如果您的操作员使用无限数量的输入，这些单元测试只能涵盖所有可能情况的一小部分。因此，测试总是弱于完整的形式证明。
如果 Props 可以表达布尔值所能表达的一切，你可能想知道为什么我们还要在 Coq 中使用布尔值。原因是 Coq 是一种 构造性逻辑 ，这正是 Vinz 在他的评论中所暗示的。这一事实最著名的后果是在 Coq 中我们无法证明以下直观原则：
Definition excluded_middle :=
forall P : Prop, P \/ ~ P.
这实质上是说每个命题要么为真，要么为假。 "How could this possibly fail?"，你可能会问自己。粗略地说，在构造逻辑（尤其是 Coq）中，每个证明都对应一个我们可以执行的算法。特别是，当您在构造逻辑中证明形式为 A \/ B 的陈述时，您可以从该证明中提取（始终终止）算法来回答 A 或 B 是否成立。因此，如果我们能够证明上述原则，我们就会有一个算法，给定一些命题，告诉我们该命题是否有效。然而，可计算性理论表明，由于不可判定性，这通常是不可能的：如果我们将 P 表示为 "program p halts on input x"，则排中将产生 halting problem 的判定器，这不能存在。
现在，Coq 中布尔值的有趣之处在于，通过构造它们允许使用排中律，因为它们 对应于我们可以 运行 的算法.具体来说，我们可以证明如下：
Lemma excluded_middle_bool :
forall b : bool, b = true \/ negb b = true.
Proof. intros b; destruct b; simpl; auto. Qed.
因此，在 Coq 中，将布尔值视为命题的特例是有用的，因为它们允许其他命题不允许的推理形式，即案例分析。
当然，你可以认为要求每个证明都对应一个算法是愚蠢的，事实上大多数逻辑都允许排中原理。默认情况下遵循这种方法的证明助手的例子包括 Isabelle/HOL and the Mizar 系统。在这些系统中，我们不必区分布尔值和命题，它们被视为同一事物。例如，伊莎贝尔只有 bool，没有 Prop。 Coq 还允许您通过假设允许您对一般命题执行案例分析的公理来模糊布尔值和命题之间的区别。另一方面，在这样的设置中，当你编写一个 returns 布尔值的函数时，你可能无法获得可以作为算法执行的东西，而 Coq 中默认情况下总是如此。
我有 JavaScript/Ruby 编程背景并且习惯了 true/false 的工作方式（在 JS 中）：
!true
// false
!false
// true
然后您可以将这些 true/false 值与 && 一起使用，例如
var a = true, b = false;
a && !b;
因此 and 和 not（以及其他 logical/boolean 运算符）是单个系统的一部分； "logical" 系统和 "boolean" 系统似乎是一回事。
然而，在 Coq 中，逻辑和布尔值是两个不同的东西。为什么是这样？下面的 quote/link 演示了如何将它们联系起来需要一个定理。
We've already seen several places where analogous structures can be found in Coq's computational (Type) and logical (Prop) worlds. Here is one more: the boolean operators andb and orb are clearly analogs of the logical connectives ∧ and ∨. This analogy can be made more precise by the following theorems, which show how to translate knowledge about andb and orb's behaviors on certain inputs into propositional facts about those inputs.
Theorem andb_prop : ∀b c, andb b c = true → b = true ∧ c = true.
http://www.seas.upenn.edu/~cis500/current/sf/Logic.html#lab211
本质上，Coq 两者都有，因为它们对不同的事物有用：布尔值对应于可以机械检查的事实（即，使用算法），而命题可以表达更多的概念。
严格来说，逻辑世界和布尔世界在 Coq 中并不是分开的：布尔世界是逻辑世界的一个子集。换句话说，您可以将每个语句表示为布尔计算，都可以将其视为一个逻辑命题（即 Prop 类型的东西）：如果 b : bool 表示一个语句，我们可以断言该语句b = true 为真，属于 Prop.
Coq 中的逻辑比布尔值更多的原因是前面语句的逆命题不成立：并非所有逻辑事实都可以被视为布尔计算。换句话说，Ruby 和 JavaScript 等普通编程语言中的布尔值并不是 Coq 中同时包含 bool 和 Prop 的情况，因为 Props 可以表达这些语言中的布尔值所不能表达的东西。
为了说明这一点，请考虑以下 Coq 谓词：
Definition commutative {T} (op : T -> T -> T) : Prop :=
forall x y, op x y = op y x.
顾名思义，这个谓词断言运算符 op 是可交换的。编程语言中的许多运算符都是可交换的：例如，对整数进行乘法和加法运算。实际上，在 Coq 中我们可以证明以下陈述（我相信这些是《软件基础》一书中的示例）：
Lemma plus_comm : commutative plus. Proof. (* ... *) Qed.
Lemma mult_comm : commutative mult. Proof. (* ... *) Qed.
现在，想想如何用更传统的语言翻译像 commutative 这样的谓词。如果这看起来很困难，那并非偶然：可以证明我们不能用这些语言编写返回布尔值的程序来测试操作是否可交换。您当然可以编写 单元测试 来检查这个事实是否适用于特定输入，例如：
2 + 3 == 3 + 2
4 * 5 == 5 * 4
但是，如果您的操作员使用无限数量的输入，这些单元测试只能涵盖所有可能情况的一小部分。因此，测试总是弱于完整的形式证明。
如果 Props 可以表达布尔值所能表达的一切，你可能想知道为什么我们还要在 Coq 中使用布尔值。原因是 Coq 是一种 构造性逻辑 ，这正是 Vinz 在他的评论中所暗示的。这一事实最著名的后果是在 Coq 中我们无法证明以下直观原则：
Definition excluded_middle :=
forall P : Prop, P \/ ~ P.
这实质上是说每个命题要么为真，要么为假。 "How could this possibly fail?"，你可能会问自己。粗略地说，在构造逻辑（尤其是 Coq）中，每个证明都对应一个我们可以执行的算法。特别是，当您在构造逻辑中证明形式为 A \/ B 的陈述时，您可以从该证明中提取（始终终止）算法来回答 A 或 B 是否成立。因此，如果我们能够证明上述原则，我们就会有一个算法，给定一些命题，告诉我们该命题是否有效。然而，可计算性理论表明，由于不可判定性，这通常是不可能的：如果我们将 P 表示为 "program p halts on input x"，则排中将产生 halting problem 的判定器，这不能存在。
现在，Coq 中布尔值的有趣之处在于，通过构造它们允许使用排中律，因为它们 对应于我们可以 运行 的算法.具体来说，我们可以证明如下：
Lemma excluded_middle_bool :
forall b : bool, b = true \/ negb b = true.
Proof. intros b; destruct b; simpl; auto. Qed.
因此，在 Coq 中，将布尔值视为命题的特例是有用的，因为它们允许其他命题不允许的推理形式，即案例分析。
当然，你可以认为要求每个证明都对应一个算法是愚蠢的，事实上大多数逻辑都允许排中原理。默认情况下遵循这种方法的证明助手的例子包括 Isabelle/HOL and the Mizar 系统。在这些系统中，我们不必区分布尔值和命题，它们被视为同一事物。例如，伊莎贝尔只有 bool，没有 Prop。 Coq 还允许您通过假设允许您对一般命题执行案例分析的公理来模糊布尔值和命题之间的区别。另一方面，在这样的设置中，当你编写一个 returns 布尔值的函数时，你可能无法获得可以作为算法执行的东西，而 Coq 中默认情况下总是如此。