<commit_before>#+Title: Theorem Proving in Lean
#+Author: [[http://www.andrew.cmu.edu/user/avigad][<NAME>]], [[http://leodemoura.github.io][<NAME>]], [[http://www.cs.cmu.edu/~soonhok][<NAME>]]

* Dependent Type Theory

Dependent type theory is a powerful and expressive language, allowing
us to express complex mathematical assertions, write complex hardware
and software specifications, and reason about both of these in a
natural and uniform way. Lean is based on a version of dependent type
theory known as the /Calculus of Inductive Constructions/, with a
countable hierarchy of non-cumulative universes and inductive
types. By the end of this chapter, you will understand much of what
this means.

** Simple Type Theory

As a foundation for mathematics, set theory has a simple ontology that
is rather appealing. Everything is a set, including numbers,
functions, triangles, stochastic processes, and Riemannian
manifolds. It is a remarkable fact that one can construct a rich
mathematical universe from a small number of axioms that describe a
few basic set-theoretic constructions.

But for many purposes, including formal theorem proving, it is better
to have an infrastructure that helps us manage and keep track of the
various kinds of mathematical objects we are working with. "Type
theory" gets its name from the fact that every expression has an
associated /type/. For example, in a given context, =x + 0= may
denote a natural number and =f= may denote a function on the natural
numbers.

Here are some examples of how we can declare objects in Lean and
check their types.
#+BEGIN_SRC lean
-- BEGIN
import standard
open bool nat

/- declare some constants -/

constant m : nat        -- m is a natural number
constant n : nat
constants b1 b2 : bool  -- here we declare two constants at once

/- check their types -/

check m
check n
check 0
check n + 0
check m * (n + 0)
check b1
check b1 && b2  -- bolean and
check b1 || b2  -- boolean or
check tt        -- boolean "true"
-- END

-- Try some examples of your own.

#+END_SRC

The first command, =import standard=, tells Lean that we intend to
use the standard library. The next command tells Lean that we
will use constants, facts, and notations from the theory of the
booleans and the theory of natural numbers. In technical terms, =bool=
and =nat= are /namespaces/; you will learn more about them later. To
shorten the examples, we will usually hide the relevant imports, when
they have already been made explicit in a previous example.

The =/-= and =-/= annotations indicate that the next line is a comment
block that is ignored by Lean. Similarly, two dashes indicate that the
rest of the line contains a comment that is also ignored. Comment
blocks can be nested, making it possible to "comment out" chunks of
code, just as in many programming languages.

The =constant= and =constants= commands introduce new constant symbols
into the working environment, and the =check= command asks Lean to
report their types. You should test this, and try typing some examples
of your own.

What makes simple type theory powerful is that one can build new types
out of others. For example, if =A= and =B= are types, =A → B= denotes
the type of functions from =A= to =B=, and =A × B= denotes the cartesian
product, that is, the type of ordered pairs consisting of an element
of =A= paired with an element of =B=.
#+BEGIN_SRC lean
import standard
open bool nat
-- BEGIN
open prod   -- notation for the product

constants m n : nat

constant f : nat → nat           -- type the arrow as "\to" or "\r"
constant f' : nat -> nat         -- alternative ASCII notation
constant p : nat × nat           -- type the product as "\times"
constant q : prod nat nat        -- alternative notation
constant g : nat → nat → nat
constant g' : nat → (nat → nat)  -- has the same type as g!
constant h : nat × nat → nat

constant F : (nat → nat) → nat   -- a "functional"

check f
check f n
check g m n
check g m
check pair m n
check pr1 p
check pr2 p
check pr1 (pair m n)
check pair (pr1 p) n
check F f
-- END

-- Write down some types, declare some constants, and check some expressions.

#+END_SRC

There are a couple of things to notice here. First, the application of
a function =f= to a value =x= is denoted =f x=. Second, when writing
type expressions, arrows associate to the /right/; for example, the
type of =g= is =nat → (nat → nat)=. Thus we can view =g= as a function
that takes natural numbers and returns a natural number. In type
theory, this is generally more convenient than writing =g= as a
function that takes a pair of natural numbers as input, and returns a
natural number as output. For example, it allows us to "partially
apply" the function =g=. The example above shows that =g m= has type
=nat → nat=, that is, the function that "waits" for a second argument,
=n=, and then returns =g m n=. Taking a function =h= of type =nat ×
nat → nat= and "redefining" it to look like =g= is a process known as
/currying/, something we will come back to below.

By now you may also have guessed that, in Lean, =pair m n= denotes the
ordered pair of =m= and =n=, and if =p= is a pair, =pr1 p= and =pr2 p=
denote the two projections.

** Types as Objects

One way in which Lean's dependent type theory extends simple type
theory is that types themselves -- entities like =nat= and =bool= --
are first-class citizens, which is to say that they themselves are
objects of study. For that to be the case, each of them also has to
have a type.
#+BEGIN_SRC lean
import standard
open bool nat prod

-- BEGIN
check nat
check bool
check nat → bool
check nat × bool
check nat → nat
check nat × nat → nat
check nat → nat → nat
check nat → (nat → nat)
check nat → nat → bool
check (nat → nat) → nat
-- END
#+END_SRC

We see that each one of the expressions above is an object of type
=Type=. We can also declare new constants and constructors for types:
#+BEGIN_SRC lean
import standard
open bool nat

-- BEGIN
constants A B : Type
constant F : Type → Type
constant G : Type → Type → Type

check A
check F A
check F nat
check G A
check G A B
check G A nat
-- END
#+END_SRC
Indeed, we have already seen an example of a function of type =Type →
Type → Type=, namely, the Cartesian product.
#+BEGIN_SRC lean
import data.nat data.prod
open nat prod

-- BEGIN
constants A B : Type

check prod
check prod A
check prod A B
check prod nat nat
-- END
#+END_SRC
Here is another example: given any type =A=, the type =list A= denotes
the type of lists of elements of type =A=.
#+BEGIN_SRC lean
import data.list
open list

constant A : Type

check list
check list A
check list nat
#+END_SRC

We will see that the ability to treat type constructors as instances
of ordinary mathematical functions is a powerful feature of dependent
type theory.

For those more comfortable with set-theoretic foundations, it may be
helpful to think of a type as nothing more than a set, in which case,
the elements of the type are just the elements of the set. But there
is a circularity lurking nearby. =Type= itself is an expression like
=nat=; if =nat= has a type, shouldn't =Type= have a type as well?
#+BEGIN_SRC lean
check Type
#+END_SRC
Lean's output seems to indicates that =Type= is an element of
itself. But this is misleading. Russell's paradox shows that it is
inconsistent with the other axioms of set theory to assume the
existence of a set of all sets, and one can derive a similar paradox in
dependent type theory. So, is Lean inconsistent?

What is going on is that Lean's foundational fragment actually has a
hierarchy of types, =Type.{1} : Type.{2} : Type.{3} : ....= Think of
=Type.{1}= as a universe of "small" or "ordinary" types. =Type.{2}= is
then a larger universe of types, which contains =Type.{1}= as an
element. When we declare a constant =A : Type=, Lean implicitly
creates a variable =l=, and declares =A : Type.{l}=. In other words,
=A= is a type in some unspecified universe. Lean silently keeps track
of implicit universe levels, but you can ask Lean's pretty printer to
make this information explicit. You can even specify universe levels
explicitly.
#+BEGIN_SRC lean
constants A B : Type
check A
check B
check Type
check Type → Type

