List.head

Stream: mathlib4

[Kevin Buzzard]

List.head in Lean 4 is not list.head in Lean 3, because List.head in Lean 4 demands that the list is nonempty, and list.head in Lean 3 demands that the base type is inhabited. In Mathlib.Init.Align we see #align list.head List.headₓ but I can't find the Lean 4 declaration List.headₓ and suspect it's not there. Should we be making the Lean 4 analogue of list.head and if so, should it be called List.headₓ or is that a silly name? If we're making it, where does it go?

[Kyle Miller]

The Lean4 version is docs4#List.head!

[Floris van Doorn]

Is it?

def head! [Inhabited α] : List α → α
  | []   => panic! "empty list"
  | a::_ => a

[Kyle Miller]

Mathematically it is, but I guess not as compiled code

[Floris van Doorn]

Can you prove in Lean 4 that [].head! = default _?

[Kyle Miller]

Yes:

example [Inhabited α] : ([] : List α).head! = default := rfl

[Arien Malec]

Where should this get #align'd?

Happy to do in the Data.List.Defs I'm working on...

[Arien Malec]

But seems like the align above is incorrect and should be #align'd there...

[Kevin Buzzard]

My understanding is that everything in Std or core gets aligned in Mathlib.Init.Align

[Arien Malec]

Hmm. so maybe I need to look at Data.List.Defs to see if the aligns need to move there....

[Kevin Buzzard]

For stuff which is defined in core/std in lean 4 but was defined in data.list.defs in Lean 3 (i.e. stuff where the declaration and the #align is commented out and replaced with a #print) I think it's fine to just uncomment the #align and leave it in mathlib4. Files in mathlib which use those declarations are going to be importing data.list.defs so they'll see the #align.

[Mario Carneiro]

list.head has not been aligned to a definition yet. My naming convention recommendation is List.headI to mean "use default in the bad case"

[Mario Carneiro]

I don't think we should align to head! because this could cause panics in code that was intending to use the default value on purpose

[Mario Carneiro]

@Kevin Buzzard said:

My understanding is that everything in Std or core gets aligned in Mathlib.Init.Align

That's not correct. The location of an #align depends on where the lean 3 file that makes the original declaration is located, not the lean 4 replacement. If it is in mathlib, it should go in the same-named mathlib4 file, and if it is in lean 3 init it should go in the same-named Mathlib.Init file. (If it is in lean 3 core but not in init, it should go in the same place as a mathlib file with the same name would.) However, if a Mathlib.Init file is nothing but #align declarations, then the contents are instead placed in Mathlib.Init.Align.