6. Poly: Polymorphism and Higher-Order Functions🔗

import LF.Induction
import LF.UsingLean

6.1. Polymorphism🔗

In this chapter we continue our development of basic concepts of functional programming. The critical new ideas are polymorphism (abstracting functions over the types of the data they manipulate) and higher-order functions (treating functions as data). We begin with polymorphism.

6.1.1. Polymorphic Lists🔗

In the last chapter, we worked with lists containing just numbers. Obviously, interesting programs also need to be able to manipulate lists with elements from other types — lists of booleans, lists of lists, etc. We could just define a new inductive datatype for each of these, for example...

inductive BoolList : Type where
  | nil
  | cons (b : Bool) (l : BoolList)

... but this would quickly become tedious: not only would we have to make up different constructor names for each datatype, but — even worse — we would also need to define new versions of all the list manipulating functions (length, ++, reverse, etc.) and all their properties (length_reverse, append_assoc, etc.) for each new definition.

To avoid this repetition, we can make the element type itself an argument to the definition. Lean calls such definitions polymorphic. Here is a polymorphic list type:

inductive MyList (α : Type) : Type where
  | nil : MyList α
  | cons (x : α) (l : MyList α) : MyList α

This is exactly like the definition of Natlist from the Lists chapter, except that a type parameter α has been added to the header on the first line, the Nat argument to the cons constructor has been replaced by this arbitrary type α, and the occurrences of Natlist in the types of the constructors have been replaced by MyList α. We can now write MyList Nat instead of a dedicated NatList type.

What sort of thing is MyList itself? A good way to think about it is as a type constructor — that is, a function from Types to Types. For any particular type α, the type MyList α is the inductively defined type of lists whose elements are of type α.

Note to developers (Yipeng Liu @berberman)

A trick used below: parenthesizing the declaration makes it a term — Lean elaborates it and prints its inferred function type, instead of the declaration signature: MyList (α : Type) : Type.

MyList : Type → Type#check (MyList)

MyList : Type → Type

The α in the definition of MyList automatically becomes a parameter to the constructors nil and cons — that is, nil and cons are now polymorphic constructors. In Lean, the type parameter is implicit by default: Lean will infer it from context. For example, MyList.nil is the empty list, and Lean figures out the element type from how it is used.

MyList.nil {α : Type} : MyList α#check MyList.nil

MyList.nil {α : Type} : MyList α

Notice the use of curly braces in {α : Type}, rather than normal parentheses (as in (α : Type)); this is Lean telling us that α is an implicit parameter.

The MyList.cons constructor also adds an element of type Nat to a list of type MyList Nat. Here is an example of forming a list containing just the natural number 3.

MyList.cons 3 MyList.nil : MyList Nat#check MyList.cons 3 MyList.nil

MyList.cons 3 MyList.nil : MyList Nat

What is the full type of MyList.nil? We can read off the result type MyList α from the definition, but to state the full type we must also bind α. Since the type argument to the constructor is implicit, it is presented with curly braces.

MyList.nil {α : Type} : MyList α#check MyList.nil

MyList.nil {α : Type} : MyList α

Recall that this type is equivalent to {α : Type} → MyList α.

The type of MyList.cons also includes an implicit type parameter:

MyList.cons {α : Type} (x : α) (l : MyList α) : MyList α#check MyList.cons

MyList.cons {α : Type} (x : α) (l : MyList α) : MyList α

Having to supply a type argument for every single use of a list constructor would be rather burdensome. Fortunately, when a type argument is implicit, Lean will try to automatically infer it from context.

We can now go back and make polymorphic versions of all the list-processing functions that we wrote before. Here is replicate, for example:

def replicate (α : Type) (x : α) (count : Nat) : MyList α :=
  match count with
  | 0 => .nil
  | count' + 1 => .cons x (replicate α x count')

Some simple facts about replicate:

theorem replicate_zero (α : Type) (a : α) :
    replicate α a 0 = MyList.nil := rfl

theorem replicate_succ (α : Type) (a : α) (count : Nat) :
    replicate α a (count + 1) = MyList.cons a (replicate α a count) := rfl

We can use replicate by applying it first to a type and then to an element of this type (and a number):

example : replicate Nat 4 2 = .cons 4 (.cons 4 .nil) := byα:Typeβ:Typeγ:Typex:αy:β⊢ replicate Nat 4 2 = MyList.cons 4 (MyList.cons 4 MyList.nil) rflAll goals completed! 🐙

To use replicate to build other kinds of lists, we simply pass a different type and an element of that type:

example : replicate Bool false 1 = .cons false .nil := byα:Typeβ:Typeγ:Typex:αy:β⊢ replicate Bool false 1 = MyList.cons false MyList.nil rflAll goals completed! 🐙

Quiz

What is the type of MyList.cons true (MyList.cons 3 MyList.nil)?

(A) MyList Nat

(B) {α : Type} → α → MyList α → MyList α

(D) MyList (Nat × Bool)

(E) Ill-typed

Show solution

(E)

Quiz

What is the type of replicate?

(A) Nat → Nat → MyList Nat

(B) (α : Type) → α → Nat → MyList α

(D) Ill-typed

Show solution

(B)

Quiz

What is the type of replicate 1 2?

(A) MyList Nat

(B) (α : Type) → α → Nat → MyList α

(D) Ill-typed

Show solution

(D)

From now on, we'll use Lean's built-in List type and its associated notation.

The built-in List is defined just like our MyList above, but with notation [] for List.nil, :: for List.cons, and [1, 2, 3] for list literals. The ++ operator is list append. The type arguments to the list constructors are implicit.

Using Lean's built-in list notations, we can now write lists in the natural way:

example : List Nat := [1, 2, 3]

6.1.1.1. Implicit Type Arguments and Argument Synthesis🔗

In our replicate function above we wrote the type parameter (α : Type) explicitly, with normal parentheses. Doing so means that we need to pass in type argument explicitly, in addition to its other arguments. We see this in its own recursive call, which must pass along the type α. But since the second argument to replicate is an element of α, it seems entirely obvious that the first argument can only be α — why should we have to write it explicitly?

Fortunately, Lean permits us to avoid this kind of redundancy. In place of any type argument we can write a "hole" _, which can be read as "Please try to figure out for yourself what belongs here." More precisely, when Lean encounters a _, it will attempt to unify all locally available information — the type of the function being applied, the types of the other arguments, and the type expected by the context in which the application appears — to determine what concrete type should replace the _.

Using holes, the replicate function can be rewritten like this:

def replicate' (α : Type) (x : α) (count : Nat) : List α :=
  match count with
  | 0 => []
  | count' + 1 => x :: replicate' _ x count'

Alternatively, and more typically for Lean, we can declare an argument to be implicit when defining the function itself, by surrounding it in curly braces instead of parentheses.

def replicate'' {α : Type} (x : α) (count : Nat) : List α :=
  match count with
  | 0 => []
  | count' + 1 => x :: replicate'' x count'

By making the type argument implicit, we no longer need to provide α to the recursive call to replicate''. For each implicit parameter, Lean automatically inserts a hidden hole _ argument for us, which is then inferred as usual.

6.1.1.2. Supplying Type Arguments Explicitly🔗

One small problem with implicit arguments is that, once in a while, Lean does not have enough local information to determine a type argument; in such cases, we need to tell Lean the type explicitly. For example, the following definition fails because Lean can't figure out the type of the empty list:

def Failed to infer type of definition `mynil`mynil := don't know how to synthesize implicit argument `α`
  @List.nil ?m.3
context:
α β γ:Typex:αy:β⊢ Type u_1[]

Failed to infer type of definition `mynil`

We can fix this with an explicit type annotation.

We use the @ prefix when we want to supply the type argument explicitly. The @ makes all implicit arguments of a function explicit:

@List.nil : {α : Type u_1} → List α#check @List.nil

def myNil' := @List.nil Nat

@List.nil : {α : Type u_1} → List α

Quiz

Which type does Lean assign to the following expression? (The square brackets in this quiz and the following ones are list brackets.)

[1, 2, 3]

(A) List Nat

(B) List Bool

(D) No type can be assigned

Show solution

(A)

Quiz

What about this one?

[3 + 4] ++ []

(A) List Nat

(B) List Bool

(D) No type can be assigned

Show solution

(A)

Quiz

What about this one?

(true && false) :: []

(A) List Nat

(B) List Bool

(D) No type can be assigned

Show solution

(B)

Quiz

What about this one?

[1, []]

(A) List Nat

(B) List (List Nat)

(D) No type can be assigned

Show solution

(D)

Quiz

What about this one?

[[1], []]

(A) List Nat

(B) List (List Nat)

(D) No type can be assigned

Show solution

(B)

Quiz

And what about this one?

[1] :: [[]]

(A) List Nat

(B) List (List Nat)

(D) No type can be assigned

Show solution

(B)

Quiz

This one?

@List.nil Bool

(A) List Nat

(B) List (List Nat)

(D) No type can be assigned

Show solution

(C)

Exercise★★(mumble_grumble) (Optional, Manually graded)

Consider the following two inductively defined types.

inductive Mumble : Type where
  | a : Mumble
  | b (x : Mumble) (y : Nat) : Mumble
  | c : Mumble

inductive Grumble (α : Type) : Type where
  | d (m : Mumble) : Grumble α
  | e (x : α) : Grumble α

Which of the following are well-typed elements of Grumble α for some type α? (Add YES or NO to each line.)

