Lean 4 Propositions and Proofs: Curry-Howard Guide

Lean 4 is simultaneously a functional programming language and an interactive theorem prover. At the heart of its logical system is the Curry-Howard correspondence: every proposition is a type, and every proof of that proposition is a term of that type. This elegant unification means that writing a proof is the same activity as writing a program — the kernel checks both with the same type checker.

`Prop` vs `Type`

In Lean 4 there are two universes that matter for logic:

Type u — the universe of ordinary data types like Nat, List α, String
Prop — the universe of propositions

-- Ordinary data lives in Type
#check Nat       -- Nat : Type
#check List Nat  -- List Nat : Type

-- Propositions live in Prop
#check 1 + 1 = 2               -- 1 + 1 = 2 : Prop
#check ∀ n : Nat, n + 0 = n    -- ∀ (n : Nat), n + 0 = n : Prop

Propositions are proof-irrelevant: any two proofs of the same proposition are definitionally equal. This is captured by proof_irrel:

-- From Init/Core.lean:
-- theorem proof_irrel {a : Prop} (h₁ h₂ : a) : h₁ = h₂ := rfl
example (p : Prop) (h₁ h₂ : p) : h₁ = h₂ := proof_irrel h₁ h₂

Because proofs are erased at runtime, choosing between two proofs of the same proposition has no computational cost.

Prop is Sort 0 and Type u is Sort (u+1). Both are special cases of the universe Sort u. The type Prop satisfies impredicativity: a ∀ over Prop landing in Prop stays in Prop.

Logical Connectives

Lean 4’s logical connectives are defined as inductive types in Init.Prelude and Init.Core.

And (∧)
Or (∨)
Not (¬) and Iff (↔)
Exists (∃) and Forall (∀)

-- And is a structure with two fields
-- structure And (a b : Prop) : Prop where
--   intro ::
--   left  : a
--   right : b

theorem and_comm (p q : Prop) (h : p ∧ q) : q ∧ p :=
  ⟨h.right, h.left⟩

-- Explicit constructor syntax
theorem and_intro (hp : p) (hq : q) : p ∧ q :=
  And.intro hp hq

-- Or has two constructors: inl and inr
-- inductive Or (a b : Prop) : Prop where
--   | inl (h : a) : Or a b
--   | inr (h : b) : Or a b

theorem or_comm (p q : Prop) (h : p ∨ q) : q ∨ p :=
  match h with
  | Or.inl hp => Or.inr hp
  | Or.inr hq => Or.inl hq

-- Not p is defined as p → False
-- @[implicit_reducible] def Not (a : Prop) : Prop := a → False

-- Iff has two fields: mp and mpr
-- structure Iff (a b : Prop) : Prop where
--   mp  : a → b
--   mpr : b → a

theorem not_not_intro (p : Prop) (hp : p) : ¬¬p :=
  fun hnotp => hnotp hp

theorem iff_comm (p q : Prop) (h : p ↔ q) : q ↔ p :=
  Iff.intro h.mpr h.mp

-- ∀ is built into the kernel as a dependent function type
-- ∃ x, p x  desugars to  Exists (fun x => p x)

theorem exists_intro : ∃ n : Nat, n > 0 :=
  ⟨1, Nat.one_pos⟩

theorem forall_imp (p q : α → Prop) (h : ∀ x, p x → q x) (hall : ∀ x, p x) : ∀ x, q x :=
  fun x => h x (hall x)

Entering Tactic Mode with `by`

The by keyword switches from term mode to tactic mode. Inside a by block, you issue a sequence of tactics that transform the proof goal.

-- Term-mode proof
theorem add_zero_term (n : Nat) : n + 0 = n := rfl

-- Tactic-mode proof of the same theorem
theorem add_zero_tactic (n : Nat) : n + 0 = n := by
  rfl

When you open a by block in an IDE like VS Code with the Lean 4 extension, you see the tactic state: the local hypotheses above the ⊢ turnstile and the current goal below it.

Core Proof Tactics

`intro` — Introduce Hypotheses

Use intro to move universally-quantified variables and hypothesis antecedents from the goal into the local context:

theorem imp_trans (p q r : Prop) : (p → q) → (q → r) → p → r := by
  intro hpq hqr hp
  -- Goal: ⊢ r
  -- hpq : p → q,  hqr : q → r,  hp : p
  exact hqr (hpq hp)

`exact` — Close a Goal Directly

exact e closes the goal if e has exactly the required type:

theorem trivial_and (p : Prop) (hp : p) : p ∧ p := by
  exact ⟨hp, hp⟩

`apply` — Apply a Function

apply f unifies the conclusion of f with the current goal and creates new goals for the premises:

theorem modus_ponens (p q : Prop) (h : p → q) (hp : p) : q := by
  apply h
  exact hp

