feat(Data): interleaving lists

[YaelDillies]

Define interleaving of lists, both as an operation and as a relation.

This will be used to define interleaving polynomials, which in turn are a central concept in the line of work that earned June Huh his 2022 Fields medal.

Zulip

---

Originally PRed as leanprover-community/mathlib4#39870 but moved to batteries at the request of @ocfnash.

There are two pain points compared to the mathlib version:

1. Batteries does not have the @[mk_iff] attribute, meaning that I had to write interleaves_iff by hand.
2. Batteries does not have the existsAndEq simproc, meaning two subproofs became annoying to write.

Both of these depend minimally on mathlib, so we could consider upstreaming them.

[wrenna-robson]

"Interleaves two lists l₁ and l₂, starting with an element of l₂."

Obviously this choice is somewhat arbitrary. But I have to say this is counter to what I would expect - intuitively I expect to start with l₁. Can you say more about this choice?

[wrenna-robson]

I would support both the upstreams you mention by the way - indeed, this is a great reason to do them! Would you be willing to prepare them as PRs?

[wrenna-robson]

https://www.symmetricfunctions.com/realRootedInterlacing.htm

Is this a good source for the concept you're referring to?

[YaelDillies]

"Interleaves two lists l₁ and l₂, starting with an element of l₂."

Obviously this choice is somewhat arbitrary. But I have to say this is counter to what I would expect - intuitively I expect to start with l₁. Can you say more about this choice?

This is the convention that the literature around real-rooted polynomials uses (assuming the lists are sorted decreasingly). This is motivated by the idea that l₂ should be the longer list.

https://www.symmetricfunctions.com/realRootedInterlacing.htm

Is this a good source for the concept you're referring to?

Certainly a great reference! This is the personal website of @PerAlexandersson, whose repo I am upstreaming this from.

[YaelDillies]

I have opened #1854 for @[mk_iff]. existsAndEq is more complicated to upstream because it depends on Qq. Are you happy for batteries to depend on Qq?

[wrenna-robson]

It looks a bit like what you have as "interleave" is called "interlace" there, unless I'm mistaken.

I think for batteries the interleaving list operation should not be defined with reference to this theory in particular. I would strongly prefer, I think, a definition like this:

def interleave : List α → List α → List α
  | [], [] => []
  | [], b :: l₂ => b :: l₂
  | a :: l₁, [] => a :: l₁
  | a :: l₁, b :: l₂ => a :: b :: interleave l₁ l₂

Now, I can also see the argument for:

def interleave : List α → List α → List α
| [], [] => []
| [], b :: l₂ => []
| a :: l₁, [] => []
| a :: l₁, b :: l₂ => a :: b :: interleave l₁ l₂

I think this might be more similar to your definition, though you seem to want to take one element in the cons, nil (or nil, cons using your argument order) case.

def interleave : List α → List α → List α
  | [], [] => []
  | [], b :: l₂ => []
  | a :: l₁, [] => [a]
  | a :: l₁, b :: l₂ => a :: b :: interleave l₁ l₂

This last definition is the same as yours with the argument order reversed - but it has the advantage that it doesn't need a termination hint.

I might characterise these as:

"take from the first list, then take from the second list, then repeat - if you ever can't take from one, return the other"
"take from the first list, then take from the second list then repeat - if you can't take from both, stop"
"take from the first list, then take from the second list then repeat - always take from the first but stop if you can't take from the second"

Alternatively I can see the argument for your argument order if "l₁.interleave l₂" is taken to mean "interleave l₁ into l₂, a la intersperse. I really don't like your behaviour of taking just the one element from one list if the other is empty - to me that produces an unsatisfying state of affairs.

So: at minimum, change your definition to

def interleave : List α → List α → List α
  | _, [] => []
  | [], a :: _ => [a]
  | b :: l₁, a :: l₂ => a :: b :: interleave l₁ l₂

interleave_cons then becomes a theorem but one fairly easily proved.

I think there's not a common consensus which one of these is right but I don't think yours is the one most people would intuitively reach for.

[YaelDillies]

Do you understand why the build fails? It looks like a pre-existing issue surfacing now because I modified the file Batteries.Data.List.

[wrenna-robson]

@YaelDillies Ah - the Qq dependency will need some discussion I think.

[wrenna-robson]

Do you understand why the build fails? It looks like a pre-existing issue surfacing now because I modified the file Batteries.Data.List.

Yes - you have changed the first line of it, removing "-- deprecated_module: ignore", which causes that warning to no longer be ignored. But that was deliberate on the part of the PR that wrote that line: reinstate it and the warning will not cause the build to fail.

