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.

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 logic adds principles such as double-negation elimination, \neg\neg P\to P, which the rules above do not provide.

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 Set is a sort for small computational data, which Lean places in Type; Lean’s Set α is the type of 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

Arguments declared before a constructor’s colon stay in scope for the type that follows. The cons line could equally be written

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

Either way, n is an implicit argument that Lean usually infers. The dependency comes from using n in the later types, not from where it is declared.

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 List.head?, which must return an Option α because its input may be empty. Vec.head instead requires a nonempty vector, so its 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, while a recursive argument of type X → False would be forbidden. Nested inductive type constructors have additional rules, described in the inductive-type reference.

If we freely admitted a type Bad with 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 call itself: it applies the function stored in its argument. But the constructor lets us store d itself, as mk d : Bad. Applying d to it gives a closed term of type False. Unfolding d and matching the constructor returns the same term:

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

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’s core language instead has primitive fixpoint terms, checked by a guardedness discipline; its recursors are defined from them. 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.

Aside: 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. Well-founded recursion even brings a difficulty of its own. Lean’s accessibility predicate Acc lives in Prop, and together with proof irrelevance it makes definitional equality undecidable; the section on normalization returns to this.

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.

A first independent Lean proof

We can now write a proof without a guide. 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

The double braces in ⦃x y : A⦄ make x and y strict implicit arguments. Lean infers them, but only once a later explicit argument, here the equality, is supplied. So hf on its own still denotes the whole quantified statement.

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. The final command, #print axioms, lists the axioms a theorem depends on; for injectiveComp it reports none.

For practice, rewrite the proof as one fun expression. Prove that injectivity of g ∘ f implies injectivity of f, using congrArg g. Then try surjectivity: a composite of surjections is surjective, and if g ∘ f is surjective, so is g. Both statements end in an existential, so their proofs must supply witnesses.

Finally, return to Vec. Define Vec.toList and prove by induction that its result has length n. Then use resizeVec with Nat.zero_add n to turn a Vec α (0 + n) into a Vec α n. 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.

How far GADTs take us

Readers who do not program in Haskell or OCaml can skip this section.

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.

A formula with free variables is not a proposition but a predicate on assignments, F : Assignment → Prop. F and G agree at every assignment, so propext and funext together give F = G. F and H disagree at (p,q,r)=(\mathrm{True},\mathrm{False},\mathrm{False}). They are merely equisatisfiable: each has a satisfying assignment. Then propext equates the propositions ∃ ρ, F ρ and ∃ ρ, H ρ, but not the predicates. Classically, Prop has two values up to propositional equality, yet three Boolean inputs permit 2^{2^3}=256 distinct truth functions.

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. Carneiro’s 2019 thesis proved Lean 3’s type theory consistent relative to ZFC with n inaccessible cardinals for every finite n. Lean 4’s extensions need further work beyond that argument.

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 four 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. Decidability of type checking says an algorithm settles every typing judgment, including every question of definitional equality. 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 2020 paper 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

inductive Acc {α : Sort u} (r : α → α → Prop) : α → Prop where
  | intro (x : α) (h : (y : α) → r y x → Acc r y) : Acc r x

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. Werner’s “Sets in Types, Types in Sets” (1997) settled the strength needed for Rocq’s calculus. ZFC with n inaccessible cardinals proves the consistency of CIC with n+1 universes, and CIC with n+2 universes proves the consistency of ZFC with n inaccessibles. Carneiro’s thesis adapts this model to Lean.

Consistency proofs and the reliability of a checker

Mario Carneiro’s February 2025 HoTTEST presentation reports a gap in the thesis, found while formalizing it. The affected theorems are unique typing and definitional inversion, which rest on a confluence argument; the talk now lists them as conjectures. The thesis’s soundness proof used unique typing, though the thesis itself notes that Barras’s encoding avoids that dependency. The talk mentions an alternative route to soundness, while some kernel optimizations still depend on the conjectured theorems.

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.

The result is relative: the accepted declarations are consistent if set theory with those universes is. The proof is itself a Lean development, so Lean also serves as the metatheory, checked by the official kernel. 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.

Moses’s critique makes claims of several kinds, and these distinctions sort them. Its normalization claim is correct; the loop above reconstructs it. What it costs is one route to consistency, not evidence of inconsistency. Its consistency claim also stands as written: no public proof covers Lean 4 as the official kernel implements it. Carneiro’s thesis covers Lean 3, and its proof now has a reported gap; con-leche covers a different checker. Its strongest evidence concerns implementations: kernel bugs, nested inductives, and validation tools run without isolation. That evidence belongs to the third row of the table, and the postmortem confirms it. Its warning about mistranslated statements belongs to the first row. Its forecast that current Lean accepts some proof of False is a judgment about implementation risk, which the foundational results here neither support nor refute.

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.