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 σ, τ:

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:

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

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


σ → τ := Π_ : σ, τ

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:

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

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

Let us go through the dramatis personae slowly




:= Π



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

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


, 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


calc expr0 op1 expr1 : proof1

... op2 expr2 : proof2

... opN exprN : proofN

Ellipsis (...) is part of the syntax



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


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


Further reading:


These notes are largely inspired by Theorem Proving in Lean