`constructor`, `left`, `right` — Build Connectives

theorem and_example (p q : Prop) (hp : p) (hq : q) : p ∧ q := by
  constructor
  · exact hp
  · exact hq

theorem or_left (p q : Prop) (hp : p) : p ∨ q := by
  left
  exact hp

theorem or_right (p q : Prop) (hq : q) : p ∨ q := by
  right
  exact hq

`obtain` — Destructure Hypotheses

obtain performs pattern matching on a hypothesis:

theorem and_elim (p q r : Prop) (h : p ∧ q) (hpqr : p → q → r) : r := by
  obtain ⟨hp, hq⟩ := h
  exact hpqr hp hq

theorem or_elim_example (p q r : Prop) (h : p ∨ q) (hpr : p → r) (hqr : q → r) : r := by
  obtain hp | hq := h
  · exact hpr hp
  · exact hqr hq

A Complete Example: `add_comm`

Here is the classic commutativity of natural number addition, proved with tactics:

theorem add_comm (a b : Nat) : a + b = b + a := by
  induction a with
  | zero =>
    simp
  | succ a ih =>
    simp [Nat.succ_add, Nat.add_succ, ih]

For arithmetic goals over Nat and Int, the omega tactic can often close them automatically: theorem add_comm (a b : Nat) : a + b = b + a := by omega.

Classical Logic

Lean 4’s core logic is constructive (no law of excluded middle by default), but Classical reasoning is available by opening Classical or importing the relevant axioms.

Law of Excluded Middle

open Classical in
theorem em_example (p : Prop) : p ∨ ¬p :=
  Classical.em p

Proof by Contradiction

open Classical in
theorem by_contradiction_example (p : Prop) (h : ¬¬p) : p :=
  Classical.byContradiction (fun hnp => h hnp)

Double Negation Elimination

open Classical in
theorem double_neg (p : Prop) : ¬¬p ↔ p :=
  Classical.not_not

Any theorem or definition that uses Classical.choice (which underlies Classical.em and Classical.byContradiction) will appear under the axioms Classical.choice, propext, and Quot.sound when you run #print axioms. This is expected and is not a sign of an error.

Propositional extensionality

propext is one of Lean 4’s core axioms. It states that if two propositions are logically equivalent, they are definitionally equal as types:

-- axiom propext {a b : Prop} : (a ↔ b) → a = b

example (p q : Prop) (h : p ↔ q) : p = q :=
  propext h

This axiom is what allows simp and rw to rewrite propositions using ↔.

Putting It All Together

Here is a self-contained proof that demonstrates several connectives and tactics:

theorem de_morgan_not_or (p q : Prop) : ¬(p ∨ q) ↔ ¬p ∧ ¬q := by
  constructor
  · intro h
    constructor
    · intro hp
      exact h (Or.inl hp)
    · intro hq
      exact h (Or.inr hq)
  · intro ⟨hnp, hnq⟩
    intro hpq
    cases hpq with
    | inl hp => exact hnp hp
    | inr hq => exact hnq hq

Introduction

Language Basics

Theorem Proving

Functional Programming

Lean 4 Propositions and Proofs: Curry-Howard Guide

`Prop` vs `Type`

Logical Connectives

Entering Tactic Mode with `by`

Core Proof Tactics

`intro` — Introduce Hypotheses

`exact` — Close a Goal Directly

`apply` — Apply a Function

`constructor`, `left`, `right` — Build Connectives

`obtain` — Destructure Hypotheses

A Complete Example: `add_comm`

Classical Logic

Law of Excluded Middle

Proof by Contradiction

Double Negation Elimination

Putting It All Together

Build docs developers (and LLMs) love

Introduction

Language Basics

Theorem Proving

Functional Programming

Documentation Index

​Prop vs Type

​Logical Connectives

​Entering Tactic Mode with by

​Core Proof Tactics

​intro — Introduce Hypotheses

​exact — Close a Goal Directly

​apply — Apply a Function

​constructor, left, right — Build Connectives

​obtain — Destructure Hypotheses

​A Complete Example: add_comm

​Classical Logic

​Law of Excluded Middle

​Proof by Contradiction

​Double Negation Elimination

​Putting It All Together

Build docs developers (and LLMs) love

`Prop` vs `Type`

Logical Connectives

Entering Tactic Mode with `by`

Core Proof Tactics

`intro` — Introduce Hypotheses

`exact` — Close a Goal Directly

`apply` — Apply a Function

`constructor`, `left`, `right` — Build Connectives

`obtain` — Destructure Hypotheses

A Complete Example: `add_comm`

Classical Logic

Law of Excluded Middle

Proof by Contradiction

Double Negation Elimination

Putting It All Together