# Lecture 1.3: Basics — More Logic and Proofs

We take a closer look at the calculus of inductive constructions (CIC) and improve our proof language proficiency by learning some new proof constructs, including heuristics for writing backward proofs in a "mindless" fashion


## Simple type theory (STT)

_Simple type theory_ (STT) or _higher-order logic_ (HOL) is a fragment of CIC

It corresponds roughly to the simply typed λ-calculus extended with an equality predicate (actually, a type-indexed family of predicates)

The original STT was simply typed; HOL systems feature top-level polymorphism


## Types and terms

Similar to simply typed λ-calculus or typed functional programming languages (ML, OCaml, Haskell)

Types `σ`, `τ`:

* type variables `α`
* basic types `T`
* complex types `T σ1 ... σN`

Some type constructors `T` are written infix, e.g. `→` (function type)

Function arrow is right-associative: `σ1 → σ2 → σ3 → τ` = `σ1 → (σ2 → (σ3 → τ))`

In Lean, type variables must be bound using `Π` or its alias `∀`, e.g. `Πα, α → α`; in STT, this is normally implicit

Terms `t`, `u`:

* variables `x`
* applications `t u`
* λ-abstractions `λx, t`

**Currying** (actually due to Schönfinkel): applications can be iterated (e.g. `f x y z`), partially applied (e.g., `f x y`; `f x`), or left unapplied (`f`)

Application is left-associative: `f x y z` = `((f x) y) z`


## Type inference and type checking

Type checking and type inference are decidable problems, but this property is quickly lost if features such as overloading or subtyping are added

The type inference algorithm, based on unification, is due to Hindley and Milner

Type judgment: `Γ ⊢ t : σ`, meaning `t` has type `σ` in context `Γ`

    Γ ⊢ t : σ → τ    Γ ⊢ u : σ
    ——————————————————————————— App
    Γ ⊢ t u : τ

    Γ, x : σ ⊢ t : τ
    ———————————————————————— Lam
    Γ ⊢ (λx : σ, t) : σ → τ

