@[reducible, inline]

abbrev Bool.xor : Bool → Bool → Bool

Boolean “exclusive or”. xor x y can be written x ^^ y.

x ^^ y is true when precisely one of x or y is true. Unlike and and or, it does not have short-circuiting behavior, because one argument's value never determines the final value. Also unlike and and or, there is no commonly-used corresponding propositional connective.

Examples:

• false ^^ false = false
• true ^^ false = true
• false ^^ true = true
• true ^^ true = false

Conventions for notations in identifiers:

• The recommended spelling of ^^ in identifiers is xor.

Equations

• xor = bne

def Bool.«term_^^_» : Lean.TrailingParserDescr

Boolean “exclusive or”. xor x y can be written x ^^ y.

x ^^ y is true when precisely one of x or y is true. Unlike and and or, it does not have short-circuiting behavior, because one argument's value never determines the final value. Also unlike and and or, there is no commonly-used corresponding propositional connective.

Examples:

• false ^^ false = false
• true ^^ false = true
• false ^^ true = true
• true ^^ true = false

Conventions for notations in identifiers:

• The recommended spelling of ^^ in identifiers is xor.

Equations

• Bool.«term_^^_» = Lean.ParserDescr.trailingNode `Bool.«term_^^_» 33 33 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol " ^^ ") (Lean.ParserDescr.cat `term 34))

instance Bool.instDecidableForallOfDecidablePred (p : Bool → Prop) [inst : DecidablePred p] : Decidable (∀ (x : Bool), p x)

Equations

• Bool.instDecidableForallOfDecidablePred p = match inst true, inst false with | isFalse ht, x => isFalse ⋯ | x, isFalse hf => isFalse ⋯ | isTrue ht, isTrue hf => isTrue ⋯

instance Bool.instDecidableExistsOfDecidablePred (p : Bool → Prop) [inst : DecidablePred p] : Decidable (∃ (x : Bool), p x)

Equations

• Bool.instDecidableExistsOfDecidablePred p = match inst true, inst false with | isTrue ht, x => isTrue ⋯ | x, isTrue hf => isTrue ⋯ | isFalse ht, isFalse hf => isFalse ⋯

@[simp]

theorem Bool.default_bool : default = false

instance Bool.instLE : LE Bool

Equations

• Bool.instLE = { le := fun (x1 x2 : Bool) => x1 = true → x2 = true }

instance Bool.instLT : LT Bool

Equations

• Bool.instLT = { lt := fun (x1 x2 : Bool) => (!x1 && x2) = true }

instance Bool.instDecidableLe (x y : Bool) : Decidable (x ≤ y)

Equations

• x.instDecidableLe y = inferInstanceAs (Decidable (x = true → y = true))

instance Bool.instDecidableLt (x y : Bool) : Decidable (x < y)

Equations

• x.instDecidableLt y = inferInstanceAs (Decidable ((!x && y) = true))

instance Bool.instMax : Max Bool

Equations

• Bool.instMax = { max := or }

instance Bool.instMin : Min Bool

Equations

• Bool.instMin = { min := and }

theorem Bool.false_ne_true : false ≠ true

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

theorem Bool.eq_false_iff {b : Bool} : b = false ↔ b ≠ true

theorem Bool.ne_false_iff {b : Bool} : b ≠ false ↔ b = true

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

@[simp]

theorem Bool.decide_eq_true {b : Bool} [Decidable (b = true)] : decide (b = true) = b

@[simp]

theorem Bool.decide_eq_false {b : Bool} [Decidable (b = false)] : decide (b = false) = !b

theorem Bool.decide_true_eq {b : Bool} [Decidable (true = b)] : decide (true = b) = b

theorem Bool.decide_false_eq {b : Bool} [Decidable (false = b)] : decide (false = b) = !b

@[simp]

theorem Bool.eq_false_imp_eq_true_iff (a b : Bool) : (a = false → b = true ↔ b = false → a = true) = True

