Theorem Proving in Lean

Building Theories and Proofs

In this chapter, we return to a discussion of pragmatic features of Lean, which make support the development of structures theories and proofs.

More on Coercions

In Section Coercions, we discussed coercions briefly, and noted that there are restrictions on the types that one can coerce from and to. Now that we have discussed inductive types, we can be more precise.

The most basic type of coercion maps elements of one type to another. For example, a coercion from nat to int allows us to view any element n : nat as an element of int. But some coercions depend on parameters; for example, for any type A, we can view any element l : list A as an element of set A, namely, the set of elements occurring in the list. The corresponding coercion is defined on the “family” of types list A, parameterized by A.

In fact, Lean allows us to declare three kinds of coercions:

from a family of types to another family of types
from a family of types to the class of sorts
from a family of types to the class of function types

The first kind of coercion allows us to view any element of a member of the source family as an element of a corresponding member of the target family. The second kind of coercion allows us to view any element of a member of the source family as a type. The third kind of coercion allows us to view any element of the source family as a function. Let us consider each of these in turn.

In type theory terminology, an element F : Πx1 : A1, ..., xn : An, Type is called a family of types. For every sequence of arguments a1 : A1, ..., an : An, F a1 ... an is a type, so we think of F as being a family parameterized by these arguments. A coercion of the first kind is of the form

c : Πx1 : A1, ..., xn : An, y : F x1 ... xn, G b1 ... bm

where G is another famly of types, and the terms b1 ... bn depend on x1, ..., xn, y. This allows us to write f t where t is of type F a1 ... an but f expects an argument of type G y1 ... ym, for some y1 ... ym. For example, if F is list : ΠA : Type, Type, G is set ΠA : Type, Type, then a coercion c : ΠA : Type, list A → set A allows us to pass an argument of type list T for some T any time an element of type set T is expected. These are the types of coercions we considered in Section Coercions.

Lean imposes the restriction that the source and target families have to be families of inductive types, as defined in Chapter Inductive Types. Note that these include parameterized structures, as discussed in the next chapter. Because inductive types are atomic — they do not unfold, definitionally, to other expressions — this reduces ambiguity and makes it easier for Lean’s elaborator to determine when to consider a coercion. This restriction turns out to be mild in practice: most natural sources and targets for coercions are defined as inductive types, and any type T can be “wrapped” as an inductive type, by writing inductive foo (T : Type) := mk : T → foo.

Let us now consider the second kind of coercion. By the class of sorts, we mean the collection of universes Type.{i}. A coercion of the second kind is of the form

c : Πx1 : A1, ..., xn : An, F x1 ... xn → Type

where F is a family of types as above. This allows us to write s : t whenever t is of type F a1 ... an. In other words, the coercion allows us to view the elements of F a1 ... an as types. We will see in a later chapter that this is very useful when defining algebraic structures in which one component, the carrier of the structure, is a Type. For example, we can define a semigroup as follows:

structure Semigroup : Type :=
(carrier : Type)
(mul : carrier → carrier → carrier)
(mul_assoc : ∀a b c : carrier, mul (mul a b) c = mul a (mul b c))

notation a `*` b := Semigroup.mul _ a b

In other words, a semigroup consists of a type, carrier, and a multiplication, mul, with the property that the multiplication is associative. The notation command allows us to write a * b instead of Semigroup.mul S a b whenever we have a b : carrier S; notice that Lean can infer the argument S from the types of a and b. The function Semigroup.carrier maps the class Semigroup to the sort Type:

structure Semigroup : Type :=
(carrier : Type)
(mul : carrier → carrier → carrier)
(mul_assoc : ∀a b c : carrier, mul (mul a b) c = mul a (mul b c))

notation a `*` b := Semigroup.mul _ a b

-- BEGIN
check Semigroup.carrier
-- END

If we declare this function to be a coercion, then whenever we have a semigroup S : Semigroup, we can write a : S instead of a : Semigroup.carrier S:

structure Semigroup : Type :=
(carrier : Type)
(mul : carrier → carrier → carrier)
(mul_assoc : ∀a b c : carrier, mul (mul a b) c = mul a (mul b c))

notation a `*` b := Semigroup.mul _ a b

