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.

Graph search and shortest path problems arise in a wide range of applications, from routing and scheduling to dependency analysis and network optimisation. They make excellent specification examples because they involve several interacting concepts — nodes, directed edges, connectivity, path validity — and because getting the specification right is non-trivial: a naive first attempt turns out to be unimplementable, a second attempt admits a trivially wrong implementation, and a correct specification requires the disjoint sum type to cleanly separate the “path found” and “no path exists” cases. This example also introduces non-empty lists as a structure with an invariant field, and illustrates the general inv naming convention for type-level constraints. 
import LeanSpec.lib.Util

​
Non-Empty Lists

Before defining graphs and paths, we need a type that guarantees a list is non-empty. A path through a graph must contain at least one edge, so an ordinary List is inadequate. A natural model is: 
structure List₁ (α : Type) where
  list : List α
  inv  : list ≠ []
An element of List₁ α is a pair of a core Lean list and a proof that the list is non-empty. The field inv is not data — it carries no computational content — but it is a constraint on the list field. The empty list is excluded from the type because [] ≠ [] is a false proposition and can never be proved. This illustrates a powerful feature of Lean structures that distinguishes them from records in most traditional languages: a field can be a proposition that restricts which values the other fields may take. The convention adopted throughout this example is that fields named inv are invariant fields — they specify constraints that any instance of the type must satisfy, and contain no data themselves. We can define a HasSubset instance for List₁ by delegating to the underlying list: 
instance : HasSubset (List₁ α) where
  Subset l₁ l₂ := l₁.list ⊆ l₂.list
Since the list is guaranteed non-empty, the functions that extract the first and last element are total (they need not return an Option): 
def List₁.first : List₁ α → α
  | ⟨a::_, _⟩ => a

def List₁.last : List₁ α → α
  | ⟨[a], _⟩      => a
  | ⟨_::a::as, _⟩ => last ⟨a::as, by simp⟩
List₁.first matches on the anonymous constructor ⟨a::_, _⟩, extracting the head of the list (the _ ignores the tail and the inv proof). List₁.last recurses: a singleton list [a] has last element a; for a longer list _::a::as, the last element is the last element of the non-empty tail a::as.

​
Graphs

​
Nodes

All we need from a node is the ability to distinguish it from other nodes, so String is sufficient: 
abbrev Node := String

example : Node := "N1"

​
Edges

An edge is directed — it has a start node, an end node, and a cost to traverse it: 
structure Edge where
  starts : Node
  ends   : Node
  cost   : Nat
deriving DecidableEq

example : Edge := {
  starts := "N1"
  ends   := "N2"
  cost   := 4
}
The deriving DecidableEq clause gives us decidable equality on Edge, which is needed for the path invariant. Edges are directed: traversing from starts to ends has cost, but the reverse direction is a different edge (or may not exist at all).

​
Graphs

A graph is simply a set of edges: 
abbrev Graph := Set Edge

def exampleGraph : Graph := {⟨"N1","N2",4⟩, ⟨"N1","N3",7⟩, ⟨"N2","N3",2⟩}

​
Paths

With edges and graphs defined, we can describe a path. Path is dependent on Graph: the type of paths over graph g is Path g, and a path over one graph is not a path over another. 
structure Path (g : Graph) where
  path : List₁ Edge
  inv  : path.list ⊆ g.val ∧ path.list.Chain' (·.ends = ·.starts)