Horizontal bars denote derivation rules in a [formal system](https://en.wikipedia.org/wiki/Formal_system)

Type annotations `t : σ` can be used to guide type inference

_Higher-order types_: types containing left-nested `→` arrows, e.g. `(σ → σ) → σ`, corresponding to functions passed as arguments


## Dependent types

Dependent types are the definining feature of the _dependent type theory_ (DTT) family of logics

Consider a function `pick` that take a natural number (`ℕ` = {0, 1, 2, ...}) and that returns a natural number between 0 and `x`

Conceptually, `pick` has a dependent type, namely `Πx : ℕ, {y : ℕ // y ≤ x}`

(The `{` ... `//` ... `}` syntax denotes a subtype; we will come back to these later)

We can think of this type as a `ℕ`-indexed family, where each member's type may depend on the index: `pick x : {y : ℕ // y ≤ x}`

Unless otherwise specificed, _dependent type_ often means a type depending on a *term*, like the above; this is what we mean when we say that simple type theory does not support dependent types

But a type may also depend on another type, e.g. `list` or `λα, list α`; `λα, α → α`

A term may depend on a type, e.g. `λα, λx : α, x` (a polymorphic identity function)

Of course, a term may also depend on a term

In summary, there are four cases for `λx, t` in CIC:

Body (`t`) |                | Argument (`x`) | Description
---------- | -------------- | -------------- | -----------
Term       | _depending on_ | Term           | A good old λ-abstraction
Type       | _depending on_ | Term           | A dependent type (stricto senso)
Term       | _depending on_ | Type           | A polymorphic term
Type       | _depending on_ | Type           | A type constructor

The last three rows correspond to the three axes of Barendregt's [lambda cube](https://en.wikipedia.org/wiki/Lambda_cube)

Alias:

> `σ → τ` := `Π_ : σ, τ`

Revised typing rule:

    Γ ⊢ t : Πx : σ, τ[x]    Γ ⊢ u : σ
    —————————————————————————————————— App'
    Γ ⊢ t u : τ[u]

    Γ, x : σ ⊢ t : τ
    ————————————————————————————— Lam'
    Γ ⊢ (λx : σ, t) : (Πx : σ, τ)

These two rules degenerate to `App` and `Lam` if `x` does not occur in `τ`

Example of `App'`:

    ⊢ pick : Πx : ℕ, {y : ℕ // y ≤ x}    ⊢ 5 : ℕ
    ————————————————————————————————————————————— App'
    ⊢ pick 5 : {y : ℕ // y ≤ 5}

Example of `Lam'`:

    α : Type, x : α ⊢ x : α
    ——————————————————————————————— Lam or Lam'
    α : Type ⊢ (λx : α, x) : α → α
    ————————————————————————————————————————————— Lam'
    ⊢ (λα : Type, λx : α, x) : (Πα : Type, α → α)


## Curry–Howard(–De Bruijn) correspondence

Also called PAT principle:

* **PAT = propositions as types**
* **PAT = proofs as terms**

De Bruijn, Curry, Howard, and possibly others independently noticed that in DTT:

* propositions are isomorphic to types
* proofs are isomorphic to terms

Hence, we _identify_ proofs and terms as well as propositions and types

Let us go through the _dramatis personae_ slowly

Types:

* `σ → τ` is the type of (total) functions from `σ` to `τ`
* `Πx : σ, τ[x]` is the dependent type from `x : σ` to `τ[x]`

Propositions:

* `φ → ψ` can be read as "`φ` implies `ψ`", or as the type of **functions** mapping proofs of `φ` to proofs of `ψ`
* `∀x : σ, ψ[x]` can be read as "for all `x`, `ψ[x]`", or as the type of **functions** mapping values `x` of type `σ` to proofs of `ψ[x]`
* `∀h : φ, ψ[h]` is the type of **functions** mapping proofs `h` of `φ` to proofs of `ψ[h]` (occasionally useful)

Alias:

> `∀` := `Π`

Terms:

* declared constants are terms
* `t u` is the application of function `t` to value `u`
* `λx, t[x]` is a function mapping `x` to `t[x]`

Proofs:

* a lemma name is a term
* `add_comm m n` is the application of `m` and `n` to the lemma `add_comm`
* assumptions of an implication can be discharged also by application, e.g. `human_imp_mortal socrates_is_human`; this is called _modus ponens_
* `λn : σ, h[n]`, where `h : φ[n]`, is a proof of `∀n : σ, φ[n]`
* `λh' : ψ, h[h']`, where `h : φ[h']`, is a proof of `∀h' : ψ, φ[h']`

The last case above is rarely needed in its full generality, but we often have the case where `φ` does not depend on `h'`:

* `λh' : ψ, h[h']`, where `h : φ`, is a proof of `∀h' : ψ, φ`, i.e. `ψ → φ` (an implication)


## Structured proofs

### `assume` _name1_ ... _nameN_

Moves variables or assumptions from the goal into the local context

Can be seen as a structured version of the `intros` tactic

### `have` _name_ `:` _proposition_

Introduced in lecture 1.2

Proves an intermediate lemma statement, which can refer to the local context

Followed by `:=`, or by `,` and one of `from`, `by`, or `begin` ... `end`

### `show` _proposition_

Repeats the goal to prove, followed by `from`, `by`, or `begin` ... `end`
Followed by `,` and one of `from`, `by`, or `begin` ... `end`

Useful for documentation purposes

### `from` _proof_

Alias:

> `, from` _lemma_ := `by` exact _lemma_

### `let` _name_ `:` _type_ `:=` _term_ `in` ...

Introduces a new local definition

Similar to `have` but for computable data

Unfolding a `let` corresponds to ζ-reduction (lecture 1.2)


## Calculational proofs

In informal mathematics, we often use transitive chains of equalities, inequalities, or equivalences (e.g. `a ≥ b ≥ c`)

In Lean, such calculational proofs are supported by `calc`

It provides a nice syntax and takes care of transitivity

Syntax:

> `calc` _expr0_ _op1_ _expr1_ `:` _proof1_
>
> `...` _op2_ _expr2_ `:` _proof2_
>
>  ⋮
> 
> `...` _opN_ _exprN_ `:` _proofN_

Ellipsis (`...`) is part of the syntax


## Demo

[`13_lecture.lean`](13_lecture.lean)


## Newly introduced syntax

### Proof language

Keyword        | Description
-------------- | ---
`assume`       | states the goal to prove
`show`         | states the goal to prove
`from`         | used together with `show` to specify a proof
`let` ... `in` | introduces a new local definition
`calc`         | combines proofs by transitivity, e.g. `a ≥ b ≥ c`

### Tactics

Name         | Description
------------ | -----------
`assumption` | solves the goal using an hypothesis from the local context
`apply`      | matches the goal with the conclusion of the rule and add the rule's hypothesis as new goals
`intro`      | moves the top quantifier from the goal to an hypothesis in the local context
`intros`     | moves all quantifiers from the goal to hyptheses in the local context
`exact`      | solves the goal by the specified term
`refine`     | fills the goal by the specified term and add all holes in the term as new goals
`dunfold`    | unfolds a definition without pattern matching (e.g. `not`)

### Tactic combinator

Syntax      | Description
----------- | -----------
`<|>`       | tries the first tactic first, and upon failure try the second tactic


## References

* [_Theorem Proving in Lean_](https://leanprover.github.io/theorem_proving_in_lean/), Chapters 2–5

Further reading:

* [_Logical Verification Course Notes_](https://www.cs.vu.nl/~jbe248/lv2017/notes.pdf) by Femke van Raamsdonk
* [_Type Theory and Formal Proof_](https://www.win.tue.nl/~wsinrpn/book_type_theory.htm) by Rob Nederpelt and Herman Geuvers
* [_Types and Programming Languages_](https://mitpress.mit.edu/books/types-and-programming-languages) by Benjamin Pierce
* [_An Introduction to Mathematical Logic and Type Theory—To Truth Through Proof_](https://www.springer.com/de/book/9781402007637) by Peter Andrews
* [_Lambda Calculus with Types_](https://www.cambridge.org/core/books/lambda-calculus-with-types/65DC18AC262498B0F93A688CBE748048) by Henk Barendregt et al.


## Acknowledgment

These notes are largely inspired by _Theorem Proving in Lean_
