Getting an element of a list in Lean

Question

I'm using Lean 4 along with Mathlib.

I'm trying to work with lists, but I can't find a function which obtains the nth entry of a list. It seems pretty hard to find for the most basic function of a list. Could someone help me get this example working?

def L1 := [1, 2, 3]
#eval ???? L1 2

Above, ???? is intended to mean some function which obtains the second entry. So here it should return 3. Here is the documentation for lists in Mathlib. My problem is that you have to supply a variable d, when I would rather just keep track that my indices do not exceed the length of the list on my own.

While I'm asking this, it would be good to get a working example of a hash map. I want to be able to use "add", "delete", and "get" for a hash map. Unfortunately the documentation here is pretty confusing. See here. I can't seem to construct a hash_fn either.

Here's some code I want to work. The functions in capital letters correspond to the lean functions that I'd like to use.

def L1 := MAKENEWHASHMAP TYPE1 TYPE2
def L2 := PUT L1 KEY1 VALUE1
#eval L2 /- This should return something resembling {(KEY1, VALUE1)}-/
def L3 := DEL L1 KEY1
#eval L3 /- This should return the empty hash map {}-/
#eval GET L2 KEY1 /- This should return VALUE1 -/

Answer 1

TL;DR

Use List.get! L1 2, L1.get! 2, or L1[2]! (They are all notation for the same thing.) However, I would very much disagree that retrieving the nth element is hardly "the most basic function of a list" in Lean.

(Also, this is an answer before the edits. Let me know if you need me to address something else in the edit. Many List functions can be found Init.Prelude, but just search these docs for other "List...." functions.)

Avoiding out-of-bounds access

Lean is a pure functional programming language, more pure than Standard ML or Haskell, or any other non-DTT programming language. Normal Lean code must not do anything mathematically impossible, including access from beyond the length of a list. (More specifically, Lean has to give a total function. See this answer.) While this is great, because it prevents a common error, it also is hard to work with sometimes. Lean has four patterns to get around this:

def l := [1, 2, 3]
def e := ([] : List Nat)

#eval l.get (2 : Fin 3)  -- 3  (Index is in `Fin (l.length)`, not `Nat`.)
#eval l[(2 : Fin 3)]     -- 3  (Short hand for l.get)
#eval e[(2 : Fin 0)]     -- Fails to compile.  Fin 0 is empty.

#eval l.get? 2   -- some 3  (Answer in an Option.)
#eval l[2]?      -- some 3  (Answer in an Option.)
#eval e[2]?      -- none    (Answer in an Option.)

#eval l.get! 2  -- 3
#eval l[2]!     -- 3
#eval e[2]!     -- 0  (If run in `#eval`, gives default value for `Nat`, which is 0)
                --     If run inside `main : IO unit`, gives runtime error.)

#eval l.getD 2 100  -- 3
#eval e.getD 2 100  -- 100  (We supplied a default value.)

The first is the most pure. By forcing the elements to be in Fin (l.length) it is impossible for there to be any out-of-bounds array access. The second returns an Option. This is just as pure and and should be familiar to anyone with experience in functional programming. It can be a bit annoying to work with Options, but there are nice patterns in functional programming for chaining together results which return Options. For simple stuff, where you don't mind a possible runtime error, you can use the third pattern. From the point of view of the type theory (and what you get when you run through #eval), if the index is out-of-bounds, it returns the default value for that type. The type must be an instance of Inhabited. For Nat, that default is 0. But when run from say main : IO unit, then it will give a runtime error, just like most languages. Finally, the fourth version lets you manually choose the default answer.

Code smell of random access lists

The type List in functional programming is not like the type List in say Python. It is essentially a linked list. For quick one-off stuff, using l[2] is no problem. But for many tasks, it would be a "code smell" to see random access of the List type in Lean. For example, this code would be O(N^2):

def sum_first_n_elements_of_list (l : List Nat) (n: Nat) :=
match n with
| 0 => 0
| k+1 => l[k]! + sum_first_n_elements_of_list l k

#eval sum_first_n_elements_of_list [0, 1, 2, 3, 4, 5] 4  -- 6

The reason is that to access the nth element, it has to traverse the list from the start.

A better approach would be to either use recursion:

def sum_first_n_elements_of_list' (l : List Nat) (n : Nat) : Nat :=
match l, n with
| _, 0 => 0
| [], _ => panic! s!"list {l} is smaller than {n}" -- explicitly handle error case!
| h :: l, k+1 => h + sum_first_n_elements_of_list' l k

#eval sum_first_n_elements_of_list' [0, 1, 2, 3, 4, 5] 4  -- 6

or to use the many predefined tools for working with lists, especially foldl:

def sum_first_n_elements_of_list'' (l : List Nat) (n : Nat) : Nat :=
(l.take n).foldl (fun partial_sum element => partial_sum + element) 0

#eval sum_first_n_elements_of_list'' [0, 1, 2, 3, 4, 5] 4  -- 6

Alternately, if random access is important, then use a different data structure like an Array, which behaves more like an array list like in Python if I understand correctly, but has some subtleties since it is inefficient unless used in a linear way (since it is not persistent). Other functional programming languages have persistent data structures for sequences that support fast random access. I don't know if Lean 4 has this yet.

Lean 3 and mathlib

(It turned out the OP actually was interested in Lean 3 and the Lean 3 version of mathlib.) The same ideas apply, but it is not as well organized. See list.nth_le (must provide proof that index is less than length), list.nth (returns option), list.inth (if type is inhabited, uses the registered default value), and list.nthd (must supply default value).

Further, those same files data.list.basic (in core Lean 3) and data.list.def (in mathlib) have many most of the list operations, which can help with the other parts of your question. If you are just interested in pure math, they are useful, but as executable algorithms, again they are often not very efficient for repeated use.