@[simp]

theorem Bool.eq_true_imp_eq_false_iff (a b : Bool) : (a = true → b = false ↔ b = true → a = false) = True

and

@[simp]

theorem Bool.and_self_left (a b : Bool) : (a && (a && b)) = (a && b)

@[simp]

theorem Bool.and_self_right (a b : Bool) : (a && b && b) = (a && b)

@[simp]

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

@[simp]

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

@[simp]

theorem Bool.eq_true_and_eq_false_self (b : Bool) : b = true ∧ b = false ↔ False

@[simp]

theorem Bool.eq_false_and_eq_true_self (b : Bool) : b = false ∧ b = true ↔ False

theorem Bool.and_comm (x y : Bool) : (x && y) = (y && x)

instance Bool.instCommutativeAnd : Std.Commutative fun (x1 x2 : Bool) => x1 && x2

theorem Bool.and_left_comm (x y z : Bool) : (x && (y && z)) = (y && (x && z))

theorem Bool.and_right_comm (x y z : Bool) : (x && y && z) = (x && z && y)

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

@[reducible, inline, deprecated Bool.and_eq_left_iff_imp (since := "2025-04-04")]

abbrev Bool.and_iff_left_iff_imp {a b : Bool} : (a && b) = a ↔ a = true → b = true

Equations

• @Bool.and_iff_left_iff_imp = @Bool.and_eq_left_iff_imp

@[reducible, inline, deprecated Bool.and_eq_right_iff_imp (since := "2025-04-04")]

abbrev Bool.and_iff_right_iff_imp {a b : Bool} : (a && b) = b ↔ b = true → a = true

Equations

• @Bool.and_iff_right_iff_imp = @Bool.and_eq_right_iff_imp

@[reducible, inline, deprecated Bool.eq_self_and (since := "2025-04-04")]

abbrev Bool.iff_self_and {a b : Bool} : a = (a && b) ↔ a = true → b = true

Equations

• @Bool.iff_self_and = @Bool.eq_self_and

@[reducible, inline, deprecated Bool.eq_and_self (since := "2025-04-04")]

abbrev Bool.iff_and_self {a b : Bool} : b = (a && b) ↔ b = true → a = true

Equations

• @Bool.iff_and_self = @Bool.eq_and_self

@[simp]

theorem Bool.not_and_eq_left_iff_and {a b : Bool} : (!a && b) = a ↔ (!a) = true ∧ (!b) = true

@[simp]

theorem Bool.and_not_eq_right_iff_and {a b : Bool} : (a && !b) = b ↔ (!a) = true ∧ (!b) = true

@[simp]

theorem Bool.eq_not_self_and {a b : Bool} : a = (!a && b) ↔ (!a) = true ∧ (!b) = true

@[simp]

theorem Bool.eq_and_not_self {a b : Bool} : b = (a && !b) ↔ (!a) = true ∧ (!b) = true

@[reducible, inline, deprecated Bool.not_and_eq_left_iff_and (since := "2025-04-04")]

abbrev Bool.not_and_iff_left_iff_imp {a b : Bool} : (!a && b) = a ↔ (!a) = true ∧ (!b) = true

Equations

• @Bool.not_and_iff_left_iff_imp = @Bool.not_and_eq_left_iff_and

@[reducible, inline, deprecated Bool.and_not_eq_right_iff_and (since := "2025-04-04")]

abbrev Bool.and_not_iff_right_iff_imp {a b : Bool} : (a && !b) = b ↔ (!a) = true ∧ (!b) = true

Equations

• @Bool.and_not_iff_right_iff_imp = @Bool.and_not_eq_right_iff_and

@[reducible, inline, deprecated Bool.eq_not_self_and (since := "2025-04-04")]

abbrev Bool.iff_not_self_and {a b : Bool} : a = (!a && b) ↔ (!a) = true ∧ (!b) = true

