# Booleans #

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

## Tags #

bool, boolean, Bool, De Morgan

@[deprecated decide_true_eq_true]
theorem Bool.decide_True (h : ) :

Alias of decide_true_eq_true.

@[deprecated decide_false_eq_false]
theorem Bool.decide_False (h : ) :

Alias of decide_false_eq_false.

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

Alias of decide_eq_true_iff.

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

Alias of decide_eq_true_iff.

@[deprecated decide_not]
theorem Bool.decide_not {p : Prop} [g : ] [h : ] :
() = !

Alias of decide_not.

@[deprecated Bool.false_ne_true]
theorem Bool.not_false' :

Alias of Bool.false_ne_true.

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

Alias of Bool.eq_iff_iff.

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

Alias of eq_true_of_ne_false.

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

Alias of eq_false_of_ne_true.

theorem Bool.or_inl {a : Bool} {b : Bool} (H : ) :
(a || b) = true
theorem Bool.or_inr {a : Bool} {b : Bool} (H : ) :
(a || b) = true
theorem Bool.and_elim_left {a : Bool} {b : Bool} :
(a && b) = true
theorem Bool.and_intro {a : Bool} {b : Bool} :
(a && b) = true
theorem Bool.and_elim_right {a : Bool} {b : Bool} :
(a && b) = 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
@[simp]
theorem Bool.le_iff_imp {x : Bool} {y : Bool} :
x y
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 : ) (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