Module 2 · Lesson 4

Collections & Arrays

Lean provides two main sequential collections: List (linked lists) andArray (dynamic arrays). Knowing when to use each is crucial.

Lists

List is a singly-linked list—the default collection in functional programming:

lean

1-- Create lists with bracket syntax
2def nums : List Nat := [1, 2, 3, 4, 5]
3def empty : List String := []
4
5-- Prepend with :: (cons)
6def moreNums := 0 :: nums  -- [0, 1, 2, 3, 4, 5]
7
8-- Concatenate with ++
9def combined := [1, 2] ++ [3, 4]  -- [1, 2, 3, 4]
10
11-- Common operations
12#eval nums.length        -- 5
13#eval nums.head?         -- some 1
14#eval nums.tail?         -- some [2, 3, 4, 5]
15#eval nums.reverse       -- [5, 4, 3, 2, 1]
16#eval nums.take 3        -- [1, 2, 3]
17#eval nums.drop 2        -- [3, 4, 5]

Arrays

Array is a dynamic array with O(1) random access:

lean

1-- Create arrays with #[] syntax
2def nums : Array Nat := #[1, 2, 3, 4, 5]
3def empty : Array String := #[]
4
5-- Random access with []
6#eval nums[0]!   -- 1
7#eval nums[2]!   -- 3
8
9-- Safe access returns Option
10#eval nums[10]?  -- none
11
12-- Push elements (creates a new array)
13def moreNums := nums.push 6  -- #[1, 2, 3, 4, 5, 6]
14
15-- Common operations
16#eval nums.size          -- 5
17#eval nums.toList        -- [1, 2, 3, 4, 5]
18#eval nums.reverse       -- #[5, 4, 3, 2, 1]

The Three Ways to Index

The ! and ?suffixes above are not decoration — they are three genuinely different answers to "what if the index is out of range?"

lean

1def nums : Array Nat := #[1, 2, 3]
2
3-- arr[i]!  : panics at runtime if out of bounds. Requires Inhabited.
4#eval nums[0]!    -- 1
5#eval nums[5]!    -- Error: index out of bounds  (a real runtime panic)
6
7-- arr[i]?  : returns Option. Always safe, you handle the none.
8#eval nums[5]?    -- none
9
10-- arr.getD i default : returns a fallback instead of failing
11#eval nums.getD 5 0   -- 0
12
13-- arr[i]   : NO suffix. Lean demands a PROOF that i is in range,
14--            and then the access cannot fail — no check at runtime.
15example : nums[1] = 2 := rfl
16
17def safeSecond (a : Array Nat) (h : 1 < a.size) : Nat := a[1]
18#eval safeSecond #[9, 8, 7] (by decide)   -- 8

💡

For literal indices on a known array, plain arr[i] works with no visible proof: Lean discharges the side condition automatically with by get_elem_tactic. The proof obligation only becomes visible when the array or the index is a variable — and at that point, providing it is exactly what buys you a bounds-check-free access.

ℹ

If you want the size in the type rather than in a proof, use Vector α n — an Array bundled with a proof that its size is n. Then v[i] for i : Fin n needs no side condition at all, and the compiler can drop every bounds check.

When to Use Which?

Use Case	List	Array
Random access (index)	O(n) - slow	O(1) - fast
Prepend (add to front)	O(1) - fast	O(n) - slow
Append (add to end)	O(n) - slow	O(1)* - fast
Pattern matching	Natural	Less common
Proofs & reasoning	Preferred	More complex

Complexity Tips

A quick mental model: Lists are great for building up results and pattern matching, while Arrays are great for indexing and bulk computation. When performance matters, convert to the structure that matches the dominant operation.

Key Takeaway

Use List for pattern matching, proofs, and when building from the front. Use Array for computation, random access, and performance-critical code.

Transforming Collections

Both List and Array support similar transformation methods:

lean

