mathlib documentation

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

@[simp]

@[simp]

@[simp]

@[simp]
theorem bool.to_bool_coe (b : bool) {h : decidable 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] :

@[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] :

@[simp]
theorem bool.to_bool_or (p q : Prop) [decidable p] [decidable q] :

@[simp]
theorem bool.to_bool_eq {p q : Prop} [decidable p] [decidable q] :
to_bool p = to_bool q (p q)

theorem bool.not_ff  :

@[simp]

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

@[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
@[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 : α) :
cond ff t e = e

@[simp]
theorem bool.cond_tt {α : Type u_1} (t e : α) :
cond tt 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} :
a → (a || b)

theorem bool.bor_inr {a b : bool} :
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) :
bxor ff 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

@[instance]

Equations
def bool.to_nat  :
bool

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

Equations
def bool.of_nat  :
bool

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

Equations
theorem bool.of_nat_le_of_nat {n m : } :

theorem bool.to_nat_le_to_nat {b₀ b₁ : bool} :
b₀ b₁b₀.to_nat b₁.to_nat