Array.partition vs Array.split

Stream: lean4

[Marcus Rossel]

What's the difference between Array.partition and Array.split?

@[inline]
def partition (p : α → Bool) (as : Array α) : Array α × Array α := Id.run do
  let mut bs := #[]
  let mut cs := #[]
  for a in as do
    if p a then
      bs := bs.push a
    else
      cs := cs.push a
  return (bs, cs)

def split (as : Array α) (p : α → Bool) : Array α × Array α :=
  as.foldl (init := (#[], #[])) fun (as, bs) a =>
    if p a then (as.push a, bs) else (as, bs.push a)

To me they look like they're doing the same thing.

[Mario Carneiro]

They are the same. There are several instances of this in the core library; I would prefer the name Array.partition to match List.partition

[Mario Carneiro]

(although the split implementation is easier to prove properties about)

[Marcus Rossel]

Mario Carneiro said:

There are several instances of this in the core library

Why is this? Is partition more efficient than split?

[Mario Carneiro]

no, I think it's just oversight

[Mario Carneiro]

I fixed a few examples of duplication yesterday

[Mario Carneiro]

I would expect that split is more efficient than partition because it doesn't have the overhead of the ForInStep stuff

[Mario Carneiro]

but I doubt the difference is noticeable

[Mario Carneiro]

the more noticeable thing is when those combinators show up in reasoning