Dependent Types from Rocq to Lean 4

Families of types and dependent functions

A familiar function has a fixed codomain: f:A\to B. A dependent function has a codomain that varies with its input:

f:\prod_{x:A}B(x).

Here B assigns a type B(x) to each x:A. To give f is to give an element f(x):B(x) uniformly for each x. Geometrically, think of a family of fibers over A and a section choosing a point in each fiber. This analogy concerns the dependency alone; continuity or smoothness would be additional conditions.

For example, let B(n) be the type of tuples of length n. A function that produces a zero tuple for every length has type \prod_{n:\mathbb N}B(n). Its result type records the length it was asked for. A function returning a list and a separate promise about its length carries similar information in a different representation.

Lean writes a dependent function type as (x : A) → B x. Application is juxtaposition, and fun x => t is function abstraction. Curly braces mark arguments that Lean should usually infer. These are the basic conventions of its dependent type language.

Here is dependent composition. The result of g depends on the value that f produces:

universe u v w

def dependentCompose {A : Type u} {B : Type v}
    {C : B → Type w} (f : A → B) (g : (b : B) → C b) :
    (a : A) → C (f a) :=
  fun a => g (f a)

Read the signature before the body. C is a family over B; g selects an element in each fiber; composing with f produces a section of the family pulled back to A. The body is ordinary composition. The type records the dependency that ordinary function notation suppresses.

Typing is expressed by a judgment, conventionally

\Gamma\vdash t:T.

It says that, under the declarations collected in the context \Gamma, the term t has type T. A context might contain A : Type, x : A, and P : A → Prop. The order matters: a declaration can depend on earlier declarations.

The colon here belongs to the language of judgments. By contrast, a proposition x ∈ S is itself a type whose inhabitants are proofs. Thus “this term has the wrong type” and “this mathematical proposition is false” are different claims.

Three rules explain dependent functions. Suppressing universe side conditions for the moment, they have the following shapes:

\frac{\Gamma\vdash A\ \mathrm{type}\qquad\Gamma,x:A\vdash B(x)\ \mathrm{type}} {\Gamma\vdash\prod_{x:A}B(x)\ \mathrm{type}}

\frac{\Gamma,x:A\vdash t:B(x)} {\Gamma\vdash(\lambda x:A.\,t):\prod_{x:A}B(x)}

\frac{\Gamma\vdash f:\prod_{x:A}B(x)\qquad\Gamma\vdash a:A} {\Gamma\vdash f\,a:B(a)}.

The first forms the function type, the second constructs a function, and the third applies it. The substitution in the final result type is the dependent part: applying g to f a produces a term of C (f a), exactly as in the example. The accompanying computation rule is beta reduction, (\lambda x.\,t)\,a\longrightarrow t[a/x], with substitution avoiding accidental capture of variables.

Why implication and universal quantification are function types

A proof of P\to Q transforms any proof of P into a proof of Q: it is a function. A proof of \forall x:A,\,P(x) supplies a proof of P(x) for every x: it is a dependent function. This is the propositions-as-types correspondence.

Syntax note. Lean’s ∀ (x : A), B x and (x : A) → B x are the same dependent function type. Binder conventions carry over: ∀ ⦃x y : A⦄, f x = f y → x = y is identical to ⦃x y : A⦄ → f x = f y → x = y. Both make x and y strict implicit arguments, inferred when a subsequent explicit argument is supplied.

The proof of an elementary implication is therefore a small program:

theorem composeImplications (P Q R : Prop)
    (hPQ : P → Q) (hQR : Q → R) : P → R :=
  fun hP => hQR (hPQ hP)

The same proof can be constructed interactively:

theorem composeImplicationsBy (P Q R : Prop)
    (hPQ : P → Q) (hQR : Q → R) : P → R := by
  intro hP
  apply hQR
  exact hPQ hP

After intro hP, the context contains a proof of P and the goal is R. Applying hQR reduces that goal to Q; the final line supplies its proof. The kernel checks the resulting proof term. See Lean’s propositions and proofs tutorial.

Other logical connectives have corresponding constructors and elimination rules:

Negation is \neg P := P\to\bot: assume P and derive a contradiction. Classical principles enter with rules such as double-negation elimination without further hypotheses.

Rocq’s forall x : A, P x becomes ∀ x : A, P x; fun x => t, intros, apply, and exact remain recognizable. The treatment of proofs and equality changes more substantially.

The Calculus of Constructions and its descendants

The Calculus of Constructions, developed by Thierry Coquand and Gérard Huet, brought together dependent types and powerful polymorphism in one typed lambda calculus. Their 1988 paper proves strong normalization: every reduction sequence from a well-typed term terminates. Extensions to the calculus require their own metatheoretic arguments.

