Propositions and Proofs

As we have mentioned, proofs and propositions are terms, with propositions as types. The universe Prop is the type of propositions. To start with, it is best to ignore the difference between Prop and Type and treat them as the same.

A logical statement like 1 ≤ 2 is a proposition and has type Prop.

The proposition 0 ≤ 2 is true and has proof Nat.zero_le 2.

A proposition may be neither proved nor disproved. So we cannot evaluate it. We can evaluate it if it is decidable.

We can combine propositions to make propositions:

• If P and Q are propositions, then P ∧ Q is the proposition "P and Q".
• If P and Q are propositions, then P ∨ Q is the proposition "P or Q".
• If P and Q are propositions, then P → Q is the proposition "if P then Q".
• If P is a proposition, then ¬ P is the proposition "not P", which is P → False.

The key idea is that function application is exactly analogous to the logical rule of inference called modus ponens.

def modus_ponens {P Q : Prop} (h₁ : P) (h₂ : P → Q) : Q

Equations

• ⋯ = ⋯

def application {α β : Type} (a : α) (f : α → β) : β

Equations

• application a f = f a

We apply modus-ponens with P being 0 ≤ 2 and P → Q being Nat.succ_le_succ applied to 0 and 2.

Some proofs at term level

def one_le_three : 1 ≤ 3

Equations

• one_le_three = ⋯

def two_le_five : 2 ≤ 5

Equations

• two_le_five = ⋯

def wrong_three_le_one (h : 2 ≤ 0) : 3 ≤ 1

Equations

• ⋯ = ⋯

Proof Irrelevance

In Lean, any two proof terms of the same proposition are equal by definition. This is called proof irrelevance.

theorem proof_irrelevance {P : Prop} (h₁ h₂ : P) : h₁ = h₂

Universes

• Universes in Lean are called Sorts, they are Sort 0, Sort 1, etc.
• Prop is Sort 0.
• Type is Sort 1.
• Type n is Sort n.succ.
• Strictly speaking, the n here is a universe level, not a natural number.

Dependent Function Types

The type of Nat.zero_le is ∀ (n : Nat), 0 ≤ n. We will write it more like a function type

def my_zero_le (n : Nat) : Nat.le 0 n

Equations

• ⋯ = ⋯

We saw that if α and β are types (or props), then α → β is the type of functions from α to β.

If instead we have β : α → Typeor β : α → Prop, then (a : α) → β a (more formally Π (a : α), β a) is the type of dependent functions from a : α to β a.