mathlib documentation

data.bool.basic

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]
theorem bool.coe_to_bool (p : Prop) [decidable p] :
@[simp]
theorem bool.of_to_bool_iff {p : Prop} [decidable p] :
@[simp]
@[simp]
@[simp]
@[simp]
theorem bool.to_bool_eq {p q : Prop} [decidable p] [decidable q] :
theorem bool.dichotomy (b : bool) :
@[simp]
theorem bool.forall_bool {p : bool → Prop} :
(∀ (b : bool), p b) p bool.ff p bool.tt
@[simp]
theorem bool.exists_bool {p : bool → Prop} :
(∃ (b : bool), p b) p bool.ff p bool.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 : α) :
cond bool.ff t e = e
@[simp]
theorem bool.cond_tt {α : Type u_1} (t e : α) :
cond bool.tt t e = t
@[simp]
theorem bool.cond_to_bool {α : Type u_1} (p : Prop) [decidable p] (t e : α) :
cond (decidable.to_bool p) t e = ite p t e
@[simp]
theorem bool.cond_bnot {α : Type u_1} (b : bool) (t e : α) :
cond (!b) t e = cond b e t
theorem bool.coe_bool_iff {a b : bool} :
a b a = b
theorem bool.eq_tt_of_ne_ff {a : bool} :
theorem bool.eq_ff_of_ne_tt {a : bool} :
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]
@[simp]
@[simp]
theorem bool.bnot_iff_not {b : bool} :
@[simp]
theorem bool.band_bnot_self (x : bool) :
@[simp]
theorem bool.bnot_band_self (x : bool) :
@[simp]
theorem bool.bor_bnot_self (x : bool) :
@[simp]
theorem bool.bnot_bor_self (x : bool) :
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) :
@[simp]
theorem bool.bxor_bnot_right (a : bool) :
@[simp]
theorem bool.bxor_bnot_bnot (a b : bool) :
bxor (!a) (!b) = bxor a b
@[simp]
theorem bool.bxor_ff_left (a : bool) :
@[simp]
theorem bool.bxor_ff_right (a : bool) :
theorem bool.bxor_iff_ne {x y : bool} :
bxor x y = bool.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} :
theorem bool.lt_iff {x y : bool} :
@[simp]
theorem bool.le_iff_imp {x y : bool} :
x y x → y
theorem bool.band_le_left (x y : bool) :
x && y x
theorem bool.band_le_right (x y : bool) :
x && y y
theorem bool.le_band {x y z : bool} :
x yx zx y && z
theorem bool.left_le_bor (x y : bool) :
x x || y
theorem bool.right_le_bor (x y : bool) :
y x || y
theorem bool.bor_le {x y z : bool} :
x zy zx || y z
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
@[simp]
theorem bool.injective_iff {α : Sort u_1} {f : bool → α} :
theorem bool.apply_apply_apply (f : boolbool) (x : bool) :
f (f (f x)) = f x

Kaminski's Equation