Init.Data.BEq

PartialEquivBEq structure

(α) [BEq α]

Full source

/-- `PartialEquivBEq α` says that the `BEq` implementation is a
partial equivalence relation, that is:
* it is symmetric: `a == b → b == a`
* it is transitive: `a == b → b == c → a == c`.
-/
class PartialEquivBEq (α) [BEq α] : Prop where
  /-- Symmetry for `BEq`. If `a == b` then `b == a`. -/
  symm : (a : α) == b → b == a
  /-- Transitivity for `BEq`. If `a == b` and `b == c` then `a == c`. -/
  trans : (a : α) == b → b == c → a == c

Partial Equivalence Relation for Boolean Equality

Informal description

The structure `PartialEquivBEq α` asserts that the boolean equality relation `==` on type `α` is a partial equivalence relation, meaning it satisfies: - Symmetry: `a == b` implies `b == a` for any `a, b : α`. - Transitivity: `a == b` and `b == c` imply `a == c` for any `a, b, c : α`.

ReflBEq structure

(α) [BEq α]

Full source

/-- `ReflBEq α` says that the `BEq` implementation is reflexive. -/
class ReflBEq (α) [BEq α] : Prop where
  /-- Reflexivity for `BEq`. -/
  refl : (a : α) == a

Reflexive Boolean Equality

Informal description

The structure `ReflBEq α` asserts that the boolean equality relation `==` on type `α` is reflexive, meaning that for any element `a : α`, the expression `a == a` evaluates to `true`.

EquivBEq structure

(α) [BEq α] : Prop extends PartialEquivBEq α, ReflBEq α

Full source

/-- `EquivBEq` says that the `BEq` implementation is an equivalence relation. -/
class EquivBEq (α) [BEq α] : Prop extends PartialEquivBEq α, ReflBEq α

Equivalence Relation for Boolean Equality

Informal description

The structure `EquivBEq` asserts that the boolean equality relation `==` on a type `α` is an equivalence relation, meaning it is reflexive and symmetric (as specified by extending `PartialEquivBEq` and `ReflBEq`). This ensures that the `BEq` implementation behaves like a proper equivalence relation.

BEq.refl theorem

[BEq α] [ReflBEq α] {a : α} : a == a

Full source

@[simp]
theorem BEq.refl [BEq α] [ReflBEq α] {a : α} : a == a :=
  ReflBEq.refl

Reflexivity of Boolean Equality

Informal description

For any type $\alpha$ with a boolean equality relation `==` that is reflexive, and for any element $a \in \alpha$, the boolean equality $a == a$ holds (i.e., evaluates to `true`).

beq_of_eq theorem

[BEq α] [ReflBEq α] {a b : α} : a = b → a == b

Full source

theorem beq_of_eq [BEq α] [ReflBEq α] {a b : α} : a = b → a == b
  | rfl => BEq.refl

Boolean Equality from Propositional Equality

Informal description

For any type $\alpha$ with a reflexive boolean equality relation `==`, and for any elements $a, b \in \alpha$, if $a = b$ holds, then $a == b$ evaluates to `true`.

BEq.symm theorem

[BEq α] [PartialEquivBEq α] {a b : α} : a == b → b == a

Full source

theorem BEq.symm [BEq α] [PartialEquivBEq α] {a b : α} : a == b → b == a :=
  PartialEquivBEq.symm

Symmetry of Boolean Equality for Partial Equivalence Relations

Informal description

For any type $\alpha$ with a boolean equality relation `==` that forms a partial equivalence relation, and for any elements $a, b \in \alpha$, if $a == b$ holds, then $b == a$ also holds.

BEq.comm theorem

[BEq α] [PartialEquivBEq α] {a b : α} : (a == b) = (b == a)

Full source

theorem BEq.comm [BEq α] [PartialEquivBEq α] {a b : α} : (a == b) = (b == a) :=
  Bool.eq_iff_iff.2 ⟨BEq.symm, BEq.symm⟩

Commutativity of Boolean Equality for Partial Equivalence Relations

Informal description

For any type $\alpha$ with a boolean equality relation `==` that forms a partial equivalence relation, and for any elements $a, b \in \alpha$, the boolean equality $a == b$ is equal to $b == a$.

bne_comm theorem

[BEq α] [PartialEquivBEq α] {a b : α} : (a != b) = (b != a)

Full source

theorem bne_comm [BEq α] [PartialEquivBEq α] {a b : α} : (a != b) = (b != a) := by
  rw [bne, BEq.comm, bne]

Commutativity of Boolean Not-Equal Operation

Informal description

For any type $\alpha$ with a boolean equality relation `==` that forms a partial equivalence relation, and for any elements $a, b \in \alpha$, the boolean not-equal operation satisfies $(a \neq b) = (b \neq a)$, where $\neq$ denotes the boolean negation of `==`.

BEq.symm_false theorem

[BEq α] [PartialEquivBEq α] {a b : α} : (a == b) = false → (b == a) = false

Full source