set_option pp.universes true    -- display universe information

check A
check B
check Type
check Type → Type

universe variable u
constant C : Type.{u}
check C
check A → C
check Type → C
#+END_SRC

In ordinary situations, however, you can ignore the universe
parameters and simply write =Type=. For most purposes, it suffices to
leave the "universe management" to Lean.

** Function Abstraction and Evaluation

We have seen that if we have =m n : nat=, then we have =pair m n : nat
× nat=. This gives us a way of creating pairs of natural numbers.
Conversely, if we have =p : nat × nat=, then we have =pr1 p : nat= and
=pr2 : nat=. This gives us a way of "using" a pair, by extracting its
two components.

We already know how to "use" a function =f : A → B=: given =a : A=, we
have =f a : B=. But how do we create a function from another
expression?

The companion to application is a process known as "abstraction," or
"lambda abstraction." Suppose that by temporarily postulating a
variable =x : A= we can construct an expression =t : B=. Then the
expression =fun x : A, t=, or, equivalently, =λx : A, t=, is an object
of type =A → B=. Think of this as the function from =A= to =B= which
maps any value =x= to the value =t=, which depends on =x=. For
example, in mathematics it is common to say "let =f= be the function
which maps any natural number =x= to =x + 5=." The expression =λx :
nat, x + 5= is just a symbolic representation of the right-hand side
of this assignment.
#+BEGIN_SRC lean
import data.nat data.bool
open nat bool

check fun x : nat, x + 5
check λx : nat, x + 5
#+END_SRC
Here are some more abstract examples:
#+BEGIN_SRC lean
import data.bool
-- BEGIN
constants A B  : Type
constants a1 a2 : A
constants b1 b2 : B

constant f : A → A
constant g : A → B
constant h : A → B → A
constant p : A → A → bool

check fun x : A, f x
check λx : A, f x
check λx : A, f (f x)
check λx : A, h x b1
check λy : B, h a1 y
check λx : A, p (f (f x)) (h (f a1) b2)
check λx : A, λy : B, h (f x) y
check λ(x : A) (y : B), h (f x) y
check λx y, h (f x) y
-- END
#+END_SRC
Lean interprets the final three examples as the same expression; in
the last expression, Lean infers the type of =x= and =y= from the
types of =f= and =h=.

Be sure to try writing some expressions of your own. Some
mathematically common examples of operations of functions can be
described in terms of lambda abstraction:
#+BEGIN_SRC lean
constants A B C : Type
constant f : A → B
constant g : B → C
constant b: B

check λx : A, x        -- the identity function on A
check λx : A, b        -- a constant function on A
check λx : A, g (f x)  -- the composition of g and f
check λx, g (f x)      -- (Lean can figure out the type of x)

-- we can abstract any of the constants in the previous definitions

check λb : B, λx : A, x
check λ(b : B) (x : A), x    -- equivalent to the previous line
check λ(g : B → C) (f : A → B) (x : A), g (f x)

-- we can even abstract over the type

check λ(A B : Type) (b : B) (x : A), x
check λ(A B C : Type) (g : B → C) (f : A → B) (x : A), g (f x)
#+END_SRC

Think about what these expressions mean. The last, for example,
denotes the function that takes three types, =A=, =B=, and =C=, and
two functions, =g : B → C= and =f : A → C=, and returns the
composition of =g= and =f=. Within a lambda expression =λx : A, t=,
the variable =x= is a "bound variable": it is really a placeholder,
whose "scope" does not extend beyond =t=. For example, the variable
=b= in the expression =λ(b : B) (x : A), x= has nothing to do with the
constant =b= declared earlier. In fact, the expression denotes the
same function as =λ(u : B) (z : A), u=. Formally, the expressions that
are the same up to a renaming of bound variables are called /alpha
equivalent/, and are considered morally "the same". Lean recognizes
this equivalence.

Notice that applying an term =t : A → B= to a term =s : A= yields an
expression =t s : B=. Returning to the previous example and renaming
bound variables for clarity, notice the types of the following
expressions:
#+BEGIN_SRC lean
constants A B C : Type
constant f : A → B
constant g : B → C
constant h : A → A
constants (a : A) (b : B)

check (λx : A, x) a
check (λx : A, b) a
check (λx : A, b) (h a)
check (λx : A, g (f x)) (h (h a))

check (λv u x, v (u x)) g f a

check (λ(Q R S : Type) (v : R → S) (u : Q → R) (x : Q), v (u x)) A B C g f a
#+END_SRC

As expected, the expression =(λx : A, x) a= has type =A=. In fact,
more should be true: applying the expression =(λx : A, x)= to =a=
should "return" the value =a=. And, indeed, it does:
#+BEGIN_SRC lean
constants A B C : Type
constant f : A → B
constant g : B → C
constant h : A → A
constants (a : A) (b : B)

eval (λx : A, x) a
eval (λx : A, b) a
eval (λx : A, b) (h a)
eval (λx : A, g (f x)) (h (h a))

eval (λv u x, v (u x)) g f a

eval (λ(Q R S : Type) (v : R → S) (u : Q → R) (x : Q), v (u x)) A B C g f a
#+END_SRC

The command =eval= tells Lean to /evaluate/ an expression. The process
of simplifying an expression =(λx, t)s= to =t[s/x]= -- that is, =t=
with =s= substituted for the variable =x= -- is known as /beta
reduction/, and two terms the beta reduce to a common term are called
/beta equivalent/. But the =eval= command carries out other forms of
reduction as well:
#+BEGIN_SRC lean
import data.nat data.prod data.bool
open nat prod bool

constants m n : nat
constant b : bool

print "reducing pairs"
eval pr1 (pair m n)
eval pr2 (pair m n)

print "reducing boolean expressions"
eval tt && ff
eval b && ff

print "reducing arithmetic expressions"
eval 0 + n
eval 2 + n
eval 2 + 3
#+END_SRC
In a later chapter, we will explain how these terms are evaluated. For
now, we only wish to emphasize that this is an important feature of
the Calculus of Inductive Constructions: every term has a
computational behavior, and supports a notion of reduction, or
/normalization/. In principle, two terms that reduce to the same value
are considered morally "the same" by the underlying logical framework, and
Lean does its best to recognize and support these identifications.

** Introducing Definitions

Declaring constants in the Lean environment is a good way to postulate
new objects to experiment with, but most of the time what we really
want to do is /define/ new objects in Lean, and prove things about
them. The =definition= command provides the means to do so:
#+BEGIN_SRC lean
constants A B C : Type
constants (a : A) (f : A → B) (g : B → C) (h : A → A)

definition gfa : C := g (f a)

check gfa
print definition gfa

-- We can omit the type when Lean can figure it out.
definition gfa' := g (f a)

print definition gfa'

definition gfha := g (f (h a))

print definition gfha

definition g_comp_f : A → C := λx, g (f x)

print definition g_comp_f
#+END_SRC

The general form of a definition is ~definition foo : T := bar~. Lean
can usually infer the type =T=, but it is often a good idea to write
it explicity. This clarifies your intention, and Lean will flag an
error if the right-hand side of the definition does not have the right
type.

Because function definitions are so common, Lean provides an
alternative notation, which puts the abstracted variables before the
colon and omits the lambda:
#+BEGIN_SRC lean
constants A B C : Type
constants (g : B → C) (f : A → B)

