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

source
theorem bool.coe_sort_tt  :
↥tt = true
source
theorem bool.coe_sort_ff  :
↥ff = false
source
theorem bool.to_bool_true {h : decidable true} :
to_bool true = tt
source
theorem bool.to_bool_false {h : decidable false} :
to_bool false = ff
source
@[simp]
theorem bool.to_bool_coe (b : bool) {h : decidable ↥b} :
to_bool ↥b = b
source
theorem bool.coe_to_bool (p : Prop) [decidable p] :
↥(to_bool p) ↔ p
source
@[simp]
theorem bool.of_to_bool_iff {p : Prop} [decidable p] :
↥(to_bool p) ↔ p
source
@[simp]
theorem bool.tt_eq_to_bool_iff {p : Prop} [decidable p] :
tt = to_bool p ↔ p
source
@[simp]
theorem bool.ff_eq_to_bool_iff {p : Prop} [decidable p] :
ff = to_bool p ↔ ¬p
source
@[simp]
theorem bool.to_bool_not (p : Prop) [decidable p] :
to_bool (¬p) = !to_bool p
source
@[simp]
theorem bool.to_bool_and (p q : Prop) [decidable p] [decidable q] :
to_bool (p ∧ q) = to_bool p && to_bool q
source
@[simp]
theorem bool.to_bool_or (p q : Prop) [decidable p] [decidable q] :
to_bool (p ∨ q) = to_bool p || to_bool q
source
@[simp]
theorem bool.to_bool_eq {p q : Prop} [decidable p] [decidable q] :
to_bool p = to_bool q ↔ (p ↔ q)
source
theorem bool.not_ff  :
¬↥ff
source
@[simp]
theorem bool.default_bool  :
default = ff
source
theorem bool.dichotomy (b : bool) :
b = ff ∨ b = tt
source
@[simp]
theorem bool.forall_bool {p : bool → Prop} :
(∀ (b : bool), p b) ↔ p ff ∧ p tt
source
@[simp]
theorem bool.exists_bool {p : bool → Prop} :
(∃ (b : bool), p b) ↔ p ff ∨ p tt
source
@[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
source
@[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
source
@[simp]
theorem bool.cond_ff {α : Type u_1} (t e : α) :
cond ff t e = e
source
@[simp]
theorem bool.cond_tt {α : Type u_1} (t e : α) :
cond tt t e = t
source
@[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
source
@[simp]
theorem bool.cond_bnot {α : Type u_1} (b : bool) (t e : α) :
cond (!b) t e = cond b e t
source
theorem bool.coe_bool_iff {a b : bool} :
↥a ↔ ↥b ↔ a = b
source
theorem bool.eq_tt_of_ne_ff {a : bool} :
a ≠ ff → a = tt
source
theorem bool.eq_ff_of_ne_tt {a : bool} :
a ≠ tt → a = ff
source
theorem bool.bor_comm (a b : bool) :
a || b = b || a
source
@[simp]
theorem bool.bor_assoc (a b c : bool) :
a || b || c = a || (b || c)
source
theorem bool.bor_left_comm (a b c : bool) :
a || (b || c) = b || (a || c)
source
theorem bool.bor_inl {a b : bool} (H : ↥a) :
↥(a || b)
source
theorem bool.bor_inr {a b : bool} (H : ↥b) :
↥(a || b)
source
theorem bool.band_comm (a b : bool) :
a && b = b && a
source
@[simp]
theorem bool.band_assoc (a b c : bool) :
a && b && c = a && (b && c)
source
theorem bool.band_left_comm (a b c : bool) :
a && (b && c) = b && (a && c)
source
theorem bool.band_elim_left {a b : bool} :
↥(a && b) → ↥a
source
theorem bool.band_intro {a b : bool} :
↥a → ↥b → ↥(a && b)
source
theorem bool.band_elim_right {a b : bool} :
↥(a && b) → ↥b
source
@[simp]
theorem bool.bnot_false  :
!ff = tt
source
@[simp]
theorem bool.bnot_true  :
!tt = ff
source
@[simp]
theorem bool.bnot_iff_not {b : bool} :
↥!b ↔ ¬↥b
source
theorem bool.eq_tt_of_bnot_eq_ff {a : bool} :
!a = ff → a = tt
source
theorem bool.eq_ff_of_bnot_eq_tt {a : bool} :
!a = tt → a = ff
source
@[simp]
theorem bool.band_bnot_self (x : bool) :
x && !x = ff
source
@[simp]
theorem bool.bnot_band_self (x : bool) :
!x && x = ff
source
@[simp]
theorem bool.bor_bnot_self (x : bool) :
x || !x = tt
source
@[simp]
theorem bool.bnot_bor_self (x : bool) :
!x || x = tt
source
theorem bool.bxor_comm (a b : bool) :
bxor a b = bxor b a
source
@[simp]
theorem bool.bxor_assoc (a b c : bool) :
bxor (bxor a b) c = bxor a (bxor b c)
source
theorem bool.bxor_left_comm (a b c : bool) :
bxor a (bxor b c) = bxor b (bxor a c)
source
@[simp]
theorem bool.bxor_bnot_left (a : bool) :
bxor (!a) a = tt
source
@[simp]
theorem bool.bxor_bnot_right (a : bool) :
bxor a (!a) = tt
source
@[simp]
theorem bool.bxor_bnot_bnot (a b : bool) :
bxor (!a) (!b) = bxor a b
source
@[simp]
theorem bool.bxor_ff_left (a : bool) :
bxor ff a = a
source
@[simp]
theorem bool.bxor_ff_right (a : bool) :
bxor a ff = a
source
theorem bool.bxor_iff_ne {x y : bool} :
bxor x y = tt ↔ x ≠ y

De Morgan's laws for booleans #

source
@[simp]
theorem bool.bnot_band (a b : bool) :
!(a && b) = !a || !b
source
@[simp]
theorem bool.bnot_bor (a b : bool) :
!(a || b) = !a && !b
source
theorem bool.bnot_inj {a b : bool} :
!a = !b → a = b
source
@[protected, instance]
def bool.linear_order  :
linear_order bool
Equations
source
@[simp]
theorem bool.ff_le {x : bool} :
ff ≤ x
source
@[simp]
theorem bool.le_tt {x : bool} :
x ≤ tt
source
theorem bool.lt_iff {x y : bool} :
x < y ↔ x = ff ∧ y = tt
source
@[simp]
theorem bool.ff_lt_tt  :
ff < tt
source
theorem bool.le_iff_imp {x y : bool} :
x ≤ y ↔ ↥x → ↥y
source
theorem bool.band_le_left (x y : bool) :
x && y ≤ x
source
theorem bool.band_le_right (x y : bool) :
x && y ≤ y
source
theorem bool.le_band {x y z : bool} :
x ≤ y → x ≤ z → x ≤ y && z
source
theorem bool.left_le_bor (x y : bool) :
x ≤ x || y
source
theorem bool.right_le_bor (x y : bool) :
y ≤ x || y
source
theorem bool.bor_le {x y z : bool} :
x ≤ z → y ≤ z → x || y ≤ z
source
def bool.to_nat (b : bool) :
ℕ

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

Equations
source
def bool.of_nat (n : ℕ) :
bool

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

Equations
source
theorem bool.of_nat_le_of_nat {n m : ℕ} (h : n ≤ m) :
bool.of_nat n ≤ bool.of_nat m
source
theorem bool.to_nat_le_to_nat {b₀ b₁ : bool} (h : b₀ ≤ b₁) :
b₀.to_nat ≤ b₁.to_nat
source
theorem bool.of_nat_to_nat (b : bool) :
bool.of_nat b.to_nat = b
source
@[simp]
theorem bool.injective_iff {α : Sort u_1} {f : bool → α} :
function.injective f ↔ f ff ≠ f tt