Module 1 · Lesson 2

Propositions as Types

Lean represents logical propositions as types. Once that idea is clear, the rest of theorem proving in Lean makes much more sense.

The Universe of Propositions

Lean has different "universes" for different kinds of types:

lean

Try it

1-- Data types live in Type
2#check Nat        -- Nat : Type
3#check String     -- String : Type
4#check List Nat   -- List Nat : Type
5
6-- Propositions live in Prop
7#check True       -- True : Prop
8#check False      -- False : Prop
9#check 2 + 2 = 4  -- 2 + 2 = 4 : Prop

Prop is special: it's the universe of things that are either true or false. Every proposition is a type, but a type specifically designed to express a logical claim.

Equality

The most common proposition is equality:

lean

Try it

1-- Equality is a proposition
2#check (5 = 5)        -- 5 = 5 : Prop
3#check (1 + 1 = 2)    -- 1 + 1 = 2 : Prop
4#check (1 + 1 = 3)    -- 1 + 1 = 3 : Prop (still a valid Prop, just false)
5
6-- Equality for any type
7#check ("hello" = "hello")  -- "hello" = "hello" : Prop
8#check ([1,2] = [1,2])      -- [1, 2] = [1, 2] : Prop

Note that 1 + 1 = 3 is a valid proposition—it's just false. You can state it, but you can't prove it.

True and False

lean

Try it

1-- True: a proposition that's trivially provable
2#check True       -- True : Prop
3example : True := trivial
4
5-- False: a proposition with no proof
6#check False      -- False : Prop
7-- example : False := ???  -- Impossible! No term has type False

True is a type with exactly one term (trivial).False is a type with no terms—that's what makes it false.

Key Takeaway

A proposition is true if you can construct a term of that type. It's false if no such term exists.

Implication: Functions

The logical "implies" (→) is represented as a function type:

lean

Try it

1-- "If A then B" is the type A → B
2-- A proof is a function from proofs of A to proofs of B
3
4example : True → True := fun _ => trivial
5
6-- "If 1 = 1, then 2 = 2"
7example : (1 = 1) → (2 = 2) := fun _ => rfl
8
9-- Read: given a proof of 1 = 1, return a proof of 2 = 2
10-- The proof of 1 = 1 isn't even used—2 = 2 is independently true

To prove an implication, you write a function. The function takes a proof of the hypothesis and produces a proof of the conclusion.

Constructors and Destructors

Every logical connective comes as a pair: a way to build a proof (the constructor, used when the connective is in the goal) and a way to take apart a proof (the destructor, used when the connective is in a hypothesis). Nearly every tactic you will learn is one of these two moves.

Connective	Build (goal)	Use (hypothesis)
A → B	`fun h => …` / `intro h`	apply it: `h a`
A ∧ B	`⟨ha, hb⟩` / `constructor`	`h.left`, `h.right` / `obtain ⟨ha, hb⟩ := h`
A ∨ B	`Or.inl` / `Or.inr` / `left`, `right`	`cases h` — you must handle both
¬A	`intro h`, then derive `False`	apply to a proof of A: `absurd ha h`
∀ x, P x	`intro x`	specialise: `h 5`
∃ x, P x	`⟨w, proof⟩` / `exact ⟨w, _⟩`	`obtain ⟨x, hx⟩ := h`
A ↔ B	`⟨mp, mpr⟩` / `constructor`	`h.mp`, `h.mpr`

💡

This table is the single most useful thing to memorise when starting out. Faced with any goal, ask: what is the outermost connective, and is it in the goal or in a hypothesis? That determines the tactic. Everything else is detail.

Conjunction: Products

"A and B" is represented as a pair:

lean

Try it

1-- And is defined like a structure
2-- structure And (a b : Prop) : Prop where
3--   left : a
4--   right : b
5
6-- To prove A ∧ B, provide proofs of both
7example : True ∧ True := ⟨trivial, trivial⟩
8
9example : (1 = 1) ∧ (2 = 2) := ⟨rfl, rfl⟩
10
11-- Access parts with .left and .right (or .1 and .2)
12example (h : True ∧ (1 = 1)) : True := h.left
13example (h : True ∧ (1 = 1)) : 1 = 1 := h.right

Disjunction: Sum Types

"A or B" is represented as a sum (tagged union):

lean

Try it

1-- Or has two constructors
2-- inductive Or (a b : Prop) : Prop where
3--   | inl : a → Or a b
4--   | inr : b → Or a b
5
6-- Prove left side
7example : True ∨ False := Or.inl trivial
8
9-- Prove right side
10example : False ∨ True := Or.inr trivial
11
12-- Either side works
13example : (1 = 1) ∨ (1 = 2) := Or.inl rfl

Negation

"Not A" is defined as "A implies False":

lean

Try it

1-- ¬A is defined as A → False
2#print Not  -- def Not (a : Prop) : Prop := a → False
3
4-- To prove ¬A, assume A and derive a contradiction
5example : ¬False := fun h => h  -- If False, then False (trivially)
6
7-- 1 ≠ 2 means (1 = 2) → False
8example : 1 ≠ 2 := by decide

