any Interest on a mergeWIth on Lists ?

Stream: lean4

[Alfredo Moreira-Rosa]

Hello,

For my Dimensional analysis library, i have implemented a more advanced merge function on lists with proofs.

Proofs are for, sorted, no_duplicate, commutative, associative, membership of the resulting merge.
Is there any interest of me sharing it all ?

I have a specilization of this function, if any interest, i can generalize it for:

def mergeWith {α} (xs ys: List α) (lt: α → α → Bool) (eq: α → α → Bool) (amerge: α → α → Option α)  : List α :=
  match xs, ys with
  | [], ys => ys
  | xs, [] => xs
  | x :: xs, y :: ys =>
    if eq x y then
      match amerge x y with
      | none => mergeWith xs ys lt eq amerge
      | some z => z :: mergeWith xs ys lt eq amerge
    else if lt x y then
      x :: mergeWith xs (y :: ys) lt eq amerge
    else
      y :: mergeWith (x :: xs) ys lt eq amerge

[Aaron Liu]

Is it faster better than docs#List.merge

[Alfredo Moreira-Rosa]

no, the goal is not to have an alternative to mergeSort. It's for having an option to do something in case of an equality when merging. something the current merge function on lists don't do.

[Alfredo Moreira-Rosa]

ah, you changed your question, to merge, then it's on the same performance, since it only differs for the equality case

[Aaron Liu]

ok that's good enough for me

[Aaron Liu]

sometimes when they're equal you do want to do something else

[Aaron Liu]

do you have a monadic version?

[Alfredo Moreira-Rosa]

no monadic version.