Documentation

Mathlib.Data.Bool.Basic

Booleans #

This file proves various trivial lemmas about booleans and their relation to decidable propositions.

Tags #

bool, boolean, Bool, De Morgan

@[simp]
theorem Bool.decide_coe (b : Bool) {h : Decidable (b = true)} :
decide (b = true) = b
theorem Bool.coe_decide (p : Prop) [d : Decidable p] :
@[simp]
theorem Bool.decide_and (p : Prop) (q : Prop) [Decidable p] [Decidable q] :
decide (p q) = (decide p && decide q)
@[simp]
theorem Bool.decide_or (p : Prop) (q : Prop) [Decidable p] [Decidable q] :
decide (p q) = (decide p || decide q)
theorem Bool.eq_iff_eq_true_iff {a : Bool} {b : Bool} :
a = b (a = true b = true)
theorem Bool.beq_eq_decide_eq {α : Type u_1} [BEq α] [LawfulBEq α] [DecidableEq α] (a : α) (b : α) :
(a == b) = decide (a = b)
theorem Bool.beq_comm {α : Type u_1} [BEq α] [LawfulBEq α] {a : α} {b : α} :
(a == b) = (b == a)
@[simp]
theorem Bool.default_bool :
default = false
@[simp]
theorem Bool.forall_bool {p : BoolProp} :
(∀ (b : Bool), p b) p false p true
@[simp]
theorem Bool.exists_bool {p : BoolProp} :
(∃ (b : Bool), p b) p false p true
instance Bool.decidableForallBool {p : BoolProp} [(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
instance Bool.decidableExistsBool {p : BoolProp} [(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
theorem Bool.cond_eq_ite {α : Type u_1} (b : Bool) (t : α) (e : α) :
(bif b then t else e) = if b = true then t else e
@[simp]
theorem Bool.cond_decide {α : Type u_1} (p : Prop) [Decidable p] (t : α) (e : α) :
(bif decide p then t else e) = if p then t else e
@[simp]
theorem Bool.cond_not {α : Type u_1} (b : Bool) (t : α) (e : α) :
(bif !b then t else e) = bif b then e else t
theorem Bool.coe_iff_coe {a : Bool} {b : Bool} :
(a = true b = true) a = b
theorem Bool.or_inl {a : Bool} {b : Bool} (H : a = true) :
(a || b) = true
theorem Bool.or_inr {a : Bool} {b : Bool} (H : b = true) :
(a || b) = true
theorem Bool.and_elim_left {a : Bool} {b : Bool} :
(a && b) = truea = true
theorem Bool.and_intro {a : Bool} {b : Bool} :
a = trueb = true(a && b) = true
theorem Bool.and_elim_right {a : Bool} {b : Bool} :
(a && b) = trueb = true
theorem Bool.eq_not_iff {a : Bool} {b : Bool} :
a = !b a b
theorem Bool.not_eq_iff {a : Bool} {b : Bool} :
(!decide (a = b)) = true a b
@[simp]
theorem Bool.not_eq_not {a : Bool} {b : Bool} :
¬a = !b a = b
@[simp]
theorem Bool.not_not_eq {a : Bool} {b : Bool} :
¬(!a) = b a = b
theorem Bool.ne_not {a : Bool} {b : Bool} :
a !b a = b
theorem Bool.not_ne {a : Bool} {b : Bool} :
(!a) b a = b
theorem Bool.not_ne_self (b : Bool) :
(!b) b
theorem Bool.self_ne_not (b : Bool) :
b !b
theorem Bool.eq_or_eq_not (a : Bool) (b : Bool) :
a = b a = !b
theorem Bool.xor_iff_ne {x : Bool} {y : Bool} :
xor x y = true x y

De Morgan's laws for booleans #

Equations
theorem Bool.lt_iff {x : Bool} {y : Bool} :
x < y x = false y = true
theorem Bool.le_iff_imp {x : Bool} {y : Bool} :
x y x = truey = true
theorem Bool.and_le_left (x : Bool) (y : Bool) :
(x && y) x
theorem Bool.and_le_right (x : Bool) (y : Bool) :
(x && y) y
theorem Bool.le_and {x : Bool} {y : Bool} {z : Bool} :
x yx zx (y && z)
theorem Bool.left_le_or (x : Bool) (y : Bool) :
x (x || y)
theorem Bool.right_le_or (x : Bool) (y : Bool) :
y (x || y)
theorem Bool.or_le {x : Bool} {y : Bool} {z : Bool} :
x zy z(x || y) z
def Bool.ofNat (n : ) :

convert a to a Bool, 0 -> false, everything else -> true

Equations
Instances For
    @[simp]
    theorem Bool.toNat_beq_zero (b : Bool) :
    (Bool.toNat b == 0) = !b
    @[simp]
    theorem Bool.toNat_bne_zero (b : Bool) :
    (Bool.toNat b != 0) = b
    @[simp]
    theorem Bool.toNat_beq_one (b : Bool) :
    (Bool.toNat b == 1) = b
    @[simp]
    theorem Bool.toNat_bne_one (b : Bool) :
    (Bool.toNat b != 1) = !b
    theorem Bool.ofNat_le_ofNat {n : } {m : } (h : n m) :
    theorem Bool.toNat_le_toNat {b₀ : Bool} {b₁ : Bool} (h : b₀ b₁) :
    @[simp]
    theorem Bool.injective_iff {α : Sort u_1} {f : Boolα} :
    theorem Bool.apply_apply_apply (f : BoolBool) (x : Bool) :
    f (f (f x)) = f x

    Kaminski's Equation

    def Bool.xor3 (x : Bool) (y : Bool) (c : Bool) :

    xor3 x y c is ((x XOR y) XOR c).

    Equations
    Instances For
      def Bool.carry (x : Bool) (y : Bool) (c : Bool) :

      carry x y c is x && y || x && c || y && c.

      Equations
      Instances For