7. Structures

Modern mathematics makes essential use of algebraic structures, which encapsulate patterns that can be instantiated in multiple settings. The subject provides various ways of defining such structures and constructing particular instances.

Lean therefore provides corresponding ways of defining structures formally and working with them. You have already seen examples of algebraic structures in Lean, such as rings and lattices, which were discussed in Chapter 2. This chapter will explain the mysterious square bracket annotations that you saw there, [Ring α] and [Lattice α]. It will also show you how to define and use algebraic structures on your own.

For more technical detail, you can consult Theorem Proving in Lean, and a paper by Anne Baanen, Use and abuse of instance parameters in the Lean mathematical library.

7.1. Structures

7.1.1. Defining Structures

• structure is a collection of data or constraints that must be satisfied.

• An instance of the structure, defined by def, is a particular bundle of data satisfying the constraints.

@[ext]  -- "Extensionality" Lean auto-generates theorems to prove two instances of a structure are equal when their components are equal
structure Point where
  x : ℝ
  y : ℝ
  z : ℝ


structure Point' where build ::
  x : ℝ
  y : ℝ
  z : ℝ


-- A structure can also specify constraints:
structure StandardTwoSimplex where
  x : ℝ
  y : ℝ
  z : ℝ
  x_nonneg : 0 ≤ x
  y_nonneg : 0 ≤ y
  z_nonneg : 0 ≤ z
  sum_eq : x + y + z = 1


-- structure can also be used to bundle together properties without the data.
structure IsLinear (f : ℝ → ℝ) where
  is_additive : ∀ x y, f (x + y) = f x + f y
  preserves_mul : ∀ x c, f (c * x) = c * f x


-- structure can be defined using a generic type product
def Point'' :=
  ℝ × ℝ × ℝ

• protected will force using Point.add_comm even when the namespace is open, which can avoid ambiguity with a generic theorem like add_comm.

protected theorem add_comm (a b : Point) : add a b = add b a := by
  rw [add, add]
  ext <;> dsimp
  repeat' apply add_comm

example (a b : Point) : add a b = add b a := by simp [add, add_comm]

7.1.2. Defining Instances of Structures

Lean provides multiple ways of defining particular instances of the Point structure.

-- named structure value
def myPoint1 : Point where
  x := 2
  y := -1
  z := 4


-- anonymous structure value
example : Point where
  x := 2
  y := -1
  z := 4


def myPoint2 : Point :=
  ⟨2, -1, 4⟩

def myPoint3 :=
  Point.mk 2 (-1) 4  -- ``.mk``: the "make" constructor

#check myPoint1

#check Point'.build 2 (-1) 4


#check Point.ext

example (a b : Point) (hx : a.x = b.x) (hy : a.y = b.y) (hz : a.z = b.z) : a = b := by
  ext
  -- · assumption
  -- · exact hx
  -- · assumption
  -- · assumption
  repeat' assumption

7.1.3. Parameterized Structures

Structures can depend on parameters. For example, we can generalize the standard 2-simplex to the standard \(n\)-simplex for any \(n\).

open BigOperators

structure StandardSimplex (n : ℕ) where
  V : Fin n → ℝ  -- vertices
  NonNeg : ∀ i : Fin n, 0 ≤ V i
  sum_eq_one : (∑ i, V i) = 1

namespace StandardSimplex

def midpoint (n : ℕ) (a b : StandardSimplex n) : StandardSimplex n
  -- We need to follow the definition of StandardSimplex and provide V i, NonNeg and sum_eq_one
    where
  V i := (a.V i + b.V i) / 2
  NonNeg := by
    intro i
    apply div_nonneg
    · linarith [a.NonNeg i, b.NonNeg i]
    norm_num
  sum_eq_one := by
    simp [div_eq_mul_inv, ← Finset.sum_mul, Finset.sum_add_distrib,
      a.sum_eq_one, b.sum_eq_one]
    field_simp

end StandardSimplex

example : AddSubgroup ℚ where  -- additive subgroup
  carrier := Set.range ((↑) : ℤ → ℚ)  -- a canonical coercion map from integers to rationals
  add_mem' := by
    rintro _ _ ⟨n, rfl⟩ ⟨m, rfl⟩
    use n + m
    simp
  zero_mem' := by
    use 0
    simp
  neg_mem' := by
    rintro _ ⟨n, rfl⟩
    use -n
    simp

7.2. Algebraic Structures

7.3. Building the Gaussian Integers