# Documentation

Std.Data.Bool

@[inline, reducible]
abbrev xor :

Boolean exclusive or

Equations
Instances For
@[inline, reducible]
abbrev Bool.not :

not x, or !x, is the boolean "not" operation (not to be confused with Not : Prop → Prop, which is the propositional connective).

Equations
Instances For
@[inline, reducible]
abbrev Bool.or (x : Bool) (y : Bool) :

or x y, or x || y, is the boolean "or" operation (not to be confused with Or : Prop → Prop → Prop, which is the propositional connective). It is @[macro_inline] because it has C-like short-circuiting behavior: if x is true then y is not evaluated.

Equations
Instances For
@[inline, reducible]
abbrev Bool.and (x : Bool) (y : Bool) :

and x y, or x && y, is the boolean "and" operation (not to be confused with And : Prop → Prop → Prop, which is the propositional connective). It is @[macro_inline] because it has C-like short-circuiting behavior: if x is false then y is not evaluated.

Equations
Instances For
@[inline, reducible]
abbrev Bool.xor :

Boolean exclusive or

Equations
Instances For
instance Bool.instDecidableForAllBool (p : ) [inst : ] :
Decidable (∀ (x : Bool), p x)
Equations
• One or more equations did not get rendered due to their size.
instance Bool.instDecidableExistsBool (p : ) [inst : ] :
Decidable (∃ (x : Bool), p x)
Equations
• One or more equations did not get rendered due to their size.
instance Bool.instLEBool :
Equations
instance Bool.instLTBool :
Equations
instance Bool.instMaxBool :
Equations
instance Bool.instMinBool :
Equations

### and #

@[simp]
theorem Bool.not_and_self (x : Bool) :
(!x && x) = false
@[simp]
theorem Bool.and_not_self (x : Bool) :
(x && !x) = false
theorem Bool.and_comm (x : Bool) (y : Bool) :
(x && y) = (y && x)
theorem Bool.and_left_comm (x : Bool) (y : Bool) (z : Bool) :
(x && (y && z)) = (y && (x && z))
theorem Bool.and_right_comm (x : Bool) (y : Bool) (z : Bool) :
(x && y && z) = (x && z && y)
theorem Bool.and_or_distrib_left (x : Bool) (y : Bool) (z : Bool) :
(x && (y || z)) = (x && y || x && z)
theorem Bool.and_or_distrib_right (x : Bool) (y : Bool) (z : Bool) :
((x || y) && z) = (x && z || y && z)
theorem Bool.and_xor_distrib_left (x : Bool) (y : Bool) (z : Bool) :
(x && xor y z) = xor (x && y) (x && z)
theorem Bool.and_xor_distrib_right (x : Bool) (y : Bool) (z : Bool) :
(xor x y && z) = xor (x && z) (y && z)
theorem Bool.not_and (x : Bool) (y : Bool) :
(!(x && y)) = (!x || !y)

De Morgan's law for boolean and

theorem Bool.and_eq_true_iff (x : Bool) (y : Bool) :
(x && y) = true
theorem Bool.and_eq_false_iff (x : Bool) (y : Bool) :
(x && y) = false

### or #

@[simp]
theorem Bool.not_or_self (x : Bool) :
(!x || x) = true
@[simp]
theorem Bool.or_not_self (x : Bool) :
(x || !x) = true
theorem Bool.or_comm (x : Bool) (y : Bool) :
(x || y) = (y || x)
theorem Bool.or_left_comm (x : Bool) (y : Bool) (z : Bool) :
(x || (y || z)) = (y || (x || z))
theorem Bool.or_right_comm (x : Bool) (y : Bool) (z : Bool) :
(x || y || z) = (x || z || y)
theorem Bool.or_and_distrib_left (x : Bool) (y : Bool) (z : Bool) :
(x || y && z) = ((x || y) && (x || z))
theorem Bool.or_and_distrib_right (x : Bool) (y : Bool) (z : Bool) :
(x && y || z) = ((x || z) && (y || z))
theorem Bool.not_or (x : Bool) (y : Bool) :
(!(x || y)) = (!x && !y)

De Morgan's law for boolean or

theorem Bool.or_eq_true_iff (x : Bool) (y : Bool) :
(x || y) = true
theorem Bool.or_eq_false_iff (x : Bool) (y : Bool) :
(x || y) = false

### xor #

