Relations

A relation on a type A is a predicate that takes two elements of A and returns a proposition, indicating whether the elements are related. In Lean, a relation is represented as a function of type A → A → Prop. Given a relation R : A → A → Prop and elements a1, a2 : A, the expression R a1 a2 asserts that a1 and a2 are related under R. Relations play a fundamental role in mathematics, capturing concepts such as order, equivalence, or divisibility, among others. In this chapter, we explore key properties that relations can satisfy, laying the groundwork for their formal use in Lean.

Since relations are predicates on two input variables, two relations are equal if and only if they relate the same elements. This can be shown by applying funext twice. Furthermore, this is equivalent to the predicates being logically equivalent on the same elements, which follows from propext.

Relations.lean

theorem TEqRel {A : Type} {R S : A → A → Prop} : R = S ↔ ∀ (a1 a2 : A), 
R a1 a2 ↔ S a1 a2 := by
  apply Iff.intro
  -- R = S → ∀ (a1 a2 : A), R a1 a2 ↔ S a1 a2
  intro h a1 a2
  apply Iff.intro
  -- R a1 a2 → S a1 a2
  intro hR
  rw [h.symm]
  exact hR
  -- S a1 a2 → R a1 a2
  intro hS
  rw [h]
  exact hS
  -- (∀ (a1 a2 : A), R a1 a2 ↔ S a1 a2) → R = S
  intro h
  apply funext
  intro a1
  apply funext
  intro a2
  apply propext
  exact h a1 a2

Examples of relations

Given a type A, we can define various relations on it. For instance, the emptyRelation relation relates no elements at all. At the other extreme, the total relation relates every element to every other element. Another important example is the diagonal relation, diag, where each element is related only to itself.

Relations.lean

-- The `empty` relation on `A` 
def empty {A : Type} : A → A → Prop := fun x y => False

-- The `total` relation on `A` 
def total {A : Type} : A → A → Prop := fun x y => True

-- The `diag` (diagonal) relation on `A`
def diag {A : Type} : A → A → Prop := fun x y => (x = y)

Types of relations

In this section, we explore various properties that a relation can satisfy.

Reflexive

A relation R : A → A → Prop is reflexive if, for every a : A, the proposition R a a holds, meaning that a is R-related to itself.

Reflexive.lean

def Reflexive {A : Type} (R : A →  A → Prop) : Prop := ∀{a : A}, R a a

Symmetric

A relation R : A → A → Prop is symmetric if, for all a1, a2 : A, whenever R a1 a2 holds, R a2 a1 must also hold.

Symmetric.lean

def Symmetric {A : Type} (R : A → A → Prop) : Prop := 
∀{a1 a2 : A}, R a1 a2 → R a2 a1

Antisymmetric

A relation R : A → A → Prop is antisymmetric if, for all a1, a2 : A, whenever R a1 a2 and R a2 a1 hold, it follows that a1 = a2.

Antisymmetric.lean

def Antisymmetric {A : Type} (R : A → A → Prop) : Prop :=
∀{a1 a2 : A}, R a1 a2 → R a2 a1 → (a1 = a2)

Transitive

A relation R : A → A → Prop is transitive if, for all a1, a2 a3 : A, whenever R a1 a2 and R a2 a3 hold, it follows that R a1 a3.

Transitive.lean

def Transitive {A : Type} (R : A → A → Prop) : Prop :=
∀{a1 a2 a3 : A}, R a1 a2 → R a2 a3 → R a1 a3

Serial

A relation R : A → A → Prop is serial if, for every a1 : A, there exists an element a2 : A such that R a1 a2

Serial.lean

def Serial {A : Type} (R : A → A → Prop) : Prop := 
∀{a1 : A}, ∃(a2 : A), R a1 a2

Euclidean

A relation R : A → A → Prop is Euclidean if, for every a1, a2 ,a3 : A, whenever R a1 a2 and R a1 a3 hold, it follows that R a2 a3.

Euclidean.lean

def Euclidean {A : Type} (R : A → A → Prop) : Prop :=
∀{a1 a2 a3 : A}, R a1 a2 → R a1 a3 → R a2 a3

Partially functional

A relation R : A → A → Prop is partially functional if, for every a1, a2, a3 : A, whenever R a1 a2 and R a1 a3 hold, it follows that a2 = a3.

PartiallyFunctional.lean

def PartiallyFunctional {A : Type} (R : A → A → Prop) : Prop :=
∀{a1 a2 a3 : A}, R a1 a2 → R a1 a3 → a2 = a3

Functional

A relation R : A → A → Prop is functional if, for every a1 : A, there exists a unique a2 : A such that R a1 a2.

Functional.lean

