Mathlib.Data.Bool.Basic

Bool.true_eq_false_eq_False theorem

: ¬true = false

Full source

theorem true_eq_false_eq_False : ¬true = false := by decide

Inequality of Boolean Constants: $\text{true} \neq \text{false}$

Informal description

The boolean value `true` is not equal to `false`, i.e., $\text{true} \neq \text{false}$.

Bool.false_eq_true_eq_False theorem

: ¬false = true

Full source

theorem false_eq_true_eq_False : ¬false = true := by decide

Inequality of Boolean Constants: $\text{false} \neq \text{true}$

Informal description

The boolean value `false` is not equal to `true`, i.e., $\text{false} \neq \text{true}$.

Bool.and_eq_true_eq_eq_true_and_eq_true theorem

(a b : Bool) : ((a && b) = true) = (a = true ∧ b = true)

Full source

theorem and_eq_true_eq_eq_true_and_eq_true (a b : Bool) :
    ((a && b) = true) = (a = true ∧ b = true) := by simp

Conjunction Truth Condition for Booleans

Informal description

For any boolean values $a$ and $b$, the conjunction $a \land b$ evaluates to `true` if and only if both $a$ and $b$ evaluate to `true`. In other words, $(a \land b) = \text{true} \leftrightarrow (a = \text{true}) \land (b = \text{true})$.

Bool.or_eq_true_eq_eq_true_or_eq_true theorem

(a b : Bool) : ((a || b) = true) = (a = true ∨ b = true)

Full source

theorem or_eq_true_eq_eq_true_or_eq_true (a b : Bool) :
    ((a || b) = true) = (a = true ∨ b = true) := by simp

Disjunction Equivalence for Booleans: $(a \lor b) = \text{true} \leftrightarrow (a = \text{true} \lor b = \text{true})$

Informal description

For any boolean values $a$ and $b$, the equality $(a \lor b) = \text{true}$ holds if and only if either $a = \text{true}$ or $b = \text{true}$.

Bool.not_eq_true_eq_eq_false theorem

(a : Bool) : (not a = true) = (a = false)

Full source

theorem not_eq_true_eq_eq_false (a : Bool) : (not a = true) = (a = false) := by cases a <;> simp

Negation of Boolean Equals True if and only if Boolean is False

Informal description

For any boolean value $a$, the statement $\neg a = \mathtt{true}$ is equivalent to $a = \mathtt{false}$.

Bool.and_eq_false_eq_eq_false_or_eq_false theorem

(a b : Bool) : ((a && b) = false) = (a = false ∨ b = false)

Full source

theorem and_eq_false_eq_eq_false_or_eq_false (a b : Bool) :
    ((a && b) = false) = (a = false ∨ b = false) := by
  cases a <;> cases b <;> simp

De Morgan's Law for Boolean Conjunction: $(a \land b) = \text{false} \leftrightarrow (a = \text{false} \lor b = \text{false})$

Informal description

For any boolean values $a$ and $b$, the conjunction $a \land b$ is false if and only if either $a$ is false or $b$ is false, i.e., $(a \land b) = \text{false} \leftrightarrow (a = \text{false} \lor b = \text{false})$.

Bool.or_eq_false_eq_eq_false_and_eq_false theorem

(a b : Bool) : ((a || b) = false) = (a = false ∧ b = false)

Full source

theorem or_eq_false_eq_eq_false_and_eq_false (a b : Bool) :
    ((a || b) = false) = (a = false ∧ b = false) := by
  cases a <;> cases b <;> simp

De Morgan's Law for Boolean Disjunction: $(a \lor b = \text{false}) \leftrightarrow (a = \text{false} \land b = \text{false})$

Informal description

For any boolean values $a$ and $b$, the disjunction $a \lor b$ is false if and only if both $a$ and $b$ are false, i.e., $(a \lor b = \text{false}) \leftrightarrow (a = \text{false} \land b = \text{false})$.

