Ordinary mathematical functions have a domain and a codomain. In Lean, we write `f : α → β`

to denote that `f`

is a function with domain `α`

and codomain `β`

. More briefly, that `f`

is a function from `α`

to `β`

.

The following is a simple example of a function from `ℕ`

to `ℤ`

that we’ve called `double`

.

`def double (n : ℕ) : ℤ := 2 * n`

We can check that `double`

has the expected type by issuing the command `#check double`

. This displays `double : ℕ → ℤ`

. Alternatively, we can *prove* that `double`

has the expected type, as in the following example.

`example : ℕ → ℤ := double`

The odd-looking statement above says, “Here’s an example, I’m going to produce a term of type `ℕ → ℤ`

. And `double`

is just such a term”. Lean’s type-checking mechanism goes to work. It finds no errors and stays quiet. Were you to replace `ℤ`

above with an `ℕ`

, you’d get an error message. Try it and see.

Lean permits a more general definition of function. The codomain of a so-called *dependent function* can depend on the type of its argument. Our aim in this post is to fill in the `sorry`

below to define a dependent function.

`def zero_vec (n : ℕ) : vector ℝ n := sorry`

**Important**: if you’re following along at home, you’ll need to place `import data.vector data.real.basic`

at the top of your Lean file.

The function `zero_vec`

should map its input `n`

to a length `n`

zero vector of real numbers. The domain of the function is still `ℕ`

, but codomain `vector ℝ n`

depends on the value `n`

.

## Lists and vectors

To start, we’ll define a function that produces a list of length `n`

consisting of real zeros. Below, note that the codomain is `list ℝ`

, the type of lists with real entries.

`def zero_list (n : ℕ) : list ℝ := list.repeat 0 n`

This is a simple application of one of the core Lean functions for working with lists. I’m sure you can guess what `list.repeat`

does. To check our intuition, we have the following special case.

`example : zero_list 5 = [0,0,0,0,0] := rfl`

The `rfl`

here is a proof by *reflexivity*, an (iterated) application of the definitions until the computer is left with two terms that are clearly equal.

What’s the difference between a vector on length `n`

and a list of length `n`

? The list type doesn’t “know” about the length of its terms. A term of type `vector ℝ n`

consists of two items of information: (1) a list and (2) a proof that the list has length `n`

. Here’s an example.

`def myvec : vector ℝ 5 := ⟨[5,10,15,20,25], rfl⟩`

The vector `myvec`

consists of the vector `[5,10,15,20,25]`

and `rfl`

, the proof that this vector has length 5.

Using the same idea, we construct a vector of length 100, consisting of zeros.

`example : vector ℝ 100 := ⟨zero_list 100, rfl⟩`

So *surely*, it’s now a simple matter of replacing 100 with `n`

to produce a vector of length `n`

. But the following doesn’t work.

`example (n : ℕ) : vector ℝ n := ⟨zero_list n, rfl⟩`

Why not? A proof by `rfl`

involves a finite computation. You can see this in action if you replace 100 above with a larger number. The proof takes longer and longer until you hit your computer’s limit. On my computer, using 5000 produces a “deep recursion” error.

When we replace 100 with `n`

, we’re asking for something entirely different. We’re asking for a proof that works when `n`

is arbitrary. This is not the same as fixing `n`

and asking a proof for that particular `n`

. In much the same way, it’s a finite computation to determine, for any given even number \(n > 2\) whether \(n\) is a sum of two primes. However, it’s quite a different thing to do that for an arbitrary \(n\).

Conveniently, core Lean has a lemma `list.length_repeat`

that shows a list produced by repeating a single term `n`

times has length `n`

.

## Dependent functions

Using `list.length_repeat`

to provide the proof, we can finally define our function.

```
def zero_vec (n : ℕ) : vector ℝ n :=
⟨zero_list n, list.length_repeat 0 n⟩
```

Issuing the `#check zero_vec`

command produces:

`zero_vec : Π (n : ℕ), vector ℝ n`

The *Pi-binder* `Π`

is merely a fancy notation for writing a dependent function type. It shouldn’t be confused with the use of `Π`

in mathematics to denote a product. For the dependent function `zero_vec`

, the domain is `ℕ`

, but we label it with a name (here `n`

) to be used as an argument for the codomain `vector ℝ n`

. There’s nothing special about `n`

. The following proves that `zero_vec`

has type `Π (m : ℕ), vector ℝ m`

.

`example : Π (m : ℕ), vector ℝ m := zero_vec`

In fact, all functions in Lean have a dependent function type. It just so happens that the codomain is a constant ‘function’ of the input value for ordinary functions.

Consider again our function `double`

.

`example : Π (n : ℕ), ℤ := double`

The above shows that `double`

is a dependent function, albeit one in which the codomain `ℤ`

does not depend on `n`

.

## Exercise

- Generalise
`zero_vec`

to a function`const_vec`

such that`const_vec c n`

is a length`n`

vector all of whose entries are`c`

, for some real constant`c`

. What is the type of`const_vec`

? - Generalise further to a function
`const_vec'`

where`const_vec' c n`

is is a length`n`

vector all of whose entries are`c`

, for some`c : α`

, for an arbitrary type`α`

. What is the type of`const_vec'`

? - (Hard) Write a function that adds two vectors of natural numbers of length
`n`

. Do this by filling in the`sorry`

below.`def add_vec {n : ℕ} (v₁ v₂`

`: vector ℕ n) : vector ℕ n := sorry`

Run a test on your definition by ensuring the following gives no error.`example : add_vec ⟨[0,1,2],rfl⟩ ⟨[5,6,7],rfl⟩ = ⟨[5,7,9], rfl⟩ := rfl`

You’ll need experience writing recursive definitions in Lean. - (Harder) Having finished the exercise above, show that the
`n`

th entry of`add_vec v₁ v₂`

is the sum of the`n`

th entries of`v₁`

and`v₂`

. That is, fill in the`sorry`

below:`lemma nth_add_nth : Π {n : ℕ} (v₁ v₂ : vector ℕ n) (a : fin n),`

`v₁.nth a + v₂.nth a = (add_vec v₁ v₂).nth a := sorry`

Pingback: What the rec? Types dependent on terms, Lean eliminators, and threshold concepts – exlean