def Functional {A : Type} (R : A → A → Prop) : Prop :=
∀(a1 : A), ∃(a2 : A), ∀(a3 : A), R a1 a3 ↔ a2 = a3

Weakly dense

A relation R : A → A → Prop is weakly dense if, for every a1 a2 : A, if R a1 a2 holds then there exists a3 : A such that R a1 a3 and R a3 a2.

WeaklyDense.lean

def WeaklyDense {A : Type} (R : A → A → Prop) : Prop :=
∀{a1 a2 : A}, (R a1 a2 → ∃(a3 : A), (R a1 a3) ∧ (R a3 a2))

Weakly connected

A relation R : A → A → Prop is weakly connected if, for all a1, a2, a3 : A, whenever R a1 a2 and R a1 a3 hold, at least one of the following three conditions must be satisfied: R a2 a3, a2 = a3, or R a3 a2.

WeaklyConnected.lean

def WeaklyConnected {A : Type} (R : A → A → Prop) : Prop :=
∀{a1 a2 a3 : A}, R a1 a2 → R a1 a3 → ((R a2 a3) ∨ (a2 = a3) ∨ (R a3 a2))

Weakly directed

A relation R : A → A → Prop is weakly directed if, for all a1, a2, a3 : A, whenever R a1 a2 and R a1 a3 then there exists a4 : A satisfying that R a2 a4 and R a3 a4.

WeaklyDirected.lean

def WeaklyDirected {A : Type} (R : A → A → Prop) : Prop :=
∀{a1 a2 a3 : A}, R a1 a2 → R a1 a3 → ∃(a4 : A), ((R a2 a4) ∧ (R a3 a4))

An example: The diagonal

The diagonal relation is a relation that satisfies all the properties above.

Diagonal.lean

-- The diagonal is reflexive
theorem TDiagRefl {A : Type} : Reflexive (@diag A) := by
  intro a
  exact rfl

-- The diagonal is symmetric
theorem TDiagSymm {A : Type} : Symmetric (@diag A) := by
  intro a1 a2 h
  exact h.symm

-- The diagonal is antisymmetric
theorem TDiagASymm {A : Type} : Antisymmetric (@diag A) := by
  intro a1 a2 h1 h2
  exact h1

-- The diagonal is transitive
theorem TDiagTrans {A : Type} : Transitive (@diag A) := by
  intro a1 a2 a3 h1 h2
  exact h1.trans h2

-- The diagonal is serial
theorem TDiagSer {A : Type} : Serial (@diag A) := by
  intro a
  apply Exists.intro a
  exact rfl

-- The diagonal is Euclidean
theorem TDiagEucl {A : Type} : Euclidean (@diag A) := by
  intro a1 a2 a3 h1 h2
  exact h1.symm.trans h2

-- The diagonal is partially functional
theorem TDiagPFunc {A : Type} : PartiallyFunctional (@diag A) := by
  intro a1 a2 a3 h1 h2
  exact h1.symm.trans h2

-- The diagonal is functional
theorem TDiagFunc {A : Type} : Functional (@diag A) := by
  intro a
  apply Exists.intro a
  intro z
  apply Iff.intro
  -- diag a z → a = z
  intro h
  exact h
  -- a = z → diag a z
  intro h
  exact h

-- The diagonal is weakly dense
theorem TDiagWDense {A : Type} : WeaklyDense (@diag A) := by
  intro a1 a2 h1
  apply Exists.intro a1
  apply And.intro
  -- Left
  exact rfl
  -- Right
  exact h1

-- The diagonal is weakly connected
theorem TDiagWConn {A : Type} : WeaklyConnected (@diag A) := by
  intro a1 a2 a3 h1 h2
  exact Or.inl (h1.symm.trans h2)

-- The diagonal is weakly directed
theorem TDiagWDir {A : Type} : WeaklyDirected (@diag A) := by
  intro a1 a2 a3 h1 h2
  apply Exists.intro a1
  apply And.intro
  -- Left
  exact h1.symm
  -- Right
  exact h2.symm

Exercises

The following exercises were extracted from Zach, R. (2019) Boxes and Diamonds: An Open Introduction to Modal Logic.

Exercises.lean

variable (A : Type)
variable (R : A → A → Prop)

-- Reflexive implies serial
theorem TRefltoSerial : Reflexive R → Serial R := by sorry

-- For a symmetric relation, transitive and Euclidean are equivalent
theorem TSymmTransIffSer (hS : Symmetric R) : Transitive R ↔ Euclidean R := by sorry

-- If a relation is symmetric then it is weakly directed
theorem TSymmtoWDir : Symmetric R → WeaklyDirected R := by sorry

-- If a relation is Euclidean and antisymmetric, then it is weakly directed
theorem TEuclASymmtoWDir : Euclidean R → Antisymmetric R → WeaklyDirected R := by sorry

