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

This section contains lemmas about booleans which were present in core Lean 3. The remainder of this file contains lemmas about booleans from mathlib 3.

theorem Bool.decide_iff (p : Prop) [d : Decidable p] :
theorem Bool.decide_true {p : Prop} [Decidable p] :
pdecide p = true
theorem Bool.bool_eq_false {b : Bool} :
¬b = trueb = false
theorem Bool.decide_false_iff (p : Prop) :
∀ {x : Decidable p}, decide p = false ¬p
theorem Bool.decide_congr {p : Prop} {q : Prop} [Decidable p] [Decidable q] (h : p q) :
@[deprecated Bool.or_eq_true_iff]
theorem Bool.coe_or_iff (x : Bool) (y : Bool) :
(x || y) = true x = true y = true

Alias of Bool.or_eq_true_iff.

@[deprecated Bool.and_eq_true_iff]
theorem Bool.coe_and_iff (x : Bool) (y : Bool) :
(x && y) = true x = true y = true

Alias of Bool.and_eq_true_iff.

theorem Bool.coe_xor_iff (a : Bool) (b : Bool) :
xor a b = true Xor' (a = true) (b = true)
@[deprecated decide_true_eq_true]

Alias of decide_true_eq_true.

@[deprecated decide_false_eq_false]

Alias of decide_false_eq_false.

@[deprecated decide_eq_true_iff]
theorem Bool.coe_decide (p : Prop) [Decidable p] :

Alias of decide_eq_true_iff.

@[deprecated decide_eq_true_iff]

Alias of decide_eq_true_iff.

@[deprecated decide_not]
theorem Bool.decide_not {p : Prop} [g : Decidable p] [h : Decidable ¬p] :

Alias of decide_not.

@[deprecated Bool.false_ne_true]

Alias of Bool.false_ne_true.

@[deprecated Bool.eq_iff_iff]
theorem Bool.eq_iff_eq_true_iff {a : Bool} {b : Bool} :
a = b (a = true b = true)

Alias of Bool.eq_iff_iff.

theorem Bool.forall_bool' {p : BoolProp} (b : Bool) :
(∀ (x : Bool), p x) p b p !b
@[simp]
theorem Bool.forall_bool {p : BoolProp} :
(∀ (b : Bool), p b) p false p true
theorem Bool.exists_bool' {p : BoolProp} (b : Bool) :
(∃ (x : Bool), p x) p b p !b
@[simp]
theorem Bool.exists_bool {p : BoolProp} :
(∃ (b : Bool), p b) p false p true
@[deprecated eq_true_of_ne_false]
theorem Bool.eq_true_of_ne_false {b : Bool} :
¬b = falseb = true

Alias of eq_true_of_ne_false.

@[deprecated eq_false_of_ne_true]
theorem Bool.eq_false_of_ne_true {b : Bool} :
¬b = trueb = false

Alias of eq_false_of_ne_true.

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
theorem Bool.ne_not {a : Bool} {b : Bool} :
a !b a = b
@[deprecated Bool.not_not_eq]
theorem Bool.not_ne {a : Bool} {b : Bool} :
¬(!a) = b a = b

Alias of Bool.not_not_eq.

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 #

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 : Nat) :

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

Equations
Instances For
    @[simp]
    theorem Bool.toNat_beq_zero (b : Bool) :
    (b.toNat == 0) = !b
    @[simp]
    theorem Bool.toNat_bne_zero (b : Bool) :
    (b.toNat != 0) = b
    @[simp]
    theorem Bool.toNat_beq_one (b : Bool) :
    (b.toNat == 1) = b
    @[simp]
    theorem Bool.toNat_bne_one (b : Bool) :
    (b.toNat != 1) = !b
    theorem Bool.ofNat_le_ofNat {n : Nat} {m : Nat} (h : n m) :
    theorem Bool.toNat_le_toNat {b₀ : Bool} {b₁ : Bool} (h : b₀ b₁) :
    b₀.toNat b₁.toNat
    theorem Bool.ofNat_toNat (b : Bool) :
    Bool.ofNat b.toNat = 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