Vectors and dependent function types

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

1. 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?
2. 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'?
3. (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.
4. (Harder) Having finished the exercise above, show that the nth entry of add_vec v₁ v₂ is the sum of the nth 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