-- If a relation is Euclidean, then it is weakly connected
theorem TEucltoWConn : Euclidean R → WeaklyConnected R := by sorry

-- If a relation is functional, then it is serial
theorem TFunctoSer : Functional R → Serial R := by sorry

-- If a relation is symmetric and transitive, then it is Euclidean
theorem TSymmTranstoEucl : Symmetric R → Transitive R → Euclidean R := by sorry

-- If a relation is reflexive and Euclidean, then it is symmetric
theorem TReflEucltoSymm : Reflexive R → Euclidean R → Symmetric R := by sorry

-- If a relation is symmetric and Euclidean, then it is transitive
theorem TSymmEucltoTrans : Symmetric R → Euclidean R → Transitive R := by sorry

-- If a relation is serial, symmetric and transitive, then it is reflexive
theorem TSerSymmTranstoRefl : Serial R → Symmetric R → Transitive R → Reflexive R := by sorry

Operations on relations

Composition

The composition of two binary relations captures the idea of chaining relations through an intermediate element. Given binary relations R and S on a type A, its composition, denoted as R ∘ S, is a new relation on A that holds between two elements a1 and a3 if there exists an intermediate element a2 such that R relates a1 to a2 and S relates a2 to a3.

Composition.lean

def composition {A : Type} (R S : A → A → Prop) : A → A → Prop := by
  intro a1 a3
  exact ∃ (a2 : A), (R a1 a2) ∧ (S a2 a3)

-- Notation for the composition (`\circ`)
notation : 65 lhs:65 " ∘ " rhs:66 => composition lhs rhs
#check R ∘ S

Inverse

Given a relation R : A → A → Prop on a type A, its inverse, denoted R^, swaps the order of its arguments. The definition of inverse takes a relation R and returns a new relation R^ where `R^ a1 a2 holds if and only if R a2 a1 holds in the original relation.

Inverse.lean

def inverse {A : Type} (R : A → A → Prop) : A → A → Prop := by
  intro a1 a2
  exact R a2 a1

-- Notation for the inverse (`^`)
notation : 65 lhs:65 "^" => inverse lhs
#check R^

Meet

Given binary relations R and S on a type A, its meet, denoted as R ∧ S, is a new relation on A that holds between two elements a1 and a2 if both R a1 a2 and S a1 a2 hold.

Meet.lean

def meet {A : Type} (R S : A → A → Prop) : A → A → Prop := by
  intro a1 a2
  exact (R a1 a2) ∧ (S a1 a2)

-- Notation for the meet  (`\and`)
notation : 65 lhs:65 " ∧ " rhs:66 => meet lhs rhs
#check R ∧ S

Join

Given binary relations R and S on a type A, its join, denoted as R ∨ S, is a new relation on A that holds between two elements a1 and a2 if either R a1 a2 or S a1 a2 hold.

Join.lean

def join {A : Type} (R S : A → A → Prop) : A → A → Prop := by
  intro a1 a2
  exact (R a1 a2) ∨ (S a1 a2)

-- Notation for the join (`\or`)
notation : 65 lhs:65 " ∨ " rhs:66 => join lhs rhs
#check R ∨ S

Exercises

The following propositions are common identities involving binary relations.

Exercises.lean

namespace Exercises
variable {A : Type}
variable (R S T : A → A → Prop)

-- Associativity of composition
theorem TAssComp : R ∘ (S ∘ T) = (R ∘ S) ∘ T := by sorry

-- The diagonal is a left neutral element for the composition
theorem TDiagL : R ∘ (@diag A) = R := by sorry

-- The diagonal is a right neutral element for the composition
theorem TDiagR : (@diag A) ∘ R = R := by sorry

-- The inverse relation of the inverse relation is the original relation
theorem TInvInv : (R^)^ = R := by sorry

-- The inverse of the composition
theorem TInvComp : (R ∘ S)^ = (S^) ∘ (R^) := by sorry

-- The inverse of the meet
theorem TInvMeet : (R ∧ S)^ = (S^) ∧ (R^) := by sorry

-- The inverse of the join
theorem TInvJoin : (R ∨ S)^ = (S^) ∨ (R^) := by sorry

-- Distributivity of composition on the left over join
theorem TDisL : R ∘ (S ∨ T) = (R ∘ S) ∨ (R ∘ T) := by sorry

-- Distributivity of composition on the right over join
theorem TDisR : (R ∨ S) ∘ T = (R ∘ T) ∨ (S ∘ T) := by sorry

-- Empty is a left zero for the composition
theorem TEmptLZ : (@empty A) ∘ R = (@empty A) := by sorry

-- Empty is a right zero for the composition
theorem TEmptRZ : R ∘ (@empty A) = (@empty A) := by sorry