For a returning type theorist, the lambda-cube description is a useful memory aid. Begin with simply typed functions. Add terms parameterized by types, type constructors parameterized by types, and types parameterized by terms. CoC combines all three forms of dependency. In the usual two-sort presentation there is a lower sort * and an upper sort \square, with *:\square. Dependent products permit all four combinations of domain and codomain sorts. There is no axiom \square:\square.

For the mathematician, the payoff is uniformity. The same substitution operation instantiates a polynomial at a number, a construction at a vector space, or a theorem at a hypothesis. Types and terms share a syntax, while typing rules prevent arbitrary self-reference.

Pure CoC does not begin with a primitive natural-number type and the induction principle used in ordinary mathematics. Polymorphism permits Church encodings: an encoded natural number can describe iteration. But obtaining the desired dependent induction and computational behavior motivates a richer system with primitive inductive definitions. The early history of Coq traces this development, including the work of Christine Paulin-Mohring.

Rocq’s core language is a version of the Calculus of Inductive Constructions, or CIC. It includes a hierarchy of universes and rules for inductive families, recursive definitions, and coinductive constructions. Its typing rules specify a much more substantial language than the original CoC.

Lean belongs to the same broad family, with its own universe discipline, definitional proof irrelevance, primitive quotients, and rules governing inductives. These choices affect both everyday proofs and the metatheory; we will examine each in turn.

Universes and the special role of propositions

Since types appear in expressions, they need types of their own. Lean uses a hierarchy:

\mathrm{Sort}\ u:\mathrm{Sort}\ (u+1).

Prop abbreviates Sort 0; Type u abbreviates Sort (u + 1); bare Type means Type 0. Consequently, Nat : Type and Type : Type 1. Universe variables such as u are level parameters, distinct from ordinary natural-number variables inside a program.

The levels constrain self-reference. In the usual expressive dependent calculi, simply imposing a universal Type : Type permits paradoxes. A hierarchy lets us quantify over a collection of types without placing that collection inside itself.

Lean’s universe rules can be compressed into one formula. If A:\mathrm{Sort}\ u and B(x):\mathrm{Sort}\ v, then

\left(\prod_{x:A}B(x)\right):\mathrm{Sort}(\operatorname{imax}(u,v)),

\operatorname{imax}(u,v)=\begin{cases}0&v=0,\\\max(u,v)&v>0.\end{cases}

Thus a proposition may quantify over objects in arbitrarily high fixed universes and remain a proposition. This is the impredicativity of Prop. For example, ∀ P : Prop, P → P is itself a proposition, although its quantifier ranges over all propositions, including that one.

Data universes are predicative. A type of functions ranging over all small types generally lives higher than those small types. Impredicativity and Type : Type are different design choices; the former does not by itself imply the latter.

One practical trap for a Rocq user is cumulativity. Rocq permits smaller universes to embed into larger ones through its typing discipline. Lean does not automatically regard a type in Type u as an inhabitant of Type (u + 1). Universe polymorphism often removes the need for lifting, but explicit constructions such as ULift are available when needed. Rocq’s rules also distinguish its computational Set sort from Prop; Lean’s ordinary small data live in Type.

Rocq’s Set is a sort; Lean’s mathematical Set α represents predicates on α. The shared spelling conceals different roles.

Induction is dependent recursion

Natural numbers are specified by a zero constructor and a successor constructor. Their dependent eliminator has the mathematical shape

\begin{aligned} \operatorname{rec}_{\mathbb N}&: \prod_{C:\mathbb N\to\mathrm{Sort}\ u} C(0)\to{}\\ &\quad\left(\prod_{n:\mathbb N}C(n)\to C(n+1)\right)\to{}\\ &\quad\prod_{n:\mathbb N}C(n). \end{aligned}

The family C is called the motive. If C(n) is a proposition, this is induction. If it is a data type, this is a recursive construction. If it varies with n, the recursion constructs different types of results at different stages. The same principle accounts for all three readings. Lean’s induction and recursion chapter shows how recursive definitions are expressed through recursors.

An indexed inductive family makes the dependency visible:

inductive Vec (α : Type u) : Nat → Type u where
  | nil : Vec α 0
  | cons {n : Nat} : α → Vec α n → Vec α (n + 1)

def Vec.head {α : Type u} {n : Nat} : Vec α (n + 1) → α
  | .cons x _ => x

Lean allows arguments to be declared before the colon, leaving their names in scope for the type that follows. These are two equivalent ways to write the cons constructor inside the declaration:

| cons {n : Nat} : α → Vec α n → Vec α (n + 1)
| cons : {n : Nat} → α → Vec α n → Vec α (n + 1)

