Contents Previous Next

Equality

module Logic.equality where

open import Logic.logicBasics using (¬; not; xor; ⟂; ⊤; singleton)
open import Lang.dataStructures using (Bool; true; false)

We start with the definition of a binary relation:

Rel : Set → Set1
Rel A = A → A → Set

Equality, or an equivalence, is the most basic comparison that can be performed between two objects. Let us first see how equality (and inequality) looks like for logic:

data _≡_ {A : Set}(x : A) : A → Set where
  refl : x ≡ x

_≢_ : {A : Set} → A → A → Set
x ≢ y = ¬ (x ≡ y)

Equality can also be derived as a negation of XOR:

\[ a \equiv b ~is~ ~True~ \implies ¬ (a \bigoplus b) ~is~ True \]

equal? : Bool → Bool → Bool
equal? a b = not (xor a b)

The laws of equality are same as what we saw earlier in equality. However, we derive the the same laws without universe polymorphism:

Properties of Equivalence Relations

Relations can conform to certain properties, which later come in handy for classifying relations and building a lot of mathematical structure.

Reflexive

A reflexive relation is one where \[ x ∙ y = y ∙ x \]

reflexive : {A : Set}
  → Rel A
  → Set
reflexive {A} _★_ = (x : A) → x ★ x

Symmetric

A symmetric relation is one where \[ x ∙ y ⟹ y ∙ x \]

symmetric : {A : Set} → Rel A → Set
symmetric {A} _★_  = (x y : A)
  → x ★ y
  → y ★ x

Transitive

A transitive relation is one where \[ x ∙ y, y ∙ z ~then~ z ∙ x \]

transitive : {A : Set} → Rel A → Set
transitive {A} _★_ = (x y z : A)
  → x ★ y
  → y ★ z
  → x ★ z

Congruent

A congruent relation is one where a function \[ x ∙ y ⟹ f(x) ∙ f(y) \] or the function f preserves the relation.

congruent : {A : Set} → Rel A → Set
congruent {A} _★_ = (f : A → A)(x y : A)
  → x ★ y
  → f x ★ f y

Substitutive

A substitutive relation is one where \[ x ∙ y ~and~ (predicate~ y) = ⊤ ⟹ (predicate~ x) = ⊤ \]

substitutive : {A : Set} → Rel A → Set1
substitutive {A} _★_ = (P : A → Set)(x y : A)
  → x ★ y
  → P x
  → P y

Equivalence relation

record Equivalence (A : Set) : Set1 where
  field
    _==_  : Rel A
    rfl   : reflexive _==_
    sym   : symmetric _==_
    trans : transitive _==_

Logical Equivalence

Note, the only difference here is that each law applies to the same datatype, be it ⟂, ⊤ or Bool.

symm : {A : Set} {x y : A}
        → x ≡ y
        → y ≡ x
symm {A} refl = refl
trans : {A : Set} {x y z : A}
        → x ≡ y
        → y ≡ z
        → x ≡ z
trans {A} refl a = a

Let us fit the above proofs of the properties of the relation ≡ to prove an equivalence relation:

Equiv : {A : Set} → Equivalence A
Equiv = record
  {
    _==_  = _≡_
    ; rfl   = \x      → refl
    ; sym   = \x y    → symm
    ; trans = \x y z  → trans
  }

To see that this applies to a singleton:

refl⊤ : singleton ≡ singleton
refl⊤  = Equivalence.rfl Equiv singleton

sym⊤ : singleton ≡ singleton → singleton ≡ singleton
sym⊤   = Equivalence.sym Equiv singleton singleton

trans⊤ : singleton ≡ singleton → singleton ≡ singleton → singleton ≡ singleton
trans⊤ = Equivalence.trans Equiv singleton singleton singleton

We cannot, however, verify this for ⟂ explicitly as we cannot produce an object that does not exist / does not have a constructor.

Inequality ≢ cannot serve as an equivalence relation as reflexivity and transitivity cannot be satisfied.

Laws of Logic