10_Structures_and_Records.org

Theorem Proving in Lean

Structures and Records

We have seen that the Calculus of Inductive Constructions includes inductive types, and the 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.

We say that a non-recursive inductive type that contains only one constructor is a structure or record. The product type is a structure/record. The dependent product type (sigma) is another example of structure/record. Whenever we defined a structure S, we usually define projection functions that allow us to “destruct” and object S and retrieve a value/field stored in it. It should not come as a surprise that the functions prod.pr1 and prod.pr2 are projections and pr stands for “projection”.

When writing programs or formalizing mathematics, it is not uncommon to define structures containing many fields. The structure command, available in Lean, automates the process. It automatically generate all projection functions, and allow us to define new structures based on previously defined ones. Lean also provides convenient notation for defining objects of a given structure.

Declaring Structures

The structure command is essentially 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:

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

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

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, 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 named mk is generated.

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.

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

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 for creating objects of struct/record types. For structures containing many fields, it is quite inconvenient to use the constructor to create objects because we have to remember the exact order the fields were defined. Therefore, Lean provides the following alternative notations for defining objects of structure/record types.

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

For example, let us define objects of the point record.

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

check {| point, x := 10, y := 20 |}
check {| point, y := 20, x := 10 |}
check ⦃ point, x := 10, y := 20 ⦄

-- order of the fields does not matter
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. Lean infers the parameters automatically for us. The parameters can be explicitly provided (if needed).

open nat
structure point (A : Type) :=
mk :: (x : A) (y : A)
-- BEGIN
check ⦃ point nat, 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 quite simple: record objects <record-obj> “provides” the value for 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 signs an error if a record object has not provided any field.

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”.

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

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

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

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, x := 10, y := 20, c := color.blue |}
          =
          {| point, x := 10, y := 20 |} :=
rfl
-- END

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

For another example, we define a structure using “multiple inheritance”, and then define an object using objects of the parent structures.

import data.nat.basic
open nat

structure s1 (A : Type) :=
(x : A) (y : A) (h : x = y)

structure s2 (A : Type) :=
(mul : A → A → A) (one : A)

structure s3 (A : Type) extends s1 A, s2 A :=
(mul_one : ∀ a : A, mul a one = a)

definition v1 : s1 nat := {| s1, x := 10, y := 10, h := rfl |}
definition v2 : s2 nat := {| s2, mul := nat.add, one := zero |}
definition v3 : s3 nat := {| s3, mul_one := add_zero, v1, v2 |}

example : s3.x v3 = 10 := rfl
example : s3.y v3 = 10 := rfl
example : s3.mul v3 = nat.add  := rfl
example : s3.one v3 = nat.zero := rfl

Structures as Classes

Structures can be tagged as a class. The class-instance resolution procedures, described in the previous chapter, 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.

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.

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, 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.

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.

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