Lecture 2.1: Functional Programming — Lists

We taking a closer look at the basics of typed functional programming: inductive types, pattern matching, recursive functions, and inductive proofs

Then we review various definitions, lemmas, and proofs about lists; these are good exercises to learn to use a proof assistant

We also review more advanced concepts of Lean's dependent type theory: type classes and decidability

Inductive types

An inductive type (also called inductive datatype, algebraic datatype, or just datatype) is a type that consists all the values that can be built using a finite number of applications of its constructors, and only those

Mottos:

For nat (= ℕ):

In addition, inductive types are always finite; succ (succ (succ ...)) is not a value, because there exists no x such that x = succ x

Already in lecture 1.1 and in the corresponding exercises, we saw some basic inductive types: the natural numbers (in Peano-style unary notation), the finite lists, and a type of arithmetic expressions

Comparison with Java

Inductive types are a concise, convenient way of representing acyclic data in a program

Compare the following Lean specification (from exercise 1.1) with the corresponding Java program, which effectively achieves the same thing:

inductive aexp
| num : ℤ → aexp
| var : string → aexp
| add : aexp → aexp → aexp
| sub : aexp → aexp → aexp
| mul : aexp → aexp → aexp
| div : aexp → aexp → aexp

In Java: ```java public interface AExp { }

public class Num implements AExp {
    public int num;
    public Num(int num) { this.num = num; }
}

public class Var implements AExp {
    public String var;
    public Var(String var) { this.var = var; }
}

public class Add implements AExp {
    public AExp left;
    public AExp right;
    public Add(AExp left, AExp right) { this.left = left; this.right = right; }
}

public class Sub implements AExp {
    public AExp left;
    public AExp right;
    public Sub(AExp left, AExp right) { this.left = left; this.right = right; }
}

public class Mul implements AExp {
    public AExp left;
    public AExp right;
    public Mul(AExp left, AExp right) { this.left = left; this.right = right; }
}

public class Div implements AExp {
    public AExp left;
    public AExp right;
    public Div(AExp left, AExp right) { this.left = left; this.right = right; }
}

``` (Admittedly, the Java version is more extensible, since users can add new "constructors" by providing new classes)

Recursive functions

If we had to implement an eval function in Java, we would probably add it as part of AExp's interface and implement it in each subclass

For Add, Sub, Mul, and Div, we would recursively call eval on the left and right objects; even Java has recursion

In Lean, the syntax is very compact: We define a single function and use pattern matching to distinguish the six cases

def eval (env : string → ℤ) : aexp → ℤ
| (aexp.num i)    := i
| (aexp.var x)    := env x
| (aexp.add e₁ e₂) := eval e₁ + eval e₂
| (aexp.sub e₁ e₂) := eval e₁ - eval e₂
| (aexp.mul e₁ e₂) := eval e₁ * eval e₂
| (aexp.div e₁ e₂) := eval e₁ / eval e₂

We can have pattern matching without recursion (e.g. in the num and var cases)

We can have also have recursion without pattern matching

Primitive recursion is when we peal off exactly one constructor from the value on which we recurse

In this (and other) cases, Lean can automatically prove termination

Later in the course, we will see what to do when the termination check fails

Pattern maching within arbitrary terms

match term1, ..., termM with

| pattern11, ..., pattern1M := result1

⋮

| patternN1, ..., patternNM := resultN

end

match allows nonrecursive pattern matching in terms

Example:

match n, xs, v with
| 0,     [],      v := ...
| n + 1, [],      v := ...
| n + 1, x :: xs, v := ...
end

In contrast to pattern matching after lemma or def, the patterns are separated by commas (,), so parentheses are optional

Inductive proofs

By the Curry–Howard correspondence, a proof by induction is the same as a recursively specified proof term

When we invoke the induction hypothesis, we are really just calling a recursive function (the lemma) recursively

This explains why the induction hypothesis has the same name as the lemma we prove

By Curry–Howard, structural induction (or mathematical induction on ℕ) is the same as primitive recursion

Lean's termination checker is used to prove well-foundedness of the induction principle

Lists

An inductive polymorphic type constructed from nil and cons

Aliases:

[] = nil

x :: xs = cons x xs

[ x1, ..., xN ] = cons x1 (... (cons xN nil)...)

Primitive recursion:

def f : list α → ...
| []        := ...
| (x :: xs) := ... x ... xs ... (f xs) ...

Structural induction:

lemma l : ∀x : list α, ...
| []        := ...
| (x :: xs) := ... x ... xs ... (l xs) ...

Pattern matching:

match xs with
| []      := ...
| x :: xs := ...
end

Overlapping patterns

It is possible to write equations with overlapping patterns, e.g.

def f {α : Type} : list α → ...
| [] := ...
| xs := ... xs ...

The first matching equation is taken

Internally, this is the same as

def f {α : Type} : list α → ...
| []        := ...
| (x :: xs) := ... (x :: xs) ...

We generally recommend the latter style, because it is less surprising

Demo (first part)

21_lecture.lean

Type classes

Type classes are Lean's implementation of interfaces

They are very generic, and associate automatically computed information to an input value (usually types or propositions)

Function parameters are marked as type class instances using [ type-class ]

Examples:

def f (p : Prop) [decidable p] : ℕ := ...

def half {α : Type} [field α] : α := 1 / 2

We do not need to provide a name the parameter; it is passed on implicitly

Division in half has an implicit type class parameter filled in with the field α value

Decidability

Propositions p : Prop are generally not decidable; we use the type class decidable p to annotate that a proposition p is decidable

decidable p is a type class containing either a proof of p or a proof of its negation ¬ p

if proposition then term else term works only for decidable proposition

Hint:

if h : p then ... else ... is useful in proofs; an alternative is by_cases

Vectors

Vectors are the dependently typed version of lists:

Inductive definition:

inductive vec (α : Type) : ℕ → Type
| vnil {} : vec 0
| vcons (a : α) (n : ℕ) (v : vec n) : vec (n + 1)

Warning: Vectors are difficult to use (some would say painful); we will review them very briefly but they are not exam material

Demo (second part)

21_lecture.lean

Hints on how to write backward proofs "mindlessly"

For logic puzzles, such as those we saw in exercise 1.3 and homework 1.3, we advocate a "mindless", "video game" style of backward reasoning that relies mostly on intro and apply (and variants such as intros and exact)

Some heuristics that often work:

It is hard to teach some of these things in class; there is no better way for you to learn this than by doing it, hence the importance of the exercises

Newly introduced syntax

Term language

Syntax Description
match ... with ... end nonrecursive pattern matching on multiple values
if ... then ... else ... case distinction on a decidable proposition
[ type-class ] parameter annotation for type class instances

Tactic

Name Description
by_cases performs a case distinction on an if condition

Commands

Name Description
export makes names (e.g., of constructors) available outside their namespaces
set_option changes or activates tracing, syntax output, etc.
parameter, parameters fixes a variable in a section; it is then added implicitly as an argument to each definition, lemma, etc.

Reference