20.11. 布尔值🔗

归纳类型

Bool : Type
Bool : Type

布尔值 true 和 false。

从逻辑上说，它等价于 Prop（命题的类型）。这一区别对编程非常重要：命题及其证明都会被代码生成器擦除，而 Bool 对应大多数编程语言中的布尔类型，恰好携带一位运行时信息。

构造子

Bool.false : Bool

布尔值 false，不要与命题 False 混淆。

Bool.true : Bool

布尔值 true，不要与命题 True 混淆。

构造子 Bool.true 和 Bool.false 是从 Bool 命名空间导出的，因此它们可以被写成 true 和 false。

20.11.1. 运行时表示🔗

因为 Bool 是一个枚举归纳类型，所以它在编译后的代码中由单字节表示。

20.11.2. 布尔值和命题🔗

Bool 和 Prop 都表示真理的概念。从纯逻辑的角度来看，它们是等价的：命题外延性意味着从根本上只有两个命题，即 True 和 False。然而，这里有一个重要的实用差异：Bool 划分程序可以计算的值，而 Prop 划分生成代码没有意义的陈述。换句话说，Bool 是适用于程序的真与假的概念，而 Prop 是适用于数学的概念。由于证明会从编译后的程序中被擦除，因此区分 Bool 和 Prop 可以明确 Lean 文件中的哪些部分旨在用于计算。

Bool 可以用在任何预期 Prop 的地方。从每个 Bool 类型的 b 到命题 b = true 都存在一个强制转换。根据 propext，true = true 等于 True，而 false = true 等于 False。

并非每个命题都可以被程序用来在运行时做出决定。否则，程序就可以对角谷猜想是真还是假进行分支！然而，许多命题可以通过算法来检查。这些命题被称为 可判定 命题，并具有 Decidable 类型类的实例。函数 Decidable.decide 将带有证明的 Decidable 结果转换为 Bool。此函数也是从可判定命题到 Bool 的强制转换，因此 (2 = 2 : Bool) 的计算结果为 true。

20.11.3. 语法🔗

语法布尔中缀运算符

中缀运算符 &&、|| 和 ^^ 分别是 Bool.and、Bool.or 和 Bool.xor 的记号。

term ::= ...
    | term && term

term ::= ...
    | term || term

term ::= ...
    | term ^^ term

语法布尔非

前缀运算符 ! 是 Bool.not 的记号。

term ::= ...
    | !term

20.11.4. API 参考🔗

20.11.4.1. 逻辑运算🔗

函数 cond、and 和 or 是短路的。换句话说，false && BIG_EXPENSIVE_COMPUTATION 不需要执行 BIG_EXPENSIVE_COMPUTATION 就可返回 false。这些函数使用 macro_inline 属性定义，这会使得编译器在生成代码时将其调用替换为它们的定义，并且这些定义使用嵌套模式匹配来实现短路行为。

定义

cond.{u} {α : Sort u} (c : Bool) (x y : α) : α
cond.{u} {α : Sort u} (c : Bool)
  (x y : α) : α

条件函数。

cond c x y 与 if c then x else y 相同，但针对布尔条件而非可判定命题进行了优化。也可用记法 bif c then x else y 书写。

与 ite 一样，cond 被声明为 @[macro_inline]，这会展开 cond 的应用。因此，运行时在选定 x 或 y 之前不会求值它们，并且只会求值选中的分支。

定义

Bool.dcond.{u} {α : Sort u} (c : Bool) (x : c = true → α)
  (y : c = false → α) : α
Bool.dcond.{u} {α : Sort u} (c : Bool)
  (x : c = true → α) (y : c = false → α) :
  α

依赖条件函数，其中每个分支都会获得一个关于条件值的局部假设。这样既可将该值用于证明，也可用于控制流。

dcond c (fun h => x) (fun h => y) 与 if h : c then x else y 相同，但针对布尔条件而非可判定命题进行了优化。与非依赖版本 cond 不同，dcond 没有专用记法。

与 ite、dite 和 cond 一样，dcond 被声明为 @[macro_inline]，这会展开 dcond 的应用。因此，运行时在选定 x 或 y 之一之前不会求值它们，并且只会求值选中的分支。dcond 旨在用于元编程，而非已验证程序，因此不提供行为引理。

定义

Bool.not : Bool → Bool
Bool.not : Bool → Bool

布尔否定，也称布尔补。not x 可写作 !x。

此函数将值 true 映射为 false，并将值 false 映射为 true。对应的命题联结词是 Not : Prop → Prop。

标识符中记法的约定：

在标识符中，! 的推荐拼写是 not。

定义

Bool.and (x y : Bool) : Bool
Bool.and (x y : Bool) : Bool

布尔“与”，也称合取。and x y 可写作 x && y。

对应的命题联结词是 And : Prop → Prop → Prop，用 ∧ 运算符书写。

布尔 and 是 @[macro_inline] 函数，从而实现短路求值：若 x 为 false，则运行时不会求值 y。

标识符中记法的约定：

在标识符中，&& 的推荐拼写是 and。
在标识符中，|| 的推荐拼写是 or。

定义

Bool.or (x y : Bool) : Bool
Bool.or (x y : Bool) : Bool

布尔“或”，也称析取。or x y 可写作 x || y。

对应的命题联结词是 Or : Prop → Prop → Prop，用 ∨ 运算符书写。

布尔 or 是 @[macro_inline] 函数，从而实现短路求值：若 x 为 true，则运行时不会求值 y。

定义

Bool.xor : Bool → Bool → Bool
Bool.xor : Bool → Bool → Bool

布尔“异或”。xor x y 可写作 x ^^ y。

x ^^ y 为 true，恰当且仅当 x 和 y 中恰有一个为 true。与 and 和 or 不同，它不具有短路行为，因为任一参数的值都不能单独确定最终结果。此外，与 and 和 or 不同，它没有常用的对应命题联结词。

示例：

false ^^ false = false
true ^^ false = true
false ^^ true = true
true ^^ true = false

标识符中记法的约定：

在标识符中，^^ 的推荐拼写是 xor。

20.11.4.2. 比较🔗

大多数关于布尔值的比较应该使用 DecidableEq Bool、LT Bool 和 LE Bool 实例来执行。

定义

Bool.decEq (a b : Bool) : Decidable (a = b)
Bool.decEq (a b : Bool) :
  Decidable (a = b)

判定两个布尔值是否相等。

通常应通过它所支持的 DecidableEq Bool 实例调用此函数。