1def nums := [1, 2, 3, 4, 5]
2
3-- Map: apply a function to each element
4#eval nums.map (· * 2)           -- [2, 4, 6, 8, 10]
5#eval nums.map toString          -- ["1", "2", "3", "4", "5"]
6
7-- Filter: keep elements matching a predicate
8#eval nums.filter (· > 2)        -- [3, 4, 5]
9#eval nums.filter (· % 2 == 0)   -- [2, 4]
10
11-- FilterMap: map and filter in one step
12#eval nums.filterMap (fun n => if n > 2 then some (n * 10) else none)
13-- [30, 40, 50]
14
15-- Find: first element matching a predicate
16#eval nums.find? (· > 3)         -- some 4

Folding and Reducing

Fold operations reduce a collection to a single value:

lean

1def nums := [1, 2, 3, 4, 5]
2
3-- foldl: fold from left to right
4#eval nums.foldl (· + ·) 0    -- 15 (sum)
5#eval nums.foldl (· * ·) 1    -- 120 (product)
6#eval nums.foldl max 0        -- 5 (maximum)
7
8-- Build a string
9#eval nums.foldl (fun acc n => acc ++ toString n) ""  -- "12345"
10
11-- foldr: fold from right to left
12#eval nums.foldr (· :: ·) []  -- [1, 2, 3, 4, 5] (copy)
13
14-- Specialized operations
15#eval nums.sum     -- 15 (requires Add instance)
16#eval nums.all (· > 0)  -- true
17#eval nums.any (· > 4)  -- true

Ranges

[start:stop] builds a range, which is a small record describing an iteration — not a list. Its job is to drive a for loop:

lean

1-- A range is a value describing start/stop/step, NOT a list
2#eval [0:5]
3-- { start := 0, stop := 5, step := 1, step_pos := _ }
4
5-- Its purpose is to be iterated
6#eval Id.run do
7  let mut acc := #[]
8  for i in [0:5] do
9    acc := acc.push i
10  return acc                -- #[0, 1, 2, 3, 4]
11
12-- With a step
13#eval Id.run do
14  let mut acc := #[]
15  for i in [1:10:2] do
16    acc := acc.push i
17  return acc                -- #[1, 3, 5, 7, 9]
18
19-- If you want an actual list, ask for one:
20#eval List.range 5          -- [0, 1, 2, 3, 4]   (0 to n-1)
21#eval List.range' 1 5 2     -- [1, 3, 5, 7, 9]   (start, count, step)
22
23-- Useful for generating test data
24def squares := (List.range 10).map (fun n => n * n)
25#eval squares  -- [0, 1, 4, 9, 16, 25, 36, 49, 64, 81]

⚠

The end of a range is exclusive, and List.range' start count step takes a count, not a stop value — List.range' 1 5 2 produces five elements starting at 1, not the elements below 5. Mixing these two up is a classic off-by-many.

Deep Dive: Array Performance

Arrays in Lean use a clever optimization: when an array has only one reference, mutations happen in-place. This means code that looks functional can be as efficient as imperative code.

lean

1-- This is efficient because 'arr' is only referenced once
2def buildArray (n : Nat) : Array Nat := Id.run do
3  let mut arr := #[]
4  for i in [0:n] do
5    arr := arr.push i
6  return arr

The compiler detects single-ownership and optimizes accordingly.

Zipping Collections

Combine two collections element-wise:

lean

1def names := ["Alice", "Bob", "Carol"]
2def ages := [30, 25, 35]
3
4-- Zip into pairs
5#eval names.zip ages
6-- [("Alice", 30), ("Bob", 25), ("Carol", 35)]
7
8-- Zip with a function. Note the argument order:
9--   List.zipWith (f : α → β → γ) (xs : List α) (ys : List β)
10-- so the FUNCTION comes first, and ys comes last.
11#eval names.zipWith (fun name age => s!"{name}: {age}") ages
12-- ["Alice: 30", "Bob: 25", "Carol: 35"]
13
14-- Pair each element with its index
15#eval names.zipIdx
16-- [("Alice", 0), ("Bob", 1), ("Carol", 2)]

