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

@[simp]

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

@[simp]

theorem Bool.false_eq_decide_iff {p : Prop} [Decidable p] : false = decide p ↔ ¬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} [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, 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, 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, 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_bool_iff {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_comm (a : Bool) (b : Bool) : (a || b) = (b || a)

theorem Bool.or_left_comm (a : Bool) (b : Bool) (c : Bool) : (a || (b || c)) = (b || (a || c))

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

theorem Bool.and_left_comm (a : Bool) (b : Bool) (c : Bool) : (a && (b && c)) = (b && (a && c))

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.and_or_distrib_left (a : Bool) (b : Bool) (c : Bool) : (a && (b || c)) = (a && b || a && c)

theorem Bool.and_or_distrib_right (a : Bool) (b : Bool) (c : Bool) : ((a || b) && c) = (a && c || b && c)

theorem Bool.or_and_distrib_left (a : Bool) (b : Bool) (c : Bool) : (a || b && c) = ((a || b) && (a || c))

theorem Bool.or_and_distrib_right (a : Bool) (b : Bool) (c : Bool) : (a && b || c) = ((a || c) && (b || c))

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

@[simp]

theorem Bool.and_not_self (x : Bool) : (x && !x) = false

@[simp]

theorem Bool.not_and_self (x : Bool) : (!x && x) = false

@[simp]

theorem Bool.or_not_self (x : Bool) : (x || !x) = true

@[simp]

theorem Bool.not_or_self (x : Bool) : (!x || x) = true

theorem Bool.xor_comm (a : Bool) (b : Bool) : xor a b = xor b a

@[simp]

theorem Bool.xor_assoc (a : Bool) (b : Bool) (c : Bool) : xor (xor a b) c = xor a (xor b c)

theorem Bool.xor_left_comm (a : Bool) (b : Bool) (c : Bool) : xor a (xor b c) = xor b (xor a c)

@[simp]

theorem Bool.xor_not_left (a : Bool) : xor (!a) a = true

@[simp]

theorem Bool.xor_not_right (a : Bool) : (xor a !a) = true

@[simp]

theorem Bool.xor_not_not (a : Bool) (b : Bool) : (xor (!a) !b) = xor a b

@[simp]

theorem Bool.xor_false_left (a : Bool) : xor false a = a

@[simp]

theorem Bool.xor_false_right (a : Bool) : xor a false = a

theorem Bool.and_xor_distrib_left (a : Bool) (b : Bool) (c : Bool) : (a && xor b c) = xor (a && b) (a && c)

theorem Bool.and_xor_distrib_right (a : Bool) (b : Bool) (c : Bool) : (xor a b && c) = xor (a && c) (b && c)

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

De Morgan's laws for booleans

@[simp]

theorem Bool.not_and (a : Bool) (b : Bool) : (!(a && b)) = (!a || !b)

@[simp]

theorem Bool.not_or (a : Bool) (b : Bool) : (!(a || b)) = (!a && !b)

theorem Bool.not_inj {a : Bool} {b : Bool} : (!a) = !b → a = b

instance Bool.linearOrder : LinearOrder Bool

Equations

• Bool.linearOrder = LinearOrder.mk Bool.linearOrder.proof_5 (id (id (id inferInstance))) inferInstance decidableLTOfDecidableLE

@[simp]

theorem Bool.false_le {x : Bool} : false ≤ x

@[simp]

theorem Bool.le_true {x : Bool} : x ≤ true

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

convert a Bool to a ℕ, false -> 0, true -> 1

Equations

• Bool.toNat b = bif b then 1 else 0

def Bool.ofNat (n : ℕ) : Bool

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

Equations

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

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)