-- BEGIN
attribute Semigroup.carrier [coercion]

example (S : Semigroup) (a b : S) : a * b * a = a * (b * a) :=
!Semigroup.mul_assoc
-- END

It is the coercion that makes it possible to write (a b : S).

By the class of function types, we mean the collection of Pi types Πz : B, C. The third kind of coercion has the form

c : Πx1 : A1, ..., xn : An, y : F x1 ... xn, Πz : B, C

where F is again a family of types and B and C can depend on x1, ..., xn, y. This makes it possible to write t s whenever t is an element of F a1 ... an. In other words, the coercion enables us to view elements of F a1 ... an as functions. Continuing the example above, we can define the notion of a morphism between semigroups:

structure Semigroup : Type :=
(carrier : Type)
(mul : carrier → carrier → carrier)
(mul_assoc : ∀a b c : carrier, mul (mul a b) c = mul a (mul b c))

notation a `*` b := Semigroup.mul _ a b

attribute Semigroup.carrier [coercion]

-- BEGIN
structure morphism (S1 S2 : Semigroup) : Type :=
(mor : S1 → S2)
(resp_mul : ∀a b : S1, mor (a * b) = (mor a) * (mor b))
-- END

In other words, a morphism from S1 to S2 is a function from the carrier of S1 to the carrier of S2 (note the implicit coercion) that respects the multiplication. The projection morphism.mor takes a morphism to the underlying function:

structure Semigroup : Type :=
(carrier : Type)
(mul : carrier → carrier → carrier)
(mul_assoc : ∀a b c : carrier, mul (mul a b) c = mul a (mul b c))

notation a `*` b := Semigroup.mul _ a b

attribute Semigroup.carrier [coercion]

structure morphism (S1 S2 : Semigroup) : Type :=
(mor : S1 → S2)
(resp_mul : ∀a b : S1, mor (a * b) = (mor a) * (mor b))

-- BEGIN
check morphism.mor
-- END

As a result, it is a prime candidate for the third type of coercion.

structure Semigroup : Type :=
(carrier : Type)
(mul : carrier → carrier → carrier)
(mul_assoc : ∀a b c : carrier, mul (mul a b) c = mul a (mul b c))

notation a `*` b := Semigroup.mul _ a b

attribute Semigroup.carrier [coercion]

structure morphism (S1 S2 : Semigroup) : Type :=
(mor : S1 → S2)
(resp_mul : ∀a b : S1, mor (a * b) = (mor a) * (mor b))

-- BEGIN
attribute morphism.mor [coercion]

example (S1 S2 : Semigroup) (f : morphism S1 S2) (a : S1) :
  f (a * a * a) = f a * f a * f a :=
calc
  f (a * a * a) = f (a * a) * f a : morphism.resp_mul f
            ... = f a * f a * f a : morphism.resp_mul f
-- END

With the coercion in place, we can write f (a * a * a) instead of morphism.mor f (a * a * a). When the morphism, f, is used where a function is expected, Lean inserts the coercion.

Remember that you can create a coercion whose scope is limited to the current module using the local modifier:

structure Semigroup : Type :=
(carrier : Type)
(mul : carrier → carrier → carrier)
(mul_assoc : ∀a b c : carrier, mul (mul a b) c = mul a (mul b c))

notation a `*` b := Semigroup.mul _ a b

attribute Semigroup.carrier [coercion]

structure morphism (S1 S2 : Semigroup) : Type :=
(mor : S1 → S2)
(resp_mul : ∀a b : S1, mor (a * b) = (mor a) * (mor b))

-- BEGIN
local attribute morphism.mor [coercion]
-- END

You can also declare a persistent coercion by assigning the attribute when you define the function initially, as described in Section Coercions. Coercions that are defined in a namespace “live” in that namespace, and are made active when the namespace is opened.

Remember also that you can instruct Lean’s pretty-printer to show coercions with set_option, and you can print all the coercions in the environment using print coercions:

structure Semigroup : Type :=
(carrier : Type)
(mul : carrier → carrier → carrier)
(mul_assoc : ∀a b c : carrier, mul (mul a b) c = mul a (mul b c))

notation a `*` b := Semigroup.mul _ a b

attribute Semigroup.carrier [coercion]

