Zulip Chat Archive

Stream: mathlib4

Topic: List.head


Kevin Buzzard (Nov 30 2022 at 17:13):

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 (Nov 30 2022 at 17:15):

The Lean4 version is docs4#List.head!

Floris van Doorn (Nov 30 2022 at 17:16):

Is it?

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

Kyle Miller (Nov 30 2022 at 17:16):

Mathematically it is, but I guess not as compiled code

Floris van Doorn (Nov 30 2022 at 17:17):

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

Kyle Miller (Nov 30 2022 at 17:19):

Yes:

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

Arien Malec (Nov 30 2022 at 17:20):

Where should this get #align'd?

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

Arien Malec (Nov 30 2022 at 17:21):

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

Kevin Buzzard (Nov 30 2022 at 17:22):

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

Arien Malec (Nov 30 2022 at 17:53):

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

Kevin Buzzard (Nov 30 2022 at 18:06):

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 (Dec 01 2022 at 05:03):

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 (Dec 01 2022 at 05:03):

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 (Dec 01 2022 at 05:08):

@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.


Last updated: Dec 20 2023 at 11:08 UTC