In the first form, the colon after } introduces the remaining function type; in the second, the whole function type follows the colon. Both make n implicit, usually inferred by Lean. The placement is stylistic; the dependency comes from using n in the subsequent types.

The element type α is a parameter: it stays fixed through the declaration. The length is an index: the constructors return different instances of the family. In head, the empty constructor cannot inhabit the input type, so there is no empty case to handle.

Compare a list operation that might fail with this signature. Here the caller must supply a nonempty vector; the result needs no optional wrapper. The mathematical precondition is expressed in the domain of the function.

Inductive declarations require restrictions. In particular, recursive occurrences must meet strict positivity conditions. To understand the terminology, consider an occurrence of a type X in an expression built from function types. Start with positive polarity: entering an arrow’s domain flips the sign, while entering its codomain preserves it. Intuitively, A → X produces an X, whereas X → A consumes one. Assuming A and B contain no X:

Strict positivity is stronger than a positive final sign: in these arrow expressions, the path to X must never enter a function’s domain. The check applies inside each constructor argument’s type, not across the outer arrows that make the constructor a function. Thus Vec α n is an allowed recursive argument to cons; an argument of type Bad → False has a forbidden negative occurrence. Nested inductive type constructors have additional rules, described in the inductive-type reference.

If we freely admitted a constructor mk : (Bad → False) → Bad, its apparent elimination rule would let us define:

d : Bad → False
d (mk f) := f (mk f)

The definition of d does not recursively call itself: it applies the function stored in its argument. For an arbitrary f : Bad → False, unfolding d and then matching the constructor gives the open reduction sequence:

d (mk f)
  → (match mk f with | mk g => g (mk g))
  → f (mk f)

The expression is open because f remains a variable; its behavior determines what happens next. The forbidden constructor nevertheless lets us package d itself as an input: mk d : Bad. Specializing to f = d therefore yields the closed term d (mk d) : False, whose reduction repeats:

d (mk d) → d (mk d) → ...

Each arrow here abbreviates unfolding and matching. Self-application emerges from the constructor and its elimination rule despite the absence of explicit recursion. The closed term’s type False is the contradiction; the loop also exposes the computational failure. The positivity check blocks the declaration of Bad before either becomes available.

Lean’s kernel checks inductive declarations and their recursors. Surface recursive definitions are compiled into applications of those principles, including well-founded recursion when needed. Rocq instead also has primitive fixpoint terms with a guardedness discipline in its core presentation. The two systems therefore organize the checking of recursion differently. Rocq’s inductive and recursive rules are the appropriate comparison, rather than the superficial similarity of pattern-matching syntax.

Off-topic details: termination through decreasing measures

A standard termination argument assigns each recursive call a measure in a well-founded order. For a natural-number measure \mu, a call from input x to input y must satisfy \mu(y)<\mu(x). Recursing on a list’s tail decreases its length; more elaborate algorithms may decrease a lexicographically ordered tuple. There can be no infinite descending chain in the chosen order. Lean’s termination_by and decreasing_by let us specify such a measure and prove the required decreases, elaborating the definition into well-founded recursion.

Sized types carry descent information in types themselves. Schematically, write \mathrm{List}_{\leq n}(A) for lists of length at most n. A helper with type \mathrm{List}_{\leq n}(A)\to\mathrm{List}_{\leq n}(A) promises not to exceed that bound. Applied to the tail of a list of length n+1, its result is still small enough for a recursive call, even if it is not a literal subtree of the original input. Size information can cross function boundaries instead of being recovered by inspecting each helper’s implementation. Actual sized calculi have additional rules, and may use ordinal bounds; Abel’s MiniAgda paper develops this approach.

An ordinary recursive-call check has no self-call to inspect in d. It calls a stored function, whose unrestricted type Bad → False imposes no descent condition. Packaging d with mk lets that call return to the same expression. Any rank strictly decreasing along this complete reduction cycle would require \mu(t)<\mu(t). A termination-tracking system must therefore reject or restrict some part of the construction; merely attaching a measure to d cannot validate the unchanged rules.

Strict positivity restricts the datatypes and eliminators we may introduce; decreasing measures justify recursive uses of the admitted principles. Sized types can connect these concerns, but a size index alone proves neither termination nor consistency. Likewise, accepting a Lean definition through well-founded recursion does not establish normalization of every term in Lean’s ambient logic, as the later counterexample will illustrate.

Computation and the two forms of equality

Dependent types make computation part of type checking. To see why, define an addition that explicitly recurses on its first argument:

def addLeft : Nat → Nat → Nat
  | 0, m => m
  | n + 1, m => Nat.succ (addLeft n m)

example (n : Nat) : addLeft 0 n = n := rfl