ℹ

The symbol ≠ is notation for ¬(... = ...), which expands to (... = ...) → False.

Iff: If and Only If

A ↔ B is a structure holding two implications. It is not the same as A = B, though for propositions the two turn out to be equivalent (that is the axiom propext).

lean

Try it

1-- structure Iff (a b : Prop) : Prop where
2--   mp  : a → b      ("modus ponens" direction)
3--   mpr : b → a      ("reverse")
4
5example (P Q : Prop) : (P ∧ Q) ↔ (Q ∧ P) :=
6  ⟨fun h => ⟨h.2, h.1⟩, fun h => ⟨h.2, h.1⟩⟩
7
8-- Using one: pick a direction
9example (P Q : Prop) (h : P ↔ Q) (hp : P) : Q := h.mp hp
10example (P Q : Prop) (h : P ↔ Q) (hq : Q) : P := h.mpr hq
11
12-- Iff is also usable by rw and simp, unlike a plain implication
13example (P Q : Prop) (h : P ↔ Q) (hp : P) : Q := by rw [← h]; exact hp

💡

Prefer ↔ over two separate lemmas when you can. It is a single name, and rw and simp can rewrite with an Iffexactly as they rewrite with an equation. A one-directional implication cannot be used that way.

Classical vs Constructive

Lean's core logic is constructive: to prove A ∨ B you must say which one holds. That means the law of excluded middle, P ∨ ¬P, is not automatic — it is an axiom you opt into.

lean

Try it

1-- Not provable constructively; available as an axiom
2example (P : Prop) : P ∨ ¬P := Classical.em P
3
4-- Also classical: double negation elimination
5example (P : Prop) (h : ¬¬P) : P := Classical.byContradiction fun hn => h hn
6
7-- From a contradiction, anything
8example (P Q : Prop) (h : P) (hn : ¬P) : Q := absurd h hn

ℹ

In practice, Lean and Mathlib use classical reasoning freely, and tactics like by_contra, push_neg, and tauto rely on it. You will see Classical.choice in the output of #print axioms for most real theorems, and that is completely normal — it is one of Lean's three standard axioms, not a red flag.

Quantifiers

Universal: For All (∀)

lean

Try it

1-- ∀ x : T, P x is a dependent function type
2-- A proof is a function that works for any x
3
4example : ∀ n : Nat, n = n := fun n => rfl
5
6-- n + 0 = n holds by rfl: Nat.add recurses on its SECOND argument,
7-- so n + 0 reduces to n by definition.
8example : ∀ n : Nat, n + 0 = n := fun _ => rfl
9
10-- 0 + n = n does NOT hold by rfl! Nothing can reduce until n is known.
11-- example : ∀ n : Nat, 0 + n = n := fun n => rfl   -- type mismatch
12example : ∀ n : Nat, 0 + n = n := fun n => Nat.zero_add n
13
14-- Multiple quantifiers
15example : ∀ a b : Nat, a + b = b + a := Nat.add_comm

⚠

That asymmetry is worth remembering — it is the single most common early surprise. n + 0 = n is definitional (provable by rfl), while 0 + n = n needs a theorem (Nat.zero_add, proved by induction). The reason is purely the direction Nat.add recurses. Whenever rfl mysteriously fails on an arithmetic identity, check whether the variable is on the side that blocks reduction.

Existential: There Exists (∃)

lean

Try it

1-- ∃ x : T, P x is a dependent pair (witness + proof)
2-- Provide a specific x and prove P holds for it
3
4example : ∃ n : Nat, n > 5 := ⟨10, by decide⟩
5
6example : ∃ n : Nat, n + n = 10 := ⟨5, rfl⟩
7
8-- The witness and proof are bundled together
9example : ∃ s : String, s.length = 5 := ⟨"hello", rfl⟩

Deep Dive: Proof Irrelevance

In Prop, all proofs of the same proposition are considered equal. This is called "proof irrelevance."

lean

Try it

1-- Two different proofs of the same thing
2example (p q : 1 = 1) : p = q := rfl
3
4-- This is why Prop is special: only truth matters, not how you proved it

This makes sense logically: if you know something is true, you don't carehow it was proven. The fact that it's true is what matters.

Summary Table

Logic	Lean Type	To Prove
A implies B	A → B	Write a function
A and B	A ∧ B	Provide both proofs
A or B	A ∨ B	Provide one proof
Not A	¬A (= A → False)	Derive contradiction
For all x, P(x)	∀ x, P x	Function over all x
Exists x, P(x)	∃ x, P x	Witness + proof

Exercise: Conjunction

Prove that if you have P and Q, then you can prove P ∧ Q.

lean

Try it

1example (P Q : Prop) (hp : P) (hq : Q) : P ∧ Q := by
2  exact And.intro hp hq

What is a Proof?Next: The Proof State