list.head vs. list.last

Stream: new members

[Joachim Breitner]

The list.head function requires [inhabited α], but list.last requires l ≠ list.nil. I understand that both are useful in different settings, and indeed there is list.ilast for the variant with [inhabited α].
For what I am doing right now I am missing the not-nil-variant of head, though. Is there a reason why it isn’t there?

[Eric Wieser]

Is it docs#list.head'?

[Eric Rodriguez]

this naming is a disaster

[Mario Carneiro]

I don't think I have ever used the l != [] functions on list. I see a use for list.head and list.head' style functions

[Mario Carneiro]

what is your application?

[Mario Carneiro]

The naming is definitely a disaster. I would use list.ihead and list.head for those two

[Mario Carneiro]

to match docs#list.nth and docs#list.inth

[Joachim Breitner]

My application is dealing with reduced non-empty word in free products, where I have to do a lot of peeking at the head and tail.

[Joachim Breitner]

But it turns what I really want is a higher level API (that uses the list internally), and then it begins to matters less how the list api looks like

[Eric Taucher]

Does this have something to do with parsing?

[Joachim Breitner]

No, I wouldn’t say so.

[Yakov Pechersky]

Maybe it's time for an explicit nonempty list as a promoted subtype and associated API?

[Joachim Breitner]

Maybe, although with head and last you might also encounter them with mixed lists, e.g. appending a non-empty to a general list.

[Joachim Breitner]

I refactored my current proof back and forth between tail and itail, and at least for me, tail works much better, so I added the equivalent head variant (with the not-nil assumption) to my file for now.

So I wonder if I should add it to the base library? If so, as head, renaming the existing function to ihead? Or some other naming convention that keeps head as it is and renames tail?

[Joachim Breitner]

Hmm, and the very next proof gets ugly (because cases doesn't work well on expressions that appear in such indices? Lack of dependent rewriting). Surprisingly tricky, all that.

[Jannis Limperg]

Try docs#tactic.interactive.cases'; it should generate equations for 'complex' indices.

[Joachim Breitner]

Ah, interesting! I’ll try it next time

[Mario Carneiro]

Joachim Breitner said:

Hmm, and the very next proof gets ugly (because cases doesn't work well on expressions that appear in such indices? Lack of dependent rewriting). Surprisingly tricky, all that.

Yes, this is why I'm not so enthusiastic to add these functions, I don't think they actually work all that well. I would use the name list.head for the option-returning one, and you can have an API to use option.get on it but most likely you just want to actually pattern match to get the name out

[Joachim Breitner]

Or maybe a subtype-based API might be useful after all

[Joachim Breitner]

You say “just pattern match”, but that doesn't work easily for last'…

Anyways, I'm tempted to side step that issue in my proof completely and use a different data structure. Probably better anyways.

[Mario Carneiro]

you can pattern match on an option-returning last

[Joachim Breitner]

Pattern matching on a complex expression (e.g. l.last') is often tedious, I find, as it tends to lose the connection to other facts about the things in the expression (e.g. l ≠ nil)