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
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:
No junk: The type contains no values beyond those expressible using the constructors
No confusion: Values built in a different ways are different
For nat
(= ℕ
):
"No junk" means that there exist no special values like, say, –1 or ε, that cannot be expressed using a finite combination of zero
and succ
"No confusion" is what ensures that zero
≠ succ
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
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)
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
match
term1,
...,
termMwith
|
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
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
An inductive polymorphic type constructed from nil
and cons
Aliases:
[]
=nil
x
::
xs =cons
x xs
[
x1, ..., xN]
=cons
x1 (... (cons
xNnil
)...)
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
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
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
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 : pthen
...else
... is useful in proofs; an alternative isby_cases
Vectors are the dependently typed version of lists:
list α
is the type of finite lists over α
vec α n
is the type of lists over α
of length n
(or vectors of size n
)
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
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:
If the goal (the formula that follows ⊢
in the goal state) is an implication, i.e. φ → ψ
, use intro hφ
or intros hφ
to move φ
into your hypotheses, where you can use it: (hφ : φ) ⊢ ψ
If the goal is a universal quantification ∀x : σ, φ
, use intro
or intros
; by Curry–Howard, implication →
is merely an instance of ∀
(= Π
), so this intro
is exactly the same command as the intro
mentioned in the previous point
Otherwise, look for an assumption (or a lemma) whose conclusion has the same shape as the goal (possibly containing variables that can be matched against the goal), and apply it; thus, if your goal is ⊢ q
and you have an assumption hpq : p -> q
, try apply hpq
Beware of negation: A goal of the form ⊢ ¬ φ
is really the same as ⊢ φ → false
, so you can use intro hφ
to get hφ : φ ⊢ false
Sometimes you can make progress by replacing the goal by false
(and then using apply
with a hypothesis of the form φ → false
or ¬ φ
), by entering apply false.elim
Often you have several choices (e.g. between or.intro_left
and or.intro_right
); remember which choices you have made, and backtrack if you reach a dead end or have the impression you are not making any progress
If you have difficulties carrying out a proof, it can be a good idea to check whether the goal actually holds (is provable) under the given assumptions; just because you started with a provable lemma statement does not mean your goal will always remain provable (e.g. if you use "unsafe" rules such as or.intro_left
)
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
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 |
Name | Description |
---|---|
by_cases |
performs a case distinction on an if condition |
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. |