structure morphism (S1 S2 : Semigroup) : Type :=
(mor : S1 → S2)
(resp_mul : ∀a b : S1, mor (a * b) = (mor a) * (mor b))

attribute morphism.mor [coercion]

-- BEGIN
theorem test (S1 S2 : Semigroup) (f : morphism S1 S2) (a : S1) :
  f (a * a * a) = f a * f a * f a :=
calc
  f (a * a * a) = f (a * a) * f a : morphism.resp_mul f
            ... = f a * f a * f a : morphism.resp_mul f

set_option pp.coercions true
check test

print coercions
-- END

Lean will also chain coercions as necessary. You can think of the coercion declarations as forming a directed graph where the nodes are families of types and the edges are the coercions between them. More precisely, each node is either a family of types, or the class of sorts, of the class of function types. The latter two are sinks in the graph. Internally, Lean automatically computes the transitive closure of this graph, in which the “paths” correspond to chains of coercions.

Elaboration and Unification

When you enter an expression like λx y z, f (x + y) z for Lean to process, you are leaving information implicit. For example, the types of x, y, and z have to be inferred from the context, the notation + may be overloaded, and there may be implicit arguments to f that need to be filled in as well.

The process of taking a partially-specified expression and inferring what is left implicit is known as elaboration. Lean’s elaboration algorithm is powerful, but at the same time, subtle and complex. Working in a system of dependent type theory requires knowing what sorts of information the elaborator can reliably infer, as well as knowing how to respond to error messages that are raised when the elaborator fails. To that end, it is helpful to have a general idea of how Lean’s elaborator works.

When Lean is parsing an expression, it first enters a preprocessing phase. First, the “holes” in a term — the unspecified values — are instantiated by metavariables ?M1, ?M2, ?M3, .... Each overloaded notation is associated with a list of choices, that is, the possible interpretations. Similarly, Lean tries to detect the points where a coercion may need to be inserted in an application s t, to make the inferred type of t match the argument type of s. These become choice points too. If one possible outcome of the elaboration procedure is that no coercion is needed, then one of the choices on the list is the identity.

After preprocessing, Lean extracts a list of constraints that need to be solved in order for the term to have a valid type. Each application term s t gives rise to a constraint T1 = T2, where t has type T1 and s has type Πx : T2, T3. Notice that the expressions T1 and T2 will often contain metavariables; they may even be metavariables themselves. Moreover, a definition of the form definition foo : T := t or a theorem of the form theorem bar : T := t generates the constraint that the inferred type of t should be T.

The elaborator now has a straightforward task: find expressions to substitute for all the metavariables so that all of the constraints are simultaneously satisifed. An assignment of terms to metavariables is known as a substitution, and the general task of finding a substitution that makes two expressions coincide is known as a unification problem. (If only one of the expressions contains metavariables, it is a special case known as a matching problem.)

Some constraints are straightforwardly handled. If f and g are distinct constants, it is clear that there is no way to unify the terms f s_1 ... s_m and g t_1 ... t_n. On the other hand, one can unify f s_1 ... s_m and f t_1 ... t_m by unifying s_1 with t_1, s_2 with t_2, and so on. If ?M is a metavariable, one can unify ?M with any term t simply by assigning t to ?M. These are all aspects of first-order unification, and such constraints are solved first.

In contrast, higher-order unification is much more tricky. Consider, for example, the expressions ?M a b and f (g a) b b. All of the following assignments to ?M are among the possible solutions:

λx y, f (g x) y y
λx y, f (g x) y b
λx y, f (g a) b y
λx y, f (g a) b b

Such problems arise in many ways. For example:

When you use induction_on x for an inductively defined type, Lean has to infer the relevant induction predicate.
When you write eq.subst e p with an equation e : a = b to convert a proposition P a to a proposition P b, Lean has to infer the relevant predicate.
When you write sigma.mk a b to build an element of Σx : A, B x from an element a : A and an element B : B a, Lean has to infer the relevant B. (And notice that there is an ambiguity; sigma.mk a b could also denote an element of Σx : A, B a, which is essentially the same as A × B a.)