Bool.not_eq_false_eq_eq_true theorem

(a : Bool) : (not a = false) = (a = true)

Full source

theorem not_eq_false_eq_eq_true (a : Bool) : (not a = false) = (a = true) := by cases a <;> simp

Negation of Boolean Equals False if and only if Boolean is True

Informal description

For any boolean value $a$, the negation of $a$ is false if and only if $a$ is true, i.e., $\neg a = \text{false} \leftrightarrow a = \text{true}$.

Bool.coe_false theorem

: ↑false = False

Full source

theorem coe_false : ↑false = False := by simp

Coercion of Boolean False to Proposition

Informal description

The coercion of the boolean value `false` to a proposition is equal to the false proposition `False`, i.e., $\uparrow\text{false} = \text{False}$.

Bool.coe_true theorem

: ↑true = True

Full source

theorem coe_true : ↑true = True := by simp

Coercion of Boolean True to Propositional True

Informal description

The canonical coercion from the boolean value `true` to the proposition `True` holds, i.e., $\text{true} = \text{True}$.

Bool.coe_sort_false theorem

: (false : Prop) = False

Full source

theorem coe_sort_false : (false : Prop) = False := by simp

Coercion of Boolean False to Proposition

Informal description

The boolean value `false` when coerced to a proposition is equal to the proposition `False`.

Bool.coe_sort_true theorem

: (true : Prop) = True

Full source

theorem coe_sort_true : (true : Prop) = True := by simp

Boolean True as Proposition is True

Informal description

The boolean value `true` when interpreted as a proposition is equal to the true proposition `True`.

Bool.decide_iff theorem

(p : Prop) [d : Decidable p] : decide p = true ↔ p

Full source

theorem decide_iff (p : Prop) [d : Decidable p] : decidedecide p = true ↔ p := by simp

Decidability Equivalence: `decide p = true ↔ p`

Informal description

For any proposition $p$ with a decidable instance, the boolean value `decide p` is equal to `true` if and only if $p$ holds.

Bool.decide_true theorem

{p : Prop} [Decidable p] : p → decide p

Full source

theorem decide_true {p : Prop} [Decidable p] : p → decide p :=
  (decide_iff p).2

Decidability Implication: $p \to \mathrm{decide}\ p$

Informal description

For any decidable proposition $p$, if $p$ holds then the boolean value `decide p` is `true`.

Bool.of_decide_true theorem

{p : Prop} [Decidable p] : decide p → p

Full source

theorem of_decide_true {p : Prop} [Decidable p] : decide p → p :=
  (decide_iff p).1

Implication from `decide p = true` to $p$ for decidable propositions

Informal description

For any decidable proposition $p$, if the boolean value `decide p` is `true`, then $p$ holds.

Bool.bool_iff_false theorem

{b : Bool} : ¬b ↔ b = false

Full source

theorem bool_iff_false {b : Bool} : ¬b¬b ↔ b = false := by cases b <;> decide

Negation of Boolean Equivalent to False

Informal description

For any boolean value $b$, the negation of $b$ is equivalent to $b$ being equal to `false`, i.e., $\neg b \leftrightarrow b = \mathrm{false}$.

Bool.bool_eq_false theorem

{b : Bool} : ¬b → b = false

Full source

theorem bool_eq_false {b : Bool} : ¬b → b = false :=
  bool_iff_false.1

False Boolean Implies Equality to `false`

Informal description

For any boolean value $b$, if $b$ is false (i.e., $\neg b$ holds), then $b$ is equal to `false`.

Bool.decide_false_iff theorem

(p : Prop) {_ : Decidable p} : decide p = false ↔ ¬p

Full source

theorem decide_false_iff (p : Prop) {_ : Decidable p} : decidedecide p = false ↔ ¬p :=
  bool_iff_false.symm.trans (not_congr (decide_iff _))

