# Documentation

## Init.Data.Bool

@[reducible, inline]
abbrev xor :

Boolean exclusive or

Equations
Instances For
@[reducible, inline]
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
@[reducible, inline]
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
@[reducible, inline]
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
@[reducible, inline]
abbrev Bool.xor :

Boolean exclusive or

Equations
Instances For
instance Bool.instDecidableForallOfDecidablePred (p : ) [inst : ] :
Decidable (∀ (x : Bool), p x)
Equations
instance Bool.instDecidableExistsOfDecidablePred (p : ) [inst : ] :
Decidable (∃ (x : Bool), p x)
Equations
@[simp]
theorem Bool.default_bool :
default = false
instance Bool.instLE :
Equations
instance Bool.instLT :
Equations
instance Bool.instDecidableLe (x : Bool) (y : Bool) :
Equations
instance Bool.instDecidableLt (x : Bool) (y : Bool) :
Decidable (x < y)
Equations
instance Bool.instMax :
Equations
instance Bool.instMin :
Equations
theorem Bool.eq_iff_iff {a : Bool} {b : Bool} :
a = b ( )
@[simp]
theorem Bool.decide_eq_true {b : Bool} [Decidable ()] :
decide () = b
@[simp]
theorem Bool.decide_eq_false {b : Bool} [Decidable ()] :
decide () = !b
@[simp]
theorem Bool.decide_true_eq {b : Bool} [Decidable ()] :
decide () = b
@[simp]
theorem Bool.decide_false_eq {b : Bool} [Decidable ()] :
decide () = !b

### and #

@[simp]
theorem Bool.and_self_left (a : Bool) (b : Bool) :
(a && (a && b)) = (a && b)
@[simp]
theorem Bool.and_self_right (a : Bool) (b : Bool) :
(a && b && b) = (a && b)
@[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)
instance Bool.instCommutativeAnd :
Std.Commutative fun (x x_1 : Bool) => x && x_1
Equations
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)
@[simp]
theorem Bool.and_iff_left_iff_imp (a : Bool) (b : Bool) :
(a && b) = a
@[simp]
theorem Bool.and_iff_right_iff_imp (a : Bool) (b : Bool) :
(a && b) = b
@[simp]
theorem Bool.iff_self_and (a : Bool) (b : Bool) :
a = (a && b)
@[simp]
theorem Bool.iff_and_self (a : Bool) (b : Bool) :
b = (a && b)

### or #

@[simp]
theorem Bool.or_self_left (a : Bool) (b : Bool) :
(a || (a || b)) = (a || b)
@[simp]
theorem Bool.or_self_right (a : Bool) (b : Bool) :
(a || b || b) = (a || b)
@[simp]
theorem Bool.not_or_self (x : Bool) :
(!x || x) = true
@[simp]
theorem Bool.or_not_self (x : Bool) :
(x || !x) = true
@[simp]
theorem Bool.or_iff_left_iff_imp (a : Bool) (b : Bool) :
(a || b) = a
@[simp]
theorem Bool.or_iff_right_iff_imp (a : Bool) (b : Bool) :
(a || b) = b
@[simp]
theorem Bool.iff_self_or (a : Bool) (b : Bool) :
a = (a || b)
@[simp]
theorem Bool.iff_or_self (a : Bool) (b : Bool) :
b = (a || b)
theorem Bool.or_comm (x : Bool) (y : Bool) :
(x || y) = (y || x)
instance Bool.instCommutativeOr :
Std.Commutative fun (x x_1 : Bool) => x || x_1
Equations
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)

### distributivity #

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.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.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)
@[simp]
theorem Bool.not_and (x : Bool) (y : Bool) :
(!(x && y)) = (!x || !y)

De Morgan's law for boolean and

@[simp]
theorem Bool.not_or (x : Bool) (y : Bool) :
(!(x || y)) = (!x && !y)

De Morgan's law for boolean or

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
@[simp]
theorem Bool.and_eq_false_imp (x : Bool) (y : Bool) :
(x && y) = false
@[simp]
theorem Bool.or_eq_true_iff (x : Bool) (y : Bool) :
(x || y) = true
@[simp]
theorem Bool.or_eq_false_iff (x : Bool) (y : Bool) :
(x || y) = false

### eq/beq/bne #

@[simp]

These two rules follow trivially by simp, but are needed to avoid non-termination in false_eq and true_eq.

