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