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

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:

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

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

Newly introduced syntax

Proof language

Tactics

Tactic combinator

References

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

Acknowledgment

These notes are largely inspired by Theorem Proving in Lean