In cases like this, Lean has to perform a backtracking search to find a suitable value of a higher-order metavariable. It is known that even second-order unification is generally undecidable. The algorithm that Lean uses is not complete (which means that it can fail to find a solution even if one exists) and potentially nonterminating. Nonetheless, it performs quite well in ordinary situations.

Moreover, the elaborator performs a global backtracking search over all the nondeterministic choice points introduced by overloads and coercions. In other words, the elaborator starts by trying to solve the equations with the first choice on each list. Each time the procedure fails, it analyzes the failure, and determines the next viable choice to try.

To complicate matters even further, sometimes the elaborator has to reduce terms using the CIC’s internal computation rules. For example, if it happens to be the case that f is defined to be λx, g x x, we can unify expressions f ?M and g a a by assigning ?M to a. In general, any number of computation steps may be needed to unify terms. It is computationally infeasible to try all possible reductions in the search, so, once again, Lean’s elaborator relies on an incomplete strategy.

The interaction of computation with higher-order unification is particularly knotty. For the most part, Lean avoids peforming computational reduction when trying to solve higher-order constraints. You can override this, however, by marking some symbols with the reducible attribute, as decribed in Section <a href=”Reducible Definitions”>Reducible Definitions.

The elaborator relies on additional tricks and gadgets to solve a list of constraints and instantiate metavariables. Below we will see that users can specify that some parts of terms should be filled in by tactics, which can, in turn, invoke arbitrary automated procedures. In the next chapter, we will discuss the mechanism of class inference, which can be configured to execute a prolog-like search for appropriate instantiations of an implicit argument. These can be used to help the elaborator find implicit facts on the fly, such as the fact that a particular set is finite, as well as implicit data, such as a default element of a type, or the appropriate multiplication in an algebraic structure.

It is important to keep in mind that all these mechanisms interact. The elaborator processes its list of constraints, trying to solve the easier ones first, postponing others until more information is available, and branching and backtracking at choice points. Even small proofs can generate hundreds or thousands of constraints. The elaboration process continues until the elaborator fails to solve a constraint and has exhausted all its backtracking options, or until all the constraints are solved. In the first case, it returns an error message which tries to provide the user with helpful information as to where and why it failed. In the second case, the type checker is asked to confirm that the assignment that the elaborator has found does indeed make the term type check. If all the metavariables in the original expression have been assigned, the result is a fully elaborated, type-correct expression. Otherwise, Lean flags the sources of the remaining metavariables as “placeholders” or “goals” that could not be filled.

Opaque Definitions

Because elaboration and unification are so complex, Lean provides various mechanism that control the process. To start with, a defined symbol can be transparent or opaque. This is a very strong, irrevocable decision: when a symbol is opaque, its definition definition is never unfolded, not even by the type checker in the kernel of Lean, whose job it is to determine whether or not a term is type correct.

Any identifier created by the theorem command is automatically marked as opaque, as consistent with the understanding is that all we care about is the fact that the theorem is true, which is to say, the proposition is asserts, viewed as a type, is inhabited. (If other theorems and definitions need to “see” the contents of a proof, you must declare it to be a definition instead.)

In contrast, an identifier created by the definition command is marked as transparent, by default. For example, if addition on the natural numbers were not transparent, the type checker would reject the equation in the check below as a type error:

import data.vector data.nat
open nat
check λ (v : vector nat (2+3)) (w : vector nat 5), v = w

Similarly, the following definition only type checks because id is transparent, and the type checker can establish that nat and id nat are definitionally equal.

import data.nat
definition id {A : Type} (a : A) : A := a
check λ (x : nat) (y : id nat), x = y

Lean provides us with an option, however, to declare a definition to be opaque as well. Opaque definitions are similar to regular definitions, but they are only transparent in the module (file) in which they are defined. The idea is that we can prove theorems about an opaque constant in the module in which it is defiend, but in other modules, we can only rely on these theorems. The actual definition is hidden/encapsulated, and the module designer is free to change it without affecting its “customers”.

Using opaque definitions is subtle. It would be problematic if the type checker could determine that the statement of a theorem which involves an opaque constant is correct within the module it is defined, but not outside the module. For that reason, an opaque definition is only treated as transparent inside of other opaque definitions/theorems in the same module. Here is an example:

import data.nat
opaque definition id {A : Type} (a : A) : A := a

