Zulip Chat Archive

Stream: new members

Topic: Thinking about lists backwards


view this post on Zulip Robert Spencer (Sep 02 2019 at 06:31):

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

view this post on Zulip Mario Carneiro (Sep 02 2019 at 06:38):

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)

view this post on Zulip Mario Carneiro (Sep 02 2019 at 06:38):

It is of course easy to define

view this post on Zulip Mario Carneiro (Sep 02 2019 at 06:42):

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.

view this post on Zulip Robert Spencer (Sep 02 2019 at 06:45):

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

view this post on Zulip Robert Spencer (Sep 02 2019 at 06:55):

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

view this post on Zulip Chris Hughes (Sep 02 2019 at 07:12):

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


Last updated: May 14 2021 at 04:22 UTC