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 n
th 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 Option
s. 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.
List.get! L1 2
,L1.get! 2
, orL1[2]!
. While theList
section of the manual isn't finished, the notation is similar toArray
. Also see the List section of this answer for why it isn't as simple answer. $\endgroup$