Thinking about lists backwards

Stream: new members

[Robert Spencer]

I have a simple question, and then a follow up philosophy question.

If I have a list, and a statement that it is not empty, is there an existing mechanism for extracting all but the last element (the equivalent of python's mylist[:-1]. In particular, one that is "supported" in terms of lemmas about its length etc.

My philosophical question is how to deal with the back of lists. Since lists are defined inductively "from the front", it is easy to talk about their heads, tails and such forth. It seems less simple to talk about their last element and the preceding sublist. How should one treat the back of a list, or operations done to the back? Should one reverse the list and then talk about the reversed head and then reverse again if necessary? Is it possible to _neatly_ do the opposite to

def foo : list ℕ → ℕ
| [] := 0
| (a :: b) := a

i.e. something along the lines of

def foo : list ℕ → ℕ
| [] := 0
| (b ++ [a]) := a

[Mario Carneiro]

There are a few variants on last available, but I guess init was not defined, or I missed it in the initial pass (although inits is there)

[Mario Carneiro]

It is of course easy to define

[Mario Carneiro]

def init {α} : list α → list α
| []     := []
| [a]    := []
| (a::l) := a :: init l

But to answer your second question, lean will certainly not let things be as nice if you want to manipulate lists from the right end. Besides the fact that both init and last are O(n) while head and tail are O(1), you can't use them in pattern matching. If you want to use pattern matching to decompose a list from the right, I suggest reversing it and then pattern matching.

[Robert Spencer]

Right. That is sort of what I thought. Thanks.

[Robert Spencer]

Ah, no I've found init in the library. It doesn't have much more than a definition that I can see though.

[Chris Hughes]

There's also list.reverse_rec_on (might be called something slightly different)