Equations

• @Bool.iff_not_self_and = @Bool.eq_not_self_and

@[reducible, inline, deprecated Bool.eq_and_not_self (since := "2025-04-04")]

abbrev Bool.iff_and_not_self {a b : Bool} : b = (a && !b) ↔ (!a) = true ∧ (!b) = true

Equations

• @Bool.iff_and_not_self = @Bool.eq_and_not_self

or

@[simp]

theorem Bool.or_self_left (a b : Bool) : (a || (a || b)) = (a || b)

@[simp]

theorem Bool.or_self_right (a b : Bool) : (a || b || b) = (a || b)

@[simp]

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

@[simp]

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

@[simp]

theorem Bool.eq_true_or_eq_false_self (b : Bool) : b = true ∨ b = false ↔ True

@[simp]

theorem Bool.eq_false_or_eq_true_self (b : Bool) : b = false ∨ b = true ↔ True

@[simp]

theorem Bool.or_eq_left_iff_imp {a b : Bool} : (a || b) = a ↔ b = true → a = true

@[simp]

theorem Bool.or_eq_right_iff_imp {a b : Bool} : (a || b) = b ↔ a = true → b = true

@[simp]

theorem Bool.eq_self_or {a b : Bool} : a = (a || b) ↔ b = true → a = true

@[simp]

theorem Bool.eq_or_self {a b : Bool} : b = (a || b) ↔ a = true → b = true

@[reducible, inline, deprecated Bool.or_eq_left_iff_imp (since := "2025-04-04")]

abbrev Bool.or_iff_left_iff_imp {a b : Bool} : (a || b) = a ↔ b = true → a = true

Equations

• @Bool.or_iff_left_iff_imp = @Bool.or_eq_left_iff_imp

@[reducible, inline, deprecated Bool.or_eq_right_iff_imp (since := "2025-04-04")]

abbrev Bool.or_iff_right_iff_imp {a b : Bool} : (a || b) = b ↔ a = true → b = true

Equations

• @Bool.or_iff_right_iff_imp = @Bool.or_eq_right_iff_imp

@[reducible, inline, deprecated Bool.eq_self_or (since := "2025-04-04")]

abbrev Bool.iff_self_or {a b : Bool} : a = (a || b) ↔ b = true → a = true

Equations

• @Bool.iff_self_or = @Bool.eq_self_or

@[reducible, inline, deprecated Bool.eq_or_self (since := "2025-04-04")]

abbrev Bool.iff_or_self {a b : Bool} : b = (a || b) ↔ a = true → b = true

Equations

• @Bool.iff_or_self = @Bool.eq_or_self

@[simp]

theorem Bool.not_or_eq_left_iff_and {a b : Bool} : (!a || b) = a ↔ a = true ∧ b = true

@[simp]

theorem Bool.or_not_eq_right_iff_and {a b : Bool} : (a || !b) = b ↔ a = true ∧ b = true

@[simp]

theorem Bool.eq_not_self_or {a b : Bool} : a = (!a || b) ↔ a = true ∧ b = true

@[simp]

theorem Bool.eq_or_not_self {a b : Bool} : b = (a || !b) ↔ a = true ∧ b = true

@[reducible, inline, deprecated Bool.not_or_eq_left_iff_and (since := "2025-04-04")]

abbrev Bool.not_or_iff_left_iff_imp {a b : Bool} : (!a || b) = a ↔ a = true ∧ b = true

Equations

• @Bool.not_or_iff_left_iff_imp = @Bool.not_or_eq_left_iff_and

@[reducible, inline, deprecated Bool.or_not_eq_right_iff_and (since := "2025-04-04")]

abbrev Bool.or_not_iff_right_iff_imp {a b : Bool} : (a || !b) = b ↔ a = true ∧ b = true

Equations

• @Bool.or_not_iff_right_iff_imp = @Bool.or_not_eq_right_iff_and