example asks Lean to check an unnamed theorem. The argument (n : Nat) is arbitrary; the proposition to prove follows :, and its proof follows :=.

rfl stands for reflexivity. In := rfl, it is a proof term with its argument inferred. The equality constructor Eq.refl n proves n = n and also works here. Writing := by rfl instead invokes the tactic of that name to construct the proof. Both use the same reflexivity principle; see Lean’s equality reference and tactic tutorial.

Reflexivity works even though the two sides look different: the defining equation for addLeft makes addLeft 0 n compute to n, even though n is unknown. The kernel’s conversion relation recognizes the two sides as definitionally equal, so a proof of n = n also proves the displayed equation. No induction lemma is needed.

Now consider the other order:

theorem addLeft_zero (n : Nat) : addLeft n 0 = n := by
  induction n with
  | zero => rfl
  | succ n ih =>
      change Nat.succ (addLeft n 0) = Nat.succ n
      exact congrArg Nat.succ ih

An unknown n does not reveal whether the first argument of addLeft is zero or a successor. Computation alone cannot finish. Induction does: the successor case lifts the induction hypothesis through the function Nat.succ.

Two relations are at work. Definitional equality belongs to the machinery of typing and conversion; it lets the checker treat suitable expressions interchangeably. Propositional equality, written a = b, is a type inside the language, and a proof inhabiting it can be passed to other functions.

The latter is an inductive family with reflexivity as its constructor. Its elimination principle says that equal things can be substituted in dependent families. This is the formal justification for transporting an object from B(a) to B(b) using a proof of a=b. Lean’s quantifiers and equality chapter develops this substitution principle.

def transport {A : Type u} (B : A → Type v)
    {a b : A} (h : a = b) (x : B a) : B b :=
  h ▸ x

def resizeVec {α : Type u} {n m : Nat}
    (h : n = m) (xs : Vec α n) : Vec α m :=
  transport (Vec α) h xs

Nothing about the vector’s entries changes. The equality proof justifies changing the index appearing in its type. This is why arithmetic identities can matter while manipulating a vector: a mathematically equal length may still require explicit transport if the two length expressions are not definitionally interchangeable.

Conversion is often explained as reducing both expressions to the same normal form. Lean’s type-system reference includes beta reduction of function applications, delta unfolding of definitions, iota reduction of recursors, and zeta substitution of let-bound values. It also includes function and structure eta rules, proof irrelevance, and quotient computation. The kernel implements an algorithmic conversion test; this is distinct from the declarative relation specified by the rules. The later normalization example will show why reducing every term to a normal form cannot provide a general implementation.

For writing proofs, a useful discipline is to ask what makes an equality available. Does it follow by unfolding and computation? Is it an induction theorem? Does it use extensionality? Each answer suggests a different Lean move: rfl or change, induction or rewriting, or an explicit extensionality principle.

How far GADTs take us

Much of the vector example is available in Haskell and OCaml through generalized algebraic datatypes, or GADTs. Their constructors can specify different result indices, and matching a constructor introduces type equations within the branch. This captures an important part of indexed inductive families. It does not by itself supply arbitrary dependence on ordinary terms.

data Nat = Z | S Nat