-- BEGIN
definition g_comp_f (x : A) : C := g (f x)

print definition g_comp_f
-- END
#+END_SRC
Here are some more examples of definitions, this time in the context
of arithmetic:
#+BEGIN_SRC lean
import data.nat
open nat

constants (m n : nat) (p q : bool)

definition m_plus_n : nat := m + n

check m_plus_n
print definition m_plus_n

-- Again, Lean can infer the type
definition m_plus_n' := m + n

print definition m_plus_n'

definition double (x : nat) : nat := x + x

print definition double
check double m
check double 3
eval double m
eval double 3

definition square (x : nat) := x * x

print definition square
eval square m
eval square 3

definition do_twice (f : nat → nat) (x : nat) : nat := f (f x)

eval do_twice double 2
#+END_SRC
As an exercise, we encourage you to use =do_twice= and =double= to
define functions that quadruple their input, and multiply the input
by 8. As a further exercise, we encourage you to try defining a
function =Do_Twice : (nat → nat) → (nat → nat)= which iterates /its/
argument twice, so that =Do_Twice do_twice= a function which iterates
/its/ input four times, and evaluate =Do_Twice do_twice double 2=.

Above, we discussed the process of "currying" a function, that is,
taking a function =f (a, b)= that takes an ordered pair as an
argument, and recasting it as a function =f' a b= which takes two
arguments successively. As another exercise, we encourage you to
complete the following definitions, which "curry" and "uncurry" a
function.
#+BEGIN_SRC lean
import data.prod
open prod

definition curry (A B C : Type) (f : A × B → C) : A → B → C := sorry

definition uncurry (A B C : Type) (f : A → B → C) : A × B → C := sorry
#+END_SRC


** Namespaces and Sections

This is a good place to introduce some organizational features of Lean
that are not a part of the axiomatic framework /per se/, but make it
possible to work in the framework more efficiently.

Lean provides us with the ability to group definitions, notations, and
other information into nested, hierarchical /namespaces/:
#+BEGIN_SRC lean
namespace foo

  constant A : Type
  constant a : A
  constant f : A → A

  definition fa : A := f a
  definition ffa : A := f (f a)

  print "inside foo"

  check A
  check a
  check f
  check fa
  check ffa
  check foo.A
  check foo.fa

end foo

print "outside the namespace"

-- check A  -- error
-- check fa -- error
check foo.A
check foo.a
check foo.f
check foo.fa
check foo.ffa

open foo

print "opened foo"

check A
check a
check fa
check foo.fa
#+END_SRC

When we declare that we are working in the namespace =foo=, every
identifier we declare has a full name with prefix "=foo.=" Within the
namespace, we can refer to identifiers by their shorter names, but
once we end the namespace, we have to use the longer names.

The =open= command brings the shorter names into the current
context. Often, when we =import= a module, we will want to open one or
more of the namespaces it contains, to have access to the short
identifiers, notations, and so on. But sometimes we will want to leave
this information hidden, for example, when they conflict with
identifiers and notations in another namespace we want to use. Thus
namespaces give us a way to manage our working environment.

For example, when we work with the natural numbers, we usually want
access to the function =plus=, and its associated notation, =+=. The
command =open nat= makes these available to us.
#+BEGIN_SRC lean
import data.nat   -- imports the nat module

check nat.add
check nat.zero

open nat -- imports short identifiers, notations, etc. into the context

check add
check zero

constants m n : nat

check m + n
check 0
check m + 0
#+END_SRC

Namespaces can be nested:
#+BEGIN_SRC lean
namespace foo

  constant A : Type
  constant a : A
  constant f : A → A

  definition fa : A := f a

  namespace bar
    definition ffa : A := f (f a)

    check fa
    check ffa
  end bar

  check fa
  check bar.ffa
end foo

check foo.fa
check foo.bar.ffa

open foo

check fa
check bar.ffa
#+END_SRC
Namespaces that have been closed can later be reopened (even in
another "module," that is, another file):
#+BEGIN_SRC lean
namespace foo
  constant A : Type
  constant a : A
  constant f : A → A

  definition fa : A := f a
end foo

check foo.A
check foo.f

namespace foo
  definition ffa : A := f (f a)
end foo
#+END_SRC

The notion of a /section/ provides another way of managing
information. When we develop a theory, we will often reuse variables
in successive definitions:
#+BEGIN_SRC lean
definition compose (A B C : Type) (g : B → C) (f : A → B) (x : A) :
  C := g (f x)

definition do_twice (A : Type) (h : A → A) (x : A) : A := h (h x)

definition do_thrice (A : Type) (h : A → A) (x : A) : A := h (h (h x))

check compose
check do_twice
check do_thrice
#+END_SRC
With a section, you can declare the variables once and for all:
#+BEGIN_SRC lean
section useful
  variables (A B C : Type)
  variables (g : B → C) (f : A → B) (h : A → A)
  variable x : A

  definition compose := g (f x)
  definition do_twice := h (h x)
  definition do_thrice := h (h (h x))

  check compose
  check do_twice
  check do_thrice
end useful

print definition compose
print definition do_twice
print definition do_thrice
#+END_SRC

The =variable= and =variables= commands look like the =constant= and
=constants= commands we used above, but there is an important
difference: rather than creating permanent entities, the declarations
tell the Lean to insert the variables as bound variables in
definitions that refer to them. Lean is smart enough to figure out
which variables are used explictly or implicity in a definition, so
the later definitions of =compose=, =do_twice=, and =do_thrice= have
exactly the same effect as the earlier ones. When the section is
closed, the variables go out of scope, and become nothing more than a
distant memory.

You do not have to name a section, which is to say, you can use an
anonymous =section= / =end= pair. But if you do name a section, you
have to close it using the same name.

Like namespaces, nested sections have to be closed in the order they
are opened. Also, a namespace cannot be opened within a section;
namespaces have to live on the outer levels.

Namespaces and sections serve different purposes: namespaces organize
data and sections declare variables for insertion in theorems. A
namespace can be viewed as a special kind of section, however. In
particular, you can use the =variable= command in a namespace, in
which case the variables you declare remain in scope until the
namespace is closed.

If you use the =open= command at the "top level" of a file to import
information from a namespace, that information remains in the context
until the end of the file. But if you use the =open= command within a
section or namespace, the information remains in the context until
that section or namespace is closed.

** Dependent Types

You now have rudimentary ways of defining functions and objects in Lean,
and we will gradually introduce you to many more. Our ultimate goal in
Lean is to /prove/ things about the objects we define, and the next
chapter will introduce you to Lean's mechanisms for stating theorems
and constructing proofs. Meanwhile, let us remain on the topic of
defining objects in dependent type theory for a just a moment longer,
in order to explain what makes dependent type theory /dependent/, and
why that is useful.

The short answer is that what makes dependent type theory dependent is
that types can depend on parameters. You have already seen a nice
example of this: the type =list A= depends on the argument =A=, and
this dependence is what distinguishes =list nat= and =list bool=. For
another example, consider the type =vec A n=, the type of vectors of
elements of =A= of length =n=. This type depends on /two/ parameters:
the type =A : Type= of the elements in the vector and the length =n :
nat=.