@[reducible, inline, deprecated Bool.eq_not_self_or (since := "2025-04-04")]

abbrev Bool.iff_not_self_or {a b : Bool} : a = (!a || b) ↔ a = true ∧ b = true

Equations

• @Bool.iff_not_self_or = @Bool.eq_not_self_or

@[reducible, inline, deprecated Bool.eq_or_not_self (since := "2025-04-04")]

abbrev Bool.iff_or_not_self {a b : Bool} : b = (a || !b) ↔ a = true ∧ b = true

Equations

• @Bool.iff_or_not_self = @Bool.eq_or_not_self

theorem Bool.or_comm (x y : Bool) : (x || y) = (y || x)

instance Bool.instCommutativeOr : Std.Commutative fun (x1 x2 : Bool) => x1 || x2

theorem Bool.or_left_comm (x y z : Bool) : (x || (y || z)) = (y || (x || z))

theorem Bool.or_right_comm (x y z : Bool) : (x || y || z) = (x || z || y)

distributivity

theorem Bool.and_or_distrib_left (x y z : Bool) : (x && (y || z)) = (x && y || x && z)

theorem Bool.and_or_distrib_right (x y z : Bool) : ((x || y) && z) = (x && z || y && z)

theorem Bool.or_and_distrib_left (x y z : Bool) : (x || y && z) = ((x || y) && (x || z))

theorem Bool.or_and_distrib_right (x y z : Bool) : (x && y || z) = ((x || z) && (y || z))

theorem Bool.and_xor_distrib_left (x y z : Bool) : (x && (y ^^ z)) = (x && y ^^ x && z)

theorem Bool.and_xor_distrib_right (x y z : Bool) : ((x ^^ y) && z) = (x && z ^^ y && z)

@[simp]

theorem Bool.not_and (x y : Bool) : (!(x && y)) = (!x || !y)

De Morgan's law for boolean and

@[simp]

theorem Bool.not_or (x y : Bool) : (!(x || y)) = (!x && !y)

De Morgan's law for boolean or

theorem Bool.and_eq_true_iff {x y : Bool} : (x && y) = true ↔ x = true ∧ y = true

theorem Bool.and_eq_false_iff {x y : Bool} : (x && y) = false ↔ x = false ∨ y = false

@[simp]

theorem Bool.and_eq_false_imp {x y : Bool} : (x && y) = false ↔ x = true → y = false

theorem Bool.or_eq_true_iff {x y : Bool} : (x || y) = true ↔ x = true ∨ y = true

@[simp]

theorem Bool.or_eq_false_iff {x y : Bool} : (x || y) = false ↔ x = false ∧ y = false

eq/beq/bne

@[simp]

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

These two rules follow trivially by simp, but are needed to avoid non-termination in false_eq and true_eq.

@[simp]

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

@[simp]

theorem Bool.false_eq (b : Bool) : (false = b) = (b = false)

@[simp]

theorem Bool.true_eq (b : Bool) : (true = b) = (b = true)

@[simp]

theorem Bool.true_beq (b : Bool) : (true == b) = b

@[simp]

theorem Bool.false_beq (b : Bool) : (false == b) = !b

instance Bool.instLawfulIdentityBeqTrue : Std.LawfulIdentity (fun (x1 x2 : Bool) => x1 == x2) true

@[simp]

theorem Bool.true_bne (b : Bool) : (true != b) = !b

@[simp]

theorem Bool.false_bne (b : Bool) : (false != b) = b

@[simp]

theorem Bool.bne_true (b : Bool) : (b != true) = !b

@[simp]

theorem Bool.bne_false (b : Bool) : (b != false) = b

instance Bool.instLawfulIdentityBneFalse : Std.LawfulIdentity (fun (x1 x2 : Bool) => x1 != x2) false

@[simp]

theorem Bool.not_beq_self (x : Bool) : ((!x) == x) = false

