structures.org

Structures

The structure command generates record types. They generalize the dependent product type by providing named fields. It can be viewed as a macro built on top of the inductive datatype provided by the Lean kernel. Every structure declaration introduces a namespace with the same name. The general form of a structure declaration is as follows:

structure <name> <parameters> <parent-structures> : Type :=
  <constructor> :: <fields>

Most parts are optional. Here is a small example

import logic

structure point (A : Type) :=
mk :: (x : A) (y : A)

Values of type point are created using point.mk a b, the fields of a point p are accessed using point.x p and point.y p. The structure command also generates useful recursors and theorems. Here are some of the constructions generated for the declaration above.

import logic

structure point (A : Type) :=
mk :: (x : A) (y : A)

-- BEGIN
check point
check point.rec_on       -- recursor
check point.induction_on -- recursor to Prop
check point.destruct     -- alias for point.rec_on
check point.x            -- projection/field accessor
check point.y            -- projection/field accessor
check point.eta          -- eta theorem
check point.x.mk         -- projection over constructor theorem
check point.y.mk         -- projection over constructor theorem
-- END

We can obtain the complete list of generated construction using the command print prefix.

import logic

structure point (A : Type) :=
mk :: (x : A) (y : A)

-- BEGIN
print prefix point
-- END

Here is some simple theorems and expressions using the generated constructions. As usual, we can avoid the prefix point by using the command open point.

import logic

structure point (A : Type) :=
mk :: (x : A) (y : A)

-- BEGIN
eval point.x (point.mk 10 20)
eval point.y (point.mk 10 20)

open point

example (A : Type) (a b : A) : x (mk a b) = a :=
x.mk a b

example (A : Type) (a b : A) : y (mk a b) = b :=
y.mk a b

example (A : Type) (a b : A) : y (mk a b) = b :=
!y.mk  -- let Lean figure out the arguments

example (A : Type) (p : point A) : mk (x p) (y p) = p :=
eta p
-- END

If the constructor is not provided, then a constructor named mk is generated.

import logic

namespace playground
-- BEGIN
structure prod (A : Type) (B : Type) :=
(pr1 : A) (pr2 : B)

check prod.mk
-- END
end playground

We can provide universe levels explicitly.

import logic

namespace playground
-- BEGIN
-- Force A and B to be types from the same universe, and return a type also in the same universe.
structure prod.{l} (A : Type.{l}) (B : Type.{l}) : Type.{max 1 l} :=
(pr1 : A) (pr2 : B)

-- Ask Lean to pretty print universe levels
set_option pp.universes true
check prod.mk
-- END
end playground

We use max 1 l as the resultant universe level to ensure the universe level is never 0 even when the parameter A and B are propositions. Recall that in Lean, Type.{0} is Prop which is impredicative and proof irrelevant.

We can extend existing structures by adding new fields.

import logic

-- BEGIN
structure point (A : Type) :=
mk :: (x : A) (y : A)

inductive color :=
red, green, blue

structure color_point (A : Type) extends point A :=
mk :: (c : color)
-- END

The type color_point inherits all the fields from point and declares a new one c : color. Lean automatically generates a coercion from color_point to point.

import logic
open num

structure point (A : Type) :=
mk :: (x : A) (y : A)

inductive color :=
red, green, blue

structure color_point (A : Type) extends point A :=
mk :: (c : color)
-- BEGIN
definition x_plus_y (p : point num) :=
point.x p + point.y p

definition green_point : color_point num :=
color_point.mk 10 20 color.green

eval x_plus_y green_point

-- Force lean to display implicit coercions
set_option pp.coercions true

check x_plus_y green_point

example : green_point = point.mk 10 20 :=
rfl

check color_point.to_point
-- END

The coercions are named to_<parent structure>. Lean always declare functions that map the child structure to its parents. We can request Lean to not mark these functions as coercions by using the private keyword.

import logic
open num

-- BEGIN
structure point (A : Type) :=
mk :: (x : A) (y : A)

inductive color :=
red, green, blue

structure color_point (A : Type) extends private point A :=
mk :: (c : color)

-- For private parent structures we have to use the coercions explicitly.
-- If we remove color_point.to_point we get a type error.
example : color_point.to_point (color_point.mk 10 20 color.blue) = point.mk 10 20 :=
rfl
-- END

We can “rename” fields inherited from parent structures using the renaming clause.

import logic

namespace playground
-- BEGIN
structure prod (A : Type) (B : Type) :=
pair :: (pr1 : A) (pr2 : B)

-- Rename fields pr1 and pr2 to x and y respectively.
structure point3 (A : Type) extends prod A A renaming pr1→x pr2→y :=
mk :: (z : A)

check point3.x
check point3.y
check point3.z

example : point3.mk 10 20 30 = prod.pair 10 20 :=
rfl
-- END

end playground

