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 : Bool) (b : Bool) : ((a && b) = true) = (a = true ∧ b = true)

theorem Bool.or_eq_true_eq_eq_true_or_eq_true (a : Bool) (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 : Bool) (b : Bool) : ((a && b) = false) = (a = false ∨ b = false)

theorem Bool.or_eq_false_eq_eq_false_and_eq_false (a : Bool) (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 : Prop} {q : Prop} [Decidable p] [Decidable q] (h : p ↔ q) : decide p = decide 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]

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)