-- these are o.k.

check λ (x : nat) (y : id nat), x = y

theorem id_eq {A : Type} (a : A) : id a = a :=
eq.refl a

definition id2 {A : Type} (a : A) : A :=
id a

-- this is rejected

/-
definition buggy_def {A : Type} (a : A) : Prop :=
∀ (b : id A), a = b
-/

The check command is type correct because it is executed in the same module as the opaque definition. The proof of id_eq is type correct, because id only needs to be transparent within the proof. Similarly, id2 is type correct because the type checker does not need to unfold id to ensure correctness. But Lean rejects buggy_def: the definition would not type check outside the module, because that requires unfolding the definition of id.

Reducible Definitions

In addition to being transparent or opaque, identifiers can be reducible or irreducible. Whereas being transparent or opaque is a fixed, irrevocable feature of an identifier, being reducible or irreducible is an attribute that can be altered. This status provides hints that govern the way the elaborator tries to solve higher-order unification problems. As with other attributes, the status of an identifier with respect to reducibility has no bearing on type checking at all, which is to say, once a fully elaborated term is type correct, marking one of the constants it contains to be reducible does not change the correctness. The type checker in the kernel of Lean ignores such attributes, and there is no problem marking a constant reducible at one point, and then irreducible later on, or vice-versa.

The purpose of the annotation is to help Lean’s unification procedure decide which declarations should be unfolded. The higher-order unification procedure has to perform case analysis, implementing a backtracking search. At various stages, the procedure has to decide whether a definition C should be unfolded or not. Here, we roughly divide this decision in two groups: simple and complex. Let us say an unfolding decision is simple if the unfolding does not require the procedure to consider an extra case split. It is complex if the unfolding produces at least one extra case, and consequently increases the search space.

Let us write reducible(C) to denote that C has been assigned the reducible attribute by a user, and irreducible(C) to denote that C has been marked irreducible. Theorems are never unfolded. For a transparent definition C, the higher-order unification procedure uses the following decision tree.

if simple unfolding decision then
  if irreducible(C) then
     do not unfold
  else
     unfold
  end
else -- complex unfolding decision
  if reducible(C) then
     unfold
  else
     do not unfold
  end
end

For an opaque definition D, the higher-order unification procedure uses the same decision tree if D was declared in the current module. Otherwise, it does not unfold D.

You can assign the reducible attribute when a symbol is defined:

definition pr1 [reducible] (A : Type) (a b : A) : A := a

The assignment persists to other modules. You can achieve the same result with the attribute command:

definition id (A : Type) (a : A) : A := a
definition pr2 (A : Type) (a b : A) : A := b

-- mark pr2 as reducible
attribute pr2 [reducible]

-- mark id and pr2 as irreducible
attribute id [irreducible]
attribute pr2 [irreducible]

The local modifier can be used to instruct Lean to limit the scope to the current module.

definition pr2 (A : Type) (a b : A) : A := b

local attribute pr2 [irreducible]

Helping the Elaborator

Because proof terms and expressions in dependent type theory can become quite complex, working in dependent type theory effectively involves relying on the system to fill in details automatically. When the elaborator fails to elaborate a term, there are two possibilities. One possibility is that there is an error in the term, and no solution is possible. In that case, your goal, as the user, is to find the error and correct it. The second possibility is that the term has a valid elaboration, but the elaborator failed to find it. In that case, you have to help the elaborator along by providing information. This section provides some guidance in both situations.

If the error message is not sufficient to allow you to identify the problem, a first strategy is to ask Lean’s pretty printer to show more information, as discussed in Section Setting Options:

set_option pp.implicit true
set_option pp.universes true
set_option pp.notation false
set_option pp.numerals false

Sometimes, the elaborator will fail with the message that the unifier has exceeded its maximum number of steps. As we noted in the last section, some elaboration problems can lead to nonterminating behavior, and so Lean simply gives up after it has reached a pre-set maximum. You can change this with the set_option command:

set_option unifier.max_steps 100000

This can sometimes help you determine whether there is an error in the term or whether the elaboration problem has simply grown too complex. In the latter case, there are steps you can take to cut down the complexity.

