def merge_by_perm

bend-mathlib@0.8.1.0 · perm.bend:147

import Base
import bendlib-kernel-list@1.0.0.0/list.bend as K

147# Merging permutes the concatenation.
148def merge_by_perm(~A: Data, ~le: A -> A -> Bool, +xs: List<&2, A>, +ys: List<&2, A>) -> K.perm(A, List.append(&2, A, xs, ys), merge_by(~A, ~le, xs, ys)):
149  match xs ys:
150    case Nil{} _:
151      perm_refl(A, ys)
152    case +x <> +xt Nil{}:
153      perm_cons(A, x, List.append(&2, A, xt, Nil{}), xt, perm_append_nil(A, xt))
154    case +x <> +xt +y <> +yt:
155      internal_merge_pick(A, le(x, y), x, xt, y, yt, merge_by(~A, ~le, xt, y <> yt), merge_by(~A, ~le, x <> xt, yt), merge_by_perm(~A, ~le, xt, y <> yt), merge_by_perm(~A, ~le, x <> xt, yt))