@[simp]
theorem Bool.false_xor (x : Bool) :
= x
@[simp]
theorem Bool.xor_false (x : Bool) :
= x
@[simp]
theorem Bool.true_xor (x : Bool) :
= !x
@[simp]
theorem Bool.xor_true (x : Bool) :
= !x
@[simp]
theorem Bool.not_xor_self (x : Bool) :
xor (!x) x = true
@[simp]
theorem Bool.xor_not_self (x : Bool) :
(xor x !x) = true
theorem Bool.not_xor (x : Bool) (y : Bool) :
xor (!x) y = !xor x y
theorem Bool.xor_not (x : Bool) (y : Bool) :
(xor x !y) = !xor x y
@[simp]
theorem Bool.not_xor_not (x : Bool) (y : Bool) :
(xor (!x) !y) = xor x y
theorem Bool.xor_self (x : Bool) :
xor x x = false
theorem Bool.xor_comm (x : Bool) (y : Bool) :
xor x y = xor y x
theorem Bool.xor_left_comm (x : Bool) (y : Bool) (z : Bool) :
xor x (xor y z) = xor y (xor x z)
theorem Bool.xor_right_comm (x : Bool) (y : Bool) (z : Bool) :
xor (xor x y) z = xor (xor x z) y
theorem Bool.xor_assoc (x : Bool) (y : Bool) (z : Bool) :
xor (xor x y) z = xor x (xor y z)
@[simp]
theorem Bool.xor_left_inj (x : Bool) (y : Bool) (z : Bool) :
xor x y = xor x z y = z
@[simp]
theorem Bool.xor_right_inj (x : Bool) (y : Bool) (z : Bool) :
xor x z = xor y z x = y

### le/lt #

@[simp]
theorem Bool.le_true (x : Bool) :
@[simp]
theorem Bool.false_le (x : Bool) :
@[simp]
theorem Bool.le_refl (x : Bool) :
x x
@[simp]
theorem Bool.lt_irrefl (x : Bool) :
¬x < x
theorem Bool.le_trans {x : Bool} {y : Bool} {z : Bool} :
x yy zx z
theorem Bool.le_antisymm {x : Bool} {y : Bool} :
x yy xx = y
theorem Bool.le_total (x : Bool) (y : Bool) :
x y y x
theorem Bool.lt_asymm {x : Bool} {y : Bool} :
x < y¬y < x
theorem Bool.lt_trans {x : Bool} {y : Bool} {z : Bool} :
x < yy < zx < z
theorem Bool.lt_iff_le_not_le {x : Bool} {y : Bool} :
x < y x y ¬y x
theorem Bool.lt_of_le_of_lt {x : Bool} {y : Bool} {z : Bool} :
x yy < zx < z
theorem Bool.lt_of_lt_of_le {x : Bool} {y : Bool} {z : Bool} :
x < yy zx < z
theorem Bool.le_of_lt {x : Bool} {y : Bool} :
x < yx y
theorem Bool.le_of_eq {x : Bool} {y : Bool} :
x = yx y
theorem Bool.ne_of_lt {x : Bool} {y : Bool} :
x < yx y
theorem Bool.lt_of_le_of_ne {x : Bool} {y : Bool} :
x yx yx < y
theorem Bool.le_of_lt_or_eq {x : Bool} {y : Bool} :
x < y x = yx y
theorem Bool.eq_true_of_true_le {x : Bool} :

### min/max #

@[simp]
theorem Bool.max_eq_or :
max = or
@[simp]
theorem Bool.min_eq_and :
min = and

### injectivity lemmas #

theorem Bool.not_inj {x : Bool} {y : Bool} :
(!x) = !yx = y
theorem Bool.not_inj_iff {x : Bool} {y : Bool} :
(!x) = !y x = y
@[deprecated Bool.not_inj_iff]
theorem Bool.not_inj' {x : Bool} {y : Bool} :
(!x) = !y x = y

Alias of Bool.not_inj_iff.

theorem Bool.and_or_inj_right {m : Bool} {x : Bool} {y : Bool} :
(x && m) = (y && m)(x || m) = (y || m)x = y
theorem Bool.and_or_inj_right_iff {m : Bool} {x : Bool} {y : Bool} :
(x && m) = (y && m) (x || m) = (y || m) x = y
@[deprecated Bool.and_or_inj_right_iff]
theorem Bool.and_or_inj_right' {m : Bool} {x : Bool} {y : Bool} :
(x && m) = (y && m) (x || m) = (y || m) x = y

Alias of Bool.and_or_inj_right_iff.

theorem Bool.and_or_inj_left {m : Bool} {x : Bool} {y : Bool} :
(m && x) = (m && y)(m || x) = (m || y)x = y
theorem Bool.and_or_inj_left_iff {m : Bool} {x : Bool} {y : Bool} :
(m && x) = (m && y) (m || x) = (m || y) x = y
@[deprecated Bool.and_or_inj_left_iff]
theorem Bool.and_or_inj_left' {m : Bool} {x : Bool} {y : Bool} :
(m && x) = (m && y) (m || x) = (m || y) x = y

Alias of Bool.and_or_inj_left_iff.

@[simp]
theorem Bool.false_eq_decide_iff {p : Prop} [h : ] :
@[simp]
theorem Bool.true_eq_decide_iff {p : Prop} [h : ] :
p

## toNat #

def Bool.toNat (b : Bool) :

convert a Bool to a Nat, false -> 0, true -> 1

Equations
• = bif b then 1 else 0
Instances For
@[simp]
@[simp]
theorem Bool.toNat_true :
theorem Bool.toNat_le_one (c : Bool) :
1