Documentation

Std.Data.Bool

@[inline, reducible]
abbrev xor :
BoolBoolBool

Boolean exclusive or

Equations
Instances For
    @[inline, reducible]
    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
      @[inline, reducible]
      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
        @[inline, reducible]
        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
          @[inline, reducible]
          abbrev Bool.xor :
          BoolBoolBool

          Boolean exclusive or

          Equations
          Instances For
            instance Bool.instDecidableForAllBool (p : BoolProp) [inst : DecidablePred p] :
            Decidable (∀ (x : Bool), p x)
            Equations
            • One or more equations did not get rendered due to their size.
            instance Bool.instDecidableExistsBool (p : BoolProp) [inst : DecidablePred p] :
            Decidable (∃ (x : Bool), p x)
            Equations
            • One or more equations did not get rendered due to their size.
            Equations
            Equations
            Equations
            Equations

            and #

            @[simp]
            theorem Bool.not_and_self (x : Bool) :
            (!x && x) = false
            @[simp]
            theorem Bool.and_not_self (x : Bool) :
            (x && !x) = false
            theorem Bool.and_comm (x : Bool) (y : Bool) :
            (x && y) = (y && x)
            theorem Bool.and_left_comm (x : Bool) (y : Bool) (z : Bool) :
            (x && (y && z)) = (y && (x && z))
            theorem Bool.and_right_comm (x : Bool) (y : Bool) (z : Bool) :
            (x && y && z) = (x && z && y)
            theorem Bool.and_or_distrib_left (x : Bool) (y : Bool) (z : Bool) :
            (x && (y || z)) = (x && y || x && z)
            theorem Bool.and_or_distrib_right (x : Bool) (y : Bool) (z : Bool) :
            ((x || y) && z) = (x && z || y && z)
            theorem Bool.and_xor_distrib_left (x : Bool) (y : Bool) (z : Bool) :
            (x && xor y z) = xor (x && y) (x && z)
            theorem Bool.and_xor_distrib_right (x : Bool) (y : Bool) (z : Bool) :
            (xor x y && z) = xor (x && z) (y && z)
            theorem Bool.not_and (x : Bool) (y : Bool) :
            (!(x && y)) = (!x || !y)

            De Morgan's law for boolean and

            theorem Bool.and_eq_true_iff (x : Bool) (y : Bool) :
            (x && y) = true x = true y = true
            theorem Bool.and_eq_false_iff (x : Bool) (y : Bool) :
            (x && y) = false x = false y = false

            or #

            @[simp]
            theorem Bool.not_or_self (x : Bool) :
            (!x || x) = true
            @[simp]
            theorem Bool.or_not_self (x : Bool) :
            (x || !x) = true
            theorem Bool.or_comm (x : Bool) (y : Bool) :
            (x || y) = (y || x)
            theorem Bool.or_left_comm (x : Bool) (y : Bool) (z : Bool) :
            (x || (y || z)) = (y || (x || z))
            theorem Bool.or_right_comm (x : Bool) (y : Bool) (z : Bool) :
            (x || y || z) = (x || z || y)
            theorem Bool.or_and_distrib_left (x : Bool) (y : Bool) (z : Bool) :
            (x || y && z) = ((x || y) && (x || z))
            theorem Bool.or_and_distrib_right (x : Bool) (y : Bool) (z : Bool) :
            (x && y || z) = ((x || z) && (y || z))
            theorem Bool.not_or (x : Bool) (y : Bool) :
            (!(x || y)) = (!x && !y)

            De Morgan's law for boolean or

            theorem Bool.or_eq_true_iff (x : Bool) (y : Bool) :
            (x || y) = true x = true y = true
            theorem Bool.or_eq_false_iff (x : Bool) (y : Bool) :
            (x || y) = false x = false y = false

            xor #

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

            le/lt #

            @[simp]
            theorem Bool.le_true (x : Bool) :
            @[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
            @[deprecated Bool.not_inj_iff]
            theorem Bool.not_inj' {x : Bool} {y : Bool} :
            (!x) = !y x = y

            Alias of Bool.not_inj_iff.

            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
            @[deprecated Bool.and_or_inj_right_iff]
            theorem Bool.and_or_inj_right' {m : Bool} {x : Bool} {y : Bool} :
            (x && m) = (y && m) (x || m) = (y || m) x = y

            Alias of Bool.and_or_inj_right_iff.

            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
            @[deprecated Bool.and_or_inj_left_iff]
            theorem Bool.and_or_inj_left' {m : Bool} {x : Bool} {y : Bool} :
            (m && x) = (m && y) (m || x) = (m || y) x = y

            Alias of Bool.and_or_inj_left_iff.

            toNat #

            def Bool.toNat (b : Bool) :

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

            Equations
            Instances For

              cond #

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

              decide #

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