Dealing with empty lists

Stream: new members

[Nam]

Hi folks, how do you often deal with empty lists. For example, how do you write List.min?

[Kevin Buzzard]

docs#list.min

[Kevin Buzzard]

That function doesn't exist. What do you mean by it?

[Nam]

Do you use subtype to restrict a list to non-empty, or use Maybe in the result?

[Kevin Buzzard]

Perhaps I can second guess your question. docs#list.nth exists, and has type list α → ℕ → option α, so it returns the n'th element of the list if it exists and none otherwise. Is this what you're asking?

[Nam]

Ah, yes, that function does not exist. I meant to write a function that returns the minimum value from a List

[Kevin Buzzard]

On the other hand docs#list.head has type list α → α but also the assumption [inhabited α] which means it can return the "default element" of alpha if the list is empty.

[Kevin Buzzard]

The real answer to your question is probably "yes we can do all of those things and indeed we do do all of those things".

[Kevin Buzzard]

For example as well as docs#list.nth we have docs#list.nth_le which asks for a proof and in return doesn't return an option.

[Nam]

Oh, interesting. Thank you Kevin. Which way do you think is used more often?

[Kevin Buzzard]

I'm sure that this will depend on what you want to do.

[Nam]

Is there a way to tell Lean that "trust me, my lists are non-empty"?

[Junyan Xu]

You can take a proof as an argument as in docs#finset.min'

[Junyan Xu]

docs#finset.min instead returns with_top which is essentially option.

[Nam]

Yes, I can provide Lean with a proof (or just admit such cases). I guess what I am wondering is if there is a way that I do not need to do that, that Lean does not need to check for such cases?

[Junyan Xu]

I guess no unless you want Lean to be able to verify a proof of false :)

[Kevin Buzzard]

You can't just promise that your list is nonempty, however you can demand that your function takes as input a proof that the list is nonempty, a bit like nth_le above.

[Kevin Buzzard]

This isn't Haskell, this is a theorem prover, and it's really important that you can't prove false things by abusing a function.

[Ruizhe Wan]

This is a question about the Natural number game (Sorry I don't know if this is the right place to post it but I could not find otherwhere to ask, and I think some people here shall be familiar with the game): in trying to use the add_left_cancel theorem to get from h2 to the goal, it says that the type of h2 should be mynat instead of Prop, which I think is problematic? I have also tried to just repeat again the proofs of all the theorems I need, but at the end I could not use induction on (a * d), so this doesn't work either, does anyone have some hint of it?
SharedScreenshot.jpg

[Kevin Buzzard]

This is the right stream, but this is a thread about empty lists. You should make a new topic, or find an old natural number game topic, and I'll answer your question there.

[Ruizhe Wan]

ok

[Matt Diamond]

@Nam I don't think anyone mentioned this, but we have docs#list.minimum... the caveat is that it may return ⊤ (which is represented by option.none) if the list is empty

[Matt Diamond]

If you want to specify a default value to handle the case of an empty list, you can use docs#with_top.untop' with the resulting value

[Matt Diamond]

so in theory you could do myList.minimum.untop' 0 and you would get the minimum back or 0 if the list is empty

[Nam]

How do I force the \a of an empty List \a?

[Nam]

[] can be any List a, or List b. If the function does not have anything else that can bind or resolve a or b, how can I help Lean know what a or b is from an empty list []?

[Junyan Xu]

([] : list \a)

[Nam]

For example, #check List.concat [] [] cannot resolve the type parameter

[Nam]

oh, let me try. thank you.

[Nam]

ah, yes, that works! thanks again.