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

Instances For

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

Instances For

source
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 ⋯

source
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 ⋯

source
@[simp]
theorem Bool.default_bool :
default = false
source
instance Bool.instLE :
LE Bool
Equations

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

source
instance Bool.instLT :
LT Bool
Equations

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

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

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

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

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

source
instance Bool.instMax :
Max Bool
Equations

- Bool.instMax = { max := or }

source
instance Bool.instMin :
Min Bool
Equations

- Bool.instMin = { min := and }

source
theorem Bool.false_ne_true :
false ≠ true
source
theorem Bool.eq_false_or_eq_true (b : Bool) :
b = true ∨ b = false
source
theorem Bool.eq_false_iff {b : Bool} :
b = false ↔ b ≠ true
source
theorem Bool.ne_false_iff {b : Bool} :
b ≠ false ↔ b = true
source
theorem Bool.eq_iff_iff {a b : Bool} :
a = b ↔ (a = true ↔ b = true)
source
@[simp]
theorem Bool.decide_eq_true {b : Bool} [Decidable (b = true)] :
decide (b = true) = b
source
@[simp]
theorem Bool.decide_eq_false {b : Bool} [Decidable (b = false)] :
decide (b = false) = !b
source
theorem Bool.decide_true_eq {b : Bool} [Decidable (true = b)] :
decide (true = b) = b
source
theorem Bool.decide_false_eq {b : Bool} [Decidable (false = b)] :
decide (false = b) = !b
source
@[simp]
theorem Bool.eq_false_imp_eq_true_iff (a b : Bool) :
(a = false → b = true ↔ b = false → a = true) = True
source
@[simp]
theorem Bool.eq_true_imp_eq_false_iff (a b : Bool) :
(a = true → b = false ↔ b = true → a = false) = True

### and #