Structures can be tagged as a class. The class-instance resolution is used to synthesize implicit arguments marked with the [] modifier. Another difference is that the structure is an instance implicit argument for every projection. The idea is that the actual structure is inferred by Lean using the class-instance resolution.

import logic

structure has_mul [class] (A : Type) :=
mk :: (mul : A → A → A)

check @has_mul.mul

-- Since [s : has_mul A] is an instance implicit argument for has_mul.mul.
-- The operation has_mul.mul can be used as a binary operator.
infixl `*`   := has_mul.mul

section
  -- The structure s in the local context is used to synthesize
  -- the implicit argument in a * b
  variables (A : Type) (s : has_mul A) (a b : A)
  check a * b
end

When a structure is marked as a class, the functions mapping a child structure to its parents is also marked as an instance unless the private modifier is used. Moreover, whenever an instances of the parent structure is required, and instance of the child structure can be provided. In the following example, we use this mechanism to “reuse” the notation defined for the parent structure with the child structure.

import logic

structure has_mul [class] (A : Type) :=
mk :: (mul : A → A → A)

-- Since [s : has_mul A] is an instance implicit argument for has_mul.mul.
-- The operation has_mul.mul can be used as a binary operator.
infixl `*`   := has_mul.mul

structure semigroup [class] (A : Type) extends has_mul A :=
mk :: (assoc : ∀ a b c, mul (mul a b) c = mul a (mul b c))

section
  -- The structure s in the local context is used to synthesize
  -- the implicit argument in a * b
  variables (A : Type) (s : semigroup A) (a b : A)
  check a * b

  -- We can see what is going by asking Lean to display implicit
  -- arguments, coercions, and disable notation.
  set_option pp.implicit true
  set_option pp.notation false
  set_option pp.coercions true

  check a * b
end

Here is a fragment of the algebraic hierarchy defined using this mechanism. In Lean, we can also inherit from multiple structures. Moreover, fields with the same name are merged. If the types do not match an error is generated. The “merge” can be avoided by using the renaming clause.

import logic

structure has_mul [class] (A : Type) :=
mk :: (mul : A → A → A)

structure has_one [class] (A : Type) :=
mk :: (one : A)

structure has_inv [class] (A : Type) :=
mk :: (inv : A → A)

infixl `*`   := has_mul.mul
postfix `⁻¹` := has_inv.inv
notation 1   := has_one.one

structure semigroup [class] (A : Type) extends has_mul A :=
mk :: (assoc : ∀ a b c, mul (mul a b) c = mul a (mul b c))

structure comm_semigroup [class] (A : Type) extends semigroup A :=
mk :: (comm : ∀ a b, mul a b = mul b a)

structure monoid [class] (A : Type) extends semigroup A, has_one A :=
mk :: (right_id : ∀ a, mul a one = a) (left_id : ∀ a, mul one a = a)

-- We can suppress := and :: when we are not declaring any new field.
structure comm_monoid [class] (A : Type) extends monoid A, comm_semigroup A

-- The common fields of monoid and comm_semigroup have been merged
print prefix comm_monoid

The renaming clause allow us to perform non-trivial merge operations such as combining an abelian group with a monoid to obtain a ring.

import logic

structure has_mul [class] (A : Type) :=
(mul : A → A → A)

structure has_one [class] (A : Type) :=
(one : A)

structure has_inv [class] (A : Type) :=
(inv : A → A)

infixl `*`   := has_mul.mul
postfix `⁻¹` := has_inv.inv
notation 1   := has_one.one

structure semigroup [class] (A : Type) extends has_mul A :=
(assoc : ∀ a b c, mul (mul a b) c = mul a (mul b c))

structure comm_semigroup [class] (A : Type) extends semigroup A renaming mul→add:=
(comm : ∀ a b, add a b = add b a)

infixl `+` := comm_semigroup.add

structure monoid [class] (A : Type) extends semigroup A, has_one A :=
(right_id : ∀ a, mul a one = a) (left_id : ∀ a, mul one a = a)

-- We can suppress := and :: when we are not declaring any new field.
structure comm_monoid [class] (A : Type) extends monoid A renaming mul→add, comm_semigroup A

structure group [class] (A : Type) extends monoid A, has_inv A :=
(is_inv : ∀ a, mul a (inv a) = one)

structure abelian_group [class] (A : Type) extends group A renaming mul→add, comm_monoid A

structure ring [class] (A : Type)
  extends abelian_group A renaming
    assoc→add.assoc
    comm→add.comm
    one→zero
    right_id→add.right_id
    left_id→add.left_id
    inv→uminus
    is_inv→uminus_is_inv,
  monoid A renaming
    assoc→mul.assoc
    right_id→mul.right_id
    left_id→mul.left_id
:=
(dist_left  : ∀ a b c, mul a (add b c) = add (mul a b) (mul a c))
(dist_right : ∀ a b c, mul (add a b) c = add (mul a c) (mul b c))