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.

Computing the quotient and remainder is a basic function provided by all programming languages, including Lean 4 itself. Although it is a simple operation, it serves as an ideal first example for exploring how Lean 4 is used as a formal specification language: it involves a precondition (a non-zero denominator), a structured result (a pair of natural numbers), and a precise mathematical relationship between inputs and outputs that can be expressed directly in the type system using subtypes and dependent functions.

​
Starting with a Proposition

The most natural first attempt at capturing the required property is a proposition — a logical statement asserting that the right kind of values exist: 
def QRProp := ∀ n d : Nat, d ≠ 0 → ∃ q r : Nat, n = d * q + r ∧ r < d
This reads: for all natural numbers n and d, if d is non-zero, then there exist natural numbers q and r such that n = d * q + r and r < d. The proposition fully describes the mathematical content of division with remainder. However, being a proposition, QRProp has no computational content. A proof of QRProp confirms that such values exist but does not produce them. To derive an actual function we need to express the specification as a type: a dependent function type whose argument types capture the inputs and preconditions, and whose return type is a subtype capturing the result together with the property it must satisfy.

​
QR₁ — The Core Specification

def QR₁ := (n d : Nat) → (d ≠ 0) →
           { qr : Nat × Nat // n = d * qr.1 + qr.2 ∧ qr.2 < d }
QR₁ is the type of functions that take a natural number n, a natural number d, and evidence that d is non-zero, and produce a pair of values that are the quotient and remainder when n is divided by d. The return type is a subtype: the data value is a pair Nat × Nat whose first element qr.1 is the quotient and whose second element qr.2 is the remainder. (Equivalently, qr.fst and qr.snd may be used in place of qr.1 and qr.2.) Any function whose type is QR₁ is, by construction, guaranteed to satisfy the division algorithm property — correctness is encoded in the type rather than checked after the fact.

​
QR₂ — Using the Universal Quantifier

It is instructive to note there is no fundamental difference between dependent function types and the universal quantifier ∀. The specification can be written equivalently as: 
def QR₂ := ∀ n d : Nat, d ≠ 0 →
           { qr : Nat × Nat // n = d * qr.1 + qr.2 ∧ qr.2 < d }
Despite the use of ∀, QR₂ is still a type, not a proposition. The ∀ symbol is notation defined in terms of the dependent function type. The choice between the two forms is a matter of style: the convention usually adopted is to use the dependent function type when specifying a computable function, and ∀ when specifying a logical property.

​
QR₃ — Omitting Inferred Type Annotations

One practical difference between the two forms is that type annotations are mandatory in a dependent function type but optional in a universal quantifier when Lean can infer the types. This allows QR₂ to be shortened to: 
def QR₃ := ∀ n d, d ≠ 0 →
           { qr : Nat × Nat // n = d * qr.1 + qr.2 ∧ qr.2 < d }
Here, Lean infers that n and d have type Nat from the context provided by d ≠ 0 and the body of the subtype predicate. QR₂ and QR₃ are definitionally equal.

​
QR₄ — Encoding the Precondition in the Argument Type

In QR₁ through QR₃, the non-zero precondition on the denominator is expressed as a separate third argument of type d ≠ 0. An alternative is to fold the constraint directly into the type of the denominator argument using a subtype: 
def QR₄ := (n : Nat) → (d : { x : Nat // x ≠ 0 }) →
           { qr : Nat × Nat // n = d * qr.1 + qr.2 ∧ qr.2 < d }
Here the second argument d has type { x : Nat // x ≠ 0 } — the subtype of natural numbers that excludes 0. The function now takes only two arguments rather than three, because the evidence of non-zeroness is bundled into d itself. The two formulations are entirely equivalent: any implementation satisfying one satisfies the other.

​
QR₅ — Moving Arguments to the Left

Lean’s def syntax allows function arguments to be moved to the left-hand side of the :=, giving a cleaner presentation: 
def QR₅ (n : Nat) (d : { x : Nat // x ≠ 0 }) :=
           { qr : Nat × Nat // n = d * qr.1 + qr.2 ∧ qr.2 < d }
QR₅ reads: a function that takes a natural number n, then a non-zero natural number d, and returns a pair of numbers (q, r) such that n = d * q + r ∧ r < d. This is the most concise and readable of the five equivalent formulations, and the style most commonly used when writing specifications for functions with preconditions.

​
Summary

The five variants QR₁ through QR₅ illustrate several key ideas in Lean 4 specification:
  • Propositions vs. types: QRProp is a proposition and has no computational content; the remaining definitions are types that a function can inhabit.
  • Subtypes carry guarantees: the return subtype encodes the correctness condition so any inhabitant is provably correct.
  • Preconditions have two homes: they can appear as explicit proof arguments (d ≠ 0) or be folded into the argument type ({ x : Nat // x ≠ 0 }).
  • ∀ and dependent → are interchangeable when writing specifications; the choice is stylistic.
  • Specify a property that determines if a number is a prime number. Use the Lean remainder on division operator (%).
  • Specify a property that determines if a number is a prime factor of another number.
  • Specify a function that computes that maximum prime factor of a natural number greater than 1.

Build docs developers (and LLMs) love

Get started for freeTalk to us