data.bool.basic

booleans #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

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} :
theorem bool.coe_to_bool (p : Prop) [decidable p] :
p
@[simp]
theorem bool.of_to_bool_iff {p : Prop} [decidable p] :
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] :
(p q)
theorem bool.not_ff  :
@[simp]
theorem bool.dichotomy (b : bool) :
@[simp]
theorem bool.forall_bool {p : bool Prop} :
( (b : bool), p b)
@[simp]
theorem bool.exists_bool {p : bool Prop} :
( (b : bool), p b)
@[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 : α) :
e = e
@[simp]
theorem bool.cond_tt {α : Type u_1} (t e : α) :
e = t
theorem bool.cond_eq_ite {α : Type u_1} (b : bool) (t e : α) :
cond b t e = ite b t e
@[simp]
theorem bool.cond_to_bool {α : Type u_1} (p : Prop) [decidable p] (t e : α) :
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.bnot_ne_id  :
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
theorem bool.band_bor_distrib_left (a b c : bool) :
a && (b || c) = a && b || a && c
theorem bool.band_bor_distrib_right (a b c : bool) :
(a || b) && c = a && c || b && c
theorem bool.bor_band_distrib_left (a b c : bool) :
a || b && c = (a || b) && (a || c)
theorem bool.bor_band_distrib_right (a b c : bool) :
a && b || c = (a || c) && (b || c)
@[simp]
theorem bool.bnot_ff  :
@[simp]
theorem bool.bnot_tt  :
theorem bool.eq_bnot_iff {a b : bool} :
a = !b a b
theorem bool.bnot_eq_iff {a b : bool} :
!a = b a b
@[simp]
theorem bool.not_eq_bnot {a b : bool} :
¬a = !b a = b
@[simp]
theorem bool.bnot_not_eq {a b : bool} :
¬!a = b a = b
theorem bool.ne_bnot {a b : bool} :
a !b a = b
theorem bool.bnot_ne {a b : bool} :
!a b a = b
theorem bool.bnot_ne_self (b : bool) :
!b b
theorem bool.self_ne_bnot (b : bool) :
b !b
theorem bool.eq_or_eq_bnot (a b : bool) :
a = b a = !b
@[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) :
= a
@[simp]
theorem bool.bxor_ff_right (a : bool) :
= a
theorem bool.band_bxor_distrib_left (a b c : bool) :
a && bxor b c = bxor (a && b) (a && c)
theorem bool.band_bxor_distrib_right (a b c : bool) :
bxor a b && c = bxor (a && c) (b && c)
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 = !b a = 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} :
x < y
@[simp]
theorem bool.ff_lt_tt  :
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 y x z x 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 z y z x || 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
theorem bool.of_nat_to_nat (b : bool) :
@[simp]
theorem bool.injective_iff {α : Sort u_1} {f : bool α} :
theorem bool.apply_apply_apply (f : bool bool) (x : bool) :
f (f (f x)) = f x

Kaminski's Equation