Lists and optional values
Prove the first-element law for every nonempty list.
In this course 7 / 14
List Nat is the type of lists of natural numbers. [5, 8, 2] has three elements in that order. [] is an empty list. The elements of a list all have the same type.
An empty list has no first element. A function that asks for the first element therefore needs a way to say “there is none”. Option Nat provides two forms: some n contains a natural number, and none represents an absent result.
xs.head? asks for the first element of a list xs and returns an Option. The supplied definition firstItem gives this operation a name. Read firstItem [5, 8, 2] as “ask for the first item of this list”.
The distinction between some 0 and none matters: a list can start with zero, or it can have no element at all. Using a special number to mean “missing” would lose that distinction.
Writing the input as x :: xs states that the list is nonempty and names both its first element and its remaining tail. After unfolding firstItem, simp knows how head? behaves on a list of that shape.
Worked example
#eval firstItem []
#eval firstItem [0, 9]
example : firstItem [] = none := by
unfold firstItem
simpThe empty-list theorem exposes the definition and simplifies that constructor. Your theorem covers every nonempty list, regardless of its tail.
A constructor such as x :: xs exposes enough shape for simplification. The theorem now covers every nonempty list, not one example.
- 3. Palindrome Easy
- 32. Valid anagram Easy
Prove that the first item of every list built as x :: xs is some x.
Suggested steps
- Expose the body of
firstItem - Simplify the nonempty-list case
These marks only recognize text. Another correct proof may use different steps; Lean checks whether it works.
\to in the editor, or click:Where you start. Everything above ⊢ may be assumed; the line below it is what you must prove.
Knowledge check
Answer without looking back, then check your reasoning.
correct