# Documentation

Mathlib.Data.Bool.Basic

# Booleans #

This file proves various trivial lemmas about booleans and their relation to decidable propositions.

## Tags #

bool, boolean, Bool, De Morgan

theorem Bool.decide_True {h : } :
@[simp]
theorem Bool.decide_coe (b : Bool) {h : Decidable ()} :
decide () = b
theorem Bool.coe_decide (p : Prop) [d : ] :
p
theorem Bool.of_decide_iff {p : Prop} [inst : ] :
p
@[simp]
theorem Bool.true_eq_decide_iff {p : Prop} [inst : ] :
p
@[simp]
theorem Bool.false_eq_decide_iff {p : Prop} [inst : ] :
theorem Bool.decide_not (p : Prop) [inst : ] :
() = !
@[simp]
theorem Bool.decide_and (p : Prop) (q : Prop) [inst : ] [inst : ] :
decide (p q) = ( && )
@[simp]
theorem Bool.decide_or (p : Prop) (q : Prop) [inst : ] [inst : ] :
decide (p q) = ( || )
theorem Bool.eq_iff_eq_true_iff {a : Bool} {b : Bool} :
a = b ( )
theorem Bool.beq_eq_decide_eq {α : Type u_1} [inst : ] (a : α) (b : α) :
(a == b) = decide (a = b)
theorem Bool.beq_comm {α : Type u_1} [inst : BEq α] [inst : ] {a : α} {b : α} :
(a == b) = (b == a)
@[simp]
theorem Bool.default_bool :
default = false
@[simp]
theorem Bool.forall_bool {p : } :
((b : Bool) → p b) p true
@[simp]
theorem Bool.exists_bool {p : } :
(b, p b) p true
instance Bool.decidableForallBool {p : } [inst : (b : Bool) → Decidable (p b)] :
Decidable ((b : Bool) → p b)

If p b is decidable for all b : bool, then ∀ b, p b is decidable

Equations
instance Bool.decidableExistsBool {p : } [inst : (b : Bool) → Decidable (p b)] :
Decidable (b, p b)

If p b is decidable for all b : bool, then ∃ b, p b is decidable