To start with, Lean provides a mechanism to break large elaboration problems down into simpler ones, with a proof ... qed block. Here is the sample proof from Section Examples of Propositional Validities, with additional proof ... qed annotations:

import logic

example (p q r : Prop) : p ∧ (q ∨ r) ↔ (p ∧ q) ∨ (p ∧ r) :=
iff.intro
  (assume H : p ∧ (q ∨ r),
    have Hp : p, from and.elim_left H,
    show (p ∧ q) ∨ (p ∧ r), from
    proof
      or.elim (and.elim_right H)
        (assume Hq : q,
          show (p ∧ q) ∨ (p ∧ r), from or.inl (and.intro Hp Hq))
        (assume Hr : r,
          show (p ∧ q) ∨ (p ∧ r), from or.inr (and.intro Hp Hr))
    qed)
  (assume H : (p ∧ q) ∨ (p ∧ r),
    show p ∧ (q ∨ r), from
    proof
      or.elim H
        (assume Hpq : p ∧ q,
          have Hp : p, from and.elim_left Hpq,
          have Hq : q, from and.elim_right Hpq,
          show p ∧ (q ∨ r), from and.intro Hp (or.inl Hq))
        (assume Hpr : p ∧ r,
          have Hp : p, from and.elim_left Hpr,
          have Hr : r, from and.elim_right Hpr,
          show p ∧ (q ∨ r), from and.intro Hp (or.inr Hr))
    qed)

Writing proof t qed as a subterm of a larger term breaks up the elaboration problem as follows: first, the elaborator tries to elaborate the surrounding term, independent of t. If it succeeds, that solution is used to constrain the type of t, and the elaborator processes that term independently. The net result is that a big elaboration problem gets broken down into smaller elaboration problems. This “localizes” the elaboration procedure, which has both positive and negative effects. A disadvantage is that information is insulated, so that the solution to one problem cannot inform the solution to another. The key advantage is that it can simplify the elaborator’s task. For example, backtracking points within a proof ... qed do not become backtracking points for the outside term; the elaborator either succeeds or fails to elaborate each independently. As another benefit, error messages are often improved; an error that ultimately stems from an incorrect choice of an overload in one subterm is not “blamed” on another part of the term.

In principle, one can write proof t qed for any term t, but it is used most effectively following a have or show, as in the example above. This is because have and show specify the intended type of the proof ... qed block, reducing any ambiguity about the subproblem the elaborator needs to solve.

The use of proof ... qed blocks with have and show illustrates two general strategies that can help the elaborator: first, breaking large problems into smaller problems, and, second, providing additional information. The first strategy can also be achieved by breaking a large definition into smaller definitions, or breaking a theorem with a large proof into auxiliary lemmas. Even breaking up long terms internal to a proof using auxiliary have statements can help locate the source of an error.

The second strategy, providing additional information, can be achieved by using have, show, and the typeof construct (see Section Notation, Overloads, and Coercions) to indicate expected types. More directly, it often help to specify the implicit arguments. When Lean cannot solve for the value of a metavariable corresponding to an implicit argument, you can always use @ to provide that argument explicitly. Doing so will either help the elaborator solve the elaboration problem, or help you find an error in the term that is blocking the intended solution.

Sections and Contexts

Lean provides various sectioning mechanisms that help structure a theory. We saw in Section Namespaces and Sections that the section command makes it possible not only to group together elements of a theory that go together, but also to declare variables that are inserted as arguments to theorems and definitions, as necessary. In fact, Lean has two ways of introducing local elements into the contexts, namely, as variables or as parameters. And it has two slightly different sectioning notions, namely, section and context. The goal of this section is to explain these variations.

Remember that the =point of the variable command is to declare variables for use in theorems, as in the following example:

import standard
open nat

section
  variables x y : ℕ

  definition double := x + x

  check double y
  check double (2 * x)

  theorem t1 : double x = 2 * x :=
  calc
    double x = x + x         : rfl
         ... = 1 * x + x     : one_mul
         ... = 1 * x + 1 * x : one_mul
         ... = (1 + 1) * x   : mul.right_distrib
         ... = 2 * x         : rfl

  check t1 y
  check t1 (2 * x)

  theorem t2 : double (2 * x) = 4 * x :=
  calc
    double (2 * x) = 2 * (2 * x) : t1
               ... = 2 * 2 * x   : mul.assoc
               ... = 4 * x       : rfl
