Documentation

Init.Data.Bool

@[reducible, inline]
abbrev Bool.xor :
BoolBoolBool

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
    Instances For

      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
        Instances For
          instance Bool.instDecidableForallOfDecidablePred (p : BoolProp) [inst : DecidablePred p] :
          Decidable (∀ (x : Bool), p x)
          Equations
            instance Bool.instLE :
            Equations
              instance Bool.instLT :
              Equations
                instance Bool.instDecidableLe (x y : Bool) :
                Equations
                  instance Bool.instDecidableLt (x y : Bool) :
                  Decidable (x < y)
                  Equations
                    Equations
                      Equations
                        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]
                        @[simp]
                        theorem Bool.eq_false_imp_eq_true_iff (a b : Bool) :
                        (a = falseb = true b = falsea = true) = True
                        @[simp]
                        theorem Bool.eq_true_imp_eq_false_iff (a b : Bool) :
                        (a = trueb = false b = truea = 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
                        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 = trueb = true
                        @[simp]
                        theorem Bool.and_eq_right_iff_imp {a b : Bool} :
                        (a && b) = b b = truea = true
                        @[simp]
                        theorem Bool.eq_self_and {a b : Bool} :
                        a = (a && b) a = trueb = true
                        @[simp]
                        theorem Bool.eq_and_self {a b : Bool} :
                        b = (a && b) b = truea = 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 = trueb = true
                        Equations
                          Instances For
                            @[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 = truea = true
                            Equations
                              Instances For
                                @[reducible, inline, deprecated Bool.eq_self_and (since := "2025-04-04")]
                                abbrev Bool.iff_self_and {a b : Bool} :
                                a = (a && b) a = trueb = true
                                Equations
                                  Instances For
                                    @[reducible, inline, deprecated Bool.eq_and_self (since := "2025-04-04")]
                                    abbrev Bool.iff_and_self {a b : Bool} :
                                    b = (a && b) b = truea = true
                                    Equations
                                      Instances For
                                        @[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
                                          Instances For
                                            @[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
                                              Instances For
                                                @[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
                                                  Instances For
                                                    @[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
                                                      Instances For

                                                        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.or_eq_left_iff_imp {a b : Bool} :
                                                        (a || b) = a b = truea = true
                                                        @[simp]
                                                        theorem Bool.or_eq_right_iff_imp {a b : Bool} :
                                                        (a || b) = b a = trueb = true
                                                        @[simp]
                                                        theorem Bool.eq_self_or {a b : Bool} :
                                                        a = (a || b) b = truea = true
                                                        @[simp]
                                                        theorem Bool.eq_or_self {a b : Bool} :
                                                        b = (a || b) a = trueb = 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 = truea = true
                                                        Equations
                                                          Instances For
                                                            @[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 = trueb = true
                                                            Equations
                                                              Instances For
                                                                @[reducible, inline, deprecated Bool.eq_self_or (since := "2025-04-04")]
                                                                abbrev Bool.iff_self_or {a b : Bool} :
                                                                a = (a || b) b = truea = true
                                                                Equations
                                                                  Instances For
                                                                    @[reducible, inline, deprecated Bool.eq_or_self (since := "2025-04-04")]
                                                                    abbrev Bool.iff_or_self {a b : Bool} :
                                                                    b = (a || b) a = trueb = true
                                                                    Equations
                                                                      Instances For
                                                                        @[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
                                                                          Instances For
                                                                            @[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
                                                                              Instances For
                                                                                @[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
                                                                                  Instances For
                                                                                    @[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
                                                                                      Instances For
                                                                                        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
                                                                                        @[simp]
                                                                                        theorem Bool.and_eq_false_imp {x y : Bool} :
                                                                                        (x && y) = false x = truey = 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]

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

                                                                                        @[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.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
                                                                                        @[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) :
                                                                                        @[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 yx = !y
                                                                                        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) :
                                                                                        @[simp]
                                                                                        theorem Bool.false_le (x : Bool) :
                                                                                        @[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 yy zx z
                                                                                        theorem Bool.le_antisymm {x y : Bool} :
                                                                                        x yy xx = 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 < yy < zx < 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 yy < zx < z
                                                                                        theorem Bool.lt_of_lt_of_le {x y z : Bool} :
                                                                                        x < yy zx < z
                                                                                        theorem Bool.le_of_lt {x y : Bool} :
                                                                                        x < yx y
                                                                                        theorem Bool.le_of_eq {x y : Bool} :
                                                                                        x = yx y
                                                                                        theorem Bool.ne_of_lt {x y : Bool} :
                                                                                        x < yx y
                                                                                        theorem Bool.lt_of_le_of_ne {x y : Bool} :
                                                                                        x yx yx < y
                                                                                        theorem Bool.le_of_lt_or_eq {x y : Bool} :
                                                                                        x < y x = yx y

                                                                                        min/max #

                                                                                        @[simp]
                                                                                        @[simp]

                                                                                        injectivity lemmas #

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

                                                                                        Converts true to 1 and false to 0.

                                                                                        Equations
                                                                                          Instances For
                                                                                            @[simp]
                                                                                            @[simp]
                                                                                            theorem Bool.toNat_le (c : Bool) :
                                                                                            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) :

                                                                                            Converts true to 1 and false to 0.

                                                                                            Equations
                                                                                              Instances For
                                                                                                @[simp]
                                                                                                @[simp]

                                                                                                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 = trueq
                                                                                                @[simp]
                                                                                                theorem Bool.not_ite_eq_true_eq_true {p : Prop} [h : Decidable p] {b c : Bool} :
                                                                                                @[simp]
                                                                                                theorem Bool.not_ite_eq_false_eq_false {p : Prop} [h : Decidable p] {b c : Bool} :
                                                                                                @[simp]
                                                                                                theorem Bool.not_ite_eq_true_eq_false {p : Prop} [h : Decidable p] {b c : Bool} :
                                                                                                @[simp]
                                                                                                theorem Bool.not_ite_eq_false_eq_true {p : Prop} [h : Decidable p] {b c : Bool} :

                                                                                                forall #

                                                                                                theorem Bool.forall_bool' {p : BoolProp} (b : Bool) :
                                                                                                (∀ (x : Bool), p x) p b p !b
                                                                                                @[simp]
                                                                                                theorem Bool.forall_bool {p : BoolProp} :
                                                                                                (∀ (b : Bool), p b) p false p true

                                                                                                exists #

                                                                                                theorem Bool.exists_bool' {p : BoolProp} (b : Bool) :
                                                                                                ( (x : Bool), p x) p b p !b
                                                                                                @[simp]
                                                                                                theorem Bool.exists_bool {p : BoolProp} :
                                                                                                ( (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
                                                                                                  Instances For
                                                                                                    @[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
                                                                                                      Instances For
                                                                                                        @[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
                                                                                                          Instances For
                                                                                                            @[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
                                                                                                              Instances For
                                                                                                                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] :
                                                                                                                @[simp]
                                                                                                                theorem true_eq_decide_iff {p : Prop} [h : Decidable 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
                                                                                                                  Instances For
                                                                                                                    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
                                                                                                                      Instances For

                                                                                                                        subtypes #

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