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

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

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

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