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.true_eq_false_eq_False : ¬true = false

theorem Bool.false_eq_true_eq_False : ¬false = true

theorem Bool.eq_false_eq_not_eq_true (b : Bool) : (¬b = true) = (b = false)

theorem Bool.eq_true_eq_not_eq_false (b : Bool) : (¬b = false) = (b = true)

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

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

theorem Bool.and_eq_true_eq_eq_true_and_eq_true (a b : Bool) : ((a && b) = true) = (a = true ∧ b = true)

theorem Bool.or_eq_true_eq_eq_true_or_eq_true (a b : Bool) : ((a || b) = true) = (a = true ∨ b = true)

theorem Bool.not_eq_true_eq_eq_false (a : Bool) : ((!a) = true) = (a = false)

theorem Bool.and_eq_false_eq_eq_false_or_eq_false (a b : Bool) : ((a && b) = false) = (a = false ∨ b = false)

theorem Bool.or_eq_false_eq_eq_false_and_eq_false (a b : Bool) : ((a || b) = false) = (a = false ∧ b = false)

theorem Bool.not_eq_false_eq_eq_true (a : Bool) : ((!a) = false) = (a = true)

theorem Bool.coe_false : (false = true) = False

theorem Bool.coe_true : (true = true) = True

theorem Bool.coe_sort_false : (false = true) = False

theorem Bool.coe_sort_true : (true = true) = True

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

theorem Bool.decide_true {p : Prop} [Decidable p] : p → decide p = true

theorem Bool.of_decide_true {p : Prop} [Decidable p] : decide p = true → p

theorem Bool.bool_iff_false {b : Bool} : ¬b = true ↔ b = false

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

theorem Bool.decide_false_iff (p : Prop) {x✝ : Decidable p} : decide p = false ↔ ¬p

theorem Bool.decide_false {p : Prop} [Decidable p] : ¬p → decide p = false

theorem Bool.of_decide_false {p : Prop} [Decidable p] : decide p = false → ¬p

theorem Bool.decide_congr {p q : Prop} [Decidable p] [Decidable q] (h : p ↔ q) : decide p = decide q

theorem Bool.coe_xor_iff (a b : Bool) : (a ^^ b) = true ↔ Xor' (a = true) (b = true)

theorem Bool.dichotomy (b : Bool) : b = false ∨ b = true

theorem Bool.not_ne_id : not ≠ id

theorem Bool.or_inl {a b : Bool} (H : a = true) : (a || b) = true

theorem Bool.or_inr {a b : Bool} (H : b = true) : (a || b) = true

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

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

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

theorem Bool.eq_not_iff {a b : Bool} : a = !b ↔ a ≠ b

theorem Bool.not_eq_iff {a b : Bool} : (!decide (a = b)) = true ↔ a ≠ b

theorem Bool.ne_not {a 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 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 y : Bool} : (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 y : Bool} : x < y ↔ x = false ∧ y = true

@[simp]

theorem Bool.false_lt_true : false < true

theorem Bool.le_iff_imp {x y : Bool} : x ≤ y ↔ x = true → y = true

theorem Bool.and_le_left (x y : Bool) : (x && y) ≤ x

theorem Bool.and_le_right (x y : Bool) : (x && y) ≤ y

theorem Bool.le_and {x y z : Bool} : x ≤ y → x ≤ z → x ≤ (y && z)

theorem Bool.left_le_or (x y : Bool) : x ≤ (x || y)

theorem Bool.right_le_or (x y : Bool) : y ≤ (x || y)

theorem Bool.or_le {x y z : Bool} : x ≤ z → y ≤ z → (x || y) ≤ z

def Bool.ofNat (n : ℕ) : 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 m : ℕ} (h : n ≤ m) : ofNat n ≤ ofNat m

theorem Bool.toNat_le_toNat {b₀ b₁ : Bool} (h : b₀ ≤ b₁) : b₀.toNat ≤ b₁.toNat

theorem Bool.ofNat_toNat (b : 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 y c : Bool) : Bool

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

Equations

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

def Bool.carry (x y 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)