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]
@[simp]
@[simp]
@[simp]
@[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
@[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
@[simp]
theorem
bool.to_bool_eq
{p q : Prop}
[decidable p]
[decidable q] :
decidable.to_bool p = decidable.to_bool q ↔ (p ↔ q)
@[instance]
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]
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_to_bool
{α : Type u_1}
(p : Prop)
[decidable p]
(t e : α) :
cond (decidable.to_bool p) t e = ite p t e
De Morgan's laws for booleans
@[instance]
Equations
- bool.decidable_linear_order = {le := λ (a b : bool), a = bool.ff ∨ b = bool.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}
convert a ℕ to a bool, 0 -> false, everything else -> true
Equations
- bool.of_nat n = decidable.to_bool (n ≠ 0)