Decidability Equivalence: $\mathrm{decide}\, p = \mathrm{false} \leftrightarrow \neg p$

Informal description

For any decidable proposition $p$, the boolean value `decide p` is equal to `false` if and only if $\neg p$ holds.

Bool.decide_false theorem

{p : Prop} [Decidable p] : ¬p → decide p = false

Full source

theorem decide_false {p : Prop} [Decidable p] : ¬p → decide p = false :=
  (decide_false_iff p).2

False Proposition Implies Boolean Evaluation is `false`

Informal description

For any decidable proposition $p$, if $\neg p$ holds, then the boolean evaluation of $p$ is equal to `false`, i.e., $\mathrm{decide}\, p = \mathrm{false}$.

Bool.of_decide_false theorem

{p : Prop} [Decidable p] : decide p = false → ¬p

Full source

theorem of_decide_false {p : Prop} [Decidable p] : decide p = false → ¬p :=
  (decide_false_iff p).1

Boolean Evaluation to False Implies Negation of Proposition

Informal description

For any decidable proposition $p$, if the boolean evaluation of $p$ is `false`, then $\neg p$ holds, i.e., $\mathrm{decide}\, p = \mathrm{false} \to \neg p$.

Bool.decide_congr theorem

{p q : Prop} [Decidable p] [Decidable q] (h : p ↔ q) : decide p = decide q

Full source

theorem decide_congr {p q : Prop} [Decidable p] [Decidable q] (h : p ↔ q) : decide p = decide q :=
  decide_eq_decide.mpr h

Equivalence of Propositions Implies Equality of Boolean Decisions

Informal description

For any two decidable propositions $p$ and $q$, if $p$ is equivalent to $q$ (i.e., $p \leftrightarrow q$), then the boolean evaluation of $p$ is equal to the boolean evaluation of $q$, i.e., $\text{decide}(p) = \text{decide}(q)$.

Bool.coe_xor_iff theorem

(a b : Bool) : xor a b ↔ Xor' (a = true) (b = true)

Full source

theorem coe_xor_iff (a b : Bool) : xorxor a b ↔ Xor' (a = true) (b = true) := by
  cases a <;> cases b <;> decide

Boolean XOR Equivalence: $\text{xor}(a, b) \leftrightarrow \text{Xor}'(a = \text{true}, b = \text{true})$

Informal description

For any boolean values $a$ and $b$, the boolean XOR operation $\text{xor}(a, b)$ holds if and only if the exclusive-or of the propositions "$a = \text{true}$" and "$b = \text{true}$" holds, i.e., $\text{xor}(a, b) \leftrightarrow \text{Xor}'(a = \text{true}, b = \text{true})$.

Bool.dichotomy theorem

(b : Bool) : b = false ∨ b = true

Full source

theorem dichotomy (b : Bool) : b = false ∨ b = true := by cases b <;> simp

Boolean Dichotomy: $b = \text{false} \lor b = \text{true}$

Informal description

For any boolean value $b$, either $b$ is `false` or $b$ is `true`.

Bool.not_ne_id theorem

: not ≠ id

Full source

theorem not_ne_id : notnot ≠ id := fun h ↦ false_ne_true <| congrFun h true

Negation is not the identity function on booleans

Informal description

The boolean negation function `not` is not equal to the identity function `id`.

Bool.or_inl theorem

{a b : Bool} (H : a) : a || b

Full source

theorem or_inl {a b : Bool} (H : a) : a || b := by simp [H]

Left Disjunction Introduction for Booleans

Informal description

For any boolean values $a$ and $b$, if $a$ is true, then the logical disjunction $a \lor b$ is true.

Bool.or_inr theorem

{a b : Bool} (H : b) : a || b

Full source

theorem or_inr {a b : Bool} (H : b) : a || b := by cases a <;> simp [H]

Right Disjunction Introduction for Booleans

Informal description