[mathlib-nightly-testing]

Mathlib CI status (docs):

• 💥 Mathlib branch batteries-pr-testing-1853 build failed against this PR. (2026-06-15 16:04:33) View Log

[YaelDillies]

It looks a bit like what you have as "interleave" is called "interlace" there, unless I'm mistaken.

I am sitting with @PerAlexandersson right now and he confirms that the naming in the literature is a mess. Different experts in the area use both names for different things, and even the same expert will not use the two names consistently. We get to set a consistent naming convention here.

[YaelDillies]

I can see the argument for your argument order if "l₁.interleave l₂" is taken to mean "interleave l₁ into l₂, a la intersperse.

Yes, this is indeed how the name is supposed to be read.

I really don't like your behaviour of taking just the one element from one list if the other is empty - to me that produces an unsatisfying state of affairs.

I do not care what l.interleave l' is if l'.length is neither l.length nor l.length + 1 . To me, this is junk. All I want is the characterisation of Interleaves. It is however very important that [].interleave [a] = [a], else there is no easy way to state my characterisation.

[wrenna-robson]

I can see the argument for your argument order if "l₁.interleave l₂" is taken to mean "interleave l₁ into l₂, a la intersperse.

Yes, this is indeed how the name is supposed to be read.

I really don't like your behaviour of taking just the one element from one list if the other is empty - to me that produces an unsatisfying state of affairs.

I do not care what l.interleave l' is if l'.length is neither l.length nor l.length + 1 . To me, this is junk. All I want is the characterisation of Interleaves. It is however very important that [].interleave [a] = [a], else there is no easy way to state my characterisation.

Understood. I think the examples of intersperse/intercalate support your argument order. This suggests to me the following definition:

def interleave : List α → List α → List α
  | [], [] => []
  | [], b :: l₂ => b :: l₂
  | a :: l₁, [] => a :: l₁
  | a :: l₁, b :: l₂ => b :: a :: interleave l₁ l₂

I think this has the behaviour that you want while I think giving the more sensible outputs in your "junk values" range. What do you think?

[PerAlexandersson]

I personally want to define interlacing so that Theorem 7.2 in This book chapter is true. The empty list should interlace lists of length 0 and 1. I agree that the definition is not totally intuitive, unless you have this background.

[wrenna-robson]

That makes sense to me. I just want to characterise interlacing in a way that fits your usage but which is also suitable for wider consumers.

[PerAlexandersson]

@wrenna-robson Yes, of course. I discussed with @YaelDillies about this a bit. So, Wagner defines two properties he calls interleaves and alternates, see my references. This is essentially splitting into two cases: both list have same length, and one list has one more element compared to the other. These two separate concepts could be useful, but for questions about polynomials with only real roots, the 'either-or' is a useful concept as well.

Now, the literature here is very inconsistent and interlaces and interleaves are somewhat synonyms, but for some authors they mean slightly different things.

The way I'd implement it, would be to have three named concepts:

• Lists of same length: a<b<a<b<a<b<a<b
• Lists where the 'largest' has one more element: b<a<b<a<b<a<b<a<b
• Either of the above (as interleave above is supposed to represent).

The first two concepts are natural from computer-science perspective, while the third is natural in the world of real-rooted polynomials.

All three concepts are useful, its only the naming that's the issue IMHO.
Riffle, alternate, interlace, interleave, intermingle, intertwine, braid, lace (this is taken), entwine?

[wrenna-robson]

Well, interleave above should, ideally, create a list which is the interleaving of two lists. The predicate should also exist (or instead of?)

[mathlib-nightly-testing]

Mathlib CI status (docs):

• ❌ Mathlib branch batteries-pr-testing-1853 built against this PR, but the archive failed. (2026-06-17 17:35:17) View Log

[YaelDillies]

The operation is useful for the characterisation and also to show that interleaving lists are sorted

[mathlib-nightly-testing]

Mathlib CI status (docs):

• ❌ Mathlib branch batteries-pr-testing-1853 built against this PR, but the archive failed. (2026-06-18 11:28:55) View Log

[wrenna-robson]

After discussion with @fgdorais, we'd quite like you to take a discussion of "interleave" to Zulip - we would like to understand what other consumers of this function might want. I can see various options being sensible.

[YaelDillies]

See https://leanprover.zulipchat.com/#narrow/channel/113488-general/topic/Interleaving.20lists/with/604506493

[eric-wieser]

I would have expected it to start with the first list!

[mathlib-nightly-testing]

Mathlib CI status (docs):

• ❌ Mathlib branch batteries-pr-testing-1853 built against this PR, but the archive failed. (2026-06-18 14:36:07) View Log