@[simp]

theorem Bool.beq_not_self (x : Bool) : (x == !x) = false

@[simp]

theorem Bool.not_bne (a b : Bool) : ((!a) != b) = !a != b

@[simp]

theorem Bool.bne_not (a b : Bool) : (a != !b) = !a != b

theorem Bool.not_bne_self (x : Bool) : ((!x) != x) = true

theorem Bool.bne_not_self (x : Bool) : (x != !x) = true

theorem Bool.not_eq_self (b : Bool) : (!b) = b ↔ False

@[simp]

theorem Bool.eq_not_self (b : Bool) : b = !b ↔ False

@[simp]

theorem Bool.beq_self_left (a b : Bool) : (a == (a == b)) = b

@[simp]

theorem Bool.beq_self_right (a b : Bool) : ((a == b) == b) = a

@[simp]

theorem Bool.bne_self_left (a b : Bool) : (a != (a != b)) = b

@[simp]

theorem Bool.bne_self_right (a b : Bool) : ((a != b) != b) = a

theorem Bool.not_bne_not (x y : Bool) : ((!x) != !y) = (x != y)

@[simp]

theorem Bool.bne_assoc (x y z : Bool) : ((x != y) != z) = (x != (y != z))

instance Bool.instAssociativeBne : Std.Associative fun (x1 x2 : Bool) => x1 != x2

@[simp]

theorem Bool.bne_right_inj {x y z : Bool} : (x != y) = (x != z) ↔ y = z

@[simp]

theorem Bool.bne_left_inj {x y z : Bool} : (x != z) = (y != z) ↔ x = y

theorem Bool.eq_not_of_ne {x y : Bool} : x ≠ y → x = !y

coercision related normal forms

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

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

theorem Bool.not_eq {a b : Bool} : (!a) = b ↔ a ≠ b

@[simp]

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

@[simp]

theorem Bool.coe_true_iff_false {a b : Bool} : (a = true ↔ b = false) ↔ a = !b

@[simp]

theorem Bool.coe_false_iff_true {a b : Bool} : (a = false ↔ b = true) ↔ (!a) = b

@[simp]

theorem Bool.coe_false_iff_false {a b : Bool} : (a = false ↔ b = false) ↔ (!a) = !b

beq properties

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

xor

theorem Bool.false_xor (x : Bool) : (false ^^ x) = x

theorem Bool.xor_false (x : Bool) : (x ^^ false) = x

theorem Bool.true_xor (x : Bool) : (true ^^ x) = !x

theorem Bool.xor_true (x : Bool) : (x ^^ true) = !x

theorem Bool.not_xor_self (x : Bool) : (!x ^^ x) = true

theorem Bool.xor_not_self (x : Bool) : (x ^^ !x) = true

theorem Bool.not_xor (x y : Bool) : (!x ^^ y) = !(x ^^ y)

theorem Bool.xor_not (x y : Bool) : (x ^^ !y) = !(x ^^ y)

theorem Bool.not_xor_not (x y : Bool) : (!x ^^ !y) = (x ^^ y)

theorem Bool.xor_self (x : Bool) : (x ^^ x) = false

theorem Bool.xor_comm (x y : Bool) : (x ^^ y) = (y ^^ x)

theorem Bool.xor_left_comm (x y z : Bool) : (x ^^ (y ^^ z)) = (y ^^ (x ^^ z))

theorem Bool.xor_right_comm (x y z : Bool) : (x ^^ y ^^ z) = (x ^^ z ^^ y)

theorem Bool.xor_assoc (x y z : Bool) : (x ^^ y ^^ z) = (x ^^ (y ^^ z))

theorem Bool.xor_right_inj {x y z : Bool} : (x ^^ y) = (x ^^ z) ↔ y = z

theorem Bool.xor_left_inj {x y z : Bool} : (x ^^ z) = (y ^^ z) ↔ x = y

