10_Structures_and_Records.org

Theorem Proving in Lean

Structures and Records

We have seen that Lean’s foundational system includes inductive types. We have, moreover, noted that it is a remarkable fact that it is possible to construct a substantial edifice of mathematics based on nothing more than the type universes, Pi types, and inductive types; everything else follows from those. The Lean standard library contains many instances of inductive types (e.g., nat, prod, list), and even the logical connectives are defined using inductive types.

Remember that a non-recursive inductive type that contains only one constructor is called a structure or record. The product type is a structure, as is the dependent product type, that is, the Sigma type. In general, whenever we define a structure S, we usually define projection functions that allow us to “destruct” each instance of S and retrieve the values that are stored in its fields. The functions prod.pr1 and prod.pr2, which return the first and second elements of a pair, are examples of such projections.

When writing programs or formalizing mathematics, it is not uncommon to define structures containing many fields. The structure command, available in Lean, provides infrastructure to support this process. When we define a structure using this command, Lean automatically generates all the projection functions. The structure command also allows us to define new structures based on previously defined ones. Moreover, Lean provides convenient notation for defining instances of a given structure. 

Declaring Structures

The structure command is essentially a “front end” for defining inductive data types. Every structure declaration introduces a namespace with the same name. The general form is as follows:

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

Most parts are optional. Here is an example:

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

Values of type point are created using point.mk a b, and 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.

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

-- BEGIN
check point              -- a Type
check point.rec_on       -- the recursor
check point.induction_on -- then recursor to Prop
check point.destruct     -- an alias for point.rec_on
check point.x            -- a projection / field accessor
check point.y            -- a projection / field accessor
-- END

You can obtain the complete list of generated constructions using the command print prefix.

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

-- BEGIN
print prefix point
-- END

Here are some simple theorems and expressions that use the generated constructions. As usual, you can avoid the prefix point by using the command open point.

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 :=
rfl

example (A : Type) (a b : A) : y (mk a b) = b :=
rfl
-- END

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

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

check prod.mk
-- END
end hide

The keyword record is an alias for structure.

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

You can provide universe levels explicitly. The annotations in the next example force the parameters A and B to be types from the same universe, and set the return type to also be in the same universe.

namespace hide
-- BEGIN
structure prod.{u} (A : Type.{u}) (B : Type.{u}) : Type.{max 1 u} :=
(pr1 : A) (pr2 : B)

set_option pp.universes true
check prod.mk
-- END
end hide

The set_option command above instructs Lean to display the universe levels.

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.

Objects

We have been using constructors to create elements of a structure (or record) type. For structures containing many fields, this is often inconvenient, because we have to remember the order in which the fields were defined. Lean therefore provides the following alternative notations for defining elements of a structure type.

{| <structure-type> (, <field-name> := <expr>)* |}
or
⦃ <structure-type> (, <field-name> := <expr>)* ⦄

For example, we use this notation to define “points.” The order that the fields are specified does not matter, so all the expressions below define the same point.

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

check {| point, x := (10 : ℕ), y := 20 |}   -- point ℕ 
check {| point, y := (20 : ℕ), x := 10 |}
check ⦃ point, x := (10 : ℕ), y := 20 ⦄

example : {| point, x := (10 : ℕ), y := 20 |} = {| point, y := 20, x := 10 |} :=
rfl

Note that point is a parametric type, but we did not provide its parameters. Here, in each case, Lean infers that we are constructing an object of type point ℕ from the fact that one of the components is specified to be of type ℕ. Of course, the parameters can be explicitly provided with the type if needed.

open nat

structure point (A : Type) :=
mk :: (x : A) (y : A)
-- BEGIN
check ⦃ point ℕ, x := 10, y := 20 ⦄
-- END

If the value of a field is not specified, Lean tries to infer it. If the unspecified fields cannot be inferred, Lean signs an error indicating the corresponding placeholder could not be synthesized.

structure my_struct :=
mk :: (A : Type) (B : Type) (a : A) (b : B)

check {| my_struct, a := 10, b := true |}

The notation for defining record objects can also be used in pattern-matching expressions.

open nat

structure big :=
(field1 : nat) (field2 : nat)
(field3 : nat) (field4 : nat)
(field5 : nat) (field6 : nat)

definition b : big := big.mk 1 2 3 4 5 6

definition v3 : nat :=
  match b with
   {| big, field3 := v |} := v
  end

example : v3 = 3 := rfl

Record update is another common operation. It consists in creating a new record object by modifying the value of one or more fields. Lean provides a variation of the notation described above for record updates.

