Bool.not_and
theorem Bool.not_and : ∀ (x y : Bool), (!(x && y)) = (!x || !y)
This is a theorem stating De Morgan's law for boolean `and` operation. In essence, it says that the negation of the conjunction (logical `and`) of two boolean values `x` and `y` is equivalent to the disjunction (logical `or`) of the negations of `x` and `y`. Mathematically, this can be written as: not (x and y) equals (not x) or (not y).
More concisely: Not (xAnd y) is equivalent to (xOr (neg x)) and (yOr (neg y)), where x, y are boolean values, xAnd is logical and, yOr is logical or, and neg is the logical negation operator.
|
Bool.xor_false
theorem Bool.xor_false : ∀ (x : Bool), xor x false = x
The theorem `Bool.xor_false` states that for any Boolean value `x`, the exclusive or (xor) of `x` and `false` is equal to `x`. In other words, when one of the inputs to the xor operation is `false`, the result is simply the other input. This is analogous to the mathematical statement: for all x in {true, false}, x XOR false equals x.
More concisely: For all Boolean values x, x XOR false equals x.
|
Bool.cond_decide
theorem Bool.cond_decide :
∀ {α : Type u_1} (p : Prop) [inst : Decidable p] (t e : α), (bif decide p then t else e) = if p then t else e := by
sorry
This theorem, `Bool.cond_decide`, states that for any type `α`, proposition `p`, and elements `t` and `e` of type `α`, the evaluation of the Boolean "if-then-else" expression that uses `decide p` (which computes the truth value of `p`) as its condition is identical to the evaluation of the traditional "if-then-else" expression with `p` as its condition. Essentially, it says that we can replace the condition `p` with `decide p` in an "if-then-else" expression without changing the result. This holds for any decidable proposition `p`.
More concisely: For any type `α`, decidable proposition `p` over `α`, and elements `t`, `e` of type `α`, `decide p t = if p then t else e`.
|
Bool.not_or
theorem Bool.not_or : ∀ (x y : Bool), (!(x || y)) = (!x && !y)
This theorem states De Morgan's law for the boolean OR operation. Specifically, it asserts that for all boolean values `x` and `y`, the negation of the OR of `x` and `y` (i.e., `!(x || y)`) is equivalent to the AND of the negations of `x` and `y` (i.e., `!x && !y`). This is a fundamental law in boolean algebra and logic.
More concisely: The negation of the OR operation is equivalent to the AND of the negations for all boolean values: !(x || y) =!x && !y.
|
Bool.cond_eq_ite
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
The theorem `Bool.cond_eq_ite` states that for any type `α`, given a boolean value `b` and two values `t` and `e` of type `α`, the conditional construct `bif b then t else e` is equivalent to the identical construct using an explicit equality check: `if b = true then t else e`. In other words, the `bif` construct and the `if...then...else` construct with an explicit equality to `true` are interchangeable in Lean 4 when dealing with boolean values.
More concisely: For any type `α` and boolean value `b` and values `t` and `e` of type `α`, `bif b then t else e` is equal to `if b = true then t else e`.
|
Bool.xor_true
theorem Bool.xor_true : ∀ (x : Bool), xor x true = !x
This theorem, `Bool.xor_true`, states that for any boolean value `x`, the exclusive or (`xor`) of `x` and `true` is equal to the negation of `x`. In simpler words, if you apply 'xor' operation between any boolean and 'true', you would get the opposite of that boolean. For instance, if `x` is `true`, its 'xor' with 'true' would be 'false' and vice versa.
More concisely: For any boolean value x, xor(x, true) = ∼x. (Here, xor denotes exclusive or, and ∼ denotes logical negation.)
|
Bool.decide_coe
theorem Bool.decide_coe : ∀ (b : Bool) [inst : Decidable (b = true)], decide (b = true) = b
The theorem `Bool.decide_coe` states that for any Boolean value `b` and a decidable proposition that `b` equals `true`, the Lean function `decide` applied to the proposition `b = true` is equal to `b` itself. In other words, if you have a Boolean `b` and can decide whether `b` is `true`, using `decide` to make this decision will give you `b` itself.
More concisely: If `b : Bool` is decidable, then `decide (b = true) = b`.
|
Bool.decide_and
theorem Bool.decide_and :
∀ (p q : Prop) [dpq : Decidable (p ∧ q)] [dp : Decidable p] [dq : Decidable q],
decide (p ∧ q) = (decide p && decide q)
This theorem, `Bool.decide_and`, states that for any two propositions `p` and `q`, given that `p` and `q` are decidable, the decision procedure for the conjunction of `p` and `q` (i.e., `p ∧ q`) is equal to the boolean 'and' (`&&`) of the decision procedures for `p` and `q` separately. In simpler terms, it shows that deciding whether both `p` and `q` are true is the same as deciding if `p` is true and then deciding if `q` is true.
More concisely: For decidable propositions `p` and `q`, `p ∧ q` is decidable and equivalent to `p && q`.
|