le/lt

@[simp]

theorem Bool.le_true (x : Bool) : x ≤ true

@[simp]

theorem Bool.false_le (x : Bool) : false ≤ x

@[simp]

theorem Bool.le_refl (x : Bool) : x ≤ x

@[simp]

theorem Bool.lt_irrefl (x : Bool) : ¬x < x

theorem Bool.le_trans {x y z : Bool} : x ≤ y → y ≤ z → x ≤ z

theorem Bool.le_antisymm {x y : Bool} : x ≤ y → y ≤ x → x = y

theorem Bool.le_total (x y : Bool) : x ≤ y ∨ y ≤ x

theorem Bool.lt_asymm {x y : Bool} : x < y → ¬y < x

theorem Bool.lt_trans {x y z : Bool} : x < y → y < z → x < z

theorem Bool.lt_iff_le_not_le {x y : Bool} : x < y ↔ x ≤ y ∧ ¬y ≤ x

theorem Bool.lt_of_le_of_lt {x y z : Bool} : x ≤ y → y < z → x < z

theorem Bool.lt_of_lt_of_le {x y z : Bool} : x < y → y ≤ z → x < z

theorem Bool.le_of_lt {x y : Bool} : x < y → x ≤ y

theorem Bool.le_of_eq {x y : Bool} : x = y → x ≤ y

theorem Bool.ne_of_lt {x y : Bool} : x < y → x ≠ y

theorem Bool.lt_of_le_of_ne {x y : Bool} : x ≤ y → x ≠ y → x < y

theorem Bool.le_of_lt_or_eq {x y : Bool} : x < y ∨ x = y → x ≤ y

theorem Bool.eq_true_of_true_le {x : Bool} : true ≤ x → x = true

theorem Bool.eq_false_of_le_false {x : Bool} : x ≤ false → x = false

min/max

@[simp]

theorem Bool.max_eq_or : max = or

@[simp]

theorem Bool.min_eq_and : min = and

injectivity lemmas

theorem Bool.not_inj {x y : Bool} : (!x) = !y → x = y

theorem Bool.not_inj_iff {x y : Bool} : (!x) = !y ↔ x = y

theorem Bool.and_or_inj_right {m x y : Bool} : (x && m) = (y && m) → (x || m) = (y || m) → x = y

theorem Bool.and_or_inj_right_iff {m x y : Bool} : (x && m) = (y && m) ∧ (x || m) = (y || m) ↔ x = y

theorem Bool.and_or_inj_left {m x y : Bool} : (m && x) = (m && y) → (m || x) = (m || y) → x = y

theorem Bool.and_or_inj_left_iff {m x y : Bool} : (m && x) = (m && y) ∧ (m || x) = (m || y) ↔ x = y

toNat

def Bool.toNat (b : Bool) : Nat

Converts true to 1 and false to 0.

Equations

• b.toNat = bif b then 1 else 0

@[simp]

theorem Bool.toNat_false : false.toNat = 0

@[simp]

theorem Bool.toNat_true : true.toNat = 1

theorem Bool.toNat_le (c : Bool) : c.toNat ≤ 1

theorem Bool.toNat_lt (b : Bool) : b.toNat < 2

@[simp]

theorem Bool.toNat_eq_zero {b : Bool} : b.toNat = 0 ↔ b = false

@[simp]

theorem Bool.toNat_eq_one {b : Bool} : b.toNat = 1 ↔ b = true

toInt

def Bool.toInt (b : Bool) : Int

Converts true to 1 and false to 0.

Equations

• b.toInt = bif b then 1 else 0

@[simp]

theorem Bool.toInt_false : false.toInt = 0

@[simp]

theorem Bool.toInt_true : true.toInt = 1

ite

@[simp]

theorem Bool.if_true_left (p : Prop) [h : Decidable p] (f : Bool) : (if p then true else f) = (decide p || f)

@[simp]

