# 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:

* **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


## 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 peel 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`](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:

* `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


## Demo (second part)

[`21_lecture.lean`](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:

* 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


## 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

* [_Theorem Proving in Lean_](https://leanprover.github.io/theorem_proving_in_lean/), Chapters 7, 8, and 10
