Rearranging a permutation into unimodal order

DefinitionUnimodal arrays#✓fully proved

An array \(a\) of natural numbers is unimodal if it is the concatenation of a strictly increasing array \(b\) followed by a strictly decreasing array \(b'\), where either part may be empty.

def Unimodal (arr : Array Nat) : Prop :=
  ∃ b b', arr = b ++ b' ∧ b.toList.Pairwise (· < ·) ∧ b'.toList.Pairwise (· > ·)

Used by 1

Used byCorrectness of the unimodal rearrangement algorithm

DefinitionNumber of differing positions#✓fully proved

For two vectors \(a, b \in \mathbb{N}^n\), this is the number of indices \(i < n\) with \(a_i \neq b_i\), that is, the Hamming distance between \(a\) and \(b\).

def differences {n : Nat} (a b : Vector Nat n) : Nat :=
  (List.finRange n).filter (fun i => a[i] ≠ b[i]) |>.length

Used by 1

Used byCorrectness of the unimodal rearrangement algorithm

TheoremCorrectness of the unimodal rearrangement algorithm#●ready to prove

Let \(a\) be an array of length \(n\) that is a permutation of \(1, \dots, n\), and let \(m(a)\) be the value that the program \(\mathrm{minRearrange}\) computes on \(a\). Then some unimodal permutation \(x\) of \(1, \dots, n\) differs from \(a\) in exactly \(m(a)\) positions, and every unimodal permutation of \(1, \dots, n\) differs from \(a\) in at least \(m(a)\) positions. So \(m(a)\) is the minimum number of positions in which \(a\) differs from a unimodal permutation of \(1, \dots, n\).

public theorem_wanted minRearrange_correct {arr : Array Nat} :
    arr.Perm (1...=arr.size).toArray →
      (∃ (x : Array Nat) (hx : x.Perm (1...=arr.size).toArray), Unimodal x ∧ differences (Vector.mk x (by simpa using hx.size_eq)) arr.toVector = minRearrange arr) ∧
      (∀ (x : Array Nat) (hx : x.Perm (1...=arr.size).toArray), Unimodal x → minRearrange arr ≤ differences (Vector.mk x (by simpa using hx.size_eq)) arr.toVector)

Sources

• NWERC 2025 Problem G, see https://2025.nwerc.eu/problem-set.pdf. Problem permute_to_unimodal of the lean-eval benchmark.

Uses 2

Statement usesUnimodal arrays · Number of differing positions

2 fully proved1 ready to prove

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.