@[simp]
@[simp]
theorem Bool.false_eq (b : Bool) :
() = ()
@[simp]
theorem Bool.true_eq (b : Bool) :
() = ()
@[simp]
theorem Bool.true_beq (b : Bool) :
() = b
@[simp]
theorem Bool.false_beq (b : Bool) :
() = !b
@[simp]
theorem Bool.beq_true (b : Bool) :
() = b
instance Bool.instLawfulIdentityBeqTrue :
Std.LawfulIdentity (fun (x x_1 : Bool) => x == x_1) true
Equations
@[simp]
theorem Bool.beq_false (b : Bool) :
() = !b
@[simp]
theorem Bool.true_bne (b : Bool) :
() = !b
@[simp]
theorem Bool.false_bne (b : Bool) :
() = b
@[simp]
theorem Bool.bne_true (b : Bool) :
() = !b
@[simp]
theorem Bool.bne_false (b : Bool) :
() = b
Equations
@[simp]
theorem Bool.not_beq_self (x : Bool) :
((!x) == x) = false
@[simp]
theorem Bool.beq_not_self (x : Bool) :
(x == !x) = false
@[simp]
theorem Bool.not_bne_self (x : Bool) :
((!x) != x) = true
@[simp]
theorem Bool.bne_not_self (x : Bool) :
(x != !x) = true
@[simp]
theorem Bool.not_eq_self (b : Bool) :
(!b) = b False
@[simp]
theorem Bool.eq_not_self (b : Bool) :
@[simp]
theorem Bool.beq_self_left (a : Bool) (b : Bool) :
(a == (a == b)) = b
@[simp]
theorem Bool.beq_self_right (a : Bool) (b : Bool) :
((a == b) == b) = a
@[simp]
theorem Bool.bne_self_left (a : Bool) (b : Bool) :
(a != (a != b)) = b
@[simp]
theorem Bool.bne_self_right (a : Bool) (b : Bool) :
((a != b) != b) = a
@[simp]
theorem Bool.not_bne_not (x : Bool) (y : Bool) :
((!x) != !y) = (x != y)
@[simp]
theorem Bool.bne_assoc (x : Bool) (y : Bool) (z : Bool) :
((x != y) != z) = (x != (y != z))
instance Bool.instAssociativeBne :
Std.Associative fun (x x_1 : Bool) => x != x_1
Equations
@[simp]
theorem Bool.bne_left_inj (x : Bool) (y : Bool) (z : Bool) :
(x != y) = (x != z) y = z
@[simp]
theorem Bool.bne_right_inj (x : Bool) (y : Bool) (z : Bool) :
(x != z) = (y != z) x = y
theorem Bool.beq_eq_decide_eq {α : Type u_1} [BEq α] [] [] (a : α) (b : α) :
(a == b) = decide (a = b)
@[simp]
theorem Bool.not_eq_not {a : Bool} {b : Bool} :
¬a = !b a = b
@[simp]
theorem Bool.not_not_eq {a : Bool} {b : Bool} :
¬(!a) = b a = b
@[simp]
theorem Bool.coe_iff_coe (a : Bool) (b : Bool) :
( ) a = b
@[simp]
theorem Bool.coe_true_iff_false (a : Bool) (b : Bool) :
( ) a = !b
@[simp]
theorem Bool.coe_false_iff_true (a : Bool) (b : Bool) :
( ) (!a) = b
@[simp]
theorem Bool.coe_false_iff_false (a : Bool) (b : Bool) :
( ) (!a) = !b

### beq properties #

theorem Bool.beq_comm {α : Type u_1} [BEq α] [] {a : α} {b : α} :
(a == b) = (b == a)

### xor #

theorem Bool.false_xor (x : Bool) :
= x
theorem Bool.xor_false (x : Bool) :
= x
theorem Bool.true_xor (x : Bool) :
= !x
theorem Bool.xor_true (x : Bool) :
= !x
theorem Bool.not_xor_self (x : Bool) :
xor (!x) x = true
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
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)
theorem Bool.xor_left_inj (x : Bool) (y : Bool) (z : Bool) :
xor x y = xor x z y = z
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
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
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

## toNat #

def Bool.toNat (b : Bool) :

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

Equations
• b.toNat = bif b then 1 else 0
Instances For
@[simp]
theorem Bool.toNat_false :
false.toNat = 0
@[simp]
theorem Bool.toNat_true :
true.toNat = 1
theorem Bool.toNat_le (c : Bool) :
c.toNat 1
@[reducible, inline, deprecated Bool.toNat_le]
abbrev Bool.toNat_le_one (c : Bool) :
c.toNat 1
Equations
Instances For
theorem Bool.toNat_lt (b : Bool) :
b.toNat < 2
@[simp]
theorem Bool.toNat_eq_zero (b : Bool) :
b.toNat = 0
@[simp]
theorem Bool.toNat_eq_one (b : Bool) :
b.toNat = 1

### ite #

