In Lean 4, the distinction between types and propositions is fundamental to writing specifications that have computational content. Understanding this distinction is the key to moving from a logical statement of a program’s behaviour to a specification that can actually be implemented and verified.Documentation Index
Fetch the complete documentation index at: https://mintlify.com/paulch42/lean-spec/llms.txt
Use this file to discover all available pages before exploring further.
Propositions Have No Computational Content
Consider specifying a function that doubles a natural number. A first attempt might express this as a proposition:n, there exists a natural number m equal to 2 * n. It is provable — but a proof of this proposition does not yield a computable function. In Lean, propositions belong to the Prop universe. They are either provable or not provable. A proof witnesses the truth of a statement but carries no data or computational content that can be extracted and run.
To obtain a computable doubling function using DoubleProp, you would need to define the function independently and then carry out a separate proof that it satisfies the proposition. For formal specification purposes, this separation is inconvenient: the specification and the evidence that an implementation satisfies it would be disconnected.
Moving to Types
Since the dependent function type corresponds to universal quantification, and the dependent product(a : A) × B a corresponds to existential quantification, a natural next step is to try replacing the propositional connectives with their type-level counterparts:
Double₁ describes a function that takes n : Nat and returns a pair: a natural number m and something capturing the relationship m = 2 * n. The problem, however, is that the second component of a dependent product must be a type, whereas m = 2 * n is a proposition — and in Lean, propositions and types inhabit different universes.
This is where Lean’s subtype resolves the tension. The subtype { a : A // P a } is a hybrid: it combines a type A (providing computational content) with a proposition P a (providing the constraint). Its elements are exactly those a : A for which P a holds.
Universal Quantification and Dependent Functions
One important subtlety: in Lean,∀ and the dependent function type (a : A) → B a are definitionally the same thing — ∀ is notation defined in terms of the dependent function type. This means both of the following specifications are identical types:
∀, QR₂ is still a type, not a proposition, because the return type contains a subtype (not a Prop). Both QR₁ and QR₂ are the type of functions that compute a quotient-remainder pair (q, r) satisfying n = d * q + r ∧ r < d.
The choice between the two forms is a matter of convention: use the dependent function syntax (n : Nat) → when specifying computable functions, and ∀ n : Nat, when stating a property or invariant. The type annotation on arguments is mandatory in the dependent function form, but can be omitted with ∀ when Lean can infer the type.
The Bottom-Up Requirement
Lean requires every value to be defined before it is used. This imposes a strict constraint on how a specification is presented: specifications must be written bottom-up, defining component types and helper definitions before the higher-level specification that depends on them. This is the opposite of the top-down style often preferred for explanatory writing, where high-level concepts are introduced first and then broken down. When reading a Lean-Spec specification file, always expect to encounter helper definitions, subtypes for components, and auxiliary propositions before the main specification type that assembles them.All specifications in this tutorial use definitions from core Lean and the std4 standard library. Familiarity with the core
List, Nat, and Set APIs, as well as std4 utilities, will help when reading the examples.