end

The definition of double does not have to declare x as an argument; Lean detects the dependence and inserts it automatically. Similarly, Lean detects the occurrence of x in t1 and t2, and inserts it automatically there, too.

Notice that the variable x is generalized immediately, so that even within the section double is a function of x, and t1 and t2 depend explicitly on x. This is what makes it possible to apply double and t1 to other expressions, like y and 2 * x. It corresponds to the ordinary mathematical locution “in this section, let x and y range over the natural numbers.” Whenever x and y occur, we assume they denotes natural numbers.

Sometimes, however, we wish to fix a single value in a section. For example, in an ordinary mathematical text, we might say “in this section, we fix a type, A, and a binary relation on A.” The notion of a parameter captures this usage:

import standard

section
  parameters {A : Type} (R : A → A → Type)
  hypothesis transR : ∀{x y z}, R x y → R y z → R x z

  variables {a b c d e : A}

  theorem t1 (H1 : R a b) (H2 : R b c) (H3 : R c d) : R a d :=
  transR (transR H1 H2) H3

  theorem t2 (H1 : R a b) (H2 : R b c) (H3 : R c d) (H4 : R d e) :
    R a e :=
  transR H1 (t1 H2 H3 H4)

  check t1
  check t2
end

check t1
check t2

Here, hypothesis functions as a synonym for parameter, so that A, R, and transR are all parameters in the section. This means that, as before, they are inserted as arguments to definitions and theorems as needed. But there is a difference: within the section, t1 is an abbreviation for @t1 A R transR, which is to say, these arguments are fixed until the section is closed. This means that you do not have to specify the explicit arguments R and transR when you write t1 H2 H3 H4, in constrast to the previous example. But it also means that you cannot specify other arguments in their place. In this example, making R a parameter is appropriate if R is the only binary relation you want to reason about in the section. If you want to apply your theorems to arbitrary binary relations within the section, make R a variable.

Notice the Lean is consistent when it comes to providing alternative syntax for Prop-valued variants of declarations:

Type	Prop
constant	axiom
variable	premise
parameter	hypothesis
take	assume

Lean also allows you to use conjecture in place of hypothesis.

Lean has another sectioning construct, the context command, which is similar to the section command. The difference has to do with the way that meta-theoretic data is handled. In a section, you can declare notation, classes, instances, rewrite rules, and so on, and they persist when the section is closed. Their scope is the entire namespace in which the section resides, and when another module imports the once containing the section and opens the relevant namespace, all these objects are available. There is a catch: in a section, a piece of notation cannot depend on a parameter. After all, a notation that is defined with respect to a fixed parameter, like R above, no longer makes sense when R is no longer fixed. As a result, in a section, if you try to define notation that depends on a parameter, Lean will flag an error.

In a context, however, all meta-theoretic data is transient; it disappears when the section is closed. This is useful when you want to define notation, rewrite rules, or class instances that are used only temporarily and not exported to the outside world. There is therefore no problem making notation depend on a parameter in a context; when the context is closed, the notation goes with it.

Here is an example of how you might use a context to define the notion of equivalence modulo an integer m. Throughout the context, m is fixed, and we can write a ≡ b for equivalence modulo m. As soon as the context is closed, however, the dependence on m becomes explicit, and the notation a ≡ b is no longer valid.

import data.int
open int eq.ops

context mod_m
  parameter (m : ℤ)
  variables (a b c : ℤ)

  definition mod_equiv := m | b - a

  notation a `≡`:50 b := mod_equiv a b

  theorem mod_refl : a ≡ a := !sub_self⁻¹ ▸ !dvd_zero

  theorem mod_sym (H : a ≡ b) : b ≡ a :=
  have H1 : m | -(b - a), from iff.mp' !dvd_neg_iff_dvd H,
  int.neg_sub b a ▸ H1

  theorem mod_trans (H1 : a ≡ b) (H2 : b ≡ c) : a ≡ c :=
  have H1 : m | (c - b) + (b - a), from !dvd_add H2 H1,
  eq.subst
    (calc
      (c - b) + (b - a) = c - b + b - a  : add.assoc
                    ... = c + -b + b - a : rfl
                    ... = c - a          : neg_add_cancel_right)
    H1