Grumble.d (Mumble.b Mumble.a 5)
@Grumble.d Mumble (Mumble.b Mumble.a 5)
@Grumble.d Bool (Mumble.b Mumble.a 5)
@Grumble.e Bool true
@Grumble.e Mumble (Mumble.b Mumble.c 0)
@Grumble.e Bool (Mumble.b Mumble.c 0)
Mumble.c

YES — Grumble.d (Mumble.b Mumble.a 5)
YES — @Grumble.d Mumble (Mumble.b Mumble.a 5)
YES — @Grumble.d Bool (Mumble.b Mumble.a 5)
YES — @Grumble.e Bool true
YES — @Grumble.e Mumble (Mumble.b Mumble.c 0)
NO — @Grumble.e Bool (Mumble.b Mumble.c 0)
NO — Mumble.c

6.1.1.3. Exercises🔗

def List.rev {α : Type} (l : List α) : List α :=
  match l with
  | .nil => .nil
  | .cons h t => rev t ++ (.cons h .nil)

theorem rev_nil {α : Type} : ([] : List α).rev = [] := byα:Type⊢ [].rev = [] rflAll goals completed! 🐙

theorem rev_cons {α : Type} {x : α} {l : List α} :
    (x :: l).rev = l.rev ++ [x] := byα:Typex:αl:List α⊢ (x :: l).rev = l.rev ++ [x] rflAll goals completed! 🐙

Exercise★★(poly_exercises)

Here are a few simple exercises, just like ones in the Lists chapter, for practice with polymorphism. Complete the proofs below. You will find the following characterizing lemmas for List.append in Lean standard library to be useful:

List.nil_append.{u} {α : Type u} (as : List α) : [] ++ as = as#check List.nil_append
List.cons_append.{u} {α : Type u} {a : α} {as bs : List α} : a :: as ++ bs = a :: (as ++ bs)#check List.cons_append

List.cons_append.{u} {α : Type u} {a : α} {as bs : List α} : a :: as ++ bs = a :: (as ++ bs)

List.nil_append.{u} {α : Type u} (as : List α) : [] ++ as = as

theorem append_nil {α : Type} {l : List α} :
    l ++ [] = l := byα:Typel:List α⊢ l ++ [] = l
  solution!
    induction l with
    | nil =>nilα:Type⊢ [] ++ [] = [] rw [List.nil_appendnilα:Type⊢ [] = []]All goals completed! 🐙
    | cons _ _ ih =>consα:Typehead✝:αtail✝:List αih:tail✝ ++ [] = tail✝⊢ head✝ :: tail✝ ++ [] = head✝ :: tail✝ rw [List.cons_append,consα:Typehead✝:αtail✝:List αih:tail✝ ++ [] = tail✝⊢ head✝ :: (tail✝ ++ []) = head✝ :: tail✝ ihconsα:Typehead✝:αtail✝:List αih:tail✝ ++ [] = tail✝⊢ head✝ :: tail✝ = head✝ :: tail✝]All goals completed! 🐙

theorem append_assoc {α : Type} {l₁ l₂ l₃ : List α} :
    l₁ ++ l₂ ++ l₃ = l₁ ++ (l₂ ++ l₃) := byα:Typel₁:List αl₂:List αl₃:List α⊢ l₁ ++ l₂ ++ l₃ = l₁ ++ (l₂ ++ l₃)
  solution!
    induction l₁ with
    | nil =>nilα:Typel₂:List αl₃:List α⊢ [] ++ l₂ ++ l₃ = [] ++ (l₂ ++ l₃) rw [List.nil_append,nilα:Typel₂:List αl₃:List α⊢ l₂ ++ l₃ = [] ++ (l₂ ++ l₃) List.nil_appendnilα:Typel₂:List αl₃:List α⊢ l₂ ++ l₃ = l₂ ++ l₃]All goals completed! 🐙
    | cons _ _ ih =>consα:Typel₂:List αl₃:List αhead✝:αtail✝:List αih:tail✝ ++ l₂ ++ l₃ = tail✝ ++ (l₂ ++ l₃)⊢ head✝ :: tail✝ ++ l₂ ++ l₃ = head✝ :: tail✝ ++ (l₂ ++ l₃)
      repeat rw [List.cons_appendconsα:Typel₂:List αl₃:List αhead✝:αtail✝:List αih:tail✝ ++ l₂ ++ l₃ = tail✝ ++ (l₂ ++ l₃)⊢ head✝ :: (tail✝ ++ l₂) ++ l₃ = head✝ :: tail✝ ++ (l₂ ++ l₃)]consα:Typel₂:List αl₃:List αhead✝:αtail✝:List αih:tail✝ ++ l₂ ++ l₃ = tail✝ ++ (l₂ ++ l₃)⊢ head✝ :: (tail✝ ++ l₂ ++ l₃) = head✝ :: tail✝ ++ (l₂ ++ l₃)consα:Typel₂:List αl₃:List αhead✝:αtail✝:List αih:tail✝ ++ l₂ ++ l₃ = tail✝ ++ (l₂ ++ l₃)⊢ head✝ :: (tail✝ ++ l₂ ++ l₃) = head✝ :: (tail✝ ++ (l₂ ++ l₃))
      rw [ihconsα:Typel₂:List αl₃:List αhead✝:αtail✝:List αih:tail✝ ++ l₂ ++ l₃ = tail✝ ++ (l₂ ++ l₃)⊢ head✝ :: (tail✝ ++ (l₂ ++ l₃)) = head✝ :: (tail✝ ++ (l₂ ++ l₃))]All goals completed! 🐙

theorem append_length {α : Type} {l₁ l₂ : List α} :
    (l₁ ++ l₂).length = l₁.length + l₂.length := byα:Typel₁:List αl₂:List α⊢ (l₁ ++ l₂).length = l₁.length + l₂.length
  solution!
    induction l₁ with
    | nil =>nilα:Typel₂:List α⊢ ([] ++ l₂).length = [].length + l₂.length
      rw [List.nil_append,nilα:Typel₂:List α⊢ l₂.length = [].length + l₂.length List.length_nil,nilα:Typel₂:List α⊢ l₂.length = 0 + l₂.length Nat.zero_addnilα:Typel₂:List α⊢ l₂.length = l₂.length]All goals completed! 🐙
    | cons _ _ ih =>consα:Typel₂:List αhead✝:αtail✝:List αih:(tail✝ ++ l₂).length = tail✝.length + l₂.length⊢ (head✝ :: tail✝ ++ l₂).length = (head✝ :: tail✝).length + l₂.length
      rw [List.length_cons,consα:Typel₂:List αhead✝:αtail✝:List αih:(tail✝ ++ l₂).length = tail✝.length + l₂.length⊢ (head✝ :: tail✝ ++ l₂).length = tail✝.length + 1 + l₂.length List.cons_append,consα:Typel₂:List αhead✝:αtail✝:List αih:(tail✝ ++ l₂).length = tail✝.length + l₂.length⊢ (head✝ :: (tail✝ ++ l₂)).length = tail✝.length + 1 + l₂.length List.length_cons,consα:Typel₂:List αhead✝:αtail✝:List αih:(tail✝ ++ l₂).length = tail✝.length + l₂.length⊢ (tail✝ ++ l₂).length + 1 = tail✝.length + 1 + l₂.length Nat.succ_add,consα:Typel₂:List αhead✝:αtail✝:List αih:(tail✝ ++ l₂).length = tail✝.length + l₂.length⊢ (tail✝ ++ l₂).length + 1 = (tail✝.length + l₂.length).succ ihconsα:Typel₂:List αhead✝:αtail✝:List αih:(tail✝ ++ l₂).length = tail✝.length + l₂.length⊢ tail✝.length + l₂.length + 1 = (tail✝.length + l₂.length).succ]All goals completed! 🐙

Exercise★★(more_poly_exercises)

Here are some slightly more interesting ones...

theorem reverse_append {α : Type} {l₁ l₂ : List α} :
    (l₁ ++ l₂).rev = l₂.rev ++ l₁.rev := byα:Typel₁:List αl₂:List α⊢ (l₁ ++ l₂).rev = l₂.rev ++ l₁.rev
  solution!
    induction l₁ with
    | nil =>nilα:Typel₂:List α⊢ ([] ++ l₂).rev = l₂.rev ++ [].rev
      rw [List.nil_append,nilα:Typel₂:List α⊢ l₂.rev = l₂.rev ++ [].rev rev_nil,nilα:Typel₂:List α⊢ l₂.rev = l₂.rev ++ [] append_nilnilα:Typel₂:List α⊢ l₂.rev = l₂.rev]All goals completed! 🐙
    | cons _ _ ih =>consα:Typel₂:List αhead✝:αtail✝:List αih:(tail✝ ++ l₂).rev = l₂.rev ++ tail✝.rev⊢ (head✝ :: tail✝ ++ l₂).rev = l₂.rev ++ (head✝ :: tail✝).rev
      rw [List.cons_append,consα:Typel₂:List αhead✝:αtail✝:List αih:(tail✝ ++ l₂).rev = l₂.rev ++ tail✝.rev⊢ (head✝ :: (tail✝ ++ l₂)).rev = l₂.rev ++ (head✝ :: tail✝).rev rev_cons,consα:Typel₂:List αhead✝:αtail✝:List αih:(tail✝ ++ l₂).rev = l₂.rev ++ tail✝.rev⊢ (tail✝ ++ l₂).rev ++ [head✝] = l₂.rev ++ (head✝ :: tail✝).rev rev_cons,consα:Typel₂:List αhead✝:αtail✝:List αih:(tail✝ ++ l₂).rev = l₂.rev ++ tail✝.rev⊢ (tail✝ ++ l₂).rev ++ [head✝] = l₂.rev ++ (tail✝.rev ++ [head✝]) ih,consα:Typel₂:List αhead✝:αtail✝:List αih:(tail✝ ++ l₂).rev = l₂.rev ++ tail✝.rev⊢ l₂.rev ++ tail✝.rev ++ [head✝] = l₂.rev ++ (tail✝.rev ++ [head✝]) append_assocconsα:Typel₂:List αhead✝:αtail✝:List αih:(tail✝ ++ l₂).rev = l₂.rev ++ tail✝.rev⊢ l₂.rev ++ (tail✝.rev ++ [head✝]) = l₂.rev ++ (tail✝.rev ++ [head✝])]All goals completed! 🐙