For any boolean values $a$ and $b$, if $b$ is true, then the logical disjunction $a \lor b$ is also true.

Bool.and_elim_left theorem

: ∀ {a b : Bool}, a && b → a

Full source

theorem and_elim_left : ∀ {a b : Bool}, a && b → a := by decide

Left Conjunct Elimination for Boolean And

Informal description

For any boolean values $a$ and $b$, if $a \land b$ is true, then $a$ is true.

Bool.and_intro theorem

: ∀ {a b : Bool}, a → b → a && b

Full source

theorem and_intro : ∀ {a b : Bool}, a → b → a && b := by decide

Introduction Rule for Boolean Conjunction

Informal description

For any boolean values $a$ and $b$, if $a$ is true and $b$ is true, then the conjunction $a \land b$ is true.

Bool.and_elim_right theorem

: ∀ {a b : Bool}, a && b → b

Full source

theorem and_elim_right : ∀ {a b : Bool}, a && b → b := by decide

Right Conjunct Elimination for Boolean And

Informal description

For any boolean values $a$ and $b$, if $a \land b$ is true, then $b$ is true.

Bool.not_eq_iff theorem

: ∀ {a b : Bool}, !a = b ↔ a ≠ b

Full source

lemma not_eq_iff : ∀ {a b : Bool}, !a = b!a = b ↔ a ≠ b := by decide

Negation Equivalence: $\neg a = b \leftrightarrow a \neq b$

Informal description

For any boolean values $a$ and $b$, the negation of $a$ equals $b$ if and only if $a$ is not equal to $b$, i.e., $\neg a = b \leftrightarrow a \neq b$.

Bool.ne_not theorem

{a b : Bool} : a ≠ !b ↔ a = b

Full source

theorem ne_not {a b : Bool} : a ≠ !ba ≠ !b ↔ a = b :=
  not_eq_not

Negation Inequality Equivalence: $a \neq \neg b \leftrightarrow a = b$

Informal description

For any boolean values $a$ and $b$, the inequality $a \neq \neg b$ holds if and only if $a = b$.

Bool.not_ne_self theorem

: ∀ b : Bool, (!b) ≠ b

Full source

lemma not_ne_self : ∀ b : Bool, (!b) ≠ b := by decide

Negation Inequality: $\neg b \neq b$ for Booleans

Informal description

For any boolean value $b$, the negation of $b$ is not equal to $b$, i.e., $\neg b \neq b$.

Bool.self_ne_not theorem

: ∀ b : Bool, b ≠ !b

Full source

lemma self_ne_not : ∀ b : Bool, b ≠ !b := by decide

Boolean Value Not Equal to Its Negation

Informal description

For every boolean value $b$, $b$ is not equal to its negation $\neg b$.

Bool.not_iff_not theorem

: ∀ {b : Bool}, !b ↔ ¬b

Full source

theorem not_iff_not : ∀ {b : Bool}, !b!b ↔ ¬b := by simp

Negation Equivalence for Booleans: $\lnot b \leftrightarrow \neg b$

Informal description

For any boolean value $b$, the negation of $b$ (denoted as $\lnot b$) is equivalent to the logical negation of $b$ (denoted as $\neg b$). In other words, $\lnot b \leftrightarrow \neg b$.

Bool.bne_eq_xor theorem

: bne = xor

Full source

theorem bne_eq_xor : bne = xor := by funext a b; revert a b; decide

Boolean Inequality as Exclusive Or

Informal description

The boolean inequality function `bne` is equal to the exclusive or (xor) operation on booleans, i.e., `bne = xor`.

Bool.xor_iff_ne theorem

: ∀ {x y : Bool}, xor x y = true ↔ x ≠ y

Full source

theorem xor_iff_ne : ∀ {x y : Bool}, xorxor x y = true ↔ x ≠ y := by decide

Exclusive Or Equals True if and only if Inputs Differ

