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]

theorem bool.coe_sort_tt :

@[simp]

theorem bool.coe_sort_ff :

@[simp]

theorem bool.to_bool_true {h : decidable true} :

to_bool true = tt

@[simp]

theorem bool.to_bool_false {h : decidable false} :

to_bool false = ff

@[simp]

theorem bool.to_bool_coe (b : bool) {h : decidable ↥b} :

to_bool ↥b = b

theorem bool.coe_to_bool (p : Prop) [decidable p] :

↥(to_bool p) ↔ p

@[simp]

theorem bool.of_to_bool_iff {p : Prop} [decidable p] :

↥(to_bool p) ↔ p

@[simp]

theorem bool.tt_eq_to_bool_iff {p : Prop} [decidable p] :

tt = to_bool p ↔ p

@[simp]

theorem bool.ff_eq_to_bool_iff {p : Prop} [decidable p] :

ff = to_bool p ↔ ¬p

@[simp]

theorem bool.to_bool_not (p : Prop) [decidable p] :

to_bool (¬p) = !to_bool p

@[simp]

theorem bool.to_bool_and (p q : Prop) [decidable p] [decidable q] :

to_bool (p ∧ q) = to_bool p && to_bool q

@[simp]

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

to_bool (p ∨ q) = to_bool p || to_bool 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.default_bool :

default bool = ff

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

bool.decidable_forall_bool = decidable_of_decidable_of_iff and.decidable bool.decidable_forall_bool._proof_1

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

bool.decidable_exists_bool = decidable_of_decidable_of_iff or.decidable bool.decidable_exists_bool._proof_1

@[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_1 : a ≠ ff) :

a = tt

theorem bool.eq_ff_of_ne_tt {a : bool} (a_1 : a ≠ tt) :

a = 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} (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_1 : ↥(a && b)) :

theorem bool.band_intro {a b : bool} (a_1 : ↥a) (a_2 : ↥b) :

↥(a && b)

theorem bool.band_elim_right {a b : bool} (a_1 : ↥(a && b)) :

@[simp]

theorem bool.bnot_false :

@[simp]

theorem bool.bnot_true :

theorem bool.eq_tt_of_bnot_eq_ff {a : bool} (a_1 : !a = ff) :

a = tt

theorem bool.eq_ff_of_bnot_eq_tt {a : bool} (a_1 : !a = tt) :

a = 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) :

@[simp]

theorem bool.bxor_ff_right (a : bool) :

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_1 : !a = !b) :

a = b

@[instance]

def bool.decidable_linear_order :

decidable_linear_order bool

Equations

bool.decidable_linear_order = {le := λ (a b : bool), a = ff ∨ b = tt, lt := λ (a b : bool), a ≤ b ∧ ¬b ≤ a, le_refl := bool.decidable_linear_order._proof_1, le_trans := bool.decidable_linear_order._proof_2, lt_iff_le_not_le := bool.decidable_linear_order._proof_3, le_antisymm := bool.decidable_linear_order._proof_4, le_total := bool.decidable_linear_order._proof_5, decidable_le := λ (a b : bool), or.decidable, decidable_eq := λ (a b : bool), bool.decidable_eq a b, decidable_lt := λ (a b : bool), and.decidable}

def bool.to_nat (b : bool) :

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

Equations

b.to_nat = cond b 1 0

def bool.of_nat (n : ℕ) :

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

Equations

bool.of_nat n = to_bool (n ≠ 0)

theorem bool.of_nat_le_of_nat {n m : ℕ} (h : n ≤ m) :

bool.of_nat n ≤ bool.of_nat 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) :

bool.of_nat b.to_nat = b