source
@[simp]
theorem Bool.and_self_left (a b : Bool) :
(a && (a && b)) = (a && b)
source
@[simp]
theorem Bool.and_self_right (a b : Bool) :
(a && b && b) = (a && b)
source
@[simp]
theorem Bool.not_and_self (x : Bool) :
(!x && x) = false
source
@[simp]
theorem Bool.and_not_self (x : Bool) :
(x && !x) = false
source
@[simp]
theorem Bool.eq_true_and_eq_false_self (b : Bool) :
b = true ∧ b = false ↔ False
source
@[simp]
theorem Bool.eq_false_and_eq_true_self (b : Bool) :
b = false ∧ b = true ↔ False
source
theorem Bool.and_comm (x y : Bool) :
(x && y) = (y && x)
source
instance Bool.instCommutativeAnd :
Std.Commutative fun (x1 x2 : Bool) => x1 && x2
source
theorem Bool.and_left_comm (x y z : Bool) :
(x && (y && z)) = (y && (x && z))
source
theorem Bool.and_right_comm (x y z : Bool) :
(x && y && z) = (x && z && y)
source
@[simp]
theorem Bool.and_eq_left_iff_imp {a b : Bool} :
(a && b) = a ↔ a = true → b = true
source
@[simp]
theorem Bool.and_eq_right_iff_imp {a b : Bool} :
(a && b) = b ↔ b = true → a = true
source
@[simp]
theorem Bool.eq_self_and {a b : Bool} :
a = (a && b) ↔ a = true → b = true
source
@[simp]
theorem Bool.eq_and_self {a b : Bool} :
b = (a && b) ↔ b = true → a = true
source
@[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

Instances For

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

Instances For

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

Instances For

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

Instances For

source
@[simp]
theorem Bool.not_and_eq_left_iff_and {a b : Bool} :
(!a && b) = a ↔ (!a) = true ∧ (!b) = true
source
@[simp]
theorem Bool.and_not_eq_right_iff_and {a b : Bool} :
(a && !b) = b ↔ (!a) = true ∧ (!b) = true
source
@[simp]
theorem Bool.eq_not_self_and {a b : Bool} :
a = (!a && b) ↔ (!a) = true ∧ (!b) = true
source
@[simp]
theorem Bool.eq_and_not_self {a b : Bool} :
b = (a && !b) ↔ (!a) = true ∧ (!b) = true
source
@[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

Instances For

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

Instances For

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

Instances For

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

Instances For

### or #

source
@[simp]
theorem Bool.or_self_left (a b : Bool) :
(a || (a || b)) = (a || b)
source
@[simp]
theorem Bool.or_self_right (a b : Bool) :
(a || b || b) = (a || b)
source
@[simp]
theorem Bool.not_or_self (x : Bool) :
(!x || x) = true
source
@[simp]
theorem Bool.or_not_self (x : Bool) :
(x || !x) = true
source
@[simp]
theorem Bool.eq_true_or_eq_false_self (b : Bool) :
b = true ∨ b = false ↔ True
source
@[simp]
theorem Bool.eq_false_or_eq_true_self (b : Bool) :
b = false ∨ b = true ↔ True
source
@[simp]
theorem Bool.or_eq_left_iff_imp {a b : Bool} :
(a || b) = a ↔ b = true → a = true
source
@[simp]
theorem Bool.or_eq_right_iff_imp {a b : Bool} :
(a || b) = b ↔ a = true → b = true
source
@[simp]
theorem Bool.eq_self_or {a b : Bool} :
a = (a || b) ↔ b = true → a = true
source
@[simp]
theorem Bool.eq_or_self {a b : Bool} :
b = (a || b) ↔ a = true → b = true
source
@[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

Instances For

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

Instances For

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

Instances For

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

Instances For

source
@[simp]
theorem Bool.not_or_eq_left_iff_and {a b : Bool} :
(!a || b) = a ↔ a = true ∧ b = true
source
@[simp]
theorem Bool.or_not_eq_right_iff_and {a b : Bool} :
(a || !b) = b ↔ a = true ∧ b = true
source
@[simp]
theorem Bool.eq_not_self_or {a b : Bool} :
a = (!a || b) ↔ a = true ∧ b = true
source
@[simp]
theorem Bool.eq_or_not_self {a b : Bool} :
b = (a || !b) ↔ a = true ∧ b = true
source
@[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

Instances For

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

Instances For

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

Instances For

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

Instances For

source
theorem Bool.or_comm (x y : Bool) :
(x || y) = (y || x)
source
instance Bool.instCommutativeOr :
Std.Commutative fun (x1 x2 : Bool) => x1 || x2
source
theorem Bool.or_left_comm (x y z : Bool) :
(x || (y || z)) = (y || (x || z))
source
theorem Bool.or_right_comm (x y z : Bool) :
(x || y || z) = (x || z || y)

### distributivity #

source
theorem Bool.and_or_distrib_left (x y z : Bool) :
(x && (y || z)) = (x && y || x && z)
source
theorem Bool.and_or_distrib_right (x y z : Bool) :
((x || y) && z) = (x && z || y && z)
source
theorem Bool.or_and_distrib_left (x y z : Bool) :
(x || y && z) = ((x || y) && (x || z))
source
theorem Bool.or_and_distrib_right (x y z : Bool) :
(x && y || z) = ((x || z) && (y || z))
source
theorem Bool.and_xor_distrib_left (x y z : Bool) :
(x && (y ^^ z)) = (x && y ^^ x && z)
source
theorem Bool.and_xor_distrib_right (x y z : Bool) :
((x ^^ y) && z) = (x && z ^^ y && z)
source
@[simp]
theorem Bool.not_and (x y : Bool) :
(!(x && y)) = (!x || !y)

De Morgan's law for boolean and

source
@[simp]
theorem Bool.not_or (x y : Bool) :
(!(x || y)) = (!x && !y)

De Morgan's law for boolean or

source
theorem Bool.and_eq_true_iff {x y : Bool} :
(x && y) = true ↔ x = true ∧ y = true
source
theorem Bool.and_eq_false_iff {x y : Bool} :
(x && y) = false ↔ x = false ∨ y = false
source
@[simp]
theorem Bool.and_eq_false_imp {x y : Bool} :
(x && y) = false ↔ x = true → y = false
source
theorem Bool.or_eq_true_iff {x y : Bool} :
(x || y) = true ↔ x = true ∨ y = true
source
@[simp]
theorem Bool.or_eq_false_iff {x y : Bool} :
(x || y) = false ↔ x = false ∧ y = false

### eq/beq/bne #

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

source
@[simp]
theorem Bool.true_eq_false :
(true = false) = False
source
@[simp]
theorem Bool.false_eq (b : Bool) :
(false = b) = (b = false)
source
@[simp]
theorem Bool.true_eq (b : Bool) :
(true = b) = (b = true)
source
@[simp]
theorem Bool.true_beq (b : Bool) :
(true == b) = b
source
@[simp]
theorem Bool.false_beq (b : Bool) :
(false == b) = !b
source
instance Bool.instLawfulIdentityBeqTrue :
Std.LawfulIdentity (fun (x1 x2 : Bool) => x1 == x2) true
source
@[simp]
theorem Bool.true_bne (b : Bool) :
(true != b) = !b
source
@[simp]
theorem Bool.false_bne (b : Bool) :
(false != b) = b
source
@[simp]
theorem Bool.bne_true (b : Bool) :
(b != true) = !b
source
@[simp]
theorem Bool.bne_false (b : Bool) :
(b != false) = b
source
instance Bool.instLawfulIdentityBneFalse :
Std.LawfulIdentity (fun (x1 x2 : Bool) => x1 != x2) false
source
@[simp]
theorem Bool.not_beq_self (x : Bool) :
((!x) == x) = false
source
@[simp]
theorem Bool.beq_not_self (x : Bool) :
(x == !x) = false
source
@[simp]
theorem Bool.not_bne (a b : Bool) :
((!a) != b) = !a != b
source
@[simp]
theorem Bool.bne_not (a b : Bool) :
(a != !b) = !a != b
source
theorem Bool.not_bne_self (x : Bool) :
((!x) != x) = true
source
theorem Bool.bne_not_self (x : Bool) :
(x != !x) = true
source
theorem Bool.not_eq_self (b : Bool) :
(!b) = b ↔ False
source
@[simp]
theorem Bool.eq_not_self (b : Bool) :
b = !b ↔ False
source
@[simp]
theorem Bool.beq_self_left (a b : Bool) :
(a == (a == b)) = b
source
@[simp]
theorem Bool.beq_self_right (a b : Bool) :
((a == b) == b) = a
source
@[simp]
theorem Bool.bne_self_left (a b : Bool) :
(a != (a != b)) = b
source
@[simp]
theorem Bool.bne_self_right (a b : Bool) :
((a != b) != b) = a
source
theorem Bool.not_bne_not (x y : Bool) :
((!x) != !y) = (x != y)
source
@[simp]
theorem Bool.bne_assoc (x y z : Bool) :
((x != y) != z) = (x != (y != z))
source
instance Bool.instAssociativeBne :
Std.Associative fun (x1 x2 : Bool) => x1 != x2
source
@[simp]
theorem Bool.bne_right_inj {x y z : Bool} :
(x != y) = (x != z) ↔ y = z
source
@[simp]
theorem Bool.bne_left_inj {x y z : Bool} :
(x != z) = (y != z) ↔ x = y
source
theorem Bool.eq_not_of_ne {x y : Bool} :
x ≠ y → x = !y

### coercision related normal forms #

source
theorem Bool.beq_eq_decide_eq {α : Type u_1} [BEq α] [LawfulBEq α] [DecidableEq α] (a b : α) :
(a == b) = decide (a = b)
source
theorem Bool.eq_not {a b : Bool} :
a = !b ↔ a ≠ b
source
theorem Bool.not_eq {a b : Bool} :
(!a) = b ↔ a ≠ b
source
@[simp]
theorem Bool.coe_iff_coe {a b : Bool} :
(a = true ↔ b = true) ↔ a = b
source
@[simp]
theorem Bool.coe_true_iff_false {a b : Bool} :
(a = true ↔ b = false) ↔ a = !b
source
@[simp]
theorem Bool.coe_false_iff_true {a b : Bool} :
(a = false ↔ b = true) ↔ (!a) = b
source
@[simp]
theorem Bool.coe_false_iff_false {a b : Bool} :
(a = false ↔ b = false) ↔ (!a) = !b

### beq properties #

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

### xor #

source
theorem Bool.false_xor (x : Bool) :
(false ^^ x) = x
source
theorem Bool.xor_false (x : Bool) :
(x ^^ false) = x
source
theorem Bool.true_xor (x : Bool) :
(true ^^ x) = !x
source
theorem Bool.xor_true (x : Bool) :
(x ^^ true) = !x
source
theorem Bool.not_xor_self (x : Bool) :
(!x ^^ x) = true
source
theorem Bool.xor_not_self (x : Bool) :
(x ^^ !x) = true
source
theorem Bool.not_xor (x y : Bool) :
(!x ^^ y) = !(x ^^ y)
source
theorem Bool.xor_not (x y : Bool) :
(x ^^ !y) = !(x ^^ y)
source
theorem Bool.not_xor_not (x y : Bool) :
(!x ^^ !y) = (x ^^ y)
source
theorem Bool.xor_self (x : Bool) :
(x ^^ x) = false
source
theorem Bool.xor_comm (x y : Bool) :
(x ^^ y) = (y ^^ x)
source
theorem Bool.xor_left_comm (x y z : Bool) :
(x ^^ (y ^^ z)) = (y ^^ (x ^^ z))
source
theorem Bool.xor_right_comm (x y z : Bool) :
(x ^^ y ^^ z) = (x ^^ z ^^ y)
source
theorem Bool.xor_assoc (x y z : Bool) :
(x ^^ y ^^ z) = (x ^^ (y ^^ z))
source
theorem Bool.xor_right_inj {x y z : Bool} :
(x ^^ y) = (x ^^ z) ↔ y = z
source
theorem Bool.xor_left_inj {x y z : Bool} :
(x ^^ z) = (y ^^ z) ↔ x = y

### le/lt #

source
@[simp]
theorem Bool.le_true (x : Bool) :
x ≤ true
source
@[simp]
theorem Bool.false_le (x : Bool) :
false ≤ x
source
@[simp]
theorem Bool.le_refl (x : Bool) :
x ≤ x
source
@[simp]
theorem Bool.lt_irrefl (x : Bool) :
¬x < x
source
theorem Bool.le_trans {x y z : Bool} :
x ≤ y → y ≤ z → x ≤ z
source
theorem Bool.le_antisymm {x y : Bool} :
x ≤ y → y ≤ x → x = y
source
theorem Bool.le_total (x y : Bool) :
x ≤ y ∨ y ≤ x
source
theorem Bool.lt_asymm {x y : Bool} :
x < y → ¬y < x
source
theorem Bool.lt_trans {x y z : Bool} :
x < y → y < z → x < z
source
theorem Bool.lt_iff_le_not_le {x y : Bool} :
x < y ↔ x ≤ y ∧ ¬y ≤ x
source
theorem Bool.lt_of_le_of_lt {x y z : Bool} :
x ≤ y → y < z → x < z
source
theorem Bool.lt_of_lt_of_le {x y z : Bool} :
x < y → y ≤ z → x < z
source
theorem Bool.le_of_lt {x y : Bool} :
x < y → x ≤ y
source
theorem Bool.le_of_eq {x y : Bool} :
x = y → x ≤ y
source
theorem Bool.ne_of_lt {x y : Bool} :
x < y → x ≠ y
source
theorem Bool.lt_of_le_of_ne {x y : Bool} :
x ≤ y → x ≠ y → x < y
source
theorem Bool.le_of_lt_or_eq {x y : Bool} :
x < y ∨ x = y → x ≤ y
source
theorem Bool.eq_true_of_true_le {x : Bool} :
true ≤ x → x = true
source
theorem Bool.eq_false_of_le_false {x : Bool} :
x ≤ false → x = false

### min/max #

source
@[simp]
theorem Bool.max_eq_or :
max = or
source
@[simp]
theorem Bool.min_eq_and :
min = and

### injectivity lemmas #

source
theorem Bool.not_inj {x y : Bool} :
(!x) = !y → x = y
source
theorem Bool.not_inj_iff {x y : Bool} :
(!x) = !y ↔ x = y
source
theorem Bool.and_or_inj_right {m x y : Bool} :
(x && m) = (y && m) → (x || m) = (y || m) → x = y
source
theorem Bool.and_or_inj_right_iff {m x y : Bool} :
(x && m) = (y && m) ∧ (x || m) = (y || m) ↔ x = y
source
theorem Bool.and_or_inj_left {m x y : Bool} :
(m && x) = (m && y) → (m || x) = (m || y) → x = y
source
theorem Bool.and_or_inj_left_iff {m x y : Bool} :
(m && x) = (m && y) ∧ (m || x) = (m || y) ↔ x = y

## toNat #

source
def Bool.toNat (b : Bool) :
Nat

Converts `true` to `1` and `false` to `0`.

Equations

- b.toNat = bif b then 1 else 0

Instances For

source
@[simp]
theorem Bool.toNat_false :
false.toNat = 0
source
@[simp]
theorem Bool.toNat_true :
true.toNat = 1
source
theorem Bool.toNat_le (c : Bool) :
c.toNat ≤ 1
source
theorem Bool.toNat_lt (b : Bool) :
b.toNat < 2
source
@[simp]
theorem Bool.toNat_eq_zero {b : Bool} :
b.toNat = 0 ↔ b = false
source
@[simp]
theorem Bool.toNat_eq_one {b : Bool} :
b.toNat = 1 ↔ b = true

## toInt #

source
def Bool.toInt (b : Bool) :
Int

Converts `true` to `1` and `false` to `0`.

Equations

- b.toInt = bif b then 1 else 0

Instances For

source
@[simp]
theorem Bool.toInt_false :
false.toInt = 0
source
@[simp]
theorem Bool.toInt_true :
true.toInt = 1

### ite #

source
@[simp]
theorem Bool.if_true_left (p : Prop) [h : Decidable p] (f : Bool) :
(if p then true else f) = (decide p || f)
source
@[simp]
theorem Bool.if_false_left (p : Prop) [h : Decidable p] (f : Bool) :
(if p then false else f) = (!decide p && f)
source
@[simp]
theorem Bool.if_true_right (p : Prop) [h : Decidable p] (t : Bool) :
(if p then t else true) = (!decide p || t)
source
@[simp]
theorem Bool.if_false_right (p : Prop) [h : Decidable p] (t : Bool) :
(if p then t else false) = (decide p && t)
source
@[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
source
@[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
source
@[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
source
@[simp]
theorem Bool.ite_eq_true_else_eq_false {b : Bool} {q : Prop} :
(if b = true then q else b = false) ↔ b = true → q
source
@[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
source
@[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
source
@[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
source
@[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
source
theorem Bool.eq_false_imp_eq_true {b : Bool} :
b = false → b = true ↔ b = true
source
theorem Bool.eq_true_imp_eq_false {b : Bool} :
b = true → b = false ↔ b = false

### forall #

source
theorem Bool.forall_bool' {p : Bool → Prop} (b : Bool) :
(∀ (x : Bool), p x) ↔ p b ∧ p !b
source
@[simp]
theorem Bool.forall_bool {p : Bool → Prop} :
(∀ (b : Bool), p b) ↔ p false ∧ p true

### exists #

source
theorem Bool.exists_bool' {p : Bool → Prop} (b : Bool) :
(∃ (x : Bool), p x) ↔ p b ∨ p !b
source
@[simp]
theorem Bool.exists_bool {p : Bool → Prop} :
(∃ (b : Bool), p b) ↔ p false ∨ p true

### cond #

source
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
source
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
source
@[simp]
theorem Bool.cond_not {α : Sort u_1} (b : Bool) (t e : α) :
(bif !b then t else e) = bif b then e else t
source
@[simp]
theorem Bool.cond_self {α : Sort u_1} (c : Bool) (t : α) :
(bif c then t else t) = t
source
@[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`.

source
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
source
@[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
source
@[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
source
@[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
source
@[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
source
theorem Bool.cond_true {α : Sort u} {a b : α} :
(bif true then a else b) = a
source
theorem Bool.cond_false {α : Sort u} {a b : α} :
(bif false then a else b) = b
source
@[simp]
theorem Bool.cond_true_left (c f : Bool) :
(bif c then true else f) = (c || f)
source
@[simp]
theorem Bool.cond_false_left (c f : Bool) :
(bif c then false else f) = (!c && f)
source
@[simp]
theorem Bool.cond_true_right (c t : Bool) :
(bif c then t else true) = (!c || t)
source
@[simp]
theorem Bool.cond_false_right (c t : Bool) :
(bif c then t else false) = (c && t)
source
@[simp]
theorem Bool.cond_then_not_self (c b : Bool) :
(bif c then !c else b) = (!c && b)
source
@[simp]
theorem Bool.cond_else_not_self (c b : Bool) :
(bif c then b else !c) = (!c || b)
source
@[simp]
theorem Bool.cond_then_self (c b : Bool) :
(bif c then c else b) = (c || b)
source
@[simp]
theorem Bool.cond_else_self (c b : Bool) :
(bif c then b else c) = (c && b)
source
@[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

Instances For

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

Instances For

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

Instances For

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

Instances For

source
theorem Bool.cond_pos {α : Sort u_1} {b : Bool} {a a' : α} (h : b = true) :
(bif b then a else a') = a
source
theorem Bool.cond_neg {α : Sort u_1} {b : Bool} {a a' : α} (h : b = false) :
(bif b then a else a') = a'
source
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 #

source
theorem Bool.decide_coe (b : Bool) [Decidable (b = true)] :
decide (b = true) = b
source
@[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)
source
@[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)
source
@[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)
source
theorem Bool.and_eq_decide (p q : Bool) :
(p && q) = decide (p = true ∧ q = true)
source
theorem Bool.or_eq_decide (p q : Bool) :
(p || q) = decide (p = true ∨ q = true)
source
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 #

source
@[simp]
theorem false_eq_decide_iff {p : Prop} [h : Decidable p] :
false = decide p ↔ ¬p
source
@[simp]
theorem true_eq_decide_iff {p : Prop} [h : Decidable p] :
true = decide p ↔ p

### coercions #

source
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 }

Instances For

source
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 }

Instances For

### subtypes #

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

### Proof by reflection support #

source
noncomputable def Bool.and' (a b : Bool) :
Bool
Equations

- a.and' b = Bool.rec false b a

Instances For

source
noncomputable def Bool.or' (a b : Bool) :
Bool
Equations

- a.or' b = Bool.rec b true a

Instances For

source
noncomputable def Bool.not' (a : Bool) :
Bool
Equations

- a.not' = Bool.rec true false a

Instances For

source
@[simp]
theorem Bool.and'_eq_and (a b : Bool) :
a.and' b = (a && b)
source
@[simp]
theorem Bool.or'_eq_or (a b : Bool) :
a.or' b = (a || b)
source
@[simp]
theorem Bool.not'_eq_not (a : Bool) :
a.not' = !a