Informal description

For any boolean values $x$ and $y$, the exclusive or (xor) of $x$ and $y$ is true if and only if $x$ is not equal to $y$.

Bool.linearOrder instance

: LinearOrder Bool

Full source

instance linearOrder : LinearOrder Bool where
  le_refl := by decide
  le_trans := by decide
  le_antisymm := by decide
  le_total := by decide
  toDecidableLE := inferInstance
  toDecidableEq := inferInstance
  toDecidableLT := inferInstance
  lt_iff_le_not_le := by decide
  max_def := by decide
  min_def := by decide

Linear Order on Booleans

Informal description

The boolean type `Bool` is equipped with a linear order where `false < true`.

Bool.lt_iff theorem

: ∀ {x y : Bool}, x < y ↔ x = false ∧ y = true

Full source

theorem lt_iff : ∀ {x y : Bool}, x < y ↔ x = false ∧ y = true := by decide

Boolean Ordering: $x < y$ iff $x$ is false and $y$ is true

Informal description

For any boolean values $x$ and $y$, the relation $x < y$ holds if and only if $x$ is false and $y$ is true.

Bool.false_lt_true theorem

: false < true

Full source

@[simp]
theorem false_lt_true : false < true :=
  lt_iff.2 ⟨rfl, rfl⟩

False is less than true in boolean order

Informal description

The boolean value `false` is strictly less than `true` in the linear order on booleans.

Bool.le_iff_imp theorem

: ∀ {x y : Bool}, x ≤ y ↔ x → y

Full source

theorem le_iff_imp : ∀ {x y : Bool}, x ≤ y ↔ x → y := by decide

Boolean Order-Implication Equivalence: $x \leq y \leftrightarrow (x \to y)$

Informal description

For any boolean values $x$ and $y$, the inequality $x \leq y$ holds if and only if the implication $x \to y$ holds (i.e., if $x$ is true then $y$ must also be true).

Bool.and_le_left theorem

: ∀ x y : Bool, (x && y) ≤ x

Full source

theorem and_le_left : ∀ x y : Bool, (x && y) ≤ x := by decide

Left Conjunct Weaker in Boolean Ordering

Informal description

For any boolean values $x$ and $y$, the conjunction $x \land y$ is less than or equal to $x$ in the boolean ordering.

Bool.and_le_right theorem

: ∀ x y : Bool, (x && y) ≤ y

Full source

theorem and_le_right : ∀ x y : Bool, (x && y) ≤ y := by decide

Right Conjunct is Upper Bound in Boolean Lattice

Informal description

For any boolean values $x$ and $y$, the conjunction $x \land y$ is less than or equal to $y$ in the boolean lattice.

Bool.le_and theorem

: ∀ {x y z : Bool}, x ≤ y → x ≤ z → x ≤ (y && z)

Full source

theorem le_and : ∀ {x y z : Bool}, x ≤ y → x ≤ z → x ≤ (y && z) := by decide

Implication of Conjunction from Implication of Both Components

Informal description

For any boolean values $x$, $y$, and $z$, if $x$ implies $y$ and $x$ implies $z$, then $x$ implies the conjunction of $y$ and $z$ (i.e., $x \leq y \land z$).

Bool.left_le_or theorem

: ∀ x y : Bool, x ≤ (x || y)

Full source

theorem left_le_or : ∀ x y : Bool, x ≤ (x || y) := by decide

Left Disjunction Dominance in Boolean Algebra

Informal description

For any boolean values $x$ and $y$, the value $x$ is less than or equal to the disjunction $x \lor y$.

Bool.right_le_or theorem

: ∀ x y : Bool, y ≤ (x || y)

Full source

theorem right_le_or : ∀ x y : Bool, y ≤ (x || y) := by decide

Right Disjunction Monotonicity for Booleans

Informal description

For any boolean values $x$ and $y$, the value $y$ is less than or equal to the disjunction $x \lor y$.

