Booleans

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

Tags

bool, boolean, Bool, De Morgan

theorem Bool.decide_True {h : Decidable True} : decide True = true

theorem Bool.decide_False {h : Decidable False} : decide False = false

@[simp]

theorem Bool.decide_coe (b : Bool) {h : Decidable (b = true)} : decide (b = true) = b

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

theorem Bool.of_decide_iff {p : Prop} [Decidable p] : decide p = true ↔ p

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

@[simp]

theorem Bool.decide_and (p : Prop) (q : Prop) [Decidable p] [Decidable q] : decide (p ∧ q) = (decide p && decide q)

@[simp]

theorem Bool.decide_or (p : Prop) (q : Prop) [Decidable p] [Decidable q] : decide (p ∨ q) = (decide p || decide q)

theorem Bool.not_false' : ¬false = true

theorem Bool.eq_iff_eq_true_iff {a : Bool} {b : Bool} : a = b ↔ (a = true ↔ b = true)

theorem Bool.beq_eq_decide_eq {α : Type u_1} [BEq α] [LawfulBEq α] [DecidableEq α] (a : α) (b : α) : (a == b) = decide (a = b)

theorem Bool.beq_comm {α : Type u_1} [BEq α] [LawfulBEq α] {a : α} {b : α} : (a == b) = (b == a)

@[simp]

theorem Bool.default_bool : default = false

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

@[simp]

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

@[simp]

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

instance Bool.decidableForallBool {p : Bool → Prop} [(b : Bool) → Decidable (p b)] : Decidable (∀ (b : Bool), p b)

If p b is decidable for all b : Bool, then ∀ b, p b is decidable

Equations

• Bool.decidableForallBool = decidable_of_decidable_of_iff (_ : p false ∧ p true ↔ ∀ (b : Bool), p b)

instance Bool.decidableExistsBool {p : Bool → Prop} [(b : Bool) → Decidable (p b)] : Decidable (∃ (b : Bool), p b)

If p b is decidable for all b : Bool, then ∃ b, p b is decidable

Equations

• Bool.decidableExistsBool = decidable_of_decidable_of_iff (_ : p false ∨ p true ↔ ∃ (b : Bool), p b)

theorem Bool.cond_eq_ite {α : Type u_1} (b : Bool) (t : α) (e : α) : (bif b then t else e) = if b = true then t else e

@[simp]

theorem Bool.cond_decide {α : Type u_1} (p : Prop) [Decidable p] (t : α) (e : α) : (bif decide p then t else e) = if p then t else e

@[simp]

theorem Bool.cond_not {α : Type u_1} (b : Bool) (t : α) (e : α) : (bif !b then t else e) = bif b then e else t

theorem Bool.not_ne_id : not ≠ id

theorem Bool.coe_iff_coe {a : Bool} {b : Bool} : (a = true ↔ b = true) ↔ a = b

theorem Bool.eq_true_of_ne_false {a : Bool} : a ≠ false → a = true

theorem Bool.eq_false_of_ne_true {a : Bool} : a ≠ true → a = false

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

@[simp]

theorem Bool.not_eq_not {a : Bool} {b : Bool} : ¬a = !b ↔ a = b

@[simp]

theorem Bool.not_not_eq {a : Bool} {b : Bool} : ¬(!a) = b ↔ a = b

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

theorem Bool.not_ne {a : Bool} {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 : 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

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 : ℕ) : 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) : (Bool.toNat b == 0) = !b

@[simp]

theorem Bool.toNat_bne_zero (b : Bool) : (Bool.toNat b != 0) = b

@[simp]

theorem Bool.toNat_beq_one (b : Bool) : (Bool.toNat b == 1) = b

@[simp]

theorem Bool.toNat_bne_one (b : Bool) : (Bool.toNat b != 1) = !b

theorem Bool.ofNat_le_ofNat {n : ℕ} {m : ℕ} (h : n ≤ m) : Bool.ofNat n ≤ Bool.ofNat m

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

theorem Bool.ofNat_toNat (b : Bool) : Bool.ofNat (Bool.toNat b) = 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

• Bool.xor3 x 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

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