# Equality

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