Bool.or_le theorem

: ∀ {x y z}, x ≤ z → y ≤ z → (x || y) ≤ z

Full source

theorem or_le : ∀ {x y z}, x ≤ z → y ≤ z → (x || y) ≤ z := by decide

Supremum Property of Boolean OR

Informal description

For any boolean values $x$, $y$, and $z$, if $x \leq z$ and $y \leq z$, then $(x \lor y) \leq z$.

Bool.ofNat definition

(n : Nat) : Bool

Full source

/-- convert a `ℕ` to a `Bool`, `0 -> false`, everything else -> `true` -/
def ofNat (n : Nat) : Bool :=
  decide (n ≠ 0)

Boolean conversion of a natural number

Informal description

The function maps a natural number $ n $ to the boolean value `false` if $ n = 0 $, and to `true` otherwise.

Bool.toNat_beq_zero theorem

(b : Bool) : (b.toNat == 0) = !b

Full source

@[simp] lemma toNat_beq_zero (b : Bool) : (b.toNat == 0) = !b := by cases b <;> rfl

Boolean to Natural Number Zero Equality: $(b.\text{toNat} = 0) \leftrightarrow \neg b$

Informal description

For any boolean value $b$, the equality $(b.\text{toNat} = 0)$ holds if and only if $\neg b$ holds, where $\text{toNat}$ converts $b$ to a natural number (0 for `false`, 1 for `true`).

Bool.toNat_bne_zero theorem

(b : Bool) : (b.toNat != 0) = b

Full source

@[simp] lemma toNat_bne_zero (b : Bool) : (b.toNat != 0) =  b := by simp [bne]

Boolean to Natural Number Nonzero Equality: $(b.\text{toNat} \neq 0) \leftrightarrow b$

Informal description