@[simp]
theorem Bool.if_true_left (p : Prop) [h : ] (f : Bool) :
(if p then true else f) = ( || f)
@[simp]
theorem Bool.if_false_left (p : Prop) [h : ] (f : Bool) :
(if p then false else f) = (! && f)
@[simp]
theorem Bool.if_true_right (p : Prop) [h : ] (t : Bool) :
(if p then t else true) = (! || t)
@[simp]
theorem Bool.if_false_right (p : Prop) [h : ] (t : Bool) :
(if p then t else false) = ( && t)
@[simp]
theorem Bool.ite_eq_true_distrib (p : Prop) [h : ] (t : Bool) (f : Bool) :
((if p then t else f) = true) = if p then else
@[simp]
theorem Bool.ite_eq_false_distrib (p : Prop) [h : ] (t : Bool) (f : Bool) :
((if p then t else f) = false) = if p then else
@[simp]
theorem Bool.not_ite_eq_true_eq_true (p : Prop) [h : ] (b : Bool) (c : Bool) :
(¬if p then else ) if p then else
@[simp]
theorem Bool.not_ite_eq_false_eq_false (p : Prop) [h : ] (b : Bool) (c : Bool) :
(¬if p then else ) if p then else
@[simp]
theorem Bool.not_ite_eq_true_eq_false (p : Prop) [h : ] (b : Bool) (c : Bool) :
(¬if p then else ) if p then else
@[simp]
theorem Bool.not_ite_eq_false_eq_true (p : Prop) [h : ] (b : Bool) (c : Bool) :
(¬if p then else ) if p then else
@[simp]
theorem Bool.eq_false_imp_eq_true (b : Bool) :
@[simp]
theorem Bool.eq_true_imp_eq_false (b : Bool) :

### cond #

theorem Bool.cond_eq_ite {α : Type u_1} (b : Bool) (t : α) (e : α) :
(bif b then t else e) = if then t else e
theorem Bool.cond_eq_if {b : Bool} :
∀ {α : Type u_1} {x y : α}, (bif b then x else y) = if then x else y
@[simp]
theorem Bool.cond_not {α : Type u_1} (b : Bool) (t : α) (e : α) :
(bif !b then t else e) = bif b then e else t
@[simp]
theorem Bool.cond_self {α : Type u_1} (c : Bool) (t : α) :
(bif c then t else t) = t
theorem Bool.cond_decide {α : Type u_1} (p : Prop) [] (t : α) (e : α) :
(bif then t else e) = if p then t else e
@[simp]
theorem Bool.cond_eq_ite_iff {α : Type u_1} (a : Bool) (p : Prop) [h : ] (x : α) (y : α) (u : α) (v : α) :
((bif a then x else y) = if p then u else v) (if then x else y) = if p then u else v
@[simp]
theorem Bool.ite_eq_cond_iff {α : Type u_1} (p : Prop) [h : ] (a : Bool) (x : α) (y : α) (u : α) (v : α) :
((if p then x else y) = bif a then u else v) (if p then x else y) = if then u else v
@[simp]
theorem Bool.cond_eq_true_distrib (c : Bool) (t : Bool) (f : Bool) :
((bif c then t else f) = true) = if then else
@[simp]
theorem Bool.cond_eq_false_distrib (c : Bool) (t : Bool) (f : Bool) :
((bif c then t else f) = false) = if then else
theorem Bool.cond_true {α : Type u} {a : α} {b : α} :
(bif true then a else b) = a
theorem Bool.cond_false {α : Type u} {a : α} {b : α} :
(bif false then a else b) = b
@[simp]
theorem Bool.cond_true_left (c : Bool) (f : Bool) :
(bif c then true else f) = (c || f)
@[simp]
theorem Bool.cond_false_left (c : Bool) (f : Bool) :
(bif c then false else f) = (!c && f)
@[simp]
theorem Bool.cond_true_right (c : Bool) (t : Bool) :
(bif c then t else true) = (!c || t)
@[simp]
theorem Bool.cond_false_right (c : Bool) (t : Bool) :
(bif c then t else false) = (c && t)
@[simp]
theorem Bool.cond_true_same (c : Bool) (b : Bool) :
(bif c then c else b) = (c || b)
@[simp]
theorem Bool.cond_false_same (c : Bool) (b : Bool) :
(bif c then b else c) = (c && b)
theorem Bool.decide_coe (b : Bool) [Decidable ()] :
decide () = b
@[simp]
theorem Bool.decide_and (p : Prop) (q : Prop) [dpq : Decidable (p q)] [dp : ] [dq : ] :
decide (p q) = ( && )
@[simp]
theorem Bool.decide_or (p : Prop) (q : Prop) [dpq : Decidable (p q)] [dp : ] [dq : ] :
decide (p q) = ( || )
@[simp]
theorem Bool.decide_iff_dist (p : Prop) (q : Prop) [dpq : Decidable (p q)] [dp : ] [dq : ] :
decide (p q) = ( == )

### decide #

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