@[inline, reducible]

abbrev xor : Bool → Bool → Bool

Boolean exclusive or

Equations

• xor = bne

@[inline, reducible]

abbrev Bool.not : Bool → Bool

not x, or !x, is the boolean "not" operation (not to be confused with Not : Prop → Prop, which is the propositional connective).

Equations

• Bool.not = not

@[inline, reducible]

abbrev Bool.or (x : Bool) (y : Bool) : Bool

or x y, or x || y, is the boolean "or" operation (not to be confused with Or : Prop → Prop → Prop, which is the propositional connective). It is @[macro_inline] because it has C-like short-circuiting behavior: if x is true then y is not evaluated.

Equations

• Bool.or = or

@[inline, reducible]

abbrev Bool.and (x : Bool) (y : Bool) : Bool

and x y, or x && y, is the boolean "and" operation (not to be confused with And : Prop → Prop → Prop, which is the propositional connective). It is @[macro_inline] because it has C-like short-circuiting behavior: if x is false then y is not evaluated.

Equations

• Bool.and = and

@[inline, reducible]

abbrev Bool.xor : Bool → Bool → Bool

Boolean exclusive or

Equations

• Bool.xor = xor

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

Equations

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

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

Equations

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

instance Bool.instLEBool : LE Bool

Equations

• Bool.instLEBool = { le := fun (x x_1 : Bool) => x = true → x_1 = true }

instance Bool.instLTBool : LT Bool

Equations

• Bool.instLTBool = { lt := fun (x x_1 : Bool) => (!x && x_1) = true }

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

Equations

• Bool.instDecidableLeBoolInstLEBool x y = inferInstanceAs (Decidable (x = true → y = true))

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

Equations

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

instance Bool.instMaxBool : Max Bool

Equations

• Bool.instMaxBool = { max := or }

instance Bool.instMinBool : Min Bool

Equations

• Bool.instMinBool = { 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 : Bool} {b : Bool} : a = b ↔ (a = true ↔ b = true)

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

and

@[simp]

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

@[simp]

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

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

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

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

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

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

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

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

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

De Morgan's law for boolean and

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

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

or

@[simp]

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

@[simp]

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

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

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

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

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

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

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

De Morgan's law for boolean or

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

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

xor

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

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

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

@[simp]

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

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

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

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

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

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

@[simp]

theorem Bool.xor_left_inj (x : Bool) (y : Bool) (z : Bool) : xor x y = xor x z ↔ y = z

@[simp]

theorem Bool.xor_right_inj (x : Bool) (y : Bool) (z : Bool) : xor x z = xor 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 : Bool} {y : Bool} {z : Bool} : x ≤ y → y ≤ z → x ≤ z

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

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

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

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

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

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

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

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

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

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

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

theorem Bool.le_of_lt_or_eq {x : Bool} {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 : Bool} {y : Bool} : (!x) = !y → x = y

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

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

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

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

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

toNat

def Bool.toNat (b : Bool) : Nat

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

Equations

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

@[simp]

theorem Bool.toNat_false : Bool.toNat false = 0

@[simp]

theorem Bool.toNat_true : Bool.toNat true = 1

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

@[inline, reducible, deprecated Bool.toNat_le]

abbrev Bool.toNat_le_one (c : Bool) : Bool.toNat c ≤ 1

Equations

• Bool.toNat_le_one = Bool.toNat_le

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

@[simp]

theorem Bool.toNat_eq_zero (b : Bool) : Bool.toNat b = 0 ↔ b = false

@[simp]

theorem Bool.toNat_eq_one (b : Bool) : Bool.toNat b = 1 ↔ b = true

cond

theorem cond_eq_if {b : Bool} : ∀ {α : Type u_1} {x y : α}, (bif b then x else y) = if b = true then x else y

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