mathlib3 documentation

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

source
theorem bool.coe_sort_tt  :
↥bool.tt = true
source
theorem bool.coe_sort_ff  :
↥bool.ff = false
source
theorem bool.to_bool_true {h : decidable true} :
decidable.to_bool true = bool.tt
source
theorem bool.to_bool_false {h : decidable false} :
decidable.to_bool false = bool.ff
source
@[simp]
theorem bool.to_bool_coe (b : bool) {h : decidable ↥b} :
decidable.to_bool ↥b = b
source
theorem bool.coe_to_bool (p : Prop) [decidable p] :
↥(decidable.to_bool p) ↔ p
source
@[simp]
theorem bool.of_to_bool_iff {p : Prop} [decidable p] :
↥(decidable.to_bool p) ↔ p
source
@[simp]
theorem bool.tt_eq_to_bool_iff {p : Prop} [decidable p] :
bool.tt = decidable.to_bool p ↔ p
source
@[simp]
theorem bool.ff_eq_to_bool_iff {p : Prop} [decidable p] :
bool.ff = decidable.to_bool p ↔ ¬p
source
@[simp]
theorem bool.to_bool_not (p : Prop) [decidable p] :
decidable.to_bool (¬p) = !decidable.to_bool p
source
@[simp]
theorem bool.to_bool_and (p q : Prop) [decidable p] [decidable q] :
decidable.to_bool (p ∧ q) = decidable.to_bool p && decidable.to_bool q
source
@[simp]
theorem bool.to_bool_or (p q : Prop) [decidable p] [decidable q] :
decidable.to_bool (p ∨ q) = decidable.to_bool p || decidable.to_bool q
source
@[simp]
theorem bool.to_bool_eq {p q : Prop} [decidable p] [decidable q] :
decidable.to_bool p = decidable.to_bool q ↔ (p ↔ q)
source
theorem bool.not_ff  :
¬↥bool.ff
source
@[simp]
theorem bool.default_bool  :
inhabited.default = bool.ff
source
theorem bool.dichotomy (b : bool) :
b = bool.ff ∨ b = bool.tt
source
@[simp]
theorem bool.forall_bool {p : bool → Prop} :
(∀ (b : bool), p b) ↔ p bool.ff ∧ p bool.tt
source
@[simp]
theorem bool.exists_bool {p : bool → Prop} :
(∃ (b : bool), p b) ↔ p bool.ff ∨ p bool.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 bool.ff t e = e
source
@[simp]
theorem bool.cond_tt {α : Type u_1} (t e : α) :
cond bool.tt t e = t
source
theorem bool.cond_eq_ite {α : Type u_1} (b : bool) (t e : α) :
cond b t e = ite ↥b t e
source
@[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
source
@[simp]
theorem bool.cond_bnot {α : Type u_1} (b : bool) (t e : α) :
cond (!b) t e = cond b e t
source
theorem bool.bnot_ne_id  :
bnot ≠ id
source
theorem bool.coe_bool_iff {a b : bool} :
↥a ↔ ↥b ↔ a = b
source
theorem bool.eq_tt_of_ne_ff {a : bool} :
a ≠ bool.ff → a = bool.tt
source
theorem bool.eq_ff_of_ne_tt {a : bool} :
a ≠ bool.tt → a = bool.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
theorem bool.band_bor_distrib_left (a b c : bool) :
a && (b || c) = a && b || a && c
source
theorem bool.band_bor_distrib_right (a b c : bool) :
(a || b) && c = a && c || b && c
source
theorem bool.bor_band_distrib_left (a b c : bool) :
a || b && c = (a || b) && (a || c)
source
theorem bool.bor_band_distrib_right (a b c : bool) :
a && b || c = (a || c) && (b || c)
source
@[simp]
theorem bool.bnot_ff  :
!bool.ff = bool.tt
source
@[simp]
theorem bool.bnot_tt  :
!bool.tt = bool.ff
source
theorem bool.eq_bnot_iff {a b : bool} :
a = !b ↔ a ≠ b
source
theorem bool.bnot_eq_iff {a b : bool} :
!a = b ↔ a ≠ b
source
@[simp]
theorem bool.not_eq_bnot {a b : bool} :
¬a = !b ↔ a = b
source
@[simp]
theorem bool.bnot_not_eq {a b : bool} :
¬!a = b ↔ a = b
source
theorem bool.ne_bnot {a b : bool} :
a ≠ !b ↔ a = b
source
theorem bool.bnot_ne {a b : bool} :
!a ≠ b ↔ a = b
source
theorem bool.bnot_ne_self (b : bool) :
!b ≠ b
source
theorem bool.self_ne_bnot (b : bool) :
b ≠ !b
source
theorem bool.eq_or_eq_bnot (a b : bool) :
a = b ∨ a = !b
source
@[simp]
theorem bool.bnot_iff_not {b : bool} :
↥!b ↔ ¬↥b
source
theorem bool.eq_tt_of_bnot_eq_ff {a : bool} :
!a = bool.ff → a = bool.tt
source
theorem bool.eq_ff_of_bnot_eq_tt {a : bool} :
!a = bool.tt → a = bool.ff
source
@[simp]
theorem bool.band_bnot_self (x : bool) :
x && !x = bool.ff
source
@[simp]
theorem bool.bnot_band_self (x : bool) :
!x && x = bool.ff
source
@[simp]
theorem bool.bor_bnot_self (x : bool) :
x || !x = bool.tt
source
@[simp]
theorem bool.bnot_bor_self (x : bool) :
!x || x = bool.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 = bool.tt
source
@[simp]
theorem bool.bxor_bnot_right (a : bool) :
bxor a (!a) = bool.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 bool.ff a = a
source
@[simp]
theorem bool.bxor_ff_right (a : bool) :
bxor a bool.ff = a
source
theorem bool.band_bxor_distrib_left (a b c : bool) :
a && bxor b c = bxor (a && b) (a && c)
source
theorem bool.band_bxor_distrib_right (a b c : bool) :
bxor a b && c = bxor (a && c) (b && c)
source
theorem bool.bxor_iff_ne {x y : bool} :
bxor x y = bool.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} :
bool.ff ≤ x
source
@[simp]
theorem bool.le_tt {x : bool} :
x ≤ bool.tt
source
theorem bool.lt_iff {x y : bool} :
x < y ↔ x = bool.ff ∧ y = bool.tt
source
@[simp]
theorem bool.ff_lt_tt  :
bool.ff < bool.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 bool.ff ≠ f bool.tt
source
theorem bool.apply_apply_apply (f : bool → bool) (x : bool) :
f (f (f x)) = f x

Kaminski's Equation