Documentation

Init.Data.Bool

@[reducible, inline]
abbrev xor :
BoolBoolBool

Boolean exclusive or

Equations
Instances For
    @[reducible, inline]
    abbrev Bool.not :

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

    Equations
    Instances For
      @[reducible, inline]
      abbrev Bool.or (x : Bool) (y : Bool) :

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

      Equations
      Instances For
        @[reducible, inline]
        abbrev Bool.and (x : Bool) (y : Bool) :

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

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

          Boolean exclusive or

          Equations
          Instances For
            instance Bool.instDecidableForallOfDecidablePred (p : BoolProp) [inst : DecidablePred p] :
            Decidable (∀ (x : Bool), p x)
            Equations
            instance Bool.instDecidableExistsOfDecidablePred (p : BoolProp) [inst : DecidablePred p] :
            Decidable (∃ (x : Bool), p x)
            Equations
            @[simp]
            theorem Bool.default_bool :
            default = false
            instance Bool.instLE :
            Equations
            instance Bool.instLT :
            Equations
            instance Bool.instDecidableLe (x : Bool) (y : Bool) :
            Equations
            instance Bool.instDecidableLt (x : Bool) (y : Bool) :
            Decidable (x < y)
            Equations
            Equations
            Equations
            theorem Bool.eq_iff_iff {a : Bool} {b : Bool} :
            a = b (a = true b = true)
            @[simp]
            theorem Bool.decide_eq_true {b : Bool} [Decidable (b = true)] :
            decide (b = true) = b
            @[simp]

            and #

            @[simp]
            theorem Bool.and_self_left (a : Bool) (b : Bool) :
            (a && (a && b)) = (a && b)
            @[simp]
            theorem Bool.and_self_right (a : Bool) (b : Bool) :
            (a && b && b) = (a && b)
            @[simp]
            theorem Bool.not_and_self (x : Bool) :
            (!x && x) = false
            @[simp]
            theorem Bool.and_not_self (x : Bool) :
            (x && !x) = false
            theorem Bool.and_comm (x : Bool) (y : Bool) :
            (x && y) = (y && x)
            instance Bool.instCommutativeAnd :
            Std.Commutative fun (x x_1 : Bool) => x && x_1
            Equations
            theorem Bool.and_left_comm (x : Bool) (y : Bool) (z : Bool) :
            (x && (y && z)) = (y && (x && z))
            theorem Bool.and_right_comm (x : Bool) (y : Bool) (z : Bool) :
            (x && y && z) = (x && z && y)
            @[simp]
            theorem Bool.and_iff_left_iff_imp (a : Bool) (b : Bool) :
            (a && b) = a a = trueb = true
            @[simp]
            theorem Bool.and_iff_right_iff_imp (a : Bool) (b : Bool) :
            (a && b) = b b = truea = true
            @[simp]
            theorem Bool.iff_self_and (a : Bool) (b : Bool) :
            a = (a && b) a = trueb = true
            @[simp]
            theorem Bool.iff_and_self (a : Bool) (b : Bool) :
            b = (a && b) b = truea = true

            or #

            @[simp]
            theorem Bool.or_self_left (a : Bool) (b : Bool) :
            (a || (a || b)) = (a || b)
            @[simp]
            theorem Bool.or_self_right (a : Bool) (b : Bool) :
            (a || b || b) = (a || b)
            @[simp]
            theorem Bool.not_or_self (x : Bool) :
            (!x || x) = true
            @[simp]
            theorem Bool.or_not_self (x : Bool) :
            (x || !x) = true
            @[simp]
            theorem Bool.or_iff_left_iff_imp (a : Bool) (b : Bool) :
            (a || b) = a b = truea = true
            @[simp]
            theorem Bool.or_iff_right_iff_imp (a : Bool) (b : Bool) :
            (a || b) = b a = trueb = true
            @[simp]
            theorem Bool.iff_self_or (a : Bool) (b : Bool) :
            a = (a || b) b = truea = true
            @[simp]
            theorem Bool.iff_or_self (a : Bool) (b : Bool) :
            b = (a || b) a = trueb = true
            theorem Bool.or_comm (x : Bool) (y : Bool) :
            (x || y) = (y || x)
            instance Bool.instCommutativeOr :
            Std.Commutative fun (x x_1 : Bool) => x || x_1
            Equations
            theorem Bool.or_left_comm (x : Bool) (y : Bool) (z : Bool) :
            (x || (y || z)) = (y || (x || z))
            theorem Bool.or_right_comm (x : Bool) (y : Bool) (z : Bool) :
            (x || y || z) = (x || z || y)

            distributivity #

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

            De Morgan's law for boolean and

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

            De Morgan's law for boolean or

            theorem Bool.and_eq_true_iff (x : Bool) (y : Bool) :
            (x && y) = true x = true y = true
            theorem Bool.and_eq_false_iff (x : Bool) (y : Bool) :
            (x && y) = false x = false y = false
            @[simp]
            theorem Bool.and_eq_false_imp (x : Bool) (y : Bool) :
            (x && y) = false x = truey = false
            theorem Bool.or_eq_true_iff (x : Bool) (y : Bool) :
            (x || y) = true x = true y = true
            @[simp]
            theorem Bool.or_eq_false_iff (x : Bool) (y : Bool) :
            (x || y) = false x = false y = false

            eq/beq/bne #

            @[simp]

            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_self (x : Bool) :
            ((!x) != x) = true
            @[simp]
            theorem Bool.bne_not_self (x : Bool) :
            (x != !x) = true
            @[simp]
            theorem Bool.not_eq_self (b : Bool) :
            (!b) = b False
            @[simp]
            theorem Bool.eq_not_self (b : Bool) :
            @[simp]
            theorem Bool.beq_self_left (a : Bool) (b : Bool) :
            (a == (a == b)) = b
            @[simp]
            theorem Bool.beq_self_right (a : Bool) (b : Bool) :
            ((a == b) == b) = a
            @[simp]
            theorem Bool.bne_self_left (a : Bool) (b : Bool) :
            (a != (a != b)) = b
            @[simp]
            theorem Bool.bne_self_right (a : Bool) (b : Bool) :
            ((a != b) != b) = a
            @[simp]
            theorem Bool.not_bne_not (x : Bool) (y : Bool) :
            ((!x) != !y) = (x != y)
            @[simp]
            theorem Bool.bne_assoc (x : Bool) (y : Bool) (z : Bool) :
            ((x != y) != z) = (x != (y != z))
            instance Bool.instAssociativeBne :
            Std.Associative fun (x x_1 : Bool) => x != x_1
            Equations
            @[simp]
            theorem Bool.bne_left_inj (x : Bool) (y : Bool) (z : Bool) :
            (x != y) = (x != z) y = z
            @[simp]
            theorem Bool.bne_right_inj (x : Bool) (y : Bool) (z : Bool) :
            (x != z) = (y != z) x = y
            theorem Bool.eq_not_of_ne {x : Bool} {y : Bool} :
            x yx = !y
            theorem Bool.beq_eq_decide_eq {α : Type u_1} [BEq α] [LawfulBEq α] [DecidableEq α] (a : α) (b : α) :
            (a == b) = decide (a = b)
            @[simp]
            theorem Bool.not_eq_not {a : Bool} {b : Bool} :
            ¬a = !b a = b
            @[simp]
            theorem Bool.not_not_eq {a : Bool} {b : Bool} :
            ¬(!a) = b a = b
            @[simp]
            theorem Bool.coe_iff_coe (a : Bool) (b : Bool) :
            (a = true b = true) a = b
            @[simp]
            theorem Bool.coe_true_iff_false (a : Bool) (b : Bool) :
            (a = true b = false) a = !b
            @[simp]
            theorem Bool.coe_false_iff_true (a : Bool) (b : Bool) :
            (a = false b = true) (!a) = b
            @[simp]
            theorem Bool.coe_false_iff_false (a : Bool) (b : Bool) :
            (a = false b = false) (!a) = !b

            beq properties #

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

            xor #

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

            le/lt #

            @[simp]
            theorem Bool.le_true (x : Bool) :
            @[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 : Bool} {y : Bool} {z : Bool} :
            x yy zx z
            theorem Bool.le_antisymm {x : Bool} {y : Bool} :
            x yy xx = y
            theorem Bool.le_total (x : Bool) (y : Bool) :
            x y y x
            theorem Bool.lt_asymm {x : Bool} {y : Bool} :
            x < y¬y < x
            theorem Bool.lt_trans {x : Bool} {y : Bool} {z : Bool} :
            x < yy < zx < z
            theorem Bool.lt_iff_le_not_le {x : Bool} {y : Bool} :
            x < y x y ¬y x
            theorem Bool.lt_of_le_of_lt {x : Bool} {y : Bool} {z : Bool} :
            x yy < zx < z
            theorem Bool.lt_of_lt_of_le {x : Bool} {y : Bool} {z : Bool} :
            x < yy zx < z
            theorem Bool.le_of_lt {x : Bool} {y : Bool} :
            x < yx y
            theorem Bool.le_of_eq {x : Bool} {y : Bool} :
            x = yx y
            theorem Bool.ne_of_lt {x : Bool} {y : Bool} :
            x < yx y
            theorem Bool.lt_of_le_of_ne {x : Bool} {y : Bool} :
            x yx yx < y
            theorem Bool.le_of_lt_or_eq {x : Bool} {y : Bool} :
            x < y x = yx y

            min/max #

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

            injectivity lemmas #

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

            toNat #

            def Bool.toNat (b : Bool) :

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

            Equations
            • b.toNat = bif b then 1 else 0
            Instances For
              @[simp]
              theorem Bool.toNat_false :
              false.toNat = 0
              @[simp]
              theorem Bool.toNat_true :
              true.toNat = 1
              theorem Bool.toNat_le (c : Bool) :
              c.toNat 1
              @[reducible, inline, deprecated Bool.toNat_le]
              abbrev Bool.toNat_le_one (c : Bool) :
              c.toNat 1
              Equations
              Instances For
                theorem Bool.toNat_lt (b : Bool) :
                b.toNat < 2
                @[simp]
                theorem Bool.toNat_eq_zero (b : Bool) :
                b.toNat = 0 b = false
                @[simp]
                theorem Bool.toNat_eq_one (b : Bool) :
                b.toNat = 1 b = true

                ite #

                @[simp]
                theorem Bool.if_true_left (p : Prop) [h : Decidable p] (f : Bool) :
                (if p then true else f) = (decide p || f)
                @[simp]
                theorem Bool.if_false_left (p : Prop) [h : Decidable p] (f : Bool) :
                (if p then false else f) = (!decide p && f)
                @[simp]
                theorem Bool.if_true_right (p : Prop) [h : Decidable p] (t : Bool) :
                (if p then t else true) = (!decide p || t)
                @[simp]
                theorem Bool.if_false_right (p : Prop) [h : Decidable p] (t : Bool) :
                (if p then t else false) = (decide p && t)
                @[simp]
                theorem Bool.ite_eq_true_distrib (p : Prop) [h : Decidable p] (t : Bool) (f : Bool) :
                ((if p then t else f) = true) = if p then t = true else f = true
                @[simp]
                theorem Bool.ite_eq_false_distrib (p : Prop) [h : Decidable p] (t : Bool) (f : Bool) :
                ((if p then t else f) = false) = if p then t = false else f = false
                @[simp]
                theorem Bool.not_ite_eq_true_eq_true (p : Prop) [h : Decidable p] (b : Bool) (c : Bool) :
                (¬if p then b = true else c = true) if p then b = false else c = false
                @[simp]
                theorem Bool.not_ite_eq_false_eq_false (p : Prop) [h : Decidable p] (b : Bool) (c : Bool) :
                (¬if p then b = false else c = false) if p then b = true else c = true
                @[simp]
                theorem Bool.not_ite_eq_true_eq_false (p : Prop) [h : Decidable p] (b : Bool) (c : Bool) :
                (¬if p then b = true else c = false) if p then b = false else c = true
                @[simp]
                theorem Bool.not_ite_eq_false_eq_true (p : Prop) [h : Decidable p] (b : Bool) (c : Bool) :
                (¬if p then b = false else c = true) if p then b = true else c = false
                @[simp]
                theorem Bool.eq_false_imp_eq_true (b : Bool) :
                b = falseb = true b = true
                @[simp]
                theorem Bool.eq_true_imp_eq_false (b : Bool) :
                b = trueb = false b = false

                cond #

                theorem Bool.cond_eq_ite {α : Type u_1} (b : Bool) (t : α) (e : α) :
                (bif b then t else e) = if b = true then t else e
                theorem Bool.cond_eq_if {b : Bool} :
                ∀ {α : Type u_1} {x y : α}, (bif b then x else y) = if b = true then x else y
                @[simp]
                theorem Bool.cond_not {α : Type u_1} (b : Bool) (t : α) (e : α) :
                (bif !b then t else e) = bif b then e else t
                @[simp]
                theorem Bool.cond_self {α : Type u_1} (c : Bool) (t : α) :
                (bif c then t else t) = t
                theorem Bool.cond_decide {α : Type u_1} (p : Prop) [Decidable p] (t : α) (e : α) :
                (bif decide p then t else e) = if p then t else e
                @[simp]
                theorem Bool.cond_eq_ite_iff {α : Type u_1} (a : Bool) (p : Prop) [h : Decidable p] (x : α) (y : α) (u : α) (v : α) :
                ((bif a then x else y) = if p then u else v) (if a = true then x else y) = if p then u else v
                @[simp]
                theorem Bool.ite_eq_cond_iff {α : Type u_1} (p : Prop) [h : Decidable p] (a : Bool) (x : α) (y : α) (u : α) (v : α) :
                ((if p then x else y) = bif a then u else v) (if p then x else y) = if a = true then u else v
                @[simp]
                theorem Bool.cond_eq_true_distrib (c : Bool) (t : Bool) (f : Bool) :
                ((bif c then t else f) = true) = if c = true then t = true else f = true
                @[simp]
                theorem Bool.cond_eq_false_distrib (c : Bool) (t : Bool) (f : Bool) :
                ((bif c then t else f) = false) = if c = true then t = false else f = false
                theorem Bool.cond_true {α : Type u} {a : α} {b : α} :
                (bif true then a else b) = a
                theorem Bool.cond_false {α : Type u} {a : α} {b : α} :
                (bif false then a else b) = b
                @[simp]
                theorem Bool.cond_true_left (c : Bool) (f : Bool) :
                (bif c then true else f) = (c || f)
                @[simp]
                theorem Bool.cond_false_left (c : Bool) (f : Bool) :
                (bif c then false else f) = (!c && f)
                @[simp]
                theorem Bool.cond_true_right (c : Bool) (t : Bool) :
                (bif c then t else true) = (!c || t)
                @[simp]
                theorem Bool.cond_false_right (c : Bool) (t : Bool) :
                (bif c then t else false) = (c && t)
                @[simp]
                theorem Bool.cond_true_same (c : Bool) (b : Bool) :
                (bif c then c else b) = (c || b)
                @[simp]
                theorem Bool.cond_false_same (c : Bool) (b : Bool) :
                (bif c then b else c) = (c && b)
                theorem Bool.cond_pos {α : Type u_1} {b : Bool} {a : α} {a' : α} (h : b = true) :
                (bif b then a else a') = a
                theorem Bool.cond_neg {α : Type u_1} {b : Bool} {a : α} {a' : α} (h : b = false) :
                (bif b then a else a') = a'
                theorem Bool.apply_cond {α : Type u_1} {β : Type u_2} (f : αβ) {b : Bool} {a : α} {a' : α} :
                f (bif b then a else a') = bif b then f a else f a'
                theorem Bool.decide_coe (b : Bool) [Decidable (b = true)] :
                decide (b = true) = b
                @[simp]
                theorem Bool.decide_and (p : Prop) (q : Prop) [dpq : Decidable (p q)] [dp : Decidable p] [dq : Decidable q] :
                decide (p q) = (decide p && decide q)
                @[simp]
                theorem Bool.decide_or (p : Prop) (q : Prop) [dpq : Decidable (p q)] [dp : Decidable p] [dq : Decidable q] :
                decide (p q) = (decide p || decide q)
                @[simp]
                theorem Bool.decide_iff_dist (p : Prop) (q : Prop) [dpq : Decidable (p q)] [dp : Decidable p] [dq : Decidable q] :
                decide (p q) = (decide p == decide q)

                decide #

                @[simp]
                theorem false_eq_decide_iff {p : Prop} [h : Decidable p] :
                @[simp]
                theorem true_eq_decide_iff {p : Prop} [h : Decidable p] :