Lean4
/-- `reorderUsing toReorder instructions` produces a reordering of `toReorder : List α`,
following the requirements imposed by `instructions : List (α × Bool)`.
These are the requirements:
* elements of `toReorder` that appear with `true` in `instructions` appear at the
*beginning* of the reordered list, in the order in which they appear in `instructions`;
* similarly, elements of `toReorder` that appear with `false` in `instructions` appear at the
*end* of the reordered list, in the order in which they appear in `instructions`;
* finally, elements of `toReorder` that do not appear in `instructions` appear "in the middle"
with the order that they had in `toReorder`.
For example,
* `reorderUsing [0, 1, 2] [(0, false)] = [1, 2, 0]`,
* `reorderUsing [0, 1, 2] [(1, true)] = [1, 0, 2]`,
* `reorderUsing [0, 1, 2] [(1, true), (0, false)] = [1, 2, 0]`.
-/
def reorderUsing (toReorder : List α) (instructions : List (α × Bool)) : List α :=
let uInstructions :=
let (as, as?) := instructions.unzip
(uniquify as).zip as?
let uToReorder := (uniquify toReorder).toArray
let reorder :=
uToReorder.qsort fun x y =>
match uInstructions.find? (Prod.fst · == x), uInstructions.find? (Prod.fst · == y) with
| none, none => (uToReorder.idxOf? x).get! ≤ (uToReorder.idxOf? y).get!
| _, _ => weight uInstructions x ≤ weight uInstructions y
(reorder.map Prod.fst).toList
