Bool : Type
The Boolean values, true and false.
Logically speaking, this is equivalent to Prop (the type of propositions). The distinction is
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.
The constructors Bool.true and Bool.false are exported from the Bool namespace, so they can be written true and false.
Because Bool is an enum inductive type, it is represented by a single byte in compiled code.
Both Bool and Prop represent notions of truth.
From a purely logical perspective, they are equivalent: propositional extensionality means that there are fundamentally only two propositions, namely True and False.
However, there is an important pragmatic difference: Bool classifies values that can be computed by programs, while Prop classifies statements for which code generation doesn't make sense.
In other words, Bool is the notion of truth and falsehood that's appropriate for programs, while Prop is the notion that's appropriate for mathematics.
Because proofs are erased from compiled programs, keeping Bool and Prop distinct makes it clear which parts of a Lean file are intended for computation.
A Bool can be used wherever a Prop is expected.
There is a coercion from every Bool b to the proposition b = true.
By propext, true = true is equal to True, and false = true is equal to False.
Not every proposition can be used by programs to make run-time decisions.
Otherwise, a program could branch on whether the Collatz conjecture is true or false!
Many propositions, however, can be checked algorithmically.
These propositions are called decidable propositions, and have instances of the Decidable type class.
The function Decidable.decide converts a proof-carrying Decidable result into a Bool.
This function is also a coercion from decidable propositions to Bool, so (2 = 2 : Bool) evaluates to true.
The infix operators &&, ||, and ^^ are notations for Bool.and, Bool.or, and Bool.xor, respectively.
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 ::= ...
| 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 ::= ...
| 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`.
The prefix operator ! is notation for 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`.
The functions cond, and, and or are short-circuiting.
In other words, false && BIG_EXPENSIVE_COMPUTATION does not need to execute BIG_EXPENSIVE_COMPUTATION before returning false.
These functions are defined using the macro_inline attribute, which causes the compiler to replace calls to them with their definitions while generating code, and the definitions use nested pattern matching to achieve the short-circuiting behavior.
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.
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.
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.
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:
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.
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:
Conventions for notations in identifiers:
The recommended spelling of ^^ in identifiers is xor.
Most comparisons on Booleans should be performed using the DecidableEq Bool, LT Bool, LE Bool instances.