{| <structure-type> (, <field-name> := <expr>)* (, <record-obj>)* |}
or
⦃ <structure-type> (, <field-name> := <expr>)* (, <record-obj>)* ⦄

The semantics is simple: record objects <record-obj> provide the values for the unspecified fields. If more than one record object is provided, then they are visited in order until Lean finds one the contains the unspecified field. Lean raises an error if any of the field names remain unspecified after all the objects are visited.

open nat

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

definition p1 : point nat := {| point, x := 10, y := 20 |}
definition p2 : point nat := {| point, x := 1, p1 |}
definition p3 : point nat := {| point, y := 1, p1 |}

example : point.y p1 = point.y p2 :=
rfl

example : point.x p1 = point.x p3 :=
rfl

Inheritance

We can extend existing structures by adding new fields. This feature allow us to simulate a form of inheritance.

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)

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, so that a color_point can be provided wherever a point is expected.

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, x := 10, y := 20, c := color.green |}

eval x_plus_y green_point    -- 30

-- display implicit coercions
set_option pp.coercions true

check x_plus_y green_point    -- num

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

check color_point.to_point    -- color_point ?A → point ?A
-- END

The coercions are named to_<parent structure>. Lean always defines functions that map the child structure to its parents, but we can ask Lean not to mark these functions as coercions by using the private keyword.

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

inductive color :=
red | green | blue

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

variable f : point ℕ → bool

check f (color_point.to_point (@color_point.mk ℕ 1 2 color.red))
-- END

For private parent structures, we have to use the coercions explicitly. If we remove color_point.to_point from the above check command, we get a type error.

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

namespace hide
-- 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 hide

In the next example, we define a structure using multiple inheritance, and then define an object using objects of the parent structures.

import data.nat
open nat

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

structure rgb_val :=
(red : nat) (green : nat) (blue : nat)

structure red_green_point (A : Type) extends point A, rgb_val :=
(no_blue : blue = 0)

definition p : point nat := {| point, x := 10, y := 10, z := 20 |}
definition r : rgb_val := {| rgb_val, red := 200, green := 50, blue := 0 |}
definition rgp : red_green_point nat := {| red_green_point, p, r, no_blue := rfl |}

example : point.x rgp = 10 := rfl
example : rgb_val.red rgp = 200 := rfl

Structures as Classes

Any structure can be tagged as a class. This makes it a suitable target for the class-instance resolution procedures that were described in the previous chapter. Declaring a structure as a class also has the effect that the structure argument in each projection is tagged as an implicit argument to be inferred by type class resolution.

For example, in the definition of the has_mul structure below, the projection has_mul.mul has an implicit argument [s : has_mul A]. This means that when we write has_mul.mul a b with a b : A, type class resolution will search for a suitable instance of has_mul A, a multiplication structure associated with A. As a result, we can define the binary notation a * b, leaving the structure implicit.

namespace hide

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

check @has_mul.mul    -- Π {A : Type} [c : has_mul A], A → A → A

infixl `*`   := has_mul.mul

section
  variables (A : Type) (s : has_mul A) (a b : A)
  check a * b
end

end hide

In the last check command, the structure s in the local context is used to synthesize the implicit argument in a * b.

When a structure is marked as a class, the functions mapping a child structure to its parents are also marked as instances unless the private modifier is used. As a result, whenever an instance 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, has_mul, with the child structure, semigroup.

namespace hide

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

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
  variables (A : Type) (s : semigroup A) (a b : A)
  check a * b
end

end hide

Once again, the structure s in the local context is used to synthesize the implicit argument in a * b. We can see what is going by asking Lean to display implicit arguments, coercions, and disable notation.

namespace hide

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

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))

-- BEGIN
section
  variables (A : Type) (s : semigroup A) (a b : A)

  set_option pp.implicit true
  set_option pp.notation false

  check a * b -- @has_mul.mul A (@semigroup.to_has_mul A s) a b : A
end
-- END

end hide

Here is a fragment of the algebraic hierarchy defined using this mechanism. In Lean, you 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.

namespace hide

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)

structure comm_monoid [class] (A : Type) extends monoid A, comm_semigroup A

print prefix comm_monoid

end hide

Notice that we can suppress := and :: when we are not declaring any new fields, as is the case for the structure comm_monoid. The print prefix command shows that the common fields of monoid and comm_semigroup have been merged.

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

namespace hide

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)

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)

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

-- BEGIN
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))
-- END

end hide