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.

Sorting is one of the most thoroughly studied problems in computer science, making it an excellent subject for exploring formal specification. The informal description is compact — a sort function takes a list and returns a list that is an ordered permutation of its input — yet formalising it correctly turns out to require care. This example demonstrates that a seemingly reasonable first specification can be subtly wrong and unimplementable, and walks through the refinements needed to arrive at a correct one. It also introduces inductive predicates as an alternative to recursive definitions. 
import LeanSpec.lib.Util

​
A Naive First Attempt

​
Ordered₁

A natural recursive predicate for “a list is sorted in ascending order” is: 
def Ordered₁ [LT α] : List α → Prop
 | [] | [_] => True
 | a::b::as => a < b ∧ Ordered₁ (b::as)
Empty and singleton lists are trivially ordered. A list of two or more items is ordered if the first item strictly precedes the second, and the tail starting from the second item is also ordered. The type class constraint [LT α] requires the element type α to support a less-than relation.

​
Permutation₁

A predicate for “two lists are permutations of each other” based on membership: 
def Permutation₁ (as bs : List α) :=
  ∀ a : α, a ∈ as ↔ a ∈ bs
Two lists are permutations of each other if they contain the same items — every element of one appears in the other and vice versa.

​
Sort₁

Combining these predicates: 
def Sort₁ [LT α] (as : List α) :=
  { sas : List α // Ordered₁ sas ∧ Permutation₁ as sas }
Sort₁ takes a list of elements with an order relation and returns a list that is both ordered and a permutation of its input. This looks correct. It isn’t.
Sort₁ is unimplementable. There is no program that can satisfy this specification for all inputs:
  1. Ordered₁ uses strict <, which rejects duplicates. Consider the input [2, 2]. Any sorted permutation of this list would also be [2, 2], but Ordered₁ requires consecutive elements to satisfy 2 < 2, which is false. No list containing duplicates can ever satisfy Ordered₁.
  2. Permutation₁ does not count occurrences. Consider the lists [1, 2] and [2, 1, 2]. The element 1 appears in both and the element 2 appears in both, so Permutation₁ [1,2] [2,1,2] holds — yet these lists are clearly not permutations of each other.
Just as there is no guarantee a postulated mathematical theorem is provable, there is no guarantee a program specification is implementable. Even a specification that type-checks perfectly can fail to capture the intended meaning.

​
The Corrected Specification

​
Ordered₂

The fix for Ordered₁ is to replace the strict less-than < with the non-strict less-than-or-equal ≤: 
def Ordered₂ [LE α] : List α → Prop
 | [] | [_] => True
 | a::b::as => a ≤ b ∧ Ordered₂ (b::as)
The structure is identical to Ordered₁ but uses ≤ (with the corresponding type class LE), which allows equal consecutive elements and therefore handles duplicate values correctly.
Strictly speaking, LE alone is insufficient — it only guarantees that some binary predicate exists on the type, not that it behaves like the familiar “less than or equal to”. The predicate should be a partial order (reflexive, antisymmetric, transitive). A fully rigorous treatment would require partial orders from mathlib4, but for the purposes of this example LE is adequate.

​
Permutation₂

The fix for Permutation₁ is to count occurrences using List.count rather than testing membership: 
def Permutation₂ [BEq α] (as bs : List α) :=
  ∀ a : α, as.count a = bs.count a
List.count is defined in std4 and counts how many times a given element appears in a list. Two lists are permutations of each other precisely when they contain the same number of occurrences of every element. The element type must support decidable equality (BEq α) for counting to work. You can inspect the type of List.count in Lean: 
#check List.count

​
Sort₂

The corrected sort specification uses both updated predicates: 
def Sort₂ [BEq α] [LE α] (as : List α) :=
  { sas : List α // Ordered₂ sas ∧ Permutation₂ as sas }
The structure is unchanged from Sort₁, but the combination of Ordered₂ (using ≤) and Permutation₂ (counting occurrences) makes this specification correct and implementable.

​
Inductive Predicates: An Alternative Approach

The predicate Ordered₂ is typical of the traditional recursive style, with the distinction that it produces a Prop rather than a Bool. Dependently typed languages like Lean offer a complementary technique: inductive predicates. An inductive predicate is an inductive definition of a proposition rather than of a data type, and a member of the resulting type is a proof of the proposition. The Ordered predicate expressed inductively is: 
inductive Ordered₃ [LE α] : List α → Prop
  | empty       : Ordered₃ []
  | singleton a : Ordered₃ [a]
  | twoplus a b as (hab : a ≤ b) (hbas : Ordered₃ (b::as)) :
                  Ordered₃ (a::b::as)
The three constructors correspond directly to the three cases in Ordered₂:
  • empty is a proof that the empty list is ordered.
  • singleton a is a proof that any singleton list [a] is ordered.
  • twoplus a b as hab hbas is a proof that the list a::b::as is ordered, given that hab is evidence a ≤ b and hbas is a proof that b::as is already ordered.
The correspondence between Ordered₂ and Ordered₃ is exact — they define the same predicate, one recursively and the other inductively. Inductive predicates are often preferred when working with Lean’s proof automation, since their constructors make it straightforward to build and decompose proofs. The Lean standard library also provides List.Chain', which generalises this pattern: 
#check List.Chain'

​
Summary

The journey from Sort₁ to Sort₂ illustrates several important lessons in formal specification:
  • Specification bugs are real. A type-correct specification can still be wrong or unimplementable.
  • Strict vs non-strict ordering matters. Using < instead of ≤ silently excludes inputs with duplicates.
  • Membership is not the same as counting. Permutation must account for multiplicity.
  • Multiple styles are available. Recursive definitions and inductive predicates express the same concepts in different ways, and the best choice depends on context.
As with programming and proof, there is no single correct way to specify a program. The specification process is iterative: as you refine a specification, clearer ways of expressing the underlying concepts emerge.
  • Specify a function that, given a natural number, returns the prime factors of the number. Use the Prime property from the last exercise.
  • Using Permutation₂, specify a function that returns all permutations of an input list.
  • The Lean standard library std4 defines an inductive proposition List.Chain'. Specify Sort using Chain'. 
#check List.Chain'

Build docs developers (and LLMs) love

Get started for freeTalk to us