The structure has two fields:
  • path is a non-empty list of edges that constitutes the path.
  • inv is the conjunction of two invariant conditions:
    • inv.left: every edge in the path belongs to the graph g.
    • inv.right: consecutive edges are connected — the ends node of each edge equals the starts node of the next. (This uses List.Chain' from std4.)
The inv field is named according to the convention: it captures constraints, holds no data, and restricts which path values are valid. Where there are multiple constraints, they are combined into a single inv field using conjunction (∧). This keeps the structure clean and means that any instance of Path g is structurally guaranteed to be a valid path over g.

​
Path Start and End Nodes

Two convenience functions extract the start and end nodes of a path: 
def Path.start (p : Path g) : Node :=
  p.path.first.starts

def Path.end (p : Path g) : Node :=
  p.path.last.ends
Because p.path is a List₁, the first and last functions are total.

​
An Example Path

Here is a concrete path over exampleGraph: 
example : Path exampleGraph := {
  path := ⟨[⟨"N1","N2",4⟩, ⟨"N2","N3",4⟩], by simp⟩,
  inv  := sorry
}
The by simp discharges the non-emptiness proof automatically. The sorry stands in for the conjunction of the two invariant proofs (membership in the graph and chain connectivity). When specifying rather than implementing, sorry is a useful placeholder for proof obligations that are not the focus of attention. A fully verified implementation would replace it with an actual proof.

​
FindPath₁ — Unimplementable

A natural first attempt at specifying graph search is: 
def FindPath₁ (g : Graph) (s e : Node) :=
  { p : Path g // p.start = s ∧ p.end = e }
Given a graph g and nodes s and e, return a path over g from s to e.
FindPath₁ is unimplementable. No program can satisfy this specification in general. The problem is that the specification demands a path be returned, but provides no guarantee that any such path exists. There are two independent reasons a path might not exist:
  1. The nodes s or e may not appear in the graph at all.
  2. Even if both nodes are in the graph, there may be no directed sequence of edges connecting s to e.
Any function of type FindPath₁ g s e would need to produce a path for every possible g, s, e — including cases where no path exists. This is impossible.

​
FindPath₂ — Trivially Implementable in the Wrong Way

Wrapping the result in Option appears to fix the problem: 
def FindPath₂ (g : Graph) (s e : Node) :=
  Option { p : Path g // p.start = s ∧ p.end = e }
This accommodates failure by allowing none to be returned when no path exists. However, it overcorrects:
FindPath₂ admits a trivially correct but useless implementation. The function that always returns none satisfies the specification:
def findPath (g : Graph) (s e : Node) :
  Option { p : Path g // p.start = s ∧ p.end = e } := none
An implementation that always reports “no path found” is useless, yet it is a valid inhabitant of FindPath₂. The specification does not distinguish between “no path exists” and “I didn’t bother to look”.
The root problem is that FindPath₂ makes no distinction between the two possible outcomes. A correct specification must require that none is returned only when no path exists — that is, none must be accompanied by proof that no path exists.

​
IsPath — Naming the Concept

Before fixing the specification, it is useful to give the concept of “a path from s to e over g” its own name: 
def IsPath (g : Graph) (s e : Node) := { p : Path g // p.start = s ∧ p.end = e }
IsPath g s e is the type of paths from s to e over g. This is the same type as in FindPath₁, simply renamed to reflect its semantic role.

​
FindPath₃ — The Correct Specification with Disjoint Sum

To correctly handle both outcomes we need a type that either contains a path or contains evidence that no path exists. At the propositional level, the negation of a proposition P is ¬ P, which is definitionally equal to P → False. At the type level, the analogous statement for a type T is T → Empty. This motivates the final specification: 
def FindPath₃ (g : Graph) (s e : Node) :=
  IsPath g s e ⊕ (IsPath g s e → Empty)
The type ⊕ is the disjoint sum (also called Sum), which packages exactly one of two alternatives:
  • Left injection (Sum.inl): a value of type IsPath g s e, i.e. an actual path from s to e.
  • Right injection (Sum.inr): a value of type IsPath g s e → Empty, i.e. a proof that no such path exists (a function that would produce an element of the empty type Empty from any hypothetical path — which is impossible unless no such path exists).
Any implementation must commit to one branch or the other. It cannot return the right injection unless it can genuinely prove that no path exists; and it cannot return the left injection unless it can produce an actual path. The trivial none escape hatch from FindPath₂ is closed.

​
Shortest Path

​
Path Cost

The cost of a path is the sum of the costs of its constituent edges: 
def Path.cost (p : Path g) : Nat :=
  (p.path.list.map (·.cost)).add 0
This maps the edge cost projection over the list of edges and sums the results.

​
ShortestPath

Finding the shortest path is an optimisation problem, and follows the same pattern as the Knapsack specification: 
def ShortestPath (g : Graph) (s e : Node) (_ : IsPath g s e) :=
  { p : IsPath g s e // ∀ q : IsPath g s e, p.val.cost ≤ q.val.cost }
The result is a path from s to e over g — of type IsPath g s e — such that every other path from s to e costs at least as much. The key difference from the FindPath specifications is the precondition (_ : IsPath g s e). By requiring the caller to supply evidence that at least one path from s to e exists, the disjoint sum from FindPath₃ is avoided: we know a solution exists, so the specification simply asks for the best one. The anonymous argument name _ signals that the precondition value is required for type-checking but is not referenced by name in the body. This precondition pattern — (_ : T) — is a common idiom for specifying functions that are only meaningful under certain conditions, without exposing the proof as a named variable.

​
Summary

This example has introduced several important patterns:
  • Invariant fields named inv: structure fields that are propositions restricting the values of data fields. They carry no runtime content but enforce type-level correctness guarantees.
  • Dependent types: Path g depends on g : Graph, ensuring that path membership and connectivity are always checked relative to a specific graph.
  • Disjoint sums for fallible search: T ⊕ (T → Empty) cleanly separates the “found” and “provably not found” cases, ruling out both unimplementable all-success specifications and trivially satisfiable all-failure implementations.
  • Preconditions that unlock simpler specifications: supplying (_ : IsPath g s e) as an argument allows ShortestPath to use a simple subtype rather than a disjoint sum.
  • Modify the specification of ShortestPath such that it does not assume the existence of a path.
  • Specify the property that a graph has no edges with identical start and end nodes.
  • Specify the property that a graph is acyclic.
  • Define non-empty lists as a subtype instead of a structure, and modify the remainder of the specification as necessary.

Build docs developers (and LLMs) love

Get started for freeTalk to us