Suppose we wish to write a function =cons= which inserts a new element
at the head of a list. What type should =cons= have? Such a function
is /polymorphic/: we expect the =cons= function for =nat=, =bool=, or
an arbitrary type =A= to behave the same way. So it makes sense to
take the type to be the first argument to =cons=, so that for any
type, =A=, =cons A= is the insertion function for lists of type
=A=. In other words, for every =A=, =cons A= is the function that
takes an element =a : A= and a list =l : list A=, and returns a new
list, so we have =cons a l : list A=.

It is clear that =cons A= should have type =A → list A → list A=. But
what type should =cons= have? A first guess might be =Type → A → list
A → list A=, but, on reflection, this does not make sense: the =A= in
this expression does not refer to anything, whereas it should refer to
the argument of type =Type=. In other words, /assuming/ =A : Type= is
the first argument to the function, the type of the next two elements
are =A= and =list A=. These types vary depending on the first
argument, =A=.

This is an instance of a /Pi type/ in dependent type theory. Given
=A : Type= and =B : A → Type=, think of =B= as a family of types over
=A=, that is, a type =B a= for each =a : A=. In that case, the type
=Πx : A, B x= denotes the type of functions =f= with the property
that, for each =a : A=, =f a= is an element of =B a=. In other words,
the type of the value returned by =f= depends on its input.

Notice that =Πx : A, B= makes sense for any expression =B :
Type=. When the value of =B= depends on =x=, =Πx : A, B= denotes a
dependent function type, as above. When =B= doesn't depend on =x=,
=Πx : A, B= is no different from the type =A → B=. Indeed, in
dependent type theory (and in Lean), the Pi construction is
fundamental, and =A → B= is nothing more than notation for =Πx : A, B=
when =B= does not depend on =A=.

Returning to the example of lists, we can model some basic list
operations as follows:
#+BEGIN_SRC lean
namespace hide
-- BEGIN
constant list : Type → Type

namespace list
  constant cons : ΠA : Type, A → list A → list A
  constant nil : ΠA : Type, list A            -- the empty list
  constant head : ΠA : Type, list A → A       -- returns the first element
  constant tail : ΠA : Type, list A → list A  -- returns the remainder
  constant append : ΠA : Type, list A → list A → list A -- concatenates two lists
end list
-- END
end hide
#+END_SRC
In fact, these are essentially the types of the defined objects in the
list library (we will explain the =@= symbol and the difference
between the round and curly brackets momentarily).
#+BEGIN_SRC lean
import data.list
open list

check list

check @cons
check @nil
check @head
check @tail
check @append
#+END_SRC

Vector operations are handled similarly:
#+BEGIN_SRC lean
import data.nat
open nat

constant vec : Type → nat → Type

namespace vec
  constant empty : ΠA : Type, vec A 0
  constant cons : Π(A : Type) (n : nat), A → vec A n → vec A (n + 1)
  constant append : Π(A : Type) (n m : nat), vec A m → vec A n → vec A (n + m)
end vec
#+END_SRC

In the coming chapters, you will come across many instances of
dependent types. Here we will mention just one more important and
illustrative example, the /Sigma types/, =Σx : A, B x=, sometimes also
known as /dependent pairs/. These are, in a sense, companions to the
Pi types. The type =Σx : A, B x= denotes the type of pairs =sigma.mk a b=
where =a : A= and =b : B a=. We can also use angle brackets =<a, b>= as notation
for =sigma a b=. We can input angle brackets using the shortcuts =\<= and =\>=.
Just as Pi types =Πx : A, B x= generalize
the notion of a function type =A → B=, Sigma types =Σx : A, B x=
generalize the cartesian product =A × B=: in the expression =sigma.mk a b=,
the type of the second element of the pair, =b : B a=, depends on
the first element of the pair, =a : A=.
#+BEGIN_SRC lean
import data.sigma
open sigma

constant A : Type
constant B : A → Type
constant a : A
constant b : B a

check sigma.mk a b
check pr1 (sigma.mk a b)
check pr2 (sigma.mk a b)

eval pr1 (sigma.mk a b)
eval pr2 (sigma.mk a b)
#+END_SRC

** Implicit Arguments

Suppose we have an implementation of lists as described above.
#+BEGIN_SRC lean
namespace hide
-- BEGIN
constant list : Type → Type

namespace list
  constant cons : ΠA : Type, A → list A → list A
  constant nil : ΠA : Type, list A
  constant append : ΠA : Type, list A → list A → list A
end list
-- END
end hide
#+END_SRC
Then, given a type =A=, some elements of =A=, and some lists of
elements of =A=, we can construct new lists using the constructors.
#+BEGIN_SRC lean
namespace hide
constant list : Type → Type

namespace list
  constant cons : ΠA : Type, A → list A → list A
  constant nil : ΠA : Type, list A
  constant append : ΠA : Type, list A → list A → list A
end list

-- BEGIN
open list

constant  A : Type
constant  a : A
constants l1 l2 : list A

check cons A a (nil A)
check append A (cons A a (nil A)) l1
check append A (append A (cons A a (nil A)) l1) l2
-- END
end hide
#+END_SRC

Because the constructors are polymorphic over types, we have to insert
the type =A= as an argument repeatedly. But this information is
redundant: one can infer the argument =A= in =cons A a (nil A)= from
the fact that the second argument, =a=, has type =A=. One can
similarly infer the argument in =nil A=, not from anything else in
that expression, but from the fact that it is sent as an argument to
the function =cons=, which expects an element of type =list A= in that
position.

This is a central feature of dependent type theory: terms carry a lot
of information, and often some of that information can be inferred
from the context. In Lean, one uses an underscore, =_=, to specify
that the system should fill in the information automatically. This is
known as an "implicit argument".
#+BEGIN_SRC lean
namespace hide
constant list : Type → Type

namespace list
  constant cons : ΠA : Type, A → list A → list A
  constant nil : ΠA : Type, list A
  constant append : ΠA : Type, list A → list A → list A
end list

open list

constant  A : Type
constant  a : A
constants l1 l2 : list A

-- BEGIN
check cons _ a (nil _)
check append _ (cons _ a (nil _)) l1
check append _ (append _ (cons _ a (nil _)) l1) l2
-- END
end hide
#+END_SRC

It is still tedious, however, to type all these underscores.  When a
function takes an argument that can generally be inferred from
context, Lean allows us to specify that this argument should, by
default, be left implicit.

#+BEGIN_SRC lean
constant list : Type → Type

namespace list
  constant cons : Π{A : Type}, A → list A → list A
  constant nil : Π{A : Type}, list A
  constant append : Π{A : Type}, list A → list A → list A
end list

open list

constant  A : Type
constant  a : A
constants l1 l2 : list A

-- BEGIN
check cons a nil
check append (cons a nil) l1
check append (append (cons a nil) l1) l2
-- END
#+END_SRC

All that has changed are the curly braces around =A : Type= in the
declaration of the constants. We can also use this device in variable
declarations and function definitions:
#+BEGIN_SRC lean
-- the polymorphic identity function<commit_msg>fix(02_Dependent_Type_Theory): avoid clashes with standard library<commit_after>#+Title: Theorem Proving in Lean
#+Author: [[http://www.andrew.cmu.edu/user/avigad][<NAME>]], [[http://leodemoura.github.io][<NAME>]], [[http://www.cs.cmu.edu/~soonhok][<NAME>]]

* Dependent Type Theory