theorem reverse_reverse {α : Type} (l : List α) :
    l.rev.rev = l := byα:Typel:List α⊢ l.rev.rev = l
  solution!
    induction l with
    | nil =>nilα:Type⊢ [].rev.rev = [] rw [rev_nil,nilα:Type⊢ [].rev = [] rev_nilnilα:Type⊢ [] = []]All goals completed! 🐙
    | cons _ _ ih =>consα:Typehead✝:αtail✝:List αih:tail✝.rev.rev = tail✝⊢ (head✝ :: tail✝).rev.rev = head✝ :: tail✝
      rw [rev_cons,consα:Typehead✝:αtail✝:List αih:tail✝.rev.rev = tail✝⊢ (tail✝.rev ++ [head✝]).rev = head✝ :: tail✝ reverse_append,consα:Typehead✝:αtail✝:List αih:tail✝.rev.rev = tail✝⊢ [head✝].rev ++ tail✝.rev.rev = head✝ :: tail✝ ih,consα:Typehead✝:αtail✝:List αih:tail✝.rev.rev = tail✝⊢ [head✝].rev ++ tail✝ = head✝ :: tail✝ rev_cons,consα:Typehead✝:αtail✝:List αih:tail✝.rev.rev = tail✝⊢ [].rev ++ [head✝] ++ tail✝ = head✝ :: tail✝ rev_nilconsα:Typehead✝:αtail✝:List αih:tail✝.rev.rev = tail✝⊢ [] ++ [head✝] ++ tail✝ = head✝ :: tail✝]consα:Typehead✝:αtail✝:List αih:tail✝.rev.rev = tail✝⊢ [] ++ [head✝] ++ tail✝ = head✝ :: tail✝
      rw [List.nil_append,consα:Typehead✝:αtail✝:List αih:tail✝.rev.rev = tail✝⊢ [head✝] ++ tail✝ = head✝ :: tail✝ List.cons_append,consα:Typehead✝:αtail✝:List αih:tail✝.rev.rev = tail✝⊢ head✝ :: ([] ++ tail✝) = head✝ :: tail✝ List.nil_appendconsα:Typehead✝:αtail✝:List αih:tail✝.rev.rev = tail✝⊢ head✝ :: tail✝ = head✝ :: tail✝]All goals completed! 🐙

6.1.2. Polymorphic Pairs🔗

Like inductives, structures can also be made polymorphic. If we generalize the definition NatProd of pairs of natural numbers from last chapter, we get polymorphic pairs, often called products:

structure MyProd (α β : Type) where
  fst : α
  snd : β

Lean's built-in product type Prod provides a Prod.mk constructor, and Prod.fst and Prod.snd functions for accessing the first and second components of the pair. It also has special syntax for creating products:

(1, true) : Nat × Bool#check (1, true)
1#eval (1, true).fst
true#eval (1, true).snd

(1, true) : Nat × Bool

true

You can also use .1 instead of .fst and .2 instead of .snd:

example : (3, 5).1 = 3 := byα:Typeβ:Typeγ:Typex:αy:β⊢ (3, 5).fst = 3 rflAll goals completed! 🐙
example : (3, 5).2 = 5 := byα:Typeβ:Typeγ:Typex:αy:β⊢ (3, 5).snd = 5 rflAll goals completed! 🐙

Lean writes the product type Prod α β as α × β. In VS Code you can type \times or \x to enter the × symbol.

The dsimp only tactic can be used to simplify (x, y).fst into x and (x, y).snd into y.

It is easy at first to get (x, y) and α × β confused. Remember that (x, y) is a value built from two other values, while α × β is a type built from two other types. If x has type α and y has type β, then (x, y) has type α × β.

The following function takes two lists and combines them into a list of pairs.

def zip {α β : Type} (l₁ : List α) (l₂ : List β) : List (α × β) :=
  match l₁, l₂ with
  | [], [] => []
  | _ :: _, [] => []
  | [], _ :: _ => []
  | x :: l₁', y :: l₂' => (x, y) :: zip l₁' l₂'

theorem zip_nil_left {α β : Type} (l₁ : List α) : zip l₁ [] = ([] : List (α × β)) := byα:Typeβ:Typel₁:List α⊢ zip l₁ [] = []
  cases l₁nilα:Typeβ:Type⊢ zip [] [] = []consα:Typeβ:Typehead✝:αtail✝:List α⊢ zip (head✝ :: tail✝) [] = [] <;>nilα:Typeβ:Type⊢ zip [] [] = []consα:Typeβ:Typehead✝:αtail✝:List α⊢ zip (head✝ :: tail✝) [] = [] rflAll goals completed! 🐙

theorem zip_nil_right {α β : Type} (l₂ : List β) : zip [] l₂ = ([] : List (α × β)) := byα:Typeβ:Typel₂:List β⊢ zip [] l₂ = []
  cases l₂nilα:Typeβ:Type⊢ zip [] [] = []consα:Typeβ:Typehead✝:βtail✝:List β⊢ zip [] (head✝ :: tail✝) = [] <;>nilα:Typeβ:Type⊢ zip [] [] = []consα:Typeβ:Typehead✝:βtail✝:List β⊢ zip [] (head✝ :: tail✝) = [] rflAll goals completed! 🐙

theorem zip_cons_cons {α β : Type} {x : α} {y : β} {l₁ : List α} {l₂ : List β} :
   zip (x :: l₁) (y :: l₂) = (x, y) :: zip l₁ l₂ := byα:Typeβ:Typex:αy:βl₁:List αl₂:List β⊢ zip (x :: l₁) (y :: l₂) = (x, y) :: zip l₁ l₂ rflAll goals completed! 🐙

Notice that the simplification lemmas zip_nil_left and zip_nil_right are not proofs by rfl. The reason is that l₁ and l₂ are variables, and matching on a variable usually gets stuck, like we have seen before in Induction when proving the zero_add theorem. To overcome this, we destruct the list so that the match knows which branch to take during the computation done by the rfl tactic.

Exercise★(zip_checks) (Optional, Manually graded)

Try answering the following questions on paper and checking your answers in Lean:

