Lemmas about booleans

These are the lemmas about booleans which were present in core Lean 3. See also the file Mathlib.Data.Bool.Basic which contains lemmas about booleans from mathlib 3.

@[simp]

theorem Bool.cond_true {α : Type u} {a : α} {b : α} : (bif true then a else b) = a

@[simp]

theorem Bool.cond_false {α : Type u} {a : α} {b : α} : (bif false then a else b) = b

@[simp]

theorem Bool.cond_self {α : Type u} (b : Bool) (a : α) : (bif b then a else a) = a

@[simp]

theorem Bool.xor_self (b : Bool) : xor b b = false

@[simp]

theorem Bool.xor_true (b : Bool) : xor b true = !b

theorem Bool.xor_false (b : Bool) : xor b false = b

@[simp]

theorem Bool.true_xor (b : Bool) : xor true b = !b

theorem Bool.false_xor (b : Bool) : xor false b = b

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)

@[simp]

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

@[simp]

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) [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

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

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

@[simp]

theorem Bool.xor_coe_iff (a : Bool) (b : Bool) : xor a b = true ↔ Xor' (a = true) (b = true)

@[simp]

theorem Bool.ite_eq_true_distrib (c : Prop) [Decidable c] (a : Bool) (b : Bool) : ((if c then a else b) = true) = if c then a = true else b = true

@[simp]

theorem Bool.ite_eq_false_distrib (c : Prop) [Decidable c] (a : Bool) (b : Bool) : ((if c then a else b) = false) = if c then a = false else b = false