Dependent type theory is a powerful and expressive language, allowing
us to express complex mathematical assertions, write complex hardware
and software specifications, and reason about both of these in a
natural and uniform way. Lean is based on a version of dependent type
theory known as the /Calculus of Inductive Constructions/, with a
countable hierarchy of non-cumulative universes and inductive
types. By the end of this chapter, you will understand much of what
this means.

** Simple Type Theory

As a foundation for mathematics, set theory has a simple ontology that
is rather appealing. Everything is a set, including numbers,
functions, triangles, stochastic processes, and Riemannian
manifolds. It is a remarkable fact that one can construct a rich
mathematical universe from a small number of axioms that describe a
few basic set-theoretic constructions.

But for many purposes, including formal theorem proving, it is better
to have an infrastructure that helps us manage and keep track of the
various kinds of mathematical objects we are working with. "Type
theory" gets its name from the fact that every expression has an
associated /type/. For example, in a given context, =x + 0= may
denote a natural number and =f= may denote a function on the natural
numbers.

Here are some examples of how we can declare objects in Lean and
check their types.
#+BEGIN_SRC lean
-- BEGIN
import standard
open bool nat

/- declare some constants -/

constant m : nat        -- m is a natural number
constant n : nat
constants b1 b2 : bool  -- here we declare two constants at once

/- check their types -/

check m
check n
check 0
check n + 0
check m * (n + 0)
check b1
check b1 && b2  -- bolean and
check b1 || b2  -- boolean or
check tt        -- boolean "true"
-- END

-- Try some examples of your own.

#+END_SRC

The first command, =import standard=, tells Lean that we intend to
use the standard library. The next command tells Lean that we
will use constants, facts, and notations from the theory of the
booleans and the theory of natural numbers. In technical terms, =bool=
and =nat= are /namespaces/; you will learn more about them later. To
shorten the examples, we will usually hide the relevant imports, when
they have already been made explicit in a previous example.

The =/-= and =-/= annotations indicate that the next line is a comment
block that is ignored by Lean. Similarly, two dashes indicate that the
rest of the line contains a comment that is also ignored. Comment
blocks can be nested, making it possible to "comment out" chunks of
code, just as in many programming languages.

The =constant= and =constants= commands introduce new constant symbols
into the working environment, and the =check= command asks Lean to
report their types. You should test this, and try typing some examples
of your own.

What makes simple type theory powerful is that one can build new types
out of others. For example, if =A= and =B= are types, =A → B= denotes
the type of functions from =A= to =B=, and =A × B= denotes the cartesian
product, that is, the type of ordered pairs consisting of an element
of =A= paired with an element of =B=.
#+BEGIN_SRC lean
import standard
open bool nat
-- BEGIN
open prod   -- notation for the product

constants m n : nat

constant f : nat → nat           -- type the arrow as "\to" or "\r"
constant f' : nat -> nat         -- alternative ASCII notation
constant p : nat × nat           -- type the product as "\times"
constant q : prod nat nat        -- alternative notation
constant g : nat → nat → nat
constant g' : nat → (nat → nat)  -- has the same type as g!
constant h : nat × nat → nat

constant F : (nat → nat) → nat   -- a "functional"

check f
check f n
check g m n
check g m
check pair m n
check pr1 p
check pr2 p
check pr1 (pair m n)
check pair (pr1 p) n
check F f
-- END

-- Write down some types, declare some constants, and check some expressions.

#+END_SRC

There are a couple of things to notice here. First, the application of
a function =f= to a value =x= is denoted =f x=. Second, when writing
type expressions, arrows associate to the /right/; for example, the
type of =g= is =nat → (nat → nat)=. Thus we can view =g= as a function
that takes natural numbers and returns a natural number. In type
theory, this is generally more convenient than writing =g= as a
function that takes a pair of natural numbers as input, and returns a
natural number as output. For example, it allows us to "partially
apply" the function =g=. The example above shows that =g m= has type
=nat → nat=, that is, the function that "waits" for a second argument,
=n=, and then returns =g m n=. Taking a function =h= of type =nat ×
nat → nat= and "redefining" it to look like =g= is a process known as
/currying/, something we will come back to below.

By now you may also have guessed that, in Lean, =pair m n= denotes the
ordered pair of =m= and =n=, and if =p= is a pair, =pr1 p= and =pr2 p=
denote the two projections.

** Types as Objects

One way in which Lean's dependent type theory extends simple type
theory is that types themselves -- entities like =nat= and =bool= --
are first-class citizens, which is to say that they themselves are
objects of study. For that to be the case, each of them also has to
have a type.
#+BEGIN_SRC lean
import standard
open bool nat prod

-- BEGIN
check nat
check bool
check nat → bool
check nat × bool
check nat → nat
check nat × nat → nat
check nat → nat → nat
check nat → (nat → nat)
check nat → nat → bool
check (nat → nat) → nat
-- END
#+END_SRC

We see that each one of the expressions above is an object of type
=Type=. We can also declare new constants and constructors for types:
#+BEGIN_SRC lean
import standard
open bool nat

-- BEGIN
constants A B : Type
constant F : Type → Type
constant G : Type → Type → Type

check A
check F A
check F nat
check G A
check G A B
check G A nat
-- END
#+END_SRC
Indeed, we have already seen an example of a function of type =Type →
Type → Type=, namely, the Cartesian product.
#+BEGIN_SRC lean
import data.nat data.prod
open nat prod

-- BEGIN
constants A B : Type

check prod
check prod A
check prod A B
check prod nat nat
-- END
#+END_SRC
Here is another example: given any type =A=, the type =list A= denotes
the type of lists of elements of type =A=.
#+BEGIN_SRC lean
import data.list
open list

constant A : Type

check list
check list A
check list nat
#+END_SRC

We will see that the ability to treat type constructors as instances
of ordinary mathematical functions is a powerful feature of dependent
type theory.

For those more comfortable with set-theoretic foundations, it may be
helpful to think of a type as nothing more than a set, in which case,
the elements of the type are just the elements of the set. But there
is a circularity lurking nearby. =Type= itself is an expression like
=nat=; if =nat= has a type, shouldn't =Type= have a type as well?
#+BEGIN_SRC lean
check Type
#+END_SRC
Lean's output seems to indicates that =Type= is an element of
itself. But this is misleading. Russell's paradox shows that it is
inconsistent with the other axioms of set theory to assume the
existence of a set of all sets, and one can derive a similar paradox in
dependent type theory. So, is Lean inconsistent?

What is going on is that Lean's foundational fragment actually has a
hierarchy of types, =Type.{1} : Type.{2} : Type.{3} : ....= Think of
=Type.{1}= as a universe of "small" or "ordinary" types. =Type.{2}= is
then a larger universe of types, which contains =Type.{1}= as an
element. When we declare a constant =A : Type=, Lean implicitly
creates a variable =l=, and declares =A : Type.{l}=. In other words,
=A= is a type in some unspecified universe. Lean silently keeps track
of implicit universe levels, but you can ask Lean's pretty printer to
make this information explicit. You can even specify universe levels
explicitly.
#+BEGIN_SRC lean
constants A B : Type
check A
check B
check Type
check Type → Type

set_option pp.universes true    -- display universe information

check A
check B
check Type
check Type → Type

universe variable u
constant C : Type.{u}
check C
check A → C
check Type → C
#+END_SRC

