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

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

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

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, α → α)
```

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)

`assume`

Moves variables or assumptions from the goal into the local context

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

tactic

`have`

`:`

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`

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`

Alias:

`, from`

lemma:=`by`

exactlemma

`let`

`:`

`:=`

`in`

...Introduces a new local definition

Similar to `have`

but for computable data

Unfolding a `let`

corresponds to ζ-reduction (lecture 1.2)

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`

expr0op1expr1`:`

proof1

`...`

op2expr2`:`

proof2⋮

`...`

opNexprN`:`

proofN

Ellipsis (`...`

) is part of the syntax

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

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

Syntax | Description |
---|---|

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

*Theorem Proving in Lean*, Chapters 2–5

Further reading:

*Logical Verification Course Notes*by Femke van Raamsdonk*Type Theory and Formal Proof*by Rob Nederpelt and Herman Geuvers*Types and Programming Languages*by Benjamin Pierce*An Introduction to Mathematical Logic and Type Theory—To Truth Through Proof*by Peter Andrews*Lambda Calculus with Types*by Henk Barendregt et al.

These notes are largely inspired by *Theorem Proving in Lean*