• Docència
    • Àlgebra Lineal i Geometria
    • Recull de qüestions
    • Recursos
    • Direcció de treballs
    • Innovació Docent
  • Recerca
    • Publicacions
    • Conferències
  • Codi
    • An Introduction to Lean 4
    • Taller de Lean 4
    • Galeria TikZ
    • Hipotrocoide
    • Evolució espacial dels virus
  • Enllaços
    • Grup d’Investigació
    • Grup d’Innovació Docent
    • Seminari Predoc
    • Congrés Investmat
  1. Relations
  • Source Code
  • An Introduction to Lean 4
  • Basic Syntax
  • Propositions
  • Quantifiers
  • Equalities
  • Functions
  • Choice
  • Subtypes
  • Relations
  • Quotients
  • Natural numbers
  • Orders
  • Empty and Unit types
  • Product and Sum types
  • Lists and Monoids

Sections

  • Examples of relations
  • Types of relations
    • An example: The diagonal
    • Exercises
  • Operations on relations
    • Exercises

Relations

Autor

Enric Cosme

Modificat

30/03/2025

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

2025 Enric Cosme Llópez

Dr. Moliner, 50 | 46100, Burjassot, València

Dissenyat amb & Quarto