What is the type of zip (i.e., what does #check @zip print?)

What does

#eval zip [1, 2] [false, false, true, true]

print?

Exercise★★★(unzip) (Manually graded)

The function unzip goes in the other direction from zip: it takes a list of pairs and returns a pair of lists.

Fill in the definition of unzip below and write simplification rules that characterize it. Make sure it that passes the given unit test. Prove unzip_test_fst and unzip_test_snd by rewriting with your simplification lemmas instead of using rfl directly. Remember that you can use dsimp only to simplify expressions accessing the fst or snd elements of a pair.

def unzip {α : Type} {β : Type} (l : List (α × β)) : List α × List β := solution!(
  match l with
  | [] => ([], [])
  | (x, y) :: l' =>
    let (l₁, l₂) := unzip l'
    (x :: l₁, y :: l₂))

-- This is a must have. One has to explicitly specify the types of the empty lists, which
-- can be done in two equivalent ways
theorem unzip_nil {α β : Type} : unzip [] = (([], []) : List α × List β) := byα:Typeβ:Type⊢ unzip [] = ([], [])
  solution!
      rflAll goals completed! 🐙
theorem unzip_nil' {α β : Type} : unzip ([] : List (α × β)) = ([], []) := byα:Typeβ:Type⊢ unzip [] = ([], [])
  solution!
      rflAll goals completed! 🐙

-- To characterize the cons branch, we can introduce a single `unzip_cons`...
theorem unzip_cons {α β : Type} {x : α} {y : β} {l : List (α × β)} :
    (unzip ((x, y) :: l)) = (x :: (unzip l).fst, y :: (unzip l).snd) := byα:Typeβ:Typex:αy:βl:List (α × β)⊢ unzip ((x, y) :: l) = (x :: (unzip l).fst, y :: (unzip l).snd)
    solution!
      rflAll goals completed! 🐙

-- ... or introduce lemmas `unzip_cons_fst/snd` which individually give both sides of `unzip_cons`
theorem unzip_cons_fst {α β : Type} {x : α} {y : β} {l : List (α × β)} :
    (unzip ((x, y) :: l)).fst = x :: (unzip l).fst := byα:Typeβ:Typex:αy:βl:List (α × β)⊢ (unzip ((x, y) :: l)).fst = x :: (unzip l).fst
    solution!
      rflAll goals completed! 🐙

theorem unzip_cons_snd {α β : Type} {x : α} {y : β} {l : List (α × β)} :
    (unzip ((x, y) :: l)).snd = y :: (unzip l).snd := byα:Typeβ:Typex:αy:βl:List (α × β)⊢ (unzip ((x, y) :: l)).snd = y :: (unzip l).snd
    solution!
      rflAll goals completed! 🐙

theorem unzip_test1 : unzip [(1, false), (2, true)] = ([1, 2], [false, true]) := by⊢ unzip [(1, false), (2, true)] = ([1, 2], [false, true])
  solution!
    rflAll goals completed! 🐙

theorem unzip_test_fst : (unzip [(1, false), (2, true)]).fst = [1, 2] := by⊢ (unzip [(1, false), (2, true)]).fst = [1, 2]
  solution!
    rw [unzip_cons_fst,⊢ 1 :: (unzip [(2, true)]).fst = [1, 2] unzip_cons_fst,⊢ 1 :: 2 :: (unzip []).fst = [1, 2] unzip_nil⊢ 1 :: 2 :: ([], []).fst = [1, 2]]All goals completed! 🐙

theorem unzip_test_snd : (unzip [(1, false), (2, true)]).snd = [false, true] := by⊢ (unzip [(1, false), (2, true)]).snd = [false, true]
  solution!
    ·⊢ (unzip [(1, false), (2, true)]).snd = [false, true] rw [unzip_cons_snd,⊢ false :: (unzip [(2, true)]).snd = [false, true] unzip_cons_snd,⊢ false :: true :: (unzip []).snd = [false, true] unzip_nil⊢ false :: true :: ([], []).snd = [false, true]]All goals completed! 🐙

-- These are the same tests but with `unzip_cons` instead
theorem unzip_test_fst' : (unzip [(1, false), (2, true)]).fst = [1, 2] := by⊢ (unzip [(1, false), (2, true)]).fst = [1, 2]
  rw [unzip_cons,⊢ (1 :: (unzip [(2, true)]).fst, false :: (unzip [(2, true)]).snd).fst = [1, 2] unzip_cons,⊢ (1 :: (2 :: (unzip []).fst, true :: (unzip []).snd).fst,
      false :: (2 :: (unzip []).fst, true :: (unzip []).snd).snd).fst =
  [1, 2] unzip_nil⊢ (1 :: (2 :: ([], []).fst, true :: ([], []).snd).fst, false :: (2 :: ([], []).fst, true :: ([], []).snd).snd).fst =
  [1, 2]]All goals completed! 🐙

theorem unzip_test_snd' : (unzip [(1, false), (2, true)]).snd = [false, true] := by⊢ (unzip [(1, false), (2, true)]).snd = [false, true]
  rw [unzip_cons,⊢ (1 :: (unzip [(2, true)]).fst, false :: (unzip [(2, true)]).snd).snd = [false, true] unzip_cons,⊢ (1 :: (2 :: (unzip []).fst, true :: (unzip []).snd).fst,
      false :: (2 :: (unzip []).fst, true :: (unzip []).snd).snd).snd =
  [false, true] unzip_nil⊢ (1 :: (2 :: ([], []).fst, true :: ([], []).snd).fst, false :: (2 :: ([], []).fst, true :: ([], []).snd).snd).snd =
  [false, true]]All goals completed! 🐙

6.1.3. Polymorphic Options🔗

Our last polymorphic type for now is polymorphic options. Lean's standard library provides Option α, with constructors none and some. (We already saw NatOption in the Lists chapter.) Let's briefly look at the definition:

namespace OptionPlayground

inductive Option (α : Type) : Type where
  | none : Option α
  | some (x : α) : Option α

end OptionPlayground

We can now rewrite the nth? function so that it works with any type of list.

def nth? {α : Type} (l : List α) (n : Nat) : Option α :=
  match l with
  | [] => none
  | x :: l' => match n with
    | 0 => some x
    | n' + 1 => nth? l' n'

theorem nth?_nil {α : Type} {n : Nat} :
  nth? ([] : List α) n = none := byα:Typen:Nat⊢ nth? [] n = none rflAll goals completed! 🐙

theorem nth?_cons_zero {α : Type} {x : α} {l' : List α} :
  nth? (x :: l') 0 = some x := byα:Typex:αl':List α⊢ nth? (x :: l') 0 = some x rflAll goals completed! 🐙

theorem nth?_cons_succ {α : Type} {x : α} {l' : List α} {n : Nat} :
  nth? (x :: l') (n + 1) = nth? l' n := byα:Typex:αl':List αn:Nat⊢ nth? (x :: l') (n + 1) = nth? l' n rflAll goals completed! 🐙

example : nth? [4, 5, 6, 7] 0 = some 4 := byα:Typeβ:Typeγ:Typex:αy:β⊢ nth? [4, 5, 6, 7] 0 = some 4 rflAll goals completed! 🐙
example : nth? [[1], [2]] 1 = some [2] := byα:Typeβ:Typeγ:Typex:αy:β⊢ nth? [[1], [2]] 1 = some [2] rflAll goals completed! 🐙
example : nth? [true] 2 = none := byα:Typeβ:Typeγ:Typex:αy:β⊢ nth? [true] 2 = none rflAll goals completed! 🐙

Exercise★(head?_poly) (Optional)

Complete the definition of a polymorphic version of the head? function from the last chapter. Be sure that it passes the unit tests below.

def head? {α : Type} (l : List α) : Option α := solution!(
  match l with
  | [] => none
  | x :: _ => some x)

theorem head?_nil {α : Type} : head? ([] : List α) = none := solution!(byα:Type⊢ head? [] = none rflAll goals completed! 🐙)

theorem head?_cons {α : Type} {head : α} {tail : List α} : head? (head :: tail) = some head :=
  solution!(byα:Typehead:αtail:List α⊢ head? (head :: tail) = some head rflAll goals completed! 🐙)

theorem test_head?1 : head? [1, 2] = some 1 := solution!(by⊢ head? [1, 2] = some 1 rflAll goals completed! 🐙)

theorem test_head?2 : head? [[1], [2]] = some [1] := solution!(by⊢ head? [[1], [2]] = some [1] rflAll goals completed! 🐙)

6.2. Functions as Data🔗

Like most modern programming languages — especially other "functional" languages, including OCaml, Haskell, Racket, Scala, and Clojure, among others — Lean treats functions as first-class citizens, allowing them to be passed as arguments to other functions, returned as results, stored in data structures, etc.

6.2.1. Higher-Order Functions🔗

Functions that manipulate other functions are often called higher-order functions. Here's a simple one:

def doIt3Times {α : Type} (f : α → α) (x : α) : α :=
  f (f (f x))

The argument f here is itself a function (from α to α); the body of doIt3Times applies f three times to some value x.

doIt3Times {α : Type} (f : α → α) (x : α) : α#check doIt3Times

example : doIt3Times Nat.minusTwo 9 = 3 := byα:Typeβ:Typeγ:Typex:αy:β⊢ doIt3Times Nat.minusTwo 9 = 3 rflAll goals completed! 🐙

example : doIt3Times not true = false := byα:Typeβ:Typeγ:Typex:αy:β⊢ doIt3Times not true = false rflAll goals completed! 🐙

doIt3Times {α : Type} (f : α → α) (x : α) : α

6.2.2. Filter🔗

Here is a more useful higher-order function, taking a list of αs and a predicate on α (a function from α to Bool) and "filtering" the list to yield a new list containing just those elements for which the predicate returns true.

def filter {α : Type} (test : α → Bool) (l : List α) : List α :=
  match l with
  | [] => []
  | x :: l' =>
    bif test x then x :: filter test l'
    else filter test l'

For example, if we apply filter to the predicate Nat.even and a list of numbers, it returns a list containing just the even members.

example : filter Nat.even [1, 2, 3, 4] = [2, 4] := byα:Typeβ:Typeγ:Typex:αy:β⊢ filter Nat.even [1, 2, 3, 4] = [2, 4] rflAll goals completed! 🐙

Here are some further examples and properties of filter.

def isLength1 {α : Type} (l : List α) : Bool :=
  l.length == 1

example : filter isLength1
    [[1, 2], [3], [4], [5, 6, 7], [], [8]]
  = [[3], [4], [8]] := byα:Typeβ:Typeγ:Typex:αy:β⊢ filter isLength1 [[1, 2], [3], [4], [5, 6, 7], [], [8]] = [[3], [4], [8]] rflAll goals completed! 🐙

theorem filter_nil {α : Type} {test : α → Bool} :
  filter test [] = [] := byα:Typetest:α → Bool⊢ filter test [] = [] rflAll goals completed! 🐙

theorem filter_cons_of_pos {α : Type} {test : α → Bool} {x : α}
    {l : List α} (h : test x = true) :
    filter test (x :: l) = x :: filter test l := byα:Typetest:α → Boolx:αl:List αh:test x = true⊢ filter test (x :: l) = x :: filter test l
  rw [filter,α:Typetest:α → Boolx:αl:List αh:test x = true⊢ (bif test x then x :: filter test l else filter test l) = x :: filter test l h,α:Typetest:α → Boolx:αl:List αh:test x = true⊢ (bif true then x :: filter test l else filter test l) = x :: filter test l Bool.cond_trueα:Typetest:α → Boolx:αl:List αh:test x = true⊢ x :: filter test l = x :: filter test l]All goals completed! 🐙

theorem filter_cons_of_neg {α : Type} {test : α → Bool} {x : α}
    {l : List α} (h : test x = false) :
    filter test (x :: l) = filter test l := byα:Typetest:α → Boolx:αl:List αh:test x = false⊢ filter test (x :: l) = filter test l
   rw [filter,α:Typetest:α → Boolx:αl:List αh:test x = false⊢ (bif test x then x :: filter test l else filter test l) = filter test l h,α:Typetest:α → Boolx:αl:List αh:test x = false⊢ (bif false then x :: filter test l else filter test l) = filter test l Bool.cond_falseα:Typetest:α → Boolx:αl:List αh:test x = false⊢ filter test l = filter test l]All goals completed! 🐙

You might have noticed that filter_cons_of_pos and filter_cons_of_neg have implicit parameters, such as x and l, that do not have type Type like α does. As it turns out, Lean allows any parameter to be implicit, not just those of type Type. This is a standard Lean convention for lemmas that are likely to be used by rw when their values can be inferred from the context.

For example, suppose you were using theorem filter_cons_of_pos to rewrite filter Nat.even (3 :: rest). Matching the latter expression against the theorem's left-hand side filter test (x :: l) establishes that test = Nat.even, x = 3, l = rest, and α = Nat. If arguments α, test, x, and l were not implicit, you'd have to write rewrite [filter_cons_of_pos Nat Nat.even 3 rest] in your proof. Since the arguments are implicit, Lean automatically inserts a hole _ for each of them when you apply the theorem, just as with implicit parameters of type Type, so they can be inferred from the context. Thus you can write rewrite [filter_cons_of_pos] instead.

Note that h : test x is not implicit, it's explicit. That's because it cannot be solved by unification, i.e., Lean can't prove that Nat.even 3 = true that way. It's a general proof obligation.

We'll follow the Lean standard convention from now on.

We can use filter to give a concise version of the countOddMembers function from the Lists chapter.

def countOddMembers (l : List Nat) : Nat := (filter Nat.odd l).length

example : countOddMembers [1, 0, 3, 1, 4, 5] = 4 := byα:Typeβ:Typeγ:Typex:αy:β⊢ countOddMembers [1, 0, 3, 1, 4, 5] = 4 rflAll goals completed! 🐙
example : countOddMembers [0, 2, 4] = 0 := byα:Typeβ:Typeγ:Typex:αy:β⊢ countOddMembers [0, 2, 4] = 0 rflAll goals completed! 🐙
example : countOddMembers [] = 0 := byα:Typeβ:Typeγ:Typex:αy:β⊢ countOddMembers [] = 0 rflAll goals completed! 🐙

6.2.3. Anonymous Functions🔗

It is arguably a little sad, in the example just above, to be forced to define the function isLength1 and give it a name just to be able to pass it as an argument to filter, since we will probably never use it again. Indeed, when using higher-order functions, we often want to pass as arguments "one-off" functions that we will never use again; having to give each of these functions a name would be tedious.

Fortunately, there is a better way. We can construct a function "on the fly" without declaring it at the top level or giving it a name. Lean provides two syntaxes for anonymous functions:

fun n => n * n — traditional lambda syntax
(· * ·) — "term with holes" syntax, where · marks arguments

example : doIt3Times (fun n => n * n) 2 = 256 := byα:Typeβ:Typeγ:Typex:αy:β⊢ doIt3Times (fun n => n * n) 2 = 256 rflAll goals completed! 🐙

The expression fun n => n * n can be read as "the function that, given a number n, yields n * n."

Lean also supports a shorter notation using · as a placeholder for the argument:

example : doIt3Times (· + 1) 0 = 3 := byα:Typeβ:Typeγ:Typex:αy:β⊢ doIt3Times (fun x => x + 1) 0 = 3 rflAll goals completed! 🐙

Here is the filter example, rewritten to use an anonymous function.

example : filter (fun l => l.length == 1)
    [[1, 2], [3], [4], [5, 6, 7], [], [8]]
  = [[3], [4], [8]] := byα:Typeβ:Typeγ:Typex:αy:β⊢ filter (fun l => l.length == 1) [[1, 2], [3], [4], [5, 6, 7], [], [8]] = [[3], [4], [8]] rflAll goals completed! 🐙

example : filter (·.length == 1)
    [[1, 2], [3], [4], [5, 6, 7], [], [8]]
  = [[3], [4], [8]] := byα:Typeβ:Typeγ:Typex:αy:β⊢ filter (fun x => x.length == 1) [[1, 2], [3], [4], [5, 6, 7], [], [8]] = [[3], [4], [8]] rflAll goals completed! 🐙

Exercise★★(filter_even_gt7)

Use filter (instead of a recursive def) to write a Lean function filterEvenGt7 that takes a list of natural numbers as input and returns a list of just those that are even and greater than 7.

def filterEvenGt7 (l : List Nat) : List Nat := solution!(
  filter (fun n => n.even && n > 7) l)

theorem test_filterEvenGt7_1 : filterEvenGt7 [1, 2, 6, 9, 10, 3, 12, 8] = [10, 12, 8] := solution!(by⊢ filterEvenGt7 [1, 2, 6, 9, 10, 3, 12, 8] = [10, 12, 8] rflAll goals completed! 🐙)

theorem test_filterEvenGt7_2 : filterEvenGt7 [5, 2, 6, 19, 129] = [] := solution!(by⊢ filterEvenGt7 [5, 2, 6, 19, 129] = [] rflAll goals completed! 🐙)

Exercise★★★(partition)

Use filter to write a Lean function partition that, given a type α, a predicate of type α → Bool and a List α, should return a pair of lists. The first member of the pair is the sublist of the original list containing the elements that satisfy the test, and the second is the sublist containing those that fail the test. The order of elements in the two sublists should be the same as their order in the original list.

def partition {α : Type} (test : α → Bool) (l : List α) : List α × List α := solution!(
  (filter test l, filter (!test ·) l))

theorem test_partition1 : partition (· % 2 != 0) [1, 2, 3, 4, 5] = ([1, 3, 5], [2, 4]) := solution!(by⊢ partition (fun x => x % 2 != 0) [1, 2, 3, 4, 5] = ([1, 3, 5], [2, 4]) rflAll goals completed! 🐙)
theorem test_partition2 : partition (fun _ => false) [5, 9, 0] = ([], [5, 9, 0]) := solution!(by⊢ partition (fun x => false) [5, 9, 0] = ([], [5, 9, 0]) rflAll goals completed! 🐙)

6.2.4. Map🔗

Another handy higher-order function is called map.

def map {α β : Type} (f : α → β) (l : List α) : List β :=
  match l with
  | [] => []
  | head :: tail => f head :: map f tail

It takes a function f and a list l = [n1, n2, n3, ...] and returns the list [f n1, f n2, f n3, ...], where f has been applied to each element of l in turn. For example:

example : map (· + 3) [2, 0, 2] = [5, 3, 5] := byα:Typeβ:Typeγ:Typex:αy:β⊢ map (fun x => x + 3) [2, 0, 2] = [5, 3, 5] rflAll goals completed! 🐙

The element types of the input and output lists need not be the same, since map takes two type arguments, α and β; it can thus be applied to a list of numbers and a function from numbers to booleans to yield a list of booleans:

example : map Nat.odd [2, 1, 2, 5] = [false, true, false, true] := byα:Typeβ:Typeγ:Typex:αy:β⊢ map Nat.odd [2, 1, 2, 5] = [false, true, false, true] rflAll goals completed! 🐙

It can even be applied to a list of numbers and a function from numbers to lists of booleans to yield a list of lists of booleans:

example : map (fun n => [n.even, n.odd]) [2, 1, 2, 5]
  = [[true, false], [false, true], [true, false], [false, true]] := byα:Typeβ:Typeγ:Typex:αy:β⊢ map (fun n => [n.even, n.odd]) [2, 1, 2, 5] = [[true, false], [false, true], [true, false], [false, true]] rflAll goals completed! 🐙

Quiz

Recall the definition of map:

def map {α β : Type} (f : α → β) (l : List α) : List β :=
  match l with
  | [] => []
  | head :: tail => f head :: map f tail

What is the type of @map?

(A) {α β : Type} → α → β → List α → List β

(B) α → β → List α → List β

(D) {α : Type} → (α → α) → List α → List α

As usual, we define the following simplification rules for map:

theorem map_nil {α : Type} {β : Type} {f : α → β} : map f [] = [] := byα:Typeβ:Typef:α → β⊢ map f [] = [] rflAll goals completed! 🐙

theorem map_cons {α : Type} {β : Type} {f : α → β} {x : α} {l : List α} :
    map f (x :: l) = f x :: map f l := byα:Typeβ:Typef:α → βx:αl:List α⊢ map f (x :: l) = f x :: map f l rflAll goals completed! 🐙

Exercise★★★(map_rev)

Show that map and List.rev commute. (Hint: You may need to define an auxiliary lemma.)

theorem map_append {α β : Type} {f : α → β} {l l' : List α} :
    map f (l ++ l') = map f l ++ map f l' := byα:Typeβ:Typef:α → βl:List αl':List α⊢ map f (l ++ l') = map f l ++ map f l'
  induction l with
  | nil =>nilα:Typeβ:Typef:α → βl':List α⊢ map f ([] ++ l') = map f [] ++ map f l' rw [map_nil,nilα:Typeβ:Typef:α → βl':List α⊢ map f ([] ++ l') = [] ++ map f l' List.nil_append,nilα:Typeβ:Typef:α → βl':List α⊢ map f l' = [] ++ map f l' List.nil_appendnilα:Typeβ:Typef:α → βl':List α⊢ map f l' = map f l']All goals completed! 🐙
  | cons _ _ ih =>consα:Typeβ:Typef:α → βl':List αhead✝:αtail✝:List αih:map f (tail✝ ++ l') = map f tail✝ ++ map f l'⊢ map f (head✝ :: tail✝ ++ l') = map f (head✝ :: tail✝) ++ map f l' rw [List.cons_append,consα:Typeβ:Typef:α → βl':List αhead✝:αtail✝:List αih:map f (tail✝ ++ l') = map f tail✝ ++ map f l'⊢ map f (head✝ :: (tail✝ ++ l')) = map f (head✝ :: tail✝) ++ map f l' map_cons,consα:Typeβ:Typef:α → βl':List αhead✝:αtail✝:List αih:map f (tail✝ ++ l') = map f tail✝ ++ map f l'⊢ f head✝ :: map f (tail✝ ++ l') = map f (head✝ :: tail✝) ++ map f l' map_cons,consα:Typeβ:Typef:α → βl':List αhead✝:αtail✝:List αih:map f (tail✝ ++ l') = map f tail✝ ++ map f l'⊢ f head✝ :: map f (tail✝ ++ l') = f head✝ :: map f tail✝ ++ map f l' ih,consα:Typeβ:Typef:α → βl':List αhead✝:αtail✝:List αih:map f (tail✝ ++ l') = map f tail✝ ++ map f l'⊢ f head✝ :: (map f tail✝ ++ map f l') = f head✝ :: map f tail✝ ++ map f l' List.cons_appendconsα:Typeβ:Typef:α → βl':List αhead✝:αtail✝:List αih:map f (tail✝ ++ l') = map f tail✝ ++ map f l'⊢ f head✝ :: (map f tail✝ ++ map f l') = f head✝ :: (map f tail✝ ++ map f l')]All goals completed! 🐙

theorem map_rev {α : Type} {β : Type} {f : α → β} {l : List α} :
    map f l.rev = (map f l).rev := byα:Typeβ:Typef:α → βl:List α⊢ map f l.rev = (map f l).rev
  solution!
    induction lnilα:Typeβ:Typef:α → β⊢ map f [].rev = (map f []).revconsα:Typeβ:Typef:α → βhead✝:αtail✝:List αtail_ih✝:map f tail✝.rev = (map f tail✝).rev⊢ map f (head✝ :: tail✝).rev = (map f (head✝ :: tail✝)).rev
    case nil =>α:Typeβ:Typef:α → β⊢ map f [].rev = (map f []).rev
     rw [rev_nil,α:Typeβ:Typef:α → β⊢ map f [] = (map f []).rev map_nil,α:Typeβ:Typef:α → β⊢ [] = [].rev rev_nilα:Typeβ:Typef:α → β⊢ [] = []]All goals completed! 🐙
    case cons _ _ ih =>α:Typeβ:Typef:α → βhead✝:αtail✝:List αih:map f tail✝.rev = (map f tail✝).rev⊢ map f (head✝ :: tail✝).rev = (map f (head✝ :: tail✝)).rev
     rw [rev_cons,α:Typeβ:Typef:α → βhead✝:αtail✝:List αih:map f tail✝.rev = (map f tail✝).rev⊢ map f (tail✝.rev ++ [head✝]) = (map f (head✝ :: tail✝)).rev map_cons,α:Typeβ:Typef:α → βhead✝:αtail✝:List αih:map f tail✝.rev = (map f tail✝).rev⊢ map f (tail✝.rev ++ [head✝]) = (f head✝ :: map f tail✝).rev map_append,α:Typeβ:Typef:α → βhead✝:αtail✝:List αih:map f tail✝.rev = (map f tail✝).rev⊢ map f tail✝.rev ++ map f [head✝] = (f head✝ :: map f tail✝).rev rev_cons,α:Typeβ:Typef:α → βhead✝:αtail✝:List αih:map f tail✝.rev = (map f tail✝).rev⊢ map f tail✝.rev ++ map f [head✝] = (map f tail✝).rev ++ [f head✝] ih,α:Typeβ:Typef:α → βhead✝:αtail✝:List αih:map f tail✝.rev = (map f tail✝).rev⊢ (map f tail✝).rev ++ map f [head✝] = (map f tail✝).rev ++ [f head✝] map_cons,α:Typeβ:Typef:α → βhead✝:αtail✝:List αih:map f tail✝.rev = (map f tail✝).rev⊢ (map f tail✝).rev ++ f head✝ :: map f [] = (map f tail✝).rev ++ [f head✝] map_nilα:Typeβ:Typef:α → βhead✝:αtail✝:List αih:map f tail✝.rev = (map f tail✝).rev⊢ (map f tail✝).rev ++ [f head✝] = (map f tail✝).rev ++ [f head✝]]All goals completed! 🐙

Exercise★★(flat_map)

The function map maps a List α to a List β using a function of type α → β. We can define a similar function, flatMap, which maps a List α to a List β using a function f of type α → List β. Your definition should work by 'flattening' the results of f, like so:

flatMap (fun n => [n, n + 1, n + 2]) [1, 5, 10]
  = [1, 2, 3, 5, 6, 7, 10, 11, 12]

def flatMap {α β : Type} (f : α → List β) (l : List α) : List β := solution!(
  match l with
  | [] => []
  | h :: t => f h ++ flatMap f t)

theorem test_flatMap : flatMap (fun n => [n, n, n]) [1, 5, 4]
  = [1, 1, 1, 5, 5, 5, 4, 4, 4] := solution!(by⊢ flatMap (fun n => [n, n, n]) [1, 5, 4] = [1, 1, 1, 5, 5, 5, 4, 4, 4] rflAll goals completed! 🐙)

theorem flatMap_nil {α : Type} {β : Type} (f : α → List β) : flatMap f [] = [] :=
   solution!(byα:Typeβ:Typef:α → List β⊢ flatMap f [] = [] rflAll goals completed! 🐙)

theorem flatMap_cons {α : Type} {β : Type} (f : α → List β) h t :
   flatMap f (h :: t) = f h ++ flatMap f t := solution!(byα:Typeβ:Typef:α → List βh:αt:List α⊢ flatMap f (h :: t) = f h ++ flatMap f t rflAll goals completed! 🐙)

Lists are not the only inductive type for which map makes sense. Here is a map for the Option type:

def optionMap {α : Type} {β : Type} (f : α → β) (x? : Option α) : Option β :=
  match x? with
  | none => none
  | some x => some (f x)

Exercise★★(implicit_args) (Optional)

The definitions and uses of filter and map use implicit arguments in many places. Replace the curly braces around the implicit arguments with explicit parentheses, and then fill in explicit type parameters where necessary and use Lean to check that you've done so correctly. (This exercise is not to be turned in; it is probably easiest to do it on a copy of this file that you can throw away afterwards.)

6.2.5. Fold🔗

An even more powerful higher-order function is fold. It is the inspiration for the "reduce" operation that lies at the heart of Google's map/reduce distributed programming framework.

def fold {α : Type} {β : Type} (f : α → β → β) (l : List α) (b : β) : β :=
  match l with
  | [] => b
  | a :: l => f a (fold f l b)

Intuitively, the behavior of the fold operation is to insert a given binary operator f between every pair of elements in a given list. For example, fold (· + ·) [1, 2, 3, 4] intuitively means 1 + 2 + 3 + 4. To make this precise, we also need a "starting element" that serves as the initial second input to f. So, for example,

fold (· + ·) [1, 2, 3, 4] 0

yields

1 + (2 + (3 + (4 + 0))).

example : fold (· && ·) [true, true, false, true] true = false := byα:Typeβ:Typeγ:Typex:αy:β⊢ fold (fun x1 x2 => x1 && x2) [true, true, false, true] true = false rflAll goals completed! 🐙

example : fold (· * ·) [1, 2, 3, 4] 1 = 24 := byα:Typeβ:Typeγ:Typex:αy:β⊢ fold (fun x1 x2 => x1 * x2) [1, 2, 3, 4] 1 = 24 rflAll goals completed! 🐙

example : fold (· ++ ·) [[1], [], [2, 3], [4]] [] = [1, 2, 3, 4] := byα:Typeβ:Typeγ:Typex:αy:β⊢ fold (fun x1 x2 => x1 ++ x2) [[1], [], [2, 3], [4]] [] = [1, 2, 3, 4] rflAll goals completed! 🐙

example : fold (fun l n => l.length + n) [[1], [], [2, 3, 2], [4]] 0 = 5 := byα:Typeβ:Typeγ:Typex:αy:β⊢ fold (fun l n => l.length + n) [[1], [], [2, 3, 2], [4]] 0 = 5 rflAll goals completed! 🐙

theorem fold_nil {α β : Type} {f : α → β → β} {b : β} :
  fold f [] b = b := byα:Typeβ:Typef:α → β → βb:β⊢ fold f [] b = b rflAll goals completed! 🐙

theorem fold_cons {α β : Type} {f : α → β → β} {a : α} {l : List α} {b : β} :
  fold f (a :: l) b = f a (fold f l b) := byα:Typeβ:Typef:α → β → βa:αl:List αb:β⊢ fold f (a :: l) b = f a (fold f l b) rflAll goals completed! 🐙

Quiz

Here is the definition of fold again:

def fold {α β : Type} (f : α → β → β) (l : List α) (b : β) : β :=
  match l with
  | [] => b
  | a :: l => f a (fold f l b)

What is the type of @fold?

(A) {α β : Type} → (α → β → β) → List α → β → β

(B) α → β → (α → β → β) → List α → β → β

(D) α → β → α → β → β → List α → β → β

Show solution

(A)

Quiz

What does fold (· + ·) [1, 2, 3, 4] 0 simplify to?

(A) [1, 2, 3, 4]

(B) 0

(D) [3, 7, 0]

Show solution

(C)

Exercise★(fold_types_different) (Optional, Manually graded)

Observe that the type of fold is parameterized by two type variables, α and β, and the parameter f is a binary operator that takes an α and a β and returns a β. The examples above show one instance where it is useful for α and β to be different. Can you think of any others?

Show solution

There are many. For example, we could use fold to count the number of true elements in a list of booleans. Here α would be Bool and β would be Nat.

6.2.6. Functions That Construct Functions🔗

Most of the higher-order functions we have talked about so far take functions as arguments. Let's look at some examples that involve returning functions as the results of other functions. To begin, here is a function that takes a value x (drawn from some type α) and returns a function from Nat to α that yields x whenever it is called, ignoring its Nat argument.

def constFun {α : Type} (x : α) : Nat → α :=
  fun _ => x

def fTrue := constFun true

example : fTrue 0 = true := byα:Typeβ:Typeγ:Typex:αy:β⊢ fTrue 0 = true rflAll goals completed! 🐙

example : constFun 5 99 = 5 := byα:Typeβ:Typeγ:Typex:αy:β⊢ constFun 5 99 = 5 rflAll goals completed! 🐙

In fact, the multiple-argument functions we have already seen are also examples of passing functions as data. To see why, recall the type of addition:

Nat.add : Nat → Nat → Nat#check Nat.add

Nat.add : Nat → Nat → Nat

def plus3 := Nat.add 3
plus3 : Nat → Nat#check plus3

example : plus3 4 = 7 := byα:Typeβ:Typeγ:Typex:αy:β⊢ plus3 4 = 7 rflAll goals completed! 🐙
example : doIt3Times plus3 0 = 9 := byα:Typeβ:Typeγ:Typex:αy:β⊢ doIt3Times plus3 0 = 9 rflAll goals completed! 🐙
example : doIt3Times (Nat.add 3) 0 = 9 := byα:Typeβ:Typeγ:Typex:αy:β⊢ doIt3Times (Nat.add 3) 0 = 9 rflAll goals completed! 🐙

plus3 : Nat → Nat

Similarly, we can write:

def fold_plus : List Nat → Nat → Nat :=
  fold (· + ·)

fold_plus : List Nat → Nat → Nat#check fold_plus

fold_plus : List Nat → Nat → Nat

What's happening here is called partial application. In Lean, the type constructor → is right-associative, meaning a function type like α → β → γ is parsed like α → (β → γ), or "a function from α to a function from β to γ."

We can think of fold not as a three-argument function, but as a one-argument function that:

Takes an argument f of type α → β → β
Returns a function of type List α → β → β that "remembers" f

When we write fold (· + ·), we're giving fold its first argument, (· + ·), and getting back a specialized function that can sum up the elements of any list of numbers. This new function still expects two more arguments: a list and a starting value.

6.3. Additional Exercises🔗

Exercise★★(fold_length)

Many common functions on lists can be implemented in terms of fold. For example, here is an alternative definition of List.length:

def foldLength {α : Type} (l : List α) : Nat :=
  fold (fun _ n => n + 1) l 0

example : foldLength [4, 7, 0] = 3 := byα:Typeβ:Typeγ:Typex:αy:β⊢ foldLength [4, 7, 0] = 3 rflAll goals completed! 🐙

Prove the correctness of foldLength.

Hint: It may help to use rw [foldLength, fold] to unfold the definition.

theorem fold_length_correct {α : Type} {l : List α} :
    foldLength l = l.length := byα:Typel:List α⊢ foldLength l = l.length
  solution!
    induction l with
    | nil =>nilα:Type⊢ foldLength [] = [].length
      rw [foldLength,nilα:Type⊢ fold (fun x n => n + 1) [] 0 = [].length fold_nil,nilα:Type⊢ 0 = [].length List.length_nilnilα:Type⊢ 0 = 0]All goals completed! 🐙
    | cons _ _ ih =>consα:Typehead✝:αtail✝:List αih:foldLength tail✝ = tail✝.length⊢ foldLength (head✝ :: tail✝) = (head✝ :: tail✝).length
      rw [foldLengthconsα:Typehead✝:αtail✝:List αih:fold (fun x n => n + 1) tail✝ 0 = tail✝.length⊢ fold (fun x n => n + 1) (head✝ :: tail✝) 0 = (head✝ :: tail✝).length] at *consα:Typehead✝:αtail✝:List αih:fold (fun x n => n + 1) tail✝ 0 = tail✝.length⊢ fold (fun x n => n + 1) (head✝ :: tail✝) 0 = (head✝ :: tail✝).length
      rw [List.length_cons,consα:Typehead✝:αtail✝:List αih:fold (fun x n => n + 1) tail✝ 0 = tail✝.length⊢ fold (fun x n => n + 1) (head✝ :: tail✝) 0 = tail✝.length + 1 fold_cons,consα:Typehead✝:αtail✝:List αih:fold (fun x n => n + 1) tail✝ 0 = tail✝.length⊢ fold (fun x n => n + 1) tail✝ 0 + 1 = tail✝.length + 1 ihconsα:Typehead✝:αtail✝:List αih:fold (fun x n => n + 1) tail✝ 0 = tail✝.length⊢ tail✝.length + 1 = tail✝.length + 1]All goals completed! 🐙

Exercise★★★(fold_map) (Manually graded)

We can also define map in terms of fold. Finish foldMap below.

def foldMap {α β : Type} (f : α → β) (l : List α) : List β := solution!(
  fold (fun x l' => f x :: l') l [])

Note to developers (Niklas Halonen @xhalo32)

Even though foldMap is not autograded, we mark it as a hole just in case in the future something depended on it.

Write down a theorem fold_map_correct stating that foldMap is correct, and prove it in Lean.

theorem fold_map_correct {α : Type} {β : Type} {f : α → β} {l : List α} :
    foldMap f l = map f l := byα:Typeβ:Typef:α → βl:List α⊢ foldMap f l = map f l
  induction l with
  | nil =>nilα:Typeβ:Typef:α → β⊢ foldMap f [] = map f []
    rw [foldMap,nilα:Typeβ:Typef:α → β⊢ fold (fun x l' => f x :: l') [] [] = map f [] fold_nil,nilα:Typeβ:Typef:α → β⊢ [] = map f [] map_nilnilα:Typeβ:Typef:α → β⊢ [] = []]All goals completed! 🐙
  | cons _ _ ih =>consα:Typeβ:Typef:α → βhead✝:αtail✝:List αih:foldMap f tail✝ = map f tail✝⊢ foldMap f (head✝ :: tail✝) = map f (head✝ :: tail✝)
    rw [foldMapconsα:Typeβ:Typef:α → βhead✝:αtail✝:List αih:fold (fun x l' => f x :: l') tail✝ [] = map f tail✝⊢ fold (fun x l' => f x :: l') (head✝ :: tail✝) [] = map f (head✝ :: tail✝)] at *consα:Typeβ:Typef:α → βhead✝:αtail✝:List αih:fold (fun x l' => f x :: l') tail✝ [] = map f tail✝⊢ fold (fun x l' => f x :: l') (head✝ :: tail✝) [] = map f (head✝ :: tail✝)
    rw [fold_cons,consα:Typeβ:Typef:α → βhead✝:αtail✝:List αih:fold (fun x l' => f x :: l') tail✝ [] = map f tail✝⊢ f head✝ :: fold (fun x l' => f x :: l') tail✝ [] = map f (head✝ :: tail✝) map_cons,consα:Typeβ:Typef:α → βhead✝:αtail✝:List αih:fold (fun x l' => f x :: l') tail✝ [] = map f tail✝⊢ f head✝ :: fold (fun x l' => f x :: l') tail✝ [] = f head✝ :: map f tail✝ ihconsα:Typeβ:Typef:α → βhead✝:αtail✝:List αih:fold (fun x l' => f x :: l') tail✝ [] = map f tail✝⊢ f head✝ :: map f tail✝ = f head✝ :: map f tail✝]All goals completed! 🐙

Exercise★★(currying) (Advanced)

The type α → β → γ can be read as describing functions that take two arguments, one of type α and another of type β, and return an output of type γ. Recall from our discussion of partial application that this type is written α → (β → γ) when fully parenthesized. That is, if we have f : α → β → γ, and we give f an input of type α, it will give us as output a function of type β → γ. If we then give that function an input of type β, it will return an output of type γ. That is, every function in Lean takes only one input, but some functions return a function as output. This is precisely what enables partial application, as we saw above with plus3.

By contrast, functions of type α × β → γ — which when fully parenthesized is written (α × β) → γ — require their single input to be a pair. Both arguments must be given at once; there is no possibility of partial application.

It is possible to convert a function between these two types. Converting from α × β → γ to α → β → γ is called currying, in honor of the logician Haskell Curry. Converting from α → β → γ to α × β → γ is called uncurrying.

We can define currying as follows:

def prodCurry {α β γ : Type} (f : α × β → γ) (x : α) (y : β) : γ := f (x, y)

As an exercise, define its inverse, prodUncurry. Then prove the theorems below to show that the two are really inverses.

def prodUncurry {α β γ : Type} (f : α → β → γ) (p : α × β) : γ := solution!(
  f p.fst p.snd)

As a (trivial) example of the usefulness of currying, we can use it to shorten one of the examples that we saw above:

example : map (Nat.add 3) [2, 0, 2] = [5, 3, 5] := byα:Typeβ:Typeγ:Typex:αy:β⊢ map (Nat.add 3) [2, 0, 2] = [5, 3, 5] rflAll goals completed! 🐙

Thought exercise: before looking at the output of the following commands, can you calculate the types of prodCurry and prodUncurry?

@prodCurry : {α β γ : Type} → (α × β → γ) → α → β → γ#check @prodCurry
@prodUncurry : {α β γ : Type} → (α → β → γ) → α × β → γ#check @prodUncurry

@prodCurry : {α β γ : Type} → (α × β → γ) → α → β → γ

@prodUncurry : {α β γ : Type} → (α → β → γ) → α × β → γ

theorem uncurry_curry {α β γ : Type} {x : α} {y : β} {f : α → β → γ} :
    prodCurry (prodUncurry f) x y = f x y := byα:Typeβ:Typeγ:Typex:αy:βf:α → β → γ⊢ prodCurry (prodUncurry f) x y = f x y
  solution!
    rflAll goals completed! 🐙

theorem curry_uncurry {α β γ : Type} {p : α × β} {f : α × β → γ} :
    prodUncurry (prodCurry f) p = f p := byα:Typeβ:Typeγ:Typep:α × βf:α × β → γ⊢ prodUncurry (prodCurry f) p = f p
  solution!
    rflAll goals completed! 🐙

Exercise★★(nth_error_informal) (Advanced, Optional, Manually graded)

Recall the definition of the nth? function:

def nth? {α : Type} (l : List α) (n : Nat) : Option α :=
  match l with
  | [] => none
  | x :: l' => match n with
    | 0 => some x
    | n' + 1 => nth? l' n'

Write a careful informal proof of the following theorem:

∀ (l : List α) (n : Nat), l.length = n → nth? l n = none

Make sure to state the induction hypothesis explicitly.

Theorem: For all types α, lists l, and natural numbers n, if l.length = n then nth? l n = none.

Proof: By induction on l. There are two cases to consider:

If l = [], we must show nth? [] n = none. This follows immediately from the definition of nth?.
Otherwise, l = x :: l' for some x and l', and the induction hypothesis tells us that l'.length = n' → nth? l' n' = none, for any n'.

Let n be the length of l. We must show that nth? (x :: l') n = none.

But we know that n = l.length = (x :: l').length = l'.length + 1. So it's enough to show nth? l' l'.length = none, which follows directly from the induction hypothesis, picking l'.length for n'.

6.3.1. Church Numerals (Advanced)🔗

The following exercises explore an alternative way of defining natural numbers using the Church numerals, which are named after their inventor, the mathematician Alonzo Church. We can represent a natural number n as a function that takes a function f as a parameter and returns f iterated n times.

namespace Church

def CNat := ∀ (α : Type), (α → α) → α → α

Let's see how to write some numbers with this notation. Iterating a function once should be the same as just applying it. Thus:

def one : CNat :=
  fun (α : Type) (f : α → α) (x : α) => f x

Similarly, two should apply f twice to its argument:

def two : CNat :=
  fun (α : Type) (f : α → α) (x : α) => f (f x)

Defining zero is somewhat trickier: how can we "apply a function zero times"? The answer is actually simple: just return the argument untouched.

def zero : CNat :=
  fun (α : Type) (_ : α → α) (x : α) => x

More generally, a number n can be written as fun α f x => f (f ... (f x) ...), with n occurrences of f. Let's informally notate that as fun α f x => f^n x, with the convention that f^0 x is just x. Note how the doIt3Times function we've defined previously is actually just the Church representation of 3.

def three : CNat := @doIt3Times

So n α f x represents "do it n times", where n is a Church numeral and "it" means applying f starting with x.

Another way to think about the Church representation is that function f represents the successor operation on α, and value x represents the zero element of α. We could even rewrite with those names to make it clearer:

def zero' : CNat :=
  fun (α : Type) (_ : α → α) (zero : α) => zero
def one' : CNat :=
  fun (α : Type) (succ : α → α) (zero : α) => succ zero
def two' : CNat :=
  fun (α : Type) (succ : α → α) (zero : α) => succ (succ zero)

If we passed in Nat.succ as succ and 0 as zero, we'd even get the Peano naturals as a result:

example : zero Nat Nat.succ 0 = 0 := byα:Typeβ:Typeγ:Typex:αy:β⊢ zero Nat Nat.succ 0 = 0 rflAll goals completed! 🐙
example : one  Nat Nat.succ 0 = 1 := byα:Typeβ:Typeγ:Typex:αy:β⊢ one Nat Nat.succ 0 = 1 rflAll goals completed! 🐙
example : two  Nat Nat.succ 0 = 2 := byα:Typeβ:Typeγ:Typex:αy:β⊢ two Nat Nat.succ 0 = 2 rflAll goals completed! 🐙

One very interesting implication of the Church numerals is that we don't strictly need the natural numbers to be built-in to a functional programming language, or even to be definable with an inductive data type. It's possible to represent them purely (if not efficiently) with functions.

Of course, it's not enough just to "represent" numerals; we need to be able to do arithmetic with the representation. Show that we can by completing the definitions of the following functions. Make sure that the corresponding unit tests pass by proving them with rfl.

Exercise★★(church_scc) (Advanced)

Define a function that computes the successor of a Church numeral. Given a Church numeral n, its successor scc n should iterate its function argument once more than n. That is, given fun X f x => f^n x as input, scc should produce fun X f x => f^(n+1) x as output. In other words, do it n times, then do it once more.

def scc (n : CNat) : CNat := solution!(
  fun (α : Type) (f : α → α) (x : α) => f (n α f x))

example : scc zero = one := solution!(byα:Typeβ:Typeγ:Typex:αy:β⊢ scc zero = one rflAll goals completed! 🐙)
theorem scc_2 : scc one = two := solution!(by⊢ scc one = two rflAll goals completed! 🐙)
theorem scc_3 : scc two = three := solution!(by⊢ scc two = three rflAll goals completed! 🐙)

Exercise★★★(church_plus) (Advanced)

Define a function that computes the addition of two Church numerals. Given fun X f x => f^n x and fun X f x => f^m x as input, plus should produce fun X f x => f^(n + m) x as output. In other words, do it n times, then do it m more times.

Hint: the "zero" argument to a Church numeral need not be just x.

def plus (n m : CNat) : CNat := solution!(
  fun (α : Type) (f : α → α) (x : α) => n α f (m α f x))

theorem plus_1 : plus zero one = one := solution!(by⊢ plus zero one = one rflAll goals completed! 🐙)
theorem plus_2 : plus two three = plus three two := solution!(by⊢ plus two three = plus three two rflAll goals completed! 🐙)
theorem plus_3 : plus (plus two two) three = plus one (plus three three) := solution!(by⊢ plus (plus two two) three = plus one (plus three three) rflAll goals completed! 🐙)

Exercise★★★(church_mult) (Advanced)

Define a function that computes the multiplication of two Church numerals.

Hint: the "successor" argument to a Church numeral need not be just f.

Warning: Lean will not let you pass CNat itself as the type α argument to a Church numeral; you will get a "sort mismatch" error between Type 1 and Type 2. Don't worry too much about what this means right now, but know that this is Lean's way of preventing a paradox in which a type contains itself. So leave the type argument unchanged.

def mult (n m : CNat) : CNat := solution!(
  fun (α : Type) (f : α → α) (x : α) => n α (m α f) x)


theorem mult_1 : mult one one = one := solution!(by⊢ mult one one = one rflAll goals completed! 🐙)
theorem mult_2 : mult zero (plus three three) = zero := solution!(by⊢ mult zero (plus three three) = zero rflAll goals completed! 🐙)
theorem mult_3 : mult two three = plus three three := solution!(by⊢ mult two three = plus three three rflAll goals completed! 🐙)

Exercise★★★(church_exp) (Advanced)

Exponentiation:

Define a function that computes the exponentiation of two Church numerals.

Hint: the type argument to a Church numeral need not just be α. Finding the right type can be tricky.

def exp (n m : CNat) : CNat := solution!(
  fun (α : Type) (f : α → α) (x : α) => m (α → α) (n α) f x)

theorem exp_1 : exp two two = plus two two := solution!(by⊢ exp two two = plus two two rflAll goals completed! 🐙)
theorem exp_2 : exp three zero = one := solution!(by⊢ exp three zero = one rflAll goals completed! 🐙)
theorem exp_3 : exp three two = plus (mult two (mult two two)) one := solution!(by⊢ exp three two = plus (mult two (mult two two)) one rflAll goals completed! 🐙)

end Church

Source revision: 9cc9a7b, committed 2026-09-28 19:09 UTC