data.bool

# booleans #

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

## Notations #

This file introduces the notation !b for bnot b, the boolean "not".

## Tags #

bool, boolean, De Morgan

theorem bool.coe_sort_tt  :
theorem bool.coe_sort_ff  :
@[simp]
theorem bool.to_bool_coe (b : bool) {h : decidable b} :
= b
theorem bool.coe_to_bool (p : Prop) [decidable p] :
@[simp]
theorem bool.of_to_bool_iff {p : Prop} [decidable p] :
@[simp]
theorem bool.tt_eq_to_bool_iff {p : Prop} [decidable p] :
p
@[simp]
theorem bool.ff_eq_to_bool_iff {p : Prop} [decidable p] :
@[simp]
theorem bool.to_bool_not (p : Prop) [decidable p] :
@[simp]
theorem bool.to_bool_and (p q : Prop) [decidable p] [decidable q] :
to_bool (p q) = &&
@[simp]
theorem bool.to_bool_or (p q : Prop) [decidable p] [decidable q] :
to_bool (p q) = ||
@[simp]
theorem bool.to_bool_eq {p q : Prop} [decidable p] [decidable q] :
= (p q)
theorem bool.not_ff  :
@[simp]
theorem bool.default_bool  :
theorem bool.dichotomy (b : bool) :
b = ff b = tt
@[simp]
theorem bool.forall_bool {p : bool → Prop} :
(∀ (b : bool), p b) p ff p tt
@[simp]
theorem bool.exists_bool {p : bool → Prop} :
(∃ (b : bool), p b) p ff p tt
@[protected, instance]
def bool.decidable_forall_bool {p : bool → Prop} [Π (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
@[protected, instance]
def bool.decidable_exists_bool {p : bool → Prop} [Π (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
@[simp]
theorem bool.cond_ff {α : Type u_1} (t e : α) :
t e = e
@[simp]
theorem bool.cond_tt {α : Type u_1} (t e : α) :
t e = t
@[simp]
theorem bool.cond_to_bool {α : Type u_1} (p : Prop) [decidable p] (t e : α) :
cond (to_bool p) t e = ite p t e
theorem bool.coe_bool_iff {a b : bool} :
a b a = b
theorem bool.eq_tt_of_ne_ff {a : bool} :
a ffa = tt
theorem bool.eq_ff_of_ne_tt {a : bool} :
a tta = ff
theorem bool.bor_comm (a b : bool) :
a || b = b || a
@[simp]
theorem bool.bor_assoc (a b c : bool) :
a || b || c = a || (b || c)
theorem bool.bor_left_comm (a b c : bool) :
a || (b || c) = b || (a || c)
theorem bool.bor_inl {a b : bool} (H : a) :
(a || b)
theorem bool.bor_inr {a b : bool} (H : b) :
(a || b)
theorem bool.band_comm (a b : bool) :
a && b = b && a
@[simp]
theorem bool.band_assoc (a b c : bool) :
a && b && c = a && (b && c)
theorem bool.band_left_comm (a b c : bool) :
a && (b && c) = b && (a && c)
theorem bool.band_elim_left {a b : bool} :
(a && b)a
theorem bool.band_intro {a b : bool} :
a → b → (a && b)
theorem bool.band_elim_right {a b : bool} :
(a && b)b
@[simp]
theorem bool.bnot_false  :
@[simp]
theorem bool.bnot_true  :
theorem bool.eq_tt_of_bnot_eq_ff {a : bool} :
!a = ffa = tt
theorem bool.eq_ff_of_bnot_eq_tt {a : bool} :
!a = tta = ff
theorem bool.bxor_comm (a b : bool) :
bxor a b = bxor b a
@[simp]
theorem bool.bxor_assoc (a b c : bool) :
bxor (bxor a b) c = bxor a (bxor b c)
theorem bool.bxor_left_comm (a b c : bool) :
bxor a (bxor b c) = bxor b (bxor a c)
@[simp]
theorem bool.bxor_bnot_left (a : bool) :
bxor (!a) a = tt
@[simp]
theorem bool.bxor_bnot_right (a : bool) :
bxor a (!a) = tt
@[simp]
theorem bool.bxor_bnot_bnot (a b : bool) :
bxor (!a) (!b) = bxor a b
@[simp]
theorem bool.bxor_ff_left (a : bool) :
a = a
@[simp]
theorem bool.bxor_ff_right (a : bool) :
bxor a ff = a
theorem bool.bxor_iff_ne {x y : bool} :
bxor x y = tt x y

### De Morgan's laws for booleans #

@[simp]
theorem bool.bnot_band (a b : bool) :
!(a && b) = !a || !b
@[simp]
theorem bool.bnot_bor (a b : bool) :
!(a || b) = !a && !b
theorem bool.bnot_inj {a b : bool} :
!a = !ba = b
@[protected, instance]
Equations
@[simp]
theorem bool.ff_le {x : bool} :
@[simp]
theorem bool.le_tt {x : bool} :
@[simp]
theorem bool.ff_lt_tt  :
def bool.to_nat (b : bool) :

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

Equations
def bool.of_nat (n : ) :

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

Equations
theorem bool.of_nat_le_of_nat {n m : } (h : n m) :
theorem bool.to_nat_le_to_nat {b₀ b₁ : bool} (h : b₀ b₁) :
b₀.to_nat b₁.to_nat
theorem bool.of_nat_to_nat (b : bool) :