Lean 4 is a dependently typed functional programming language that can serve as a powerful specification language. Because the specification language, programming language, and proof framework are all the same language in Lean, formal specifications are not just precise and unambiguous — they can be directly executed, type-checked, and verified. This page gives an overview of the Lean 4 features most relevant to writing formal program specifications.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.
Lean Logic
Lean’s logic includes the standard propositional connectives and quantifiers familiar from first-order logic:| Connective | Meaning |
|---|---|
P ∧ Q | Conjunction |
P ∨ Q | Disjunction |
P → Q | Implication |
P ↔ Q | Logical Equivalence |
¬ P | Negation |
∀x, P x | Universal Quantification |
∃x, P x | Existential Quantification |
True | Always true proposition |
False | Never true proposition |
Lean Types
Some of the types provided by Lean are:| Type | Meaning |
|---|---|
T × U | Cartesian Product |
T ⊕ U | Disjoint Union |
T → U | Function Type |
Nat | Natural Numbers |
String | Character Sequences |
List T | Finite Sequences of T’s |
(a:A) → B a | Dependent Function |
(a:A) × B a | Dependent Product |
T → U and product T × U are special cases of the dependent forms in which there is no dependence between the type arguments.
Propositions vs Types for Specification
A central distinction in Lean is between propositions and types. Consider specifying a function that doubles a natural number. One natural attempt is to write this as a proposition:n, there exists a natural number m equal to 2 * n.” It is a valid proposition, and it is provable. However, propositions in Lean have no computational content — they are either provable or not provable, and a proof does not yield a runnable function. To obtain a computable doubling function from DoubleProp, you would have to separately define the function and then prove it satisfies the proposition.
Types, by contrast, carry data and computational content. An element of a type is a value (or function) that can be computed. The goal when writing a Lean-Spec specification is to construct a type that captures the same meaning as the proposition, so that an element of the type is a function satisfying the specification.
Lean’s dependent types make this possible. Because the dependent function type corresponds to universal quantification, and the dependent product corresponds to existential quantification, we can move directly from a logical statement to a type. The key bridging construct is the subtype { a : A // P a }, which combines a type A with a proposition P a — its elements are exactly those a : A for which P a holds. Using a subtype, the doubling specification becomes a genuine type:
Double₂ is a type. Any function of type Double₂ is, by construction, a doubling function — no separate proof required.
Naming Conventions
Lean-Spec follows standard Lean naming conventions throughout:- Type and proposition names are camel case with an initial upper case letter (e.g.
DoubleProp,Double₂,QR₁). - Function names are camel case with an initial lower case letter (e.g.
double,double₁).