Equations
theorem Bool.cond_eq_ite {α : Type u_1} (b : Bool) (t : α) (e : α) :
(bif b then t else e) = if then t else e
@[simp]
theorem Bool.cond_decide {α : Type u_1} (p : Prop) [inst : ] (t : α) (e : α) :
(bif then t else e) = if p then t else e
@[simp]
theorem Bool.cond_not {α : Type u_1} (b : Bool) (t : α) (e : α) :
(bif !b then t else e) = bif b then e else t
theorem Bool.coe_bool_iff {a : Bool} {b : Bool} :
( ) a = b
theorem Bool.or_comm (a : Bool) (b : Bool) :
(a || b) = (b || a)
theorem Bool.or_left_comm (a : Bool) (b : Bool) (c : Bool) :
(a || (b || c)) = (b || (a || c))
theorem Bool.or_inl {a : Bool} {b : Bool} (H : ) :
(a || b) = true
theorem Bool.or_inr {a : Bool} {b : Bool} (H : ) :
(a || b) = true
theorem Bool.and_comm (a : Bool) (b : Bool) :
(a && b) = (b && a)
theorem Bool.and_left_comm (a : Bool) (b : Bool) (c : Bool) :
(a && (b && c)) = (b && (a && c))
theorem Bool.and_elim_left {a : Bool} {b : Bool} :
(a && b) = true
theorem Bool.and_intro {a : Bool} {b : Bool} :
(a && b) = true
theorem Bool.and_elim_right {a : Bool} {b : Bool} :
(a && b) = true
theorem Bool.and_or_distrib_left (a : Bool) (b : Bool) (c : Bool) :
(a && (b || c)) = (a && b || a && c)
theorem Bool.and_or_distrib_right (a : Bool) (b : Bool) (c : Bool) :
((a || b) && c) = (a && c || b && c)
theorem Bool.or_and_distrib_left (a : Bool) (b : Bool) (c : Bool) :
(a || b && c) = ((a || b) && (a || c))
theorem Bool.or_and_distrib_right (a : Bool) (b : Bool) (c : Bool) :
(a && b || c) = ((a || c) && (b || c))
theorem Bool.eq_not_iff {a : Bool} {b : Bool} :
a = !b a b
theorem Bool.not_eq_iff {a : Bool} {b : Bool} :
(!decide (a = b)) = true 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
theorem Bool.ne_not {a : Bool} {b : Bool} :
a !b a = b
theorem Bool.not_ne {a : Bool} {b : Bool} :
(!a) b a = b
theorem Bool.not_ne_self (b : Bool) :
(!b) b
theorem Bool.eq_or_eq_not (a : Bool) (b : Bool) :
a = b a = !b
@[simp]
theorem Bool.and_not_self (x : Bool) :
(x && !x) = false
@[simp]
theorem Bool.not_and_self (x : Bool) :
(!x && x) = false
@[simp]
theorem Bool.or_not_self (x : Bool) :
(x || !x) = true
@[simp]
theorem Bool.not_or_self (x : Bool) :
(!x || x) = true
theorem Bool.xor_comm (a : Bool) (b : Bool) :
xor a b = xor b a
@[simp]
theorem Bool.xor_assoc (a : Bool) (b : Bool) (c : Bool) :
xor (xor a b) c = xor a (xor b c)
theorem Bool.xor_left_comm (a : Bool) (b : Bool) (c : Bool) :
xor a (xor b c) = xor b (xor a c)
@[simp]
theorem Bool.xor_not_left (a : Bool) :
xor (!a) a = true
@[simp]
theorem Bool.xor_not_right (a : Bool) :
(xor a !a) = true
@[simp]
theorem Bool.xor_not_not (a : Bool) (b : Bool) :
(xor (!a) !b) = xor a b
@[simp]
theorem Bool.xor_false_left (a : Bool) :
= a
@[simp]
theorem Bool.xor_false_right (a : Bool) :
= a
theorem Bool.and_xor_distrib_left (a : Bool) (b : Bool) (c : Bool) :
(a && xor b c) = xor (a && b) (a && c)
theorem Bool.and_xor_distrib_right (a : Bool) (b : Bool) (c : Bool) :
(xor a b && c) = xor (a && c) (b && c)
theorem Bool.xor_iff_ne {x : Bool} {y : Bool} :
xor x y = true x y

### De Morgan's laws for booleans #

@[simp]
theorem Bool.not_and (a : Bool) (b : Bool) :
(!decide ((a && b) = (!a || !b))) = true
@[simp]
theorem Bool.not_or (a : Bool) (b : Bool) :
(!decide ((a || b) = (!a && !b))) = true
theorem Bool.not_inj {a : Bool} {b : Bool} :
(!decide (a = !b)) = truea = b
instance Bool.linearOrder :
Equations
@[simp]
theorem Bool.false_le {x : Bool} :
@[simp]
theorem Bool.le_true {x : Bool} :
theorem Bool.lt_iff {x : Bool} {y : Bool} :
x < y
@[simp]
theorem Bool.le_iff_imp {x : Bool} {y : Bool} :
x y
theorem Bool.and_le_left (x : Bool) (y : Bool) :
(x && y) x
theorem Bool.and_le_right (x : Bool) (y : Bool) :
(x && y) y
theorem Bool.le_and {x : Bool} {y : Bool} {z : Bool} :
x yx zx (y && z)
theorem Bool.left_le_or (x : Bool) (y : Bool) :
x (x || y)
theorem Bool.right_le_or (x : Bool) (y : Bool) :
y (x || y)
theorem Bool.or_le {x : Bool} {y : Bool} {z : Bool} :
x zy z(x || y) z
def Bool.toNat (b : Bool) :

convert a bool to a ℕ, false -> 0, true -> 1

Equations
• = bif b then 1 else 0
def Bool.ofNat (n : ) :

convert a ℕ to a bool, 0 -> false, everything else -> true

Equations
theorem Bool.ofNat_le_ofNat {n : } {m : } (h : n m) :
theorem Bool.toNat_le_toNat {b₀ : Bool} {b₁ : Bool} (h : b₀ b₁) :
theorem Bool.ofNat_toNat (b : Bool) :
= b
@[simp]
theorem Bool.injective_iff {α : Sort u_1} {f : Boolα} :
theorem Bool.apply_apply_apply (f : ) (x : Bool) :
f (f (f x)) = f x

Kaminski's Equation