theorem Bool.if_false_left (p : Prop) [h : Decidable p] (f : Bool) : (if p then false else f) = (!decide p && f)

@[simp]

theorem Bool.if_true_right (p : Prop) [h : Decidable p] (t : Bool) : (if p then t else true) = (!decide p || t)

@[simp]

theorem Bool.if_false_right (p : Prop) [h : Decidable p] (t : Bool) : (if p then t else false) = (decide p && t)

@[simp]

theorem Bool.ite_eq_true_distrib (p : Prop) [h : Decidable p] (t f : Bool) : ((if p then t else f) = true) = if p then t = true else f = true

@[simp]

theorem Bool.ite_eq_false_distrib (p : Prop) [h : Decidable p] (t f : Bool) : ((if p then t else f) = false) = if p then t = false else f = false

@[simp]

theorem Bool.ite_eq_false {b : Bool} {p q : Prop} : (if b = false then p else q) ↔ if b = true then q else p

@[simp]

theorem Bool.ite_eq_true_else_eq_false {b : Bool} {q : Prop} : (if b = true then q else b = false) ↔ b = true → q

@[simp]

theorem Bool.not_ite_eq_true_eq_true {p : Prop} [h : Decidable p] {b c : Bool} : (¬if p then b = true else c = true) ↔ if p then b = false else c = false

@[simp]

theorem Bool.not_ite_eq_false_eq_false {p : Prop} [h : Decidable p] {b c : Bool} : (¬if p then b = false else c = false) ↔ if p then b = true else c = true

@[simp]

theorem Bool.not_ite_eq_true_eq_false {p : Prop} [h : Decidable p] {b c : Bool} : (¬if p then b = true else c = false) ↔ if p then b = false else c = true

@[simp]

theorem Bool.not_ite_eq_false_eq_true {p : Prop} [h : Decidable p] {b c : Bool} : (¬if p then b = false else c = true) ↔ if p then b = true else c = false

theorem Bool.eq_false_imp_eq_true {b : Bool} : b = false → b = true ↔ b = true

theorem Bool.eq_true_imp_eq_false {b : Bool} : b = true → b = false ↔ b = false

forall

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

exists

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

cond

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

theorem Bool.cond_eq_if {b : Bool} {α✝ : Sort u_1} {x y : α✝} : (bif b then x else y) = if b = true then x else y

@[simp]

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

@[simp]

theorem Bool.cond_self {α : Sort u_1} (c : Bool) (t : α) : (bif c then t else t) = t

@[simp]

theorem Bool.cond_prop {b : Bool} {p q : Prop} : (bif b then p else q) ↔ if b = true then p else q

If the return values are propositions, there is no harm in simplifying a bif to an if.

