Getting the last element of a list

Stream: new members

[Roman]

Hello, I got some trouble getting the first exercise done in https://lean-lang.org/functional_programming_in_lean/Getting-to-Know-Lean/Polymorphism/#Functional-Programming-in-Lean--Getting-to-Know-Lean--Polymorphism--Exercises
I mainly did something like :

def lastEntry (xs : List α) : Option α :=
    match xs with
    | [] => none
    | α :: ys => match ys with
        |[] => some α
        | _ :: _ => lastEntry ys

Where using [x] was possible :

def lastEntry (xs : List α) : Option α :=
    match xs with
    | [] => none
    | [x] => some x
    | α :: ys => lastEntry ys

But I can't see it being mentionned on the book so far, [] and :: are thought

[Damiano Testa]

It is not clear to me what the issue is, but the two definitions that you mention are provably equal:

@[simp]
def lastEntry (xs : List α) : Option α :=
    match xs with
    | [] => none
    | [x] => some x
    | α :: ys => lastEntry ys

@[simp]
def lastEntry' (xs : List α) : Option α :=
    match xs with
    | [] => none
    | α :: ys => match ys with
        |[] => some α
        | _ :: _ => lastEntry ys

example (xs : List α) : lastEntry xs = lastEntry' xs := by
  repeat first | simp | split

[Roman]

Hello, well I just wanted to check with you if it was intentional to have left out [x] or not from the book (unless I missed it).
I haven't touched at proofs or anything yet but that looks cool

[Damiano Testa]

Ah, I see!

So, the example above shows that indeed the two definitions are provably equal.

[Damiano Testa]

If I were to guess at the goal of #fpil at that point, it is probably showing that matching can be nested. Of course, improved pattern-matching (as in your second definition) is also incredibly important and I guess that it will come at some point.

[Damiano Testa]

I would probably ascribe this to the fact that the book is written "linearly" and one of the two concepts has to appear before the other.

[Kyle Miller]

It looks like the book introduces [a,b,c] notation as being short for List.cons a (List.cons b (List.cons c List.nil)), and that [] is short for List.nil, in section 1.6.1.

By extension, [x] is short for List.cons x List.nil (or x :: []).

The match patterns are allowed to be compound patterns.

[Kyle Miller]

The howManyDogs example shows that compound patterns are possible (with Sum.inl _ :: morePets, i.e. List.cons (Sum.inl _) morePets). That seems to be the only example, except for the failed sameLength.

[Kyle Miller]

This is all to say that

def lastEntry (xs : List α) : Option α :=
    match xs with
    | [] => none
    | α :: ys => match ys with
        |[] => some α
        | _ :: _ => lastEntry ys

is equivalent to

def lastEntry (xs : List α) : Option α :=
    match xs with
    | [] => none
    | α :: [] => some α
    | α :: ys => lastEntry ys

and so you can use the notation introduced earlier to write α :: [] as [α] if you want. That's not essential to the problem however.

[Roman]

Thank you really much for your answers,

By extension, [x] is short for List.cons x List.nil (or x :: []).

This is exactly what I struggled with, It all make much more sense now, pattern matching is still matching against the List's constructor because it is just like I wrote List.cons List.nil x, quite an awesome language

[Roman]

I took the liberty to make this (hopefully) clearer in the book https://github.com/leanprover/fp-lean/pull/223/files#diff-b8f529a5e781a75e8e74be85fc70eebb6ca2d56630594e3472f66746cbb15ee3
If you guys have time to spare I would appreciate your expertise, I don't have the shoulder to modify the book, as I am still reading it lol but hopefully you'll be able to see my intent and certain passage can be clarified