ℹ

zip stops at the shorter list — no error, no padding. [1,2,3].zip [10] is [(1, 10)]. That is usually what you want, but it means a length mismatch fails silently, so check lengths first if they are supposed to agree.

Converting Between List and Array

lean

1def myList : List Nat := [1, 2, 3]
2def myArray : Array Nat := #[1, 2, 3]
3
4-- List to Array
5#eval myList.toArray   -- #[1, 2, 3]
6
7-- Array to List  
8#eval myArray.toList   -- [1, 2, 3]
9
10-- Chain operations
11#eval #[1, 2, 3].toList.reverse.toArray  -- #[3, 2, 1]

HashMap and HashSet

For efficient key-value storage and membership testing, use Std.HashMap andStd.HashSet:

lean

1-- These two imports go at the TOP of the file, before any definition
2import Std.Data.HashMap
3import Std.Data.HashSet
4
5open Std
6
7-- Create a HashMap. ∅ (or {}) is the empty map; the type annotation
8-- is what tells Lean which map you mean.
9def ages : HashMap String Nat := (∅ : HashMap String Nat)
10  |>.insert "Alice" 30
11  |>.insert "Bob" 25
12
13-- Lookup — three equivalent spellings
14#eval ages["Alice"]?         -- some 30   (GetElem? syntax, most idiomatic)
15#eval ages.get? "Alice"      -- some 30
16#eval ages["Unknown"]?       -- none
17
18-- Total lookup with a fallback
19#eval ages.getD "Unknown" 0  -- 0
20
21-- Check membership, count, enumerate
22#eval ages.contains "Bob"    -- true
23#eval ages.size              -- 2
24#eval ages.toList            -- [("Alice", 30), ("Bob", 25)]
25
26-- HashSet for unique values
27def seen : HashSet String := (∅ : HashSet String)
28  |>.insert "a"
29  |>.insert "b"
30  |>.insert "a"  -- Duplicate, ignored
31
32#eval seen.size              -- 2
33#eval seen.contains "a"      -- true

⚠

HashMap.toList returns entries in unspecifiedorder — it depends on hash values, not insertion order. Never rely on it for output you compare against a fixed expectation; sort first. If you need deterministic ordering, use Std.TreeMap instead, which keeps keys sorted.

ℹ

HashMap and HashSet require BEq and Hashable instances for the key type. Most standard types already have these.

Strings as Collections

Strings can be treated as collections of characters:

lean

1-- Iterate over characters
2#eval "hello".toList           -- ['h', 'e', 'l', 'l', 'o']
3
4-- Map over characters (String.map exists and returns a String)
5#eval "hello".map Char.toUpper -- "HELLO"
6
7-- Fold characters
8#eval "hello".foldl (fun acc c => acc ++ toString c ++ "-") ""
9-- "h-e-l-l-o-"
10
11-- Check all/any
12#eval "HELLO".all Char.isUpper     -- true
13#eval "Hello".any Char.isLower     -- true
14
15-- There is NO String.filter. Go through the character list:
16#eval "he11o".toList.filter Char.isAlpha           -- ['h', 'e', 'o']
17#eval String.ofList ("he11o".toList.filter Char.isAlpha)  -- "heo"

ℹ

String supports the operations that can be done in a single UTF-8 pass (map, foldl, all, any) but not ones that would need arbitrary indexing. For anything else, the round trip .toList → operate → String.ofList is the normal idiom, and it is what the missing functions would do anyway.

💡

When you need to do heavy computation, convert to Array. When you need to do pattern matching or prove properties, convert to List.

Exercise: Transform an Array

Convert an Array to a List, filter even numbers, and convert back to an array.

lean

1def nums : Array Nat := #[1, 2, 3, 4, 5, 6]
2
3def evens : Array Nat :=
4  nums.toList.filter (· % 2 == 0) |>.toArray
5
6#eval evens  -- #[2, 4, 6]

Recursive Data Next: Pattern Matching