In ordinary situations, however, you can ignore the universe
parameters and simply write =Type=. For most purposes, it suffices to
leave the "universe management" to Lean.

** Function Abstraction and Evaluation

We have seen that if we have =m n : nat=, then we have =pair m n : nat
× nat=. This gives us a way of creating pairs of natural numbers.
Conversely, if we have =p : nat × nat=, then we have =pr1 p : nat= and
=pr2 : nat=. This gives us a way of "using" a pair, by extracting its
two components.

We already know how to "use" a function =f : A → B=: given =a : A=, we
have =f a : B=. But how do we create a function from another
expression?

The companion to application is a process known as "abstraction," or
"lambda abstraction." Suppose that by temporarily postulating a
variable =x : A= we can construct an expression =t : B=. Then the
expression =fun x : A, t=, or, equivalently, =λx : A, t=, is an object
of type =A → B=. Think of this as the function from =A= to =B= which
maps any value =x= to the value =t=, which depends on =x=. For
example, in mathematics it is common to say "let =f= be the function
which maps any natural number =x= to =x + 5=." The expression =λx :
nat, x + 5= is just a symbolic representation of the right-hand side
of this assignment.
#+BEGIN_SRC lean
import data.nat data.bool
open nat bool

check fun x : nat, x + 5
check λx : nat, x + 5
#+END_SRC
Here are some more abstract examples:
#+BEGIN_SRC lean
import data.bool
-- BEGIN
constants A B  : Type
constants a1 a2 : A
constants b1 b2 : B

constant f : A → A
constant g : A → B
constant h : A → B → A
constant p : A → A → bool

check fun x : A, f x
check λx : A, f x
check λx : A, f (f x)
check λx : A, h x b1
check λy : B, h a1 y
check λx : A, p (f (f x)) (h (f a1) b2)
check λx : A, λy : B, h (f x) y
check λ(x : A) (y : B), h (f x) y
check λx y, h (f x) y
-- END
#+END_SRC
Lean interprets the final three examples as the same expression; in
the last expression, Lean infers the type of =x= and =y= from the
types of =f= and =h=.

Be sure to try writing some expressions of your own. Some
mathematically common examples of operations of functions can be
described in terms of lambda abstraction:
#+BEGIN_SRC lean
constants A B C : Type
constant f : A → B
constant g : B → C
constant b: B

check λx : A, x        -- the identity function on A
check λx : A, b        -- a constant function on A
check λx : A, g (f x)  -- the composition of g and f
check λx, g (f x)      -- (Lean can figure out the type of x)

-- we can abstract any of the constants in the previous definitions

check λb : B, λx : A, x
check λ(b : B) (x : A), x    -- equivalent to the previous line
check λ(g : B → C) (f : A → B) (x : A), g (f x)

-- we can even abstract over the type

check λ(A B : Type) (b : B) (x : A), x
check λ(A B C : Type) (g : B → C) (f : A → B) (x : A), g (f x)
#+END_SRC

Think about what these expressions mean. The last, for example,
denotes the function that takes three types, =A=, =B=, and =C=, and
two functions, =g : B → C= and =f : A → C=, and returns the
composition of =g= and =f=. Within a lambda expression =λx : A, t=,
the variable =x= is a "bound variable": it is really a placeholder,
whose "scope" does not extend beyond =t=. For example, the variable
=b= in the expression =λ(b : B) (x : A), x= has nothing to do with the
constant =b= declared earlier. In fact, the expression denotes the
same function as =λ(u : B) (z : A), u=. Formally, the expressions that
are the same up to a renaming of bound variables are called /alpha
equivalent/, and are considered morally "the same". Lean recognizes
this equivalence.

Notice that applying an term =t : A → B= to a term =s : A= yields an
expression =t s : B=. Returning to the previous example and renaming
bound variables for clarity, notice the types of the following
expressions:
#+BEGIN_SRC lean
constants A B C : Type
constant f : A → B
constant g : B → C
constant h : A → A
constants (a : A) (b : B)

check (λx : A, x) a
check (λx : A, b) a
check (λx : A, b) (h a)
check (λx : A, g (f x)) (h (h a))

check (λv u x, v (u x)) g f a

check (λ(Q R S : Type) (v : R → S) (u : Q → R) (x : Q), v (u x)) A B C g f a
#+END_SRC

As expected, the expression =(λx : A, x) a= has type =A=. In fact,
more should be true: applying the expression =(λx : A, x)= to =a=
should "return" the value =a=. And, indeed, it does:
#+BEGIN_SRC lean
constants A B C : Type
constant f : A → B
constant g : B → C
constant h : A → A
constants (a : A) (b : B)

eval (λx : A, x) a
eval (λx : A, b) a
eval (λx : A, b) (h a)
eval (λx : A, g (f x)) (h (h a))

eval (λv u x, v (u x)) g f a

eval (λ(Q R S : Type) (v : R → S) (u : Q → R) (x : Q), v (u x)) A B C g f a
#+END_SRC

The command =eval= tells Lean to /evaluate/ an expression. The process
of simplifying an expression =(λx, t)s= to =t[s/x]= -- that is, =t=
with =s= substituted for the variable =x= -- is known as /beta
reduction/, and two terms the beta reduce to a common term are called
/beta equivalent/. But the =eval= command carries out other forms of
reduction as well:
#+BEGIN_SRC lean
import data.nat data.prod data.bool
open nat prod bool

constants m n : nat
constant b : bool

print "reducing pairs"
eval pr1 (pair m n)
eval pr2 (pair m n)

print "reducing boolean expressions"
eval tt && ff
eval b && ff

print "reducing arithmetic expressions"
eval 0 + n
eval 2 + n
eval 2 + 3
#+END_SRC
In a later chapter, we will explain how these terms are evaluated. For
now, we only wish to emphasize that this is an important feature of
the Calculus of Inductive Constructions: every term has a
computational behavior, and supports a notion of reduction, or
/normalization/. In principle, two terms that reduce to the same value
are considered morally "the same" by the underlying logical framework, and
Lean does its best to recognize and support these identifications.

** Introducing Definitions

Declaring constants in the Lean environment is a good way to postulate
new objects to experiment with, but most of the time what we really
want to do is /define/ new objects in Lean, and prove things about
them. The =definition= command provides the means to do so:
#+BEGIN_SRC lean
constants A B C : Type
constants (a : A) (f : A → B) (g : B → C) (h : A → A)

definition gfa : C := g (f a)

check gfa
print definition gfa

-- We can omit the type when Lean can figure it out.
definition gfa' := g (f a)

print definition gfa'

definition gfha := g (f (h a))

print definition gfha

definition g_comp_f : A → C := λx, g (f x)

print definition g_comp_f
#+END_SRC

The general form of a definition is ~definition foo : T := bar~. Lean
can usually infer the type =T=, but it is often a good idea to write
it explicity. This clarifies your intention, and Lean will flag an
error if the right-hand side of the definition does not have the right
type.

Because function definitions are so common, Lean provides an
alternative notation, which puts the abstracted variables before the
colon and omits the lambda:
#+BEGIN_SRC lean
constants A B C : Type
constants (g : B → C) (f : A → B)

-- BEGIN
definition g_comp_f (x : A) : C := g (f x)

print definition g_comp_f
-- END
#+END_SRC
Here are some more examples of definitions, this time in the context
of arithmetic:
#+BEGIN_SRC lean
import data.nat
open nat

constants (m n : nat) (p q : bool)

