Contents Previous Next


module Logic.equality where

open import Types.relations using (Rel; Equivalence)
open import Logic.logicBasics using (¬; not; xor;;; singleton)
open import Lang.dataStructures using (Bool; true; false)

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:

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

symmetric : {A : Set} {x y : A}
         x ≡ y
         y ≡ x
symmetric {A} refl = refl
transitive : {A : Set} {x y z : A}
         x ≡ y
         y ≡ z
         x ≡ z
transitive {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
    _==_  = __
    ; refl  = \x       refl
    ; sym   = \x y     symmetric
    ; trans = \x y z   transitive

To see that this applies to a singleton:

refl⊤ : singleton ≡ singleton
refl⊤  = Equivalence.refl 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, though symmetry can:

symmetric≢ : {A : Set} {x y : A}
         x ≢ y
         y ≢ x
symmetric≢ np p = np (symmetric p)

Laws of Logic