Skip to main content

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.

Subtypes are the central tool in Lean-Spec. The form { a : A // P a } creates a type whose elements are exactly those elements of A satisfying proposition P. This hybrid construct — combining a type for computational content with a proposition for constraints — is what makes Lean’s dependent type system uniquely suited to program specification.

​
The Subtype

A subtype { a : A // P a } is read as “the type of values a of type A such that P a holds.” The type A supplies the data (the computational content), and the proposition P a constrains which elements of A are permitted. To see how this resolves the specification problem, consider the progression of attempts to specify a doubling function: 
-- Proposition (no computational content)
def DoubleProp := ∀n : Nat, ∃m : Nat, m = 2 * n

-- Type using subtype (this IS a specification)
def Double₂ := (n : Nat) → { m : Nat // m = 2 * n }

-- Same, with args on the left
def Double₃ (n : Nat) := { m : Nat // m = 2 * n }
DoubleProp is a proposition: provable, but with no computational content. Double₂ and Double₃ are types. Any element of Double₂ is a function that, given a natural number n, returns a natural number m together with evidence that m = 2 * n. Throughout the tutorial, the style of Double₃ — moving function arguments to the left of := — is generally preferred.

​
Implementing a Specification

A function satisfying Double₃ must provide both the computed value and the required evidence: 
def double (n : Nat) : { m : Nat // m = 2 * n } :=
  {val := 2 * n, property := rfl}
The result is a structure with two fields:
  • val — the computational content, the actual number returned (2 * n).
  • property — the evidence that val satisfies the constraint (rfl, which works here because 2 * n = 2 * n holds by reflexivity).
We can verify that double implements Double₃ for any n: 
variable (n : Nat)
#check (double n : Double₃ n)
And since Double₂ and Double₃ express the same thing, we also have: 
#check (double : Double₂)
When presented with #eval double 4, Lean outputs 8 rather than the subtype structure {val := 8, property := rfl}. Lean automatically strips non-computational content when evaluating, so the output is the plain number.

​
Preconditions as Subtype Arguments

Preconditions — requirements on the inputs of a function — can be expressed in two equivalent ways using subtypes. Consider specifying quotient and remainder, which requires the divisor to be non-zero: 
-- As a precondition argument
def QR₁ := (n d : Nat) → (d ≠ 0) →
           { qr : Nat × Nat // n = d * qr.1 + qr.2 ∧ qr.2 < d }

-- As a separate argument with evidence embedded in a subtype
def QR₄ := (n : Nat) → (d : { x : Nat // x ≠ 0 }) →
           { qr : Nat × Nat // n = d * qr.1 + qr.2 ∧ qr.2 < d }
In QR₁, the non-zero precondition is a separate argument d ≠ 0 alongside the plain d : Nat. In QR₄, the precondition is folded into the type of d itself: the second argument is the subtype of natural numbers that excludes zero, so the separate evidence argument is no longer needed. Both specifications are equivalent; choosing between them is a matter of taste. QR₄ is slightly more self-contained — the type of d directly expresses the constraint — while QR₁ separates the value from its precondition more explicitly.

​
Dependent Types and Invariants

The same technique that embeds postconditions into return types can be used to embed invariants directly into data structure definitions. Lean structures support this natively: a field whose type is a Prop is a constraint, not data. For example, a type of non-empty lists can be defined as: 
structure List₁ (α : Type) where
  list : List α
  inv  : list ≠ []
An element of List₁ contains a List α (which is structurally capable of being empty) and a proof that the list is non-empty. Because we can never prove [] ≠ [], there is no way to construct an element of List₁ whose list field is the empty list. The constraint is enforced at the type level — violations are impossible by construction. By convention, fields named inv capture invariants: they contain no data, but restrict which values the other fields may take. When there are multiple constraints, a single inv field is used as their conjunction, or subscripted fields inv₁, inv₂, etc. are used for clarity.

​
Non-Computational Content

An element of { a : A // P a } is strictly a pair: the value a (computational content) and evidence of P a (non-computational). Lean can often coerce a subtype value to its embedded value automatically in contexts where a plain A is expected. When automatic coercion is not available, val must be accessed explicitly. From a programming perspective, the evidence component is irrelevant to execution. It does not intrude when constructing specifications, it is essential when deriving or verifying implementations, and it is automatically removed by the compiler. The non-computational fields in subtypes and inv fields in structures have no runtime cost.

Build docs developers (and LLMs) love

Get started for freeTalk to us