20.11. 布尔值🔗

inductive type

Bool : Type
Bool : Type

The Boolean values, true and false.

Logically speaking, this is equivalent to Prop (the type of propositions). The distinction is public important for programming: both propositions and their proofs are erased in the code generator, while Bool corresponds to the Boolean type in most programming languages and carries precisely one bit of run-time information.

Constructors

Bool.false : Bool

The Boolean value false, not to be confused with the proposition False.

Bool.true : Bool

The Boolean value true, not to be confused with the proposition True.

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

20.11.1. 运行时表示🔗

由于 Bool 是 enum inducing 类型，因此它在编译代码中由单个字节表示。

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。

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

20.11.3. 句法🔗

syntaxBoolean Infix Operators

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

term ::= ...
    | Boolean “and”, also known as conjunction. `and x y` can be written `x && y`.

The corresponding propositional connective is `And : Prop → Prop → Prop`, written with the `∧`
operator.

The Boolean `and` is a `@[macro_inline]` function in order to give it short-circuiting evaluation:
if `x` is `false` then `y` is not evaluated at runtime.


Conventions for notations in identifiers:

 * The recommended spelling of `&&` in identifiers is `and`.term && term

term ::= ...
    | Boolean “or”, also known as disjunction. `or x y` can be written `x || y`.

The corresponding propositional connective is `Or : Prop → Prop → Prop`, written with the `∨`
operator.

The Boolean `or` is a `@[macro_inline]` function in order to give it short-circuiting evaluation:
if `x` is `true` then `y` is not evaluated at runtime.


Conventions for notations in identifiers:

 * The recommended spelling of `||` in identifiers is `or`.term || term

term ::= ...
    | Boolean “exclusive or”. `xor x y` can be written `x ^^ y`.

`x ^^ y` is `true` when precisely one of `x` or `y` is `true`. Unlike `and` and `or`, it does not
have short-circuiting behavior, because one argument's value never determines the final value. Also
unlike `and` and `or`, there is no commonly-used corresponding propositional connective.

Examples:
 * `false ^^ false = false`
 * `true ^^ false = true`
 * `false ^^ true = true`
 * `true ^^ true = false`


Conventions for notations in identifiers:

 * The recommended spelling of `^^` in identifiers is `xor`.term ^^ term

syntaxBoolean Negation

前缀运算符 ! 是 Bool.not 的表示法。

term ::= ...
    | Boolean negation, also known as Boolean complement. `not x` can be written `!x`.

This is a function that maps the value `true` to `false` and the value `false` to `true`. The
propositional connective is `Not : Prop → Prop`.


Conventions for notations in identifiers:

 * The recommended spelling of `!` in identifiers is `not`.!term

20.11.4. API 参考🔗

20.11.4.1. 逻辑运算🔗

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

def

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

The conditional function.

cond c x y is the same as if c then x else y, but optimized for a Boolean condition rather than a decidable proposition. It can also be written using the notation bif c then x else y.

Just like ite, cond is declared @[macro_inline], which causes applications of cond to be unfolded. As a result, x and y are not evaluated at runtime until one of them is selected, and only the selected branch is evaluated.

def

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 → α) :
  α

The dependent conditional function, in which each branch is provided with a local assumption about the condition's value. This allows the value to be used in proofs as well as for control flow.

dcond c (fun h => x) (fun h => y) is the same as if h : c then x else y, but optimized for a Boolean condition rather than a decidable proposition. Unlike the non-dependent version cond, there is no special notation for dcond.

Just like ite, dite, and cond, dcond is declared @[macro_inline], which causes applications of dcond to be unfolded. As a result, x and y are not evaluated at runtime until one of them is selected, and only the selected branch is evaluated. dcond is intended for metaprogramming use, rather than for use in verified programs, so behavioral lemmas are not provided.

def

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

Boolean negation, also known as Boolean complement. not x can be written !x.

This is a function that maps the value true to false and the value false to true. The propositional connective is Not : Prop → Prop.

Conventions for notations in identifiers:

The recommended spelling of ! in identifiers is not.

def

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

Boolean “and”, also known as conjunction. and x y can be written x && y.

The corresponding propositional connective is And : Prop → Prop → Prop, written with the ∧ operator.

The Boolean and is a @[macro_inline] function in order to give it short-circuiting evaluation: if x is false then y is not evaluated at runtime.

Conventions for notations in identifiers:

The recommended spelling of && in identifiers is and.
The recommended spelling of || in identifiers is or.

def

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

Boolean “or”, also known as disjunction. or x y can be written x || y.

The corresponding propositional connective is Or : Prop → Prop → Prop, written with the ∨ operator.

The Boolean or is a @[macro_inline] function in order to give it short-circuiting evaluation: if x is true then y is not evaluated at runtime.

def

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

Boolean “exclusive or”. xor x y can be written x ^^ y.

x ^^ y is true when precisely one of x or y is true. Unlike and and or, it does not have short-circuiting behavior, because one argument's value never determines the final value. Also unlike and and or, there is no commonly-used corresponding propositional connective.

Examples:

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

Conventions for notations in identifiers:

The recommended spelling of ^^ in identifiers is xor.

20.11.4.2. 比较🔗

大多数布尔值比较应使用 DecidableEq Bool、LT Bool、LE Bool 实例执行。

def

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

Decides whether two Booleans are equal.

This function should normally be called via the DecidableEq Bool instance that it exists to support.