ホーム / Technical /

From MyNat to Integers: Structures and Equivalence Relations" or "Toward Building Integers: Structures and Setoid

Friday, 14 August 2026

Lean Mathematics Technical

t f B! P L

So far we have been building the natural numbers from scratch using MyNat. Starting with this article, we move on to building the integers from scratch. This article covers the structures and equivalence relations we will need along the way.

Structures

A structure is declared with the structure command. It is a keyword for bundling multiple pieces of data together as a single type. The pieces of data a structure holds are called fields. In the example below, x and y are fields. 

structure Point where
  x : Int
  y : Int

There are two ways to create a value of a structure type. One is to use the { } syntax, and the other is to use the mk constructor. 

#check {x := 1, y := 2 : Point}
#check Point.mk
#check Point.mk 1 2
#eval
  let p := Point.mk 1 2
  p.x

Equivalence relations

An equivalence relation r : α → α → Prop is a relation that satisfies the following three properties.

  • Reflexivity: r x x
  • Symmetry: r x y implies r y x
  • Transitivity: r x y and r y z together imply r x z

Equality is one example of an equivalence relation, and equivalence relations share many of the properties that equality has. In Lean, the structure that witnesses a relation being an equivalence relation is Equivalence, defined as follows. 

structure Equivalence {α : Sort u} (r : α → α → Prop) : Prop where
  /-- An equivalence relation is reflexive: `r x x` -/
  refl  : ∀ x, r x x
  /-- An equivalence relation is symmetric: `r x y` implies `r y x` -/
  symm  : ∀ {x y}, r x y → r y x
  /-- An equivalence relation is transitive: `r x y` and `r y z` imply `r x z` -/
  trans : ∀ {x y z}, r x y → r y z → r x z

To show that an equivalence relation is reflexive, we use the refl field. 

example {α : Type} (r : α → α → Prop) (h: Equivalence r) : ∀ x, r x x := by
  exact h.refl

To get a better feel for equivalence relations, let's prove that the relation defined by x = y for an arbitrary type α is always an equivalence relation. The constructor tactic splits the Equivalence structure into a proof obligation for each of its fields. 

example {α : Type} : Equivalence (fun x y : α => x = y) := by
  constructor

  case refl =>
    intro x
    rfl

  case symm =>
    intro x y h
    rw [h]

  case trans =>
    intro x y z hxy hyz
    rw [hxy, hyz]

Setoid

A Setoid is a type equipped with a designated equivalence relation, written ≈. The relation r : α → α → Prop itself is represented by the type class Setoid α. In Lean, Setoid is defined as follows. 

class Setoid (α : Sort u) where
  /-- `x ≈ y` is the designated equivalence relation of a Setoid. -/
  r : α → α → Prop
  /-- The relation `x ≈ y` is an equivalence relation. -/
  iseqv : Equivalence r

Next time, we will use these structures and equivalence relations to build the integers from pairs of MyNat values.

The full code is available in this repository.

QooQ