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 : Decidable True) : decide True = true

Alias of decide_true_eq_true.

@[deprecated decide_false_eq_false]

theorem Bool.decide_False (h : Decidable False) : decide False = false

Alias of decide_false_eq_false.

@[deprecated decide_eq_true_iff]

theorem Bool.coe_decide (p : Prop) [Decidable p] : decide p = true ↔ p

Alias of decide_eq_true_iff.

@[deprecated decide_eq_true_iff]

theorem Bool.of_decide_iff (p : Prop) [Decidable p] : decide p = true ↔ p

Alias of decide_eq_true_iff.

@[deprecated decide_not]

theorem Bool.decide_not {p : Prop} [g : Decidable p] [h : Decidable ¬p] : (decide ¬p) = !decide p

Alias of decide_not.

@[deprecated Bool.false_ne_true]

theorem Bool.not_false' : false ≠ 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.dichotomy (b : Bool) : b = false ∨ b = true

theorem Bool.forall_bool' {p : Bool → Prop} (b : Bool) : (∀ (x : Bool), p x) ↔ p b ∧ p !b

@[simp]

theorem Bool.forall_bool {p : Bool → Prop} : (∀ (b : Bool), p b) ↔ p false ∧ p true

theorem Bool.exists_bool' {p : Bool → Prop} (b : Bool) : (∃ (x : Bool), p x) ↔ p b ∨ p !b

@[simp]

theorem Bool.exists_bool {p : Bool → Prop} : (∃ (b : Bool), p b) ↔ p false ∨ p true

theorem Bool.not_ne_id : not ≠ id

@[deprecated eq_true_of_ne_false]

theorem Bool.eq_true_of_ne_false {b : Bool} : ¬b = false → b = true

Alias of eq_true_of_ne_false.

@[deprecated eq_false_of_ne_true]

theorem Bool.eq_false_of_ne_true {b : Bool} : ¬b = true → b = 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) = true → a = true

theorem Bool.and_intro {a : Bool} {b : Bool} : a = true → b = true → (a && b) = true

theorem Bool.and_elim_right {a : Bool} {b : Bool} : (a && b) = true → 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.not_iff_not {b : Bool} : (!b) = true ↔ ¬b = true

theorem Bool.eq_true_of_not_eq_false' {a : Bool} : (!decide (a = false)) = true → a = true

theorem Bool.eq_false_of_not_eq_true' {a : Bool} : (!decide (a = true)) = true → a = false

theorem Bool.bne_eq_xor : bne = xor

theorem Bool.xor_iff_ne {x : Bool} {y : Bool} : xor x y = true ↔ x ≠ y

De Morgan's laws for booleans

instance Bool.linearOrder : LinearOrder Bool

Equations

• Bool.linearOrder = LinearOrder.mk Bool.linearOrder.proof_5 inferInstance inferInstance inferInstance Bool.linearOrder.proof_6 Bool.linearOrder.proof_7 Bool.linearOrder.proof_8

theorem Bool.lt_iff {x : Bool} {y : Bool} : x < y ↔ x = false ∧ y = true

@[simp]

theorem Bool.false_lt_true : false < true

theorem Bool.le_iff_imp {x : Bool} {y : Bool} : x ≤ y ↔ x = true → y = 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 ≤ y → x ≤ z → x ≤ (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 ≤ z → y ≤ z → (x || y) ≤ z

def Bool.ofNat (n : Nat) : Bool

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

Equations

• Bool.ofNat n = decide (n ≠ 0)

@[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) : Bool.ofNat n ≤ Bool.ofNat 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 → α} : Function.Injective f ↔ f false ≠ f true

theorem Bool.apply_apply_apply (f : Bool → Bool) (x : Bool) : f (f (f x)) = f x

Kaminski's Equation

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

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

Equations

• x.xor3 y c = xor (xor x y) c

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

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

Equations

• x.carry y c = (x && y || x && c || y && c)