theorem Bool.cond_decide {α : Sort 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_eq_ite_iff {α : Sort u_1} {a : Bool} {p : Prop} [h : Decidable p] {x y u v : α} : ((bif a then x else y) = if p then u else v) ↔ (if a = true then x else y) = if p then u else v

@[simp]

theorem Bool.ite_eq_cond_iff {α : Sort u_1} {p : Prop} {a : Bool} [h : Decidable p] {x y u v : α} : ((if p then x else y) = bif a then u else v) ↔ (if p then x else y) = if a = true then u else v

@[simp]

theorem Bool.cond_eq_true_distrib (c t f : Bool) : ((bif c then t else f) = true) = if c = true then t = true else f = true

@[simp]

theorem Bool.cond_eq_false_distrib (c t f : Bool) : ((bif c then t else f) = false) = if c = true then t = false else f = false

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

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

@[simp]

theorem Bool.cond_true_left (c f : Bool) : (bif c then true else f) = (c || f)

@[simp]

theorem Bool.cond_false_left (c f : Bool) : (bif c then false else f) = (!c && f)

@[simp]

theorem Bool.cond_true_right (c t : Bool) : (bif c then t else true) = (!c || t)

@[simp]

theorem Bool.cond_false_right (c t : Bool) : (bif c then t else false) = (c && t)

@[simp]

theorem Bool.cond_then_not_self (c b : Bool) : (bif c then !c else b) = (!c && b)

@[simp]

theorem Bool.cond_else_not_self (c b : Bool) : (bif c then b else !c) = (!c || b)

@[simp]

theorem Bool.cond_then_self (c b : Bool) : (bif c then c else b) = (c || b)

@[simp]

theorem Bool.cond_else_self (c b : Bool) : (bif c then b else c) = (c && b)

@[reducible, inline, deprecated Bool.cond_then_not_self (since := "2025-04-04")]

abbrev Bool.cond_true_not_same (c b : Bool) : (bif c then !c else b) = (!c && b)

Equations

• Bool.cond_true_not_same = Bool.cond_then_not_self

@[reducible, inline, deprecated Bool.cond_else_not_self (since := "2025-04-04")]

abbrev Bool.cond_false_not_same (c b : Bool) : (bif c then b else !c) = (!c || b)

Equations

• Bool.cond_false_not_same = Bool.cond_else_not_self

@[reducible, inline, deprecated Bool.cond_then_self (since := "2025-04-04")]

abbrev Bool.cond_true_same (c b : Bool) : (bif c then c else b) = (c || b)

Equations

• Bool.cond_true_same = Bool.cond_then_self

@[reducible, inline, deprecated Bool.cond_else_self (since := "2025-04-04")]

abbrev Bool.cond_false_same (c b : Bool) : (bif c then b else c) = (c && b)

Equations

• Bool.cond_false_same = Bool.cond_else_self

theorem Bool.cond_pos {α : Sort u_1} {b : Bool} {a a' : α} (h : b = true) : (bif b then a else a') = a

theorem Bool.cond_neg {α : Sort u_1} {b : Bool} {a a' : α} (h : b = false) : (bif b then a else a') = a'

theorem Bool.apply_cond {α : Sort u_1} {β : Sort u_2} (f : α → β) {b : Bool} {a a' : α} : f (bif b then a else a') = bif b then f a else f a'

decidability

theorem Bool.decide_coe (b : Bool) [Decidable (b = true)] : decide (b = true) = b

@[simp]

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

@[simp]

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

@[simp]

theorem Bool.decide_iff_dist (p q : Prop) [dpq : Decidable (p ↔ q)] [dp : Decidable p] [dq : Decidable q] : decide (p ↔ q) = (decide p == decide q)

theorem Bool.and_eq_decide (p q : Bool) : (p && q) = decide (p = true ∧ q = true)

theorem Bool.or_eq_decide (p q : Bool) : (p || q) = decide (p = true ∨ q = true)

theorem Bool.decide_beq_decide (p q : Prop) [dpq : Decidable (p ↔ q)] [dp : Decidable p] [dq : Decidable q] : (decide p == decide q) = decide (p ↔ q)

decide

@[simp]

theorem false_eq_decide_iff {p : Prop} [h : Decidable p] : false = decide p ↔ ¬p

@[simp]

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

coercions

def boolPredToPred {α : Sort u_1} : Coe (α → Bool) (α → Prop)

This should not be turned on globally as an instance because it degrades performance in Mathlib, but may be used locally.

Equations

• boolPredToPred = { coe := fun (r : α → Bool) (a : α) => r a = true }

def boolRelToRel {α : Sort u_1} : Coe (α → α → Bool) (α → α → Prop)

This should not be turned on globally as an instance because it degrades performance in Mathlib, but may be used locally.

Equations

• boolRelToRel = { coe := fun (r : α → α → Bool) (a b : α) => r a b = true }

subtypes

@[simp]

theorem Subtype.beq_iff {α : Type u} [BEq α] {p : α → Prop} {x y : { a : α // p a }} : (x == y) = (x.val == y.val)