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.

The knapsack problem is a classic combinatorial optimisation problem: given a collection of items each with a weight and a value, choose a subset of items whose total weight fits within a given capacity and whose total value is as large as possible. It is an excellent example for formal specification because the what (a maximum-value feasible selection) is easy to state precisely, even though the how (finding such a selection efficiently) is computationally hard. This example shows how Lean 4’s subtype mechanism allows us to characterise optimal solutions directly in the type system, with no thought at all for how an implementation might work. 
import LeanSpec.lib.Util

​
Item

The first step is to define a structure representing a single item that can be placed in the knapsack. 
structure Item where
  value : Nat
  cost  : Nat
deriving BEq
Each item has a value (how desirable it is) and a cost (how much weight it contributes). The deriving BEq clause automatically generates a decidable equality instance, which is needed later for counting occurrences in lists. Note that two distinct items can have the same value and cost — the problem allows multiple copies of physically identical items. A structure in Lean 4 is the equivalent of a record or struct in other languages, packaging separate fields into a single unit. As we will see in later definitions, Lean structures are considerably more expressive than records in most languages because fields can be propositions that constrain the values of other fields.

​
Cost and Value of a Selection

The total cost of a list of items is the sum of the individual item costs: 
def cost (items : List Item) : Nat :=
  (items.map Item.cost).add 0
This maps the Item.cost projection over the list to obtain a list of natural numbers, then sums them. Similarly, the total value is: 
def value (items : List Item) : Nat :=
  (items.map Item.value).add 0
These two functions are the objective function (value, to be maximised) and the feasibility constraint (cost, which must not exceed the knapsack capacity).

​
SubList — Accounting for Duplicates

A candidate selection must be drawn from the available items. The right notion here is not a subset (which ignores duplicates) but a sublist that respects multiplicity: if a candidate selection contains two copies of some item, the source collection must also contain at least two copies of that item. 
def SubList [BEq α] (as bs : List α) :=
  ∀ a : α, as.count a ≤ bs.count a
SubList as bs holds when, for every element a, the number of times a appears in as does not exceed the number of times it appears in bs. This is a count-aware generalisation of the subset relation, and it correctly handles items with identical fields.

​
Candidate Solutions

​
Approach 1: A Predicate on Lists

A list of items is a candidate solution if it is a sublist of the available items and its total cost is within the knapsack’s capacity: 
def Candidate₁ (capacity : Nat) (source : List Item) (candidate : List Item) :=
  SubList candidate source ∧ cost candidate ≤ capacity
Candidate₁ is a predicate: given a capacity, a source list, and a candidate list, it is the proposition that candidate is a feasible selection.

​
Approach 2: A Type of Candidates

Alternatively, we can package the feasibility conditions directly into a subtype: 
def Candidate₂ (capacity : Nat) (source : List Item) :=
  { cand : List Item // SubList cand source ∧ cost cand ≤ capacity }
An element of type Candidate₂ capacity source is a feasible selection: the subtype condition guarantees that any value of this type already satisfies both the sublist and cost constraints. Nothing additional needs to be checked.

​
Specifying the Knapsack Problem

​
Knapsack₁ — Using the Predicate Approach

With Candidate₁ as a predicate, the knapsack problem is specified as finding an item list that is a candidate solution and that no other candidate solution exceeds in value: 
def Knapsack₁ (capacity : Nat) (source : List Item) :=
  { optimal : List Item
    // Candidate₁ capacity source optimal ∧
       ∀ is : List Item, Candidate₁ capacity source is → value is ≤ value optimal }
The subtype property has two parts: optimal must itself be a candidate (Candidate₁ capacity source optimal), and for every other list is that is also a candidate, the value of is must not exceed the value of optimal. This is a precise, executable-free characterisation of optimality. This is a compelling demonstration of where formal specification excels. The specification captures the problem by characterising the properties any solution must exhibit, with no thought for how an implementation might search for or construct such a solution. The pattern — define feasibility, then assert that the result is at least as good as every other feasible solution — recurs throughout the specification of optimisation problems.

​
Knapsack₂ — Using the Type Approach

When Candidate₂ is used to define the type of feasible solutions, the knapsack specification becomes: 
def Knapsack₂ (capacity : Nat) (source : List Item) :=
  { optimal : Candidate₂ capacity source
    // ∀ cand : Candidate₂ capacity source, value cand.val ≤ value optimal.val }
Here the data component of the subtype is not a bare List Item but a Candidate₂ capacity source — an element that already carries proof of feasibility. As a result, the subtype property no longer needs to state that optimal is a candidate; it can simply assert that every other candidate has value no greater than optimal. The optimality condition is simpler and the feasibility condition is elevated into the type itself. The .val projections (cand.val, optimal.val) access the underlying List Item from the Candidate₂ subtype, which is needed to apply the value function.

​
Comparing the Two Formulations

Both Knapsack₁ and Knapsack₂ correctly specify the same problem. The difference is where feasibility lives:
Knapsack₁Knapsack₂
Data componentList Item (unconstrained)Candidate₂ (already feasible)
Subtype propertyMust assert feasibility and optimalityNeed only assert optimality
Quantifier rangeAll List Item that happen to be candidatesAll Candidate₂ values (all feasible by construction)
Knapsack₂ is generally preferable: by encoding feasibility in the type of the optimal value, the subtype property is kept simpler and any function returning a Candidate₂ is guaranteed feasible by type-checking alone.

Build docs developers (and LLMs) love

Get started for freeTalk to us