theorem BEq.symm_false [BEq α] [PartialEquivBEq α] {a b : α} : (a == b) = false → (b == a) = false :=
  BEq.comm (α := α) ▸ id

Symmetry of False Boolean Equality in Partial Equivalence Relations

Informal description

For any type $\alpha$ with a boolean equality relation `==` that forms a partial equivalence relation, and for any elements $a, b \in \alpha$, if $a == b$ evaluates to `false`, then $b == a$ also evaluates to `false$.

BEq.trans theorem

[BEq α] [PartialEquivBEq α] {a b c : α} : a == b → b == c → a == c

Full source

theorem BEq.trans [BEq α] [PartialEquivBEq α] {a b c : α} : a == b → b == c → a == c :=
  PartialEquivBEq.trans

Transitivity of Boolean Equality in Partial Equivalence Relations

Informal description

For any type $\alpha$ with a boolean equality relation `==` that forms a partial equivalence relation, and for any elements $a, b, c \in \alpha$, if $a == b$ and $b == c$ hold, then $a == c$ also holds.

BEq.congr_left theorem

[BEq α] [PartialEquivBEq α] {a b c : α} (h : a == b) : (a == c) = (b == c)

Full source

theorem BEq.congr_left [BEq α] [PartialEquivBEq α] {a b c : α} (h : a == b) :
    (a == c) = (b == c) :=
  Bool.eq_iff_iff.mpr ⟨BEq.trans (BEq.symm h), BEq.trans h⟩

Left Congruence of Boolean Equality in Partial Equivalence Relations

Informal description

For any type $\alpha$ with a boolean equality relation `==` that forms a partial equivalence relation, and for any elements $a, b, c \in \alpha$, if $a == b$ holds, then the boolean equality $(a == c) = (b == c)$ holds for any $c \in \alpha$.

BEq.congr_right theorem

[BEq α] [PartialEquivBEq α] {a b c : α} (h : b == c) : (a == b) = (a == c)

Full source

theorem BEq.congr_right [BEq α] [PartialEquivBEq α] {a b c : α} (h : b == c) :
    (a == b) = (a == c) :=
  Bool.eq_iff_iff.mpr ⟨fun h' => BEq.trans h' h, fun h' => BEq.trans h' (BEq.symm h)⟩

Right Congruence of Boolean Equality in Partial Equivalence Relations

Informal description

For any type $\alpha$ with a boolean equality relation `==` that forms a partial equivalence relation, and for any elements $a, b, c \in \alpha$, if $b == c$ holds, then the boolean equality $(a == b) = (a == c)$ holds.

BEq.neq_of_neq_of_beq theorem

[BEq α] [PartialEquivBEq α] {a b c : α} : (a == b) = false → b == c → (a == c) = false

Full source

theorem BEq.neq_of_neq_of_beq [BEq α] [PartialEquivBEq α] {a b c : α} :
    (a == b) = false → b == c → (a == c) = false :=
  fun h₁ h₂ => Bool.eq_false_iff.2 fun h₃ => Bool.eq_false_iff.1 h₁ (BEq.trans h₃ (BEq.symm h₂))

Transitivity of Boolean Inequality in Partial Equivalence Relations

Informal description

For any type $\alpha$ with a boolean equality relation `==` that forms a partial equivalence relation, and for any elements $a, b, c \in \alpha$, if $a == b$ evaluates to `false` and $b == c$ holds, then $a == c$ evaluates to `false`.

BEq.neq_of_beq_of_neq theorem

[BEq α] [PartialEquivBEq α] {a b c : α} : a == b → (b == c) = false → (a == c) = false

Full source

theorem BEq.neq_of_beq_of_neq [BEq α] [PartialEquivBEq α] {a b c : α} :
    a == b → (b == c) = false → (a == c) = false :=
  fun h₁ h₂ => Bool.eq_false_iff.2 fun h₃ => Bool.eq_false_iff.1 h₂ (BEq.trans (BEq.symm h₁) h₃)

Transitivity of Boolean Inequality via Boolean Equality

Informal description

For any type $\alpha$ with a boolean equality relation `==` that forms a partial equivalence relation, and for any elements $a, b, c \in \alpha$, if $a == b$ holds and $b == c$ evaluates to `false`, then $a == c$ evaluates to `false$.

instEquivBEqOfLawfulBEq instance

[BEq α] [LawfulBEq α] : EquivBEq α

Full source

instance (priority := low) [BEq α] [LawfulBEq α] : EquivBEq α where
  refl := LawfulBEq.rfl
  symm h := beq_iff_eq.2 <| Eq.symm <| beq_iff_eq.1 h
  trans hab hbc := beq_iff_eq.2 <| (beq_iff_eq.1 hab).trans <| beq_iff_eq.1 hbc

Lawful Boolean Equality is an Equivalence Relation

Informal description

For any type $\alpha$ with a boolean equality operation `==` that is lawful (i.e., agrees with propositional equality), the boolean equality relation `==` forms an equivalence relation on $\alpha$.