For any boolean value $b$, the inequality $(b.\text{toNat} \neq 0)$ holds if and only if $b$ holds, where $\text{toNat}$ converts $b$ to a natural number (0 for `false`, 1 for `true$).

Bool.toNat_beq_one theorem

(b : Bool) : (b.toNat == 1) = b

Full source

@[simp] lemma toNat_beq_one (b : Bool) : (b.toNat == 1) =  b := by cases b <;> rfl

Boolean to Natural Number Equivalence: $b.\text{toNat} = 1 \leftrightarrow b$

Informal description

For any boolean value $b$, the natural number representation of $b$ equals $1$ if and only if $b$ is true. In other words, $b.\text{toNat} = 1 \leftrightarrow b$.

Bool.toNat_bne_one theorem

(b : Bool) : (b.toNat != 1) = !b

Full source

@[simp] lemma toNat_bne_one (b : Bool) : (b.toNat != 1) = !b := by simp [bne]

Boolean to Natural Number Inequality: $b.\text{toNat} \neq 1 \leftrightarrow \neg b$

Informal description

For any boolean value $b$, the natural number representation of $b$ is not equal to $1$ if and only if $b$ is false. In other words, $b.\text{toNat} \neq 1 \leftrightarrow \neg b$.

Bool.ofNat_le_ofNat theorem

{n m : Nat} (h : n ≤ m) : ofNat n ≤ ofNat m

Full source

theorem ofNat_le_ofNat {n m : Nat} (h : n ≤ m) : ofNat n ≤ ofNat m := by
  simp only [ofNat, ne_eq, _root_.decide_not]
  cases Nat.decEq n 0 with
  | isTrue hn => rw [_root_.decide_eq_true hn]; exact Bool.false_le _
  | isFalse hn =>
    cases Nat.decEq m 0 with
    | isFalse hm => rw [_root_.decide_eq_false hm]; exact Bool.le_true _
    | isTrue hm => subst hm; have h := Nat.le_antisymm h (Nat.zero_le n); contradiction

Monotonicity of Boolean Conversion with Respect to Natural Number Order

Informal description

For any natural numbers $n$ and $m$ such that $n \leq m$, the boolean conversion of $n$ is less than or equal to the boolean conversion of $m$.

Bool.toNat_le_toNat theorem

{b₀ b₁ : Bool} (h : b₀ ≤ b₁) : toNat b₀ ≤ toNat b₁

Full source

theorem toNat_le_toNat {b₀ b₁ : Bool} (h : b₀ ≤ b₁) : toNat b₀ ≤ toNat b₁ := by
  cases b₀ <;> cases b₁ <;> simp_all +decide

Natural Number Representation Preserves Boolean Order

Informal description

For any two boolean values $b₀$ and $b₁$ such that $b₀ \leq b₁$, the natural number representation of $b₀$ is less than or equal to the natural number representation of $b₁$.

Bool.ofNat_toNat theorem

(b : Bool) : ofNat (toNat b) = b

Full source

theorem ofNat_toNat (b : Bool) : ofNat (toNat b) = b := by
  cases b <;> rfl

Boolean-Natural Number Conversion Identity: $\mathrm{ofNat} \circ \mathrm{toNat} = \mathrm{id}$

Informal description

For any boolean value $b$, converting $b$ to a natural number and then back to a boolean yields $b$ itself, i.e., $\mathrm{ofNat}(\mathrm{toNat}(b)) = b$.

Bool.injective_iff theorem

{α : Sort*} {f : Bool → α} : Function.Injective f ↔ f false ≠ f true

Full source

@[simp]
theorem injective_iff {α : Sort*} {f : Bool → α} : Function.InjectiveFunction.Injective f ↔ f false ≠ f true :=
  ⟨fun Hinj Heq ↦ false_ne_true (Hinj Heq), fun H x y hxy ↦ by
    cases x <;> cases y
    · rfl
    · exact (H hxy).elim
    · exact (H hxy.symm).elim
    · rfl⟩

Injectivity Criterion for Boolean Functions: $f$ injective $\iff$ $f(\mathrm{false}) \neq f(\mathrm{true})$

Informal description

A function $f : \mathrm{Bool} \to \alpha$ is injective if and only if $f(\mathrm{false}) \neq f(\mathrm{true})$.

Bool.apply_apply_apply theorem

(f : Bool → Bool) (x : Bool) : f (f (f x)) = f x

Full source

/-- **Kaminski's Equation** -/
theorem apply_apply_apply (f : Bool → Bool) (x : Bool) : f (f (f x)) = f x := by
  cases x <;> cases h₁ : f true <;> cases h₂ : f false <;> simp only [h₁, h₂]

Triple Application Identity for Boolean Functions: $f^3 = f$

Informal description

For any boolean function $f : \mathrm{Bool} \to \mathrm{Bool}$ and any boolean value $x \in \{\mathrm{false}, \mathrm{true}\}$, the triple application of $f$ equals a single application, i.e., $f(f(f(x))) = f(x)$.

Bool.xor3 definition

(x y c : Bool)

Full source

/-- `xor3 x y c` is `((x XOR y) XOR c)`. -/
protected def xor3 (x y c : Bool) :=
  xor (xor x y) c

Triple XOR operation on booleans

Informal description

The function `xor3` takes three boolean values `x`, `y`, and `c` and computes `(x XOR y) XOR c`, where XOR denotes the exclusive or operation.

Bool.carry definition

(x y c : Bool)

Full source

/-- `carry x y c` is `x && y || x && c || y && c`. -/
protected def carry (x y c : Bool) :=
  x && yx && y || x && cx && y || x && c || y && c

Carry bit of three boolean inputs

Informal description

The function `carry` takes three boolean values `x`, `y`, and `c` and returns `(x ∧ y) ∨ (x ∧ c) ∨ (y ∧ c)`, which represents the carry bit in a full adder circuit when adding three binary digits.

Tags