data Vec (n :: Nat) a where
  VNil  :: Vec 'Z a
  VCons :: a -> Vec n a -> Vec ('S n) a

headVec :: Vec ('S n) a -> a
headVec (VCons x _) = x

type z = Z
type 'n s = S of 'n

type (_, _) vec =
  | VNil : (z, 'a) vec
  | VCons : 'a * ('n, 'a) vec -> ('n s, 'a) vec

let head_vec : type n a. (n s, a) vec -> a = function
  | VCons (x, _) -> x

data SNat (n :: Nat) where
  SZ :: SNat 'Z
  SS :: SNat n -> SNat ('S n)

replicateVec :: SNat n -> a -> Vec n a
replicateVec SZ     _ = VNil
replicateVec (SS n) x = VCons x (replicateVec n x)

data SomeVec a where
  SomeVec :: SNat n -> Vec n a -> SomeVec a

type family Add (n :: Nat) (m :: Nat) :: Nat where
  Add 'Z     m = m
  Add ('S n) m = 'S (Add n m)

append :: Vec n a -> Vec m a -> Vec (Add n m) a
append VNil ys = ys
append (VCons x xs) ys = VCons x (append xs ys)

type (_, _, _) plus =
  | PlusZ : (z, 'm, 'm) plus
  | PlusS : ('n, 'm, 'k) plus -> ('n s, 'm, 'k s) plus

let rec append : type n m k a.
    (n, m, k) plus -> (n, a) vec -> (m, a) vec -> (k, a) vec =
  fun sum xs ys ->
    match sum, xs with
    | PlusZ, VNil -> ys
    | PlusS smaller, VCons (x, rest) ->
        VCons (x, append smaller rest ys)

Proof irrelevance and what can be extracted from existence

Lean identifies all proofs of a fixed proposition definitionally:

example (P : Prop) (h₁ h₂ : P) : h₁ = h₂ := rfl

This says that once the proposition P is fixed, the identity of its proof is irrelevant to conversion. The reference on propositions marks this as a property of the type system itself.

A visible benefit is array access with a proof that the index is in bounds. Imagine an operation get xs i h, where h : i < xs.size. Two parts of a program may establish the same bound differently, supplying proofs h₁ and h₂. We want get xs i h₁ and get xs i h₂ to agree without reconciling those proofs. Lean’s array notation makes this concrete:

example {α : Type u} (xs : Array α) (h₁ h₂ : 0 < xs.size) :
    xs[0]'h₁ = xs[0]'h₂ := rfl

The apostrophe supplies the bounds proof explicitly. In ordinary xs[0] notation, Lean attempts to construct that proof automatically, so two accesses can look identical while carrying different evidence. Proof irrelevance makes these differing proof arguments interchangeable by conversion. A proof-relevant system might instead establish independence from them with a separate lemma.

Ordinary Rocq Prop does not have this general definitional identification. One can assume propositional proof irrelevance in Rocq, but an axiom proving h₁ = h₂ does not make the checker identify the terms directly. Modern Rocq also has SProp, a separate sort with definitional proof irrelevance and its own restrictions.

The distinction between a proof and data becomes concrete with existential quantification. Both of the following involve a witness, but they support different operations:

def WitnessData (α : Type u) (P : α → Prop) :=
  {x : α // P x}

theorem forgetWitness {α : Type u} {P : α → Prop}
    (w : WitnessData α P) : ∃ x, P x :=
  ⟨w.val, w.property⟩

noncomputable def chooseWitness {α : Type u} {P : α → Prop}
    (h : ∃ x, P x) : WitnessData α P :=
  ⟨Classical.choose h, Classical.choose_spec h⟩

In ∃ x, P x, the comma separates the bound variable x from the proposition P x; it does not construct a pair. Lean infers x : α from P : α → Prop. The fully annotated form is ∃ x : α, P x, which expands to Exists (fun x : α => P x). The angle brackets in forgetWitness supply the witness w.val and the proof w.property that it satisfies P.

The subtype {x : α // P x} is data: we can project its stored witness. The existential type ∃ x, P x belongs to Prop, so its inhabitants are proofs and obey Lean’s restrictions on eliminating propositions into data. In typing notation, (∃ x, P x) : Prop, while h : (∃ x, P x) says that h proves that proposition. The ordinary eliminator for existence lets us reason about a witness to establish another proposition, but does not generally expose the witness as computational data. The reverse direction above uses classical choice and is marked noncomputable.

Why impose this restriction? Suppose one existential proof used witness 0 and another used witness 1. Proof irrelevance identifies the proofs of that same existential proposition. A computational projection that distinguished them would make the identification incompatible with computation. Classical.choose instead selects an unspecified witness satisfying the predicate; it need not return the witness used to construct the proof. For a fixed predicate, changing the existential proof cannot change that selection.

More generally, \sum_{x:A}B(x), a dependent pair or sigma type, packages an object with data whose type depends on it. When the second component is a proposition, a subtype is often the convenient Lean representation. When both components carry data, use a sigma type. An existential proposition forgets the computational distinction between witnesses.

There are controlled exceptions to the prohibition on eliminating propositions into data. Empty propositions and suitable single-constructor propositions have stronger elimination rules; equality supports transport. Thus “nothing can ever move from Prop to Type” is too strong. The restriction concerns which distinctions a recursor is allowed to observe. Rocq also restricts elimination from Prop, even though ordinary Prop there lacks Lean’s general definitional proof irrelevance.

Extensional mathematics and primitive quotients

Mathematicians normally identify functions that agree at every argument. In Lean this is a theorem, funext, used as follows:

example {A : Type u} {B : Type v} (f g : A → B)
    (h : ∀ x, f x = g x) : f = g :=
  funext h

Pointwise equality need not be definitional equality of the functions. The theorem gives a propositional equality, which permits substitution without making their implementations convertible.

For reasoning about programs, distinguish a function from an implementation with a particular execution history. This distinction already matters without function extensionality: β-reduction identifies (fun y => y) x with x, although an operational semantics that counts β-steps distinguishes their evaluation costs. An equality that identifies these expressions cannot simultaneously preserve that step count. Ordinary function types do not expose source syntax or execution traces for inspection.

Function extensionality also identifies sorting functions that agree on every input despite different running times. Given e : f = g, any observer must satisfy observe f = observe g, by congrArg observe e; even a postulated cost observer cannot consistently distinguish them. To study costs, represent algorithms as syntax with an evaluator that counts steps, or instrument them to return a result and a cost, with type List Nat → List Nat × Nat. Equal sorted outputs need not imply equal result-cost pairs. Dependent types support these richer models; the chosen representation determines which distinctions survive.

Rocq’s standard library supplies function extensionality as an axiom, but omitting it does not restore the operational distinctions already lost through definitional equality.

Extensionality also affects computation involving equality proofs: transports using funext can block kernel reduction while compiled execution erases them. Lean’s Axioms and Computation illustrates this difference between evaluation routes.

Similarly, propositional extensionality, propext, turns an equivalence P ↔︎ Q into an equality P = Q.

In particular, any two proved propositions are equal. Given proofs a : A and b : B, the functions fun _ => b and fun _ => a prove the two implications: each ignores its input and returns the available proof of its conclusion.

Does this erase the distinctions between formulas? Consider three Boolean variables and the formulas

F=p\land q\land r,\qquad G=r\land p\land q,\qquad H=p\lor q\lor r.

At the all-true assignment, all three propositions equal True. But formulas describe dependence on assignments: F and G agree everywhere, whereas F and H disagree at (p,q,r)=(\mathrm{True},\mathrm{False},\mathrm{False}). The latter are merely equisatisfiable: each has a satisfying assignment. Equisatisfiability preserves existence of a model, not agreement under every assignment.

In Lean, represent these meanings as predicates F G : Assignment → Prop. Equivalence means ∀ ρ, F ρ ↔︎ G ρ; propext and funext then give F = G. Equisatisfiability means (∃ ρ, F ρ) ↔︎ (∃ σ, G σ): propext equates these existential propositions, not the predicates. The witnesses may differ. Classically, Prop has two values up to propositional equality, yet three Boolean inputs permit 2^{2^3}=256 distinct truth functions. Equality of propositions does not discard dependencies that remain explicit in a function’s arguments.

Representing subsets by membership predicates, these principles turn pointwise equivalence into equality:

def SubsetOf (A : Type u) := A → Prop

theorem subsetExt {A : Type u} (S T : SubsetOf A)
    (h : ∀ x, S x ↔ T x) : S = T :=
  funext (fun x => propext (h x))

#print axioms subsetExt

The last command exposes the theorem’s axiom dependencies: propext and Quot.sound. Lean derives function extensionality from quotients, as we will see below.

Lean’s primitive Quot identifies representatives related by r propositionally. To define a function on the quotient, supply a function f on representatives and a proof h that it respects r. The computation rule is

\operatorname{Quot.lift}\ f\ h\ (\operatorname{Quot.mk}\ r\ a)\equiv f(a).

For example, quotient natural numbers by parity:

def SameParity (a b : Nat) : Prop := a % 2 = b % 2

def parityValue : Quot SameParity → Nat :=
  Quot.lift (fun n => n % 2) (fun _ _ h => h)

example : parityValue (Quot.mk SameParity 5) = 1 := rfl

example : Quot.mk SameParity 1 = Quot.mk SameParity 3 :=
  Quot.sound (by rfl)

Quotient soundness supplies the last equality without making its representatives definitionally identical. The library wrapper Quotient packages an equivalence relation with its laws; see the quotient reference.

Standard Rocq CIC has no corresponding primitive quotient. A common approach uses setoids: carriers with equivalence relations, and functions proved to respect them. Other quotient constructions require further assumptions or particular encodings.

def Pointwise {A : Sort u} {B : A → Sort v}
    (f g : (x : A) → B x) : Prop :=
  ∀ x, f x = g x

def rebuild {A : Sort u} {B : A → Sort v}
    (q : Quot (@Pointwise A B)) : (x : A) → B x :=
  fun x =>
    Quot.lift (fun f => f x) (fun _ _ h => h x) q

theorem funextFromQuot {A : Sort u} {B : A → Sort v}
    (f g : (x : A) → B x)
    (h : ∀ x, f x = g x) : f = g :=
  congrArg rebuild (Quot.sound h)

#print axioms funextFromQuot

What evolved from early Lean to Lean 4

Lean began in 2013; Lean 3 was released in 2017; Lean 4 development began in 2018, with version 4.0 released in September 2023. The official history describes the progression from a prover centered on C++ infrastructure to a system implemented largely in Lean itself.

There was also a foundational branch that is easy to forget. Lean 2 supported a separate HoTT mode with proof irrelevance disabled and univalence postulated. Sebastian Ullrich’s account of Lean’s development records that experiment. Modern Lean’s mainstream mathematical foundation follows the proof-irrelevant branch; its extensionality and quotient features should be understood in that setting.

Lean 3 already allowed tactics and other extensions to be written in Lean. Lean 4 substantially expanded this architecture through an extensible parser, hygienic macros, elaboration machinery, and a compiler intended to make Lean a useful programming language. The Lean 4 system paper, by de Moura and Ullrich, explains these engineering choices. They change how the prover can be extended and how efficiently proof search can be implemented.

The logical changes also matter. Carneiro’s 2024 Lean4Lean paper identifies kernel support for nested inductive types and eta for structures as changes that substantially affect the metatheory. Structure eta identifies a structure with the result of rebuilding it from its fields, just as function eta identifies fun x => f x with f. Such rules remove bookkeeping from proofs, but their interaction with other conversion rules needs justification.

A nested inductive type places recursion underneath another type constructor. For example, a rose tree contains a list of subtrees:

inductive Rose (α : Type u) where
  | node : α → List (Rose α) → Rose α

Here the recursive occurrence sits underneath List. Generating and checking the elimination machinery is more involved than for a binary tree. This raises soundness questions about the generated recursors even without invoking non-terminating reduction. A consistency argument for Lean 3 therefore needs further work to cover Lean 4’s extensions.

The layers matter when learning the language. A numeral is surface syntax. Notation, implicit arguments, coercions, and type-class search help turn an expression into a fully specified term. Tactics solve elaboration goals by constructing terms. The kernel checks the resulting declarations. The compiler provides a further route from executable definitions to running programs. Lean’s elaboration and compilation reference separates these stages.

This explains why “I know the logic” and “I can use Lean fluently” are different achievements. A mathematician may understand a theorem perfectly while needing help with instance search or with the library’s preferred representation. A former Coq user may recognize the proof term while misreading a coercion or assuming the wrong transparency behavior.

A compact comparison helps locate those surprises:

Rocq also supports eta conversion for functions and primitive records. Its conversion rules specify these features beyond the broad comparison in the table.

What the normalization result actually says

We can now separate three metatheoretic properties. Strong normalization says every reduction sequence from a well-typed term terminates. Canonicity, in a specified fragment and with specified axioms, says closed terms of data types compute to appropriate canonical values, such as numerals. Consistency says there is no closed proof of False under the designated assumptions. These properties interact, but they are not synonyms.

Normalization and an analysis of normal forms can establish consistency: if every closed proof normalizes, and no normal form can inhabit False, then no such proof exists. Losing that method does not exhibit a proof of False. A semantic model offers another route: interpret types as suitable objects and False as empty, then prove that derivable judgments preserve the interpretation.

Abel and Coquand’s 2019 preprint, published in 2020, exhibits non-normalizing proof terms. Their closed example uses propositional extensionality as well as impredicativity and proof-irrelevant equality. It does not require a recursive definition or an assumption of False. We can reconstruct the mechanism in Lean 4, starting with the computational rule that makes it possible.

example (A : Type) (h : A = A) (x : A) : cast h x = x := rfl

#reduce (fun (h : Nat = Nat) => cast h (37 : Nat))
-- fun h => 37

namespace ReductionLoop
set_option linter.defProp false

def T : Prop := ∀ P : Prop, P → P
def ident : T → T := fun z => z
def diagonal (z : T) : T := z (T → T) ident z

def trueEq {A B : Prop} (a : A) (b : B) : A = B :=
  propext ⟨fun _ => b, fun _ => a⟩

def rolled : T := fun P p =>
  cast (trueEq (A := T → T) (B := P) ident p) diagonal

def loop : T := diagonal rolled

#print axioms loop
-- [propext]
end ReductionLoop

Denotational semantics and the meaning of a dependent type

A reduction describes how an expression changes during computation. A denotation assigns the expression a mathematical meaning. These are different kinds of account: a function can denote a perfectly ordinary mathematical object even when a particular reduction strategy fails to produce a normal form for its expression.

Start with a data fragment containing dependent functions. An environment \rho assigns mathematical values to the variables in a context. We want a typing judgment to imply membership:

\Gamma\vdash t:A \quad\Longrightarrow\quad \llbracket t\rrbracket_\rho\in\llbracket A\rrbracket_\rho \quad(\rho\models\Gamma).

Interpret a type as a set, a family as a set-valued assignment, and a dependent function as a graph selecting one element from each fiber:

\llbracket\prod_{x:A}B(x)\rrbracket_\rho =\prod_{a\in\llbracket A\rrbracket_\rho} \llbracket B(x)\rrbracket_{\rho[x\mapsto a]}.

For a finite example, take A=\{0,1\}, B(0)=\{a,b\}, and B(1)=\{c\}. The dependent product contains exactly two graphs:

\{(0,a),(1,c)\},\qquad\{(0,b),(1,c)\}.

A lambda expression specifying the first choice denotes the first graph. Applying it to 1 denotes c. Beta reduction preserves that meaning because substituting an argument in a body agrees with evaluating the body in an environment assigning that argument to the bound variable. That statement is the semantic substitution lemma behind the familiar computation rule.

To interpret universes, we need collections of sets with the closure properties demanded by the typing rules. Merely saying “let a universe contain all sets” does not produce a set. Which closure conditions we choose, and whether product formation remains in the same universe, determine the required set-theoretic assumptions.

Consistency proofs and the reliability of a checker

Mario Carneiro’s February 2025 HoTTEST presentation reports a gap found while formalizing earlier metatheory, around definitional inversion and the confluence argument. It distinguishes proved results from conjectures and describes an alternative route toward soundness.

As of October 13, 2026, the con-leche project constructs a set-theoretic interpretation and proves that every environment accepted by its verified checker has a model. It assumes set theory with an ω-chain of Grothendieck universes; the interpretation of accepted declarations is then proved to exist. Since False denotes the empty set, no accepted theorem can inhabit it. The checker deliberately differs from the official kernel, including its handling of inductives, so the result covers con-leche’s accepted declarations without automatically covering everything the official kernel accepts.

This is a relative consistency result: the checker is the object of study, while Lean serves as the metatheory in which the conditional result is proved. The set-theoretic assumptions remain explicit. Connecting that theorem to an executable checker also requires accounting for its parsing, runtime, and input handling.

This leads to four separate questions about an individual formalization:

Success at one level does not discharge the others. A correct kernel can check an unintended theorem. A plausible mathematical theory can have a defective implementation. A theorem about one checker may omit parts of the runtime used to execute it.

De Moura’s August 24, 2026 postmortem documents kernel and runtime soundness bugs and reports fixes in Lean 4.33.1. It explains why adversarial developments need validation beyond an ordinary build, including statement comparison and external checking. These exploits concern the behavior of the affected implementations.

#print axioms answers the dependency question. Statement inspection and implementation validation answer others. A successful build provides evidence about a particular checking run; assessing its trust assumptions also requires knowing how tactics, native computation, and imported artifacts enter that run.

The linked critique usefully prompts these questions. Its forecasts about undiscovered contradictions are judgments about risk, beyond what the normalization counterexample establishes. Evaluating them requires the specific rules, models, and implementations examined here.

A first independent Lean proof

Return now to writing a proof. The composite of two injective functions is injective; an explicit definition keeps every step visible:

def IsInjective {A : Type u} {B : Type v} (f : A → B) : Prop :=
  ∀ ⦃x y : A⦄, f x = f y → x = y

theorem injectiveComp {A : Type u} {B : Type v} {C : Type w}
    (f : A → B) (g : B → C)
    (hf : IsInjective f) (hg : IsInjective g) :
    IsInjective (fun x => g (f x)) := by
  intro x y h
  apply hf
  apply hg
  exact h

#print axioms injectiveComp

intro x y h introduces and names three local assumptions. Unfolding IsInjective exposes two universally quantified variables followed by an implication. After intro, the new assumptions and remaining goal are:

x y : A
h : g (f x) = g (f y)
⊢ x = y

Mathematically: let x, y be arbitrary and assume h. We could write intro a b hab and later exact hab. The remaining tactics work backward: apply hf asks for f x = f y, then apply hg asks for g (f x) = g (f y), supplied by exact h. No classical axiom is required.

For practice, rewrite the proof as one fun expression. Prove that injectivity of g ∘ f implies injectivity of f, using congrArg g. Try the surjectivity statements too: these exercise existential proofs and the distinction between witnesses and returned data.

Finally, return to Vec. Prove a property by induction on its constructors, then change a length expression using resizeVec. This brings together the three skills on which the rest depends: reading a dependent signature, understanding the motive of induction, and recognizing when equality requires transport.

The opening basis theorem now has a more precise shape. It can assert that a natural number and a family of vectors satisfying the basis properties exist, package them as data with proofs attached, or define a particular basis using classical choice. Each formulation makes a different promise about computation and observation. Reading Lean means seeing those promises in the type.

The accompanying Lean file contains the Lean examples in order. The GADT examples are collected in Haskell and OCaml files. The Lean examples were checked with Lean 4.34.1, using its bundled library and no Mathlib dependency. For continued study, use Theorem Proving in Lean 4 alongside the Rocq reference manual: read the common construction first, then compare the rules that differ.