A competition programming problem about permuting a permutation to be unimodal

Problem statement

Notes: Unavailable.

Source: NWERC 2025 Problem G, see https://2025.nwerc.eu/problem-set.pdf

Informal solution: See https://2025.nwerc.eu/solutions.pdf for a sketch of the correctness, which goes in two steps: construct a quadratic-time dynamic programming solution, then efficiently evaluate that in O(n log n). The hard part is showing the correspondence between LISs of prefixes of the constructed sequence and values of the DP.

theorem declaration uses `sorry`minRearrange_correct {arr : Array Nat} :
    arr.Perm (1...=arr.size).toArray →
      (∃ (x : Array Nat) (hx : x.Perm (1...=arr.size).toArray), LeanEval.ProgramVerification.Unimodal x ∧ LeanEval.ProgramVerification.differences (Vector.mk x (byarr:Array Natx:Array Nathx:x.Perm (1...=arr.size).toArray⊢ x.size = arr.size simpa using hx.size_eqAll goals completed! 🐙)) arr.toVector = LeanEval.ProgramVerification.minRearrange arr) ∧
      (∀ (x : Array Nat) (hx : x.Perm (1...=arr.size).toArray), LeanEval.ProgramVerification.Unimodal x → LeanEval.ProgramVerification.minRearrange arr ≤ LeanEval.ProgramVerification.differences (Vector.mk x (byarr:Array Natx:Array Nathx:x.Perm (1...=arr.size).toArray⊢ x.size = arr.size simpa using hx.size_eqAll goals completed! 🐙)) arr.toVector) := byarr:Array Nat⊢ arr.Perm (1...=arr.size).toArray →
  (∃ x hx, Unimodal x ∧ differences (Vector.mk x ⋯) arr.toVector = minRearrange arr) ∧
    ∀ (x : Array Nat) (hx : x.Perm (1...=arr.size).toArray),
      Unimodal x → minRearrange arr ≤ differences (Vector.mk x ⋯) arr.toVector
  sorryAll goals completed! 🐙