@[reducible, inline]

abbrev xor : Bool → Bool → Bool

Boolean exclusive or

Equations

• xor = bne

@[reducible, inline]

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

@[reducible, inline]

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

@[reducible, inline]

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

@[reducible, inline]

abbrev Bool.xor : Bool → Bool → Bool

Boolean exclusive or

Equations

• Bool.xor = xor

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 (x x_1 : Bool) => x = true → x_1 = true }

instance Bool.instLT : LT Bool

Equations

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

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

Equations

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

instance Bool.instDecidableLt (x : Bool) (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 : Bool} {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

@[simp]

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

@[simp]

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

and

@[simp]

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

@[simp]

theorem Bool.and_self_right (a : Bool) (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 : Bool) (y : Bool) : (x && y) = (y && x)

instance Bool.instCommutativeAnd : Std.Commutative fun (x x_1 : Bool) => x && x_1

Equations

• Bool.instCommutativeAnd = ⋯

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)

@[simp]

theorem Bool.and_iff_left_iff_imp (a : Bool) (b : Bool) : (a && b) = a ↔ a = true → b = true

@[simp]

theorem Bool.and_iff_right_iff_imp (a : Bool) (b : Bool) : (a && b) = b ↔ b = true → a = true

@[simp]

theorem Bool.iff_self_and (a : Bool) (b : Bool) : a = (a && b) ↔ a = true → b = true

@[simp]

theorem Bool.iff_and_self (a : Bool) (b : Bool) : b = (a && b) ↔ b = true → a = true

or

@[simp]

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

@[simp]

theorem Bool.or_self_right (a : Bool) (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_iff_left_iff_imp (a : Bool) (b : Bool) : (a || b) = a ↔ b = true → a = true

@[simp]

theorem Bool.or_iff_right_iff_imp (a : Bool) (b : Bool) : (a || b) = b ↔ a = true → b = true

@[simp]

theorem Bool.iff_self_or (a : Bool) (b : Bool) : a = (a || b) ↔ b = true → a = true

@[simp]

theorem Bool.iff_or_self (a : Bool) (b : Bool) : b = (a || b) ↔ a = true → b = true

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

instance Bool.instCommutativeOr : Std.Commutative fun (x x_1 : Bool) => x || x_1

Equations

• Bool.instCommutativeOr = ⋯

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)

distributivity

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

@[simp]

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

De Morgan's law for boolean and

@[simp]

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

De Morgan's law for boolean or

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

@[simp]

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

@[simp]

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

@[simp]

theorem Bool.or_eq_false_iff (x : Bool) (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

@[simp]

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

instance Bool.instLawfulIdentityBeqTrue : Std.LawfulIdentity (fun (x x_1 : Bool) => x == x_1) true

Equations

• Bool.instLawfulIdentityBeqTrue = ⋯

@[simp]

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

@[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 (x x_1 : Bool) => x != x_1) false

Equations

• Bool.instLawfulIdentityBneFalse = ⋯

@[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_self (x : Bool) : ((!x) != x) = true

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

instance Bool.instAssociativeBne : Std.Associative fun (x x_1 : Bool) => x != x_1

Equations

• Bool.instAssociativeBne = ⋯

@[simp]

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

@[simp]

theorem Bool.bne_right_inj (x : Bool) (y : Bool) (z : Bool) : (x != z) = (y != z) ↔ 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)

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

theorem Bool.coe_false_iff_false (a : Bool) (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) : xor false x = x

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

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

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

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

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

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)

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

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

• 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

@[reducible, inline, deprecated Bool.toNat_le]

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

Equations

• Bool.toNat_le_one = Bool.toNat_le

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

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 : Bool) (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 : Bool) (f : Bool) : ((if p then t else f) = false) = if p then t = false else f = false

@[simp]

theorem Bool.not_ite_eq_true_eq_true (p : Prop) [h : Decidable p] (b : Bool) (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 : Bool) (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 : Bool) (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 : Bool) (c : Bool) : (¬if p then b = false else c = true) ↔ if p then b = true else c = false

@[simp]

theorem Bool.eq_false_imp_eq_true (b : Bool) : b = false → b = true ↔ b = true

@[simp]

theorem Bool.eq_true_imp_eq_false (b : Bool) : b = true → b = false ↔ b = false

cond

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

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

@[simp]

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

@[simp]

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

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_eq_ite_iff {α : Type 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 {α : Type u_1} (p : Prop) [h : Decidable p] (a : Bool) (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 : Bool) (t : Bool) (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 : Bool) (t : Bool) (f : Bool) : ((bif c then t else f) = false) = if c = true then t = false else f = false

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

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

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

@[simp]

theorem Bool.decide_and (p : Prop) (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 : Prop) (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 : Prop) (q : Prop) [dpq : Decidable (p ↔ q)] [dp : Decidable p] [dq : Decidable q] : decide (p ↔ q) = (decide p == decide 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