definition m_plus_n : nat := m + n

check m_plus_n
print definition m_plus_n

-- Again, Lean can infer the type
definition m_plus_n' := m + n

print definition m_plus_n'

definition double (x : nat) : nat := x + x

print definition double
check double m
check double 3
eval double m
eval double 3

definition square (x : nat) := x * x

print definition square
eval square m
eval square 3

definition do_twice (f : nat → nat) (x : nat) : nat := f (f x)

eval do_twice double 2
#+END_SRC
As an exercise, we encourage you to use =do_twice= and =double= to
define functions that quadruple their input, and multiply the input
by 8. As a further exercise, we encourage you to try defining a
function =Do_Twice : (nat → nat) → (nat → nat)= which iterates /its/
argument twice, so that =Do_Twice do_twice= a function which iterates
/its/ input four times, and evaluate =Do_Twice do_twice double 2=.

Above, we discussed the process of "currying" a function, that is,
taking a function =f (a, b)= that takes an ordered pair as an
argument, and recasting it as a function =f' a b= which takes two
arguments successively. As another exercise, we encourage you to
complete the following definitions, which "curry" and "uncurry" a
function.
#+BEGIN_SRC lean
import data.prod
open prod

definition curry (A B C : Type) (f : A × B → C) : A → B → C := sorry

definition uncurry (A B C : Type) (f : A → B → C) : A × B → C := sorry
#+END_SRC


** Namespaces and Sections

This is a good place to introduce some organizational features of Lean
that are not a part of the axiomatic framework /per se/, but make it
possible to work in the framework more efficiently.

Lean provides us with the ability to group definitions, notations, and
other information into nested, hierarchical /namespaces/:
#+BEGIN_SRC lean
namespace foo

  constant A : Type
  constant a : A
  constant f : A → A

  definition fa : A := f a
  definition ffa : A := f (f a)

  print "inside foo"

  check A
  check a
  check f
  check fa
  check ffa
  check foo.A
  check foo.fa

end foo

print "outside the namespace"

-- check A  -- error
-- check fa -- error
check foo.A
check foo.a
check foo.f
check foo.fa
check foo.ffa

open foo

print "opened foo"

check A
check a
check fa
check foo.fa
#+END_SRC

When we declare that we are working in the namespace =foo=, every
identifier we declare has a full name with prefix "=foo.=" Within the
namespace, we can refer to identifiers by their shorter names, but
once we end the namespace, we have to use the longer names.

The =open= command brings the shorter names into the current
context. Often, when we =import= a module, we will want to open one or
more of the namespaces it contains, to have access to the short
identifiers, notations, and so on. But sometimes we will want to leave
this information hidden, for example, when they conflict with
identifiers and notations in another namespace we want to use. Thus
namespaces give us a way to manage our working environment.

For example, when we work with the natural numbers, we usually want
access to the function =plus=, and its associated notation, =+=. The
command =open nat= makes these available to us.
#+BEGIN_SRC lean
import data.nat   -- imports the nat module

check nat.add
check nat.zero

open nat -- imports short identifiers, notations, etc. into the context

check add
check zero

constants m n : nat

check m + n
check 0
check m + 0
#+END_SRC

Namespaces can be nested:
#+BEGIN_SRC lean
namespace foo

  constant A : Type
  constant a : A
  constant f : A → A

  definition fa : A := f a

  namespace bar
    definition ffa : A := f (f a)

    check fa
    check ffa
  end bar

  check fa
  check bar.ffa
end foo

check foo.fa
check foo.bar.ffa

open foo

check fa
check bar.ffa
#+END_SRC
Namespaces that have been closed can later be reopened (even in
another "module," that is, another file):
#+BEGIN_SRC lean
namespace foo
  constant A : Type
  constant a : A
  constant f : A → A

  definition fa : A := f a
end foo

check foo.A
check foo.f

namespace foo
  definition ffa : A := f (f a)
end foo
#+END_SRC

The notion of a /section/ provides another way of managing
information. When we develop a theory, we will often reuse variables
in successive definitions:
#+BEGIN_SRC lean
definition compose (A B C : Type) (g : B → C) (f : A → B) (x : A) :
  C := g (f x)

definition do_twice (A : Type) (h : A → A) (x : A) : A := h (h x)

definition do_thrice (A : Type) (h : A → A) (x : A) : A := h (h (h x))

check compose
check do_twice
check do_thrice
#+END_SRC
With a section, you can declare the variables once and for all:
#+BEGIN_SRC lean
section useful
  variables (A B C : Type)
  variables (g : B → C) (f : A → B) (h : A → A)
  variable x : A

  definition compose := g (f x)
  definition do_twice := h (h x)
  definition do_thrice := h (h (h x))

  check compose
  check do_twice
  check do_thrice
end useful

print definition compose
print definition do_twice
print definition do_thrice
#+END_SRC

The =variable= and =variables= commands look like the =constant= and
=constants= commands we used above, but there is an important
difference: rather than creating permanent entities, the declarations
tell the Lean to insert the variables as bound variables in
definitions that refer to them. Lean is smart enough to figure out
which variables are used explictly or implicity in a definition, so
the later definitions of =compose=, =do_twice=, and =do_thrice= have
exactly the same effect as the earlier ones. When the section is
closed, the variables go out of scope, and become nothing more than a
distant memory.

You do not have to name a section, which is to say, you can use an
anonymous =section= / =end= pair. But if you do name a section, you
have to close it using the same name.

Like namespaces, nested sections have to be closed in the order they
are opened. Also, a namespace cannot be opened within a section;
namespaces have to live on the outer levels.

Namespaces and sections serve different purposes: namespaces organize
data and sections declare variables for insertion in theorems. A
namespace can be viewed as a special kind of section, however. In
particular, you can use the =variable= command in a namespace, in
which case the variables you declare remain in scope until the
namespace is closed.

If you use the =open= command at the "top level" of a file to import
information from a namespace, that information remains in the context
until the end of the file. But if you use the =open= command within a
section or namespace, the information remains in the context until
that section or namespace is closed.

** Dependent Types

You now have rudimentary ways of defining functions and objects in Lean,
and we will gradually introduce you to many more. Our ultimate goal in
Lean is to /prove/ things about the objects we define, and the next
chapter will introduce you to Lean's mechanisms for stating theorems
and constructing proofs. Meanwhile, let us remain on the topic of
defining objects in dependent type theory for a just a moment longer,
in order to explain what makes dependent type theory /dependent/, and
why that is useful.

The short answer is that what makes dependent type theory dependent is
that types can depend on parameters. You have already seen a nice
example of this: the type =list A= depends on the argument =A=, and
this dependence is what distinguishes =list nat= and =list bool=. For
another example, consider the type =vec A n=, the type of vectors of
elements of =A= of length =n=. This type depends on /two/ parameters:
the type =A : Type= of the elements in the vector and the length =n :
nat=.

Suppose we wish to write a function =cons= which inserts a new element
at the head of a list. What type should =cons= have? Such a function
is /polymorphic/: we expect the =cons= function for =nat=, =bool=, or
an arbitrary type =A= to behave the same way. So it makes sense to
take the type to be the first argument to =cons=, so that for any
type, =A=, =cons A= is the insertion function for lists of type
=A=. In other words, for every =A=, =cons A= is the function that
takes an element =a : A= and a list =l : list A=, and returns a new
list, so we have =cons a l : list A=.