end mod_m

check mod_refl
check mod_sym
check mod_trans

More on Namespaces

Recall from Section Namespaces and Sections that namespaces not only package shorter names for theorems and identifiers, but also things like notation, coercions, classes, rewrite rules, and so on. You can ask Lean to display a list of these “metaclasses”:

print metaclasses

These can be opened independently using modifiers to the open command:

import data.nat

open [declarations] nat
open [notations] nat
open [coercions] nat
open [classes] nat
open [abbreviations] nat
open [tactic-hints] nat
open [reduce-hints] nat

For example, open [coercions] nat makes the coercions in the namespace nat available (and nothing else). You can multiple metaclasses on one line:

import data.nat

open [declarations] [notations] [coercions] nat

You can also open a namespace while /excluding certain metaclasses. For example,

import data.nat

open - [notations] [coercions] nat

imports all metaclasses but [notations] and [coercions]. Remember also that you can limit the scope of an open command by putting it in a section. For example,

import data.nat

section
  open [notations] nat

  /- ... -/
end

imports notation from nat only within the section.

You can also import only certain theorems by providing an explicit list in parentheses:

import data.nat
open nat (add add.assoc add.comm)

check add
check add.assoc
check add.comm

Or, when importing theorems and definitions, you can rename them at the same time:

import data.nat
open nat (renaming add -> plus)

check plus

Or you can exclude a list of items from being imported:

import data.nat
open nat (hiding add)

Within a namespace, you can declare certain identifiers to be protected. This means that when the namespace is opened, the short version of these names are not made available:

namespace foo
  protected definition bar (A : Type) (x : A) := x
end foo

open foo
check foo.bar  -- "check bar" yields an error

In the Lean library, this is used for common names. For example, we want to write nat.rec_on, int.rec_on, and list.rec_on, even when all of these namespaces are open, to avoid ambiguity and overloading. You can always define a local abbreviation to use the shorter name:

import data.list
open list
local abbreviation induction_on := @list.induction_on
check induction_on

Alternatively, you can “unprotect” the definition by renaming it when you open the namespace:

import data.list
open list (renaming induction_on → induction_on)
check induction_on

As yet a third alternative, you obtain an alias for the shorter name by opening the namespace for that identifier only:

import data.list
open list (induction_on)
check induction_on

You may find that at times you want to cobble together a namespace, with notation, rewrite rules, or whatever, from existing namespaces. Lean provides an export command for that. The export command supports the same options and modifiers as the open command: when you export to a namespace, aliases for all the items you export become part of the new namespace. For example, below we define a new namespace, my_namespace, which includes items from bool, nat, and list.

import standard

namespace my_namespace
  export bool (hiding measurable)
  export nat
  export list
end my_namespace

check my_namespace.band
check my_namespace.add
check my_namespace.append

open my_namespace

check band
check add
check append

This makes it possible for you to define nicely prepackaged configurations for those who will use your theories later on.

Sometimes it is useful to hide auxiliary definitions and theorems from the outside world, for example, so that they do not clutter up the namespace. The private keyword allows you to do this. A private definition is always opaque, and the name of a private definition is only visible in the module/file where it was declared.

import data.nat
open nat

private definition inc (x : nat) := x + 1
private theorem inc_eq_succ (x : nat) : succ x = inc x :=
  rfl

In this example, the definition inc and theorem inc_eq_succ are not visible or accessible in modules that import this one.

Provide feedback

Saved searches

Use saved searches to filter your results more quickly

08_Building_Theories_and_Proofs.org

08_Building_Theories_and_Proofs.org

Theorem Proving in Lean

Building Theories and Proofs

More on Coercions

Elaboration and Unification

Opaque Definitions

Reducible Definitions

Helping the Elaborator

Sections and Contexts

More on Namespaces

Files

08_Building_Theories_and_Proofs.org

Latest commit

History

08_Building_Theories_and_Proofs.org

File metadata and controls

Theorem Proving in Lean

Building Theories and Proofs

More on Coercions

Elaboration and Unification

Opaque Definitions

Reducible Definitions

Helping the Elaborator

Sections and Contexts

More on Namespaces