List.union

Stream: mathlib4

[Johan Commelin]

@[simp] theorem nil_union (l : List α) : nil.union l = l := by simp [List.union, foldr]

@[simp] theorem cons_union (a : α) (l₁ l₂ : List α) :
    (a :: l₁).union l₂ = (l₁.union l₂).insert a := by simp [List.union, foldr]

Why do these not use union notation? Now they are basically unusable.

[Eric Wieser]

This is a question about mathlib3, right? Looks like docs4#List.cons_union used notation in docs#list.cons_union. Is this a mathport bug?

[Johan Commelin]

It looks like a Std bug.

[Johan Commelin]

This is in Std/Data/List/Lemmas and it's not using any notation.

[Johan Commelin]

I'm currently just passing the instance to simp. I don't think mathlib uses it too much anyway.

[Mario Carneiro]

I'm not sure I would call it a bug, but we need versions of these theorems that use the notation as well. I'm not even sure the notation is available in that file

[Eric Wieser]

I'd argue we don't need versions that use the .union spelling, as long as we have a lemma to refold union to the notation

[Mario Carneiro]

I mean the notation might not be imported, or even if it is it might not be desirable. This is std we're talking about, programmers won't reach for the funny cup operator when they can call list.union

[Eric Wieser]

The notation docs4#List.instUnionList is also in Std

[Mario Carneiro]

it is, but not all of Std imports every other part

[Mario Carneiro]

I don't think it would be a huge deal to have it imported if it isn't already though

[Johan Commelin]

@Mario Carneiro I personally don't really care about what Std looks like. But we'll have a naming clash if we want both versions.

[Johan Commelin]

Why do we want ∪ notation for List?

[Mario Carneiro]

'cause it's called union I guess?

[Mario Carneiro]

I'm neutral on the notation. There are a lot of weird lemmas about list.union that don't really make sense if you think about it like a set union

[Mario Carneiro]

like the fact that the left list is a prefix and the right list is a sublist subperm

[Mario Carneiro]

I'm okay with eric's suggestion as well, of having a simp lemma to fold the notation and state all the lemmas with the notation

[Eric Wieser]

I'm also fine with removing the notation; I just think having two ways to spell exactly the same thing is a disaster when building a library of theorems.

[Johan Commelin]

I vote for removing the notation. Unless Std wants to use the notation everywhere.

[James Gallicchio]

I would never use this notation in programming-stuff. too confusing.

[Chris Hughes]

We have the same problem for List.insert

[Johan Commelin]

Just simp only [instInsertList]

[Johan Commelin]

After that, everything works.

[Chris Hughes]

But which is the notation we should be using?

[Yaël Dillies]

docs4#HasInsert.Insert ?

[Yaël Dillies]

Hmm, that doesn't exist

[Chris Hughes]

It's docs4#Insert.insert

[Chris Hughes]

docs4#Insert

[Chris Hughes]

Why did we even introduce has_insert.insert? It's a notation typeclass for something we don't even have notation for

[Yaël Dillies]

Yes it is. The notation is {a, b, c}

[Chris Hughes]

So we need to refactor Std to get rid of all mention of List.insert?

[Johan Commelin]

I think it's not clear whether Std wants to use notation for Lists or avoid it. But it shouldn't try to do both.

[Johan Commelin]

Is this blocking the port of Data.List.Perm in a nasty way? Or can you work around it?

[Mario Carneiro]

Using set notation for lists seems misleading at best

[Mario Carneiro]

although I think it won't activate unless you use a bunch of inserts on empty, while the simp normal form for the empty list is of course []

[Mario Carneiro]

so in the case of insert I'm inclined to rewrite from Insert.insert to List.insert

[Chris Hughes]

What about just deleting the Insert instance for list then?

[Mario Carneiro]

or that

[Mario Carneiro]

maybe it would be best to try these refactors out in mathlib3 first though

[Chris Hughes]

That's different from the mathlib3 convention where we use has_insert.insert everywhere for lists

[Johan Commelin]

That's going to be another speedbump for the port.

[Johan Commelin]

I would rather just simp [instInsertList] and continue.

[Johan Commelin]

Once Std figures out which of the two options it prefers, we can adjust mathlib

[Mario Carneiro]

Is there a need to make an immediate ruling? I think you can add simp lemmas to work around any impedance mismatch if you want to have a particular behavior for the port

[Johan Commelin]

Right, that's basically what I'm suggesting, I think

[Chris Hughes]

For the port we'll use List.insert because that's what the lemmas in Std already use. I'll make a PR changing everything I can find

[Chris Hughes]

https://github.com/leanprover-community/mathlib4/pull/1487

[Eric Wieser]

Chris Hughes said:

That's different from the mathlib3 convention where we use has_insert.insert everywhere for lists

Do you have an example? I've never seen insert used on lists before.

[Eric Wieser]

Seems pretty random; docs#list.suffix_insert vs docs#list.sublist_insert are right next to each other and use different choices.

[Eric Wieser]

It looks to me like this is entirely accidental, and the author didn't realize that list.insert was protected so insert x l and l.insert x are not syntactically identical