It is clear that =cons A= should have type =A → list A → list A=. But
what type should =cons= have? A first guess might be =Type → A → list
A → list A=, but, on reflection, this does not make sense: the =A= in
this expression does not refer to anything, whereas it should refer to
the argument of type =Type=. In other words, /assuming/ =A : Type= is
the first argument to the function, the type of the next two elements
are =A= and =list A=. These types vary depending on the first
argument, =A=.

This is an instance of a /Pi type/ in dependent type theory. Given
=A : Type= and =B : A → Type=, think of =B= as a family of types over
=A=, that is, a type =B a= for each =a : A=. In that case, the type
=Πx : A, B x= denotes the type of functions =f= with the property
that, for each =a : A=, =f a= is an element of =B a=. In other words,
the type of the value returned by =f= depends on its input.

Notice that =Πx : A, B= makes sense for any expression =B :
Type=. When the value of =B= depends on =x=, =Πx : A, B= denotes a
dependent function type, as above. When =B= doesn't depend on =x=,
=Πx : A, B= is no different from the type =A → B=. Indeed, in
dependent type theory (and in Lean), the Pi construction is
fundamental, and =A → B= is nothing more than notation for =Πx : A, B=
when =B= does not depend on =A=.

Returning to the example of lists, we can model some basic list
operations as follows:
#+BEGIN_SRC lean
namespace hide
-- BEGIN
constant list : Type → Type

namespace list
  constant cons : ΠA : Type, A → list A → list A
  constant nil : ΠA : Type, list A            -- the empty list
  constant head : ΠA : Type, list A → A       -- returns the first element
  constant tail : ΠA : Type, list A → list A  -- returns the remainder
  constant append : ΠA : Type, list A → list A → list A -- concatenates two lists
end list
-- END
end hide
#+END_SRC
In fact, these are essentially the types of the defined objects in the
list library (we will explain the =@= symbol and the difference
between the round and curly brackets momentarily).
#+BEGIN_SRC lean
import data.list
open list

check list

check @cons
check @nil
check @head
check @tail
check @append
#+END_SRC

Vector operations are handled similarly:
#+BEGIN_SRC lean
import data.nat
open nat

constant vec : Type → nat → Type

namespace vec
  constant empty : ΠA : Type, vec A 0
  constant cons : Π(A : Type) (n : nat), A → vec A n → vec A (n + 1)
  constant append : Π(A : Type) (n m : nat), vec A m → vec A n → vec A (n + m)
end vec
#+END_SRC

In the coming chapters, you will come across many instances of
dependent types. Here we will mention just one more important and
illustrative example, the /Sigma types/, =Σx : A, B x=, sometimes also
known as /dependent pairs/. These are, in a sense, companions to the
Pi types. The type =Σx : A, B x= denotes the type of pairs =sigma.mk a b=
where =a : A= and =b : B a=. We can also use angle brackets =<a, b>= as notation
for =sigma a b=. We can input angle brackets using the shortcuts =\<= and =\>=.
Just as Pi types =Πx : A, B x= generalize
the notion of a function type =A → B=, Sigma types =Σx : A, B x=
generalize the cartesian product =A × B=: in the expression =sigma.mk a b=,
the type of the second element of the pair, =b : B a=, depends on
the first element of the pair, =a : A=.
#+BEGIN_SRC lean
import data.sigma
open sigma

constant A : Type
constant B : A → Type
constant a : A
constant b : B a

check sigma.mk a b
check pr1 (sigma.mk a b)
check pr2 (sigma.mk a b)

eval pr1 (sigma.mk a b)
eval pr2 (sigma.mk a b)
#+END_SRC

** Implicit Arguments

Suppose we have an implementation of lists as described above.
#+BEGIN_SRC lean
namespace hide
-- BEGIN
constant list : Type → Type

namespace list
  constant cons : ΠA : Type, A → list A → list A
  constant nil : ΠA : Type, list A
  constant append : ΠA : Type, list A → list A → list A
end list
-- END
end hide
#+END_SRC
Then, given a type =A=, some elements of =A=, and some lists of
elements of =A=, we can construct new lists using the constructors.
#+BEGIN_SRC lean
namespace hide
constant list : Type → Type

namespace list
  constant cons : ΠA : Type, A → list A → list A
  constant nil : ΠA : Type, list A
  constant append : ΠA : Type, list A → list A → list A
end list

-- BEGIN
open hide.list

constant  A : Type
constant  a : A
constants l1 l2 : list A

check cons A a (nil A)
check append A (cons A a (nil A)) l1
check append A (append A (cons A a (nil A)) l1) l2
-- END
end hide
#+END_SRC

Because the constructors are polymorphic over types, we have to insert
the type =A= as an argument repeatedly. But this information is
redundant: one can infer the argument =A= in =cons A a (nil A)= from
the fact that the second argument, =a=, has type =A=. One can
similarly infer the argument in =nil A=, not from anything else in
that expression, but from the fact that it is sent as an argument to
the function =cons=, which expects an element of type =list A= in that
position.

This is a central feature of dependent type theory: terms carry a lot
of information, and often some of that information can be inferred
from the context. In Lean, one uses an underscore, =_=, to specify
that the system should fill in the information automatically. This is
known as an "implicit argument".
#+BEGIN_SRC lean
namespace hide
constant list : Type → Type

namespace list
  constant cons : ΠA : Type, A → list A → list A
  constant nil : ΠA : Type, list A
  constant append : ΠA : Type, list A → list A → list A
end list

open hide.list

constant  A : Type
constant  a : A
constants l1 l2 : list A

-- BEGIN
check cons _ a (nil _)
check append _ (cons _ a (nil _)) l1
check append _ (append _ (cons _ a (nil _)) l1) l2
-- END
end hide
#+END_SRC

It is still tedious, however, to type all these underscores.  When a
function takes an argument that can generally be inferred from
context, Lean allows us to specify that this argument should, by
default, be left implicit.

#+BEGIN_SRC lean
namespace hide

constant list : Type → Type

namespace list
  constant cons : Π{A : Type}, A → list A → list A
  constant nil : Π{A : Type}, list A
  constant append : Π{A : Type}, list A → list A → list A
end list

open hide.list

constant  A : Type
constant  a : A
constants l1 l2 : list A

-- BEGIN
check cons a nil
check append (cons a nil) l1
check append (append (cons a nil) l1) l2
-- END

end hide
#+END_SRC

All that has changed are the curly braces around =A : Type= in the
declaration of the constants. We can also use this device in variable
declarations and function definitions:
#+BEGIN_SRC lean
-- the polymorphic identity function
{'fraction_non_alphanumeric': 0.07731823833518749, 'fraction_numerical': 0.002388587134349846, 'mean_word_length': 3.579680827152169, 'pattern_counts': {'":': 2, '<': 13, '<?xml version=': 0, '>': 15, 'https://': 0, 'lorem ipsum': 0, 'www.': 4, 'xml': 0}, 'pii_count': 0, 'substrings_counts': 0, 'word_list_counts': {'cursed_substrings.json': 0, 'profanity_word_list.json': 0, 'sexual_word_list.json': 0, 'zh_pornsignals.json': 0}}
{'dir': 'git-commits-cleaned', 'id': '1048436', 'n_tokens_mistral': 18913, 'n_tokens_neox': 18326, 'n_words': 10850}