From acccd364a986165877caf55601962c0c6bcdba7d Mon Sep 17 00:00:00 2001
From: Julia Markus Himmel <2065352+TwoFX@users.noreply.github.com>
Date: Wed, 6 May 2026 08:04:41 +0200
Subject: [PATCH 1/3] feat: a competition programming problem about permuting a
 permutation to be unimodal

---
 .../PermuteToUnimodal.lean                    | 74 +++++++++++++++++++
 manifests/problems.toml                       | 10 +++
 2 files changed, 84 insertions(+)
 create mode 100644 LeanEval/ProgramVerification/PermuteToUnimodal.lean

diff --git a/LeanEval/ProgramVerification/PermuteToUnimodal.lean b/LeanEval/ProgramVerification/PermuteToUnimodal.lean
new file mode 100644
index 0000000..91a2d15
--- /dev/null
+++ b/LeanEval/ProgramVerification/PermuteToUnimodal.lean
@@ -0,0 +1,74 @@
+import EvalTools.Markers
+
+namespace LeanEval
+namespace ProgramVerification
+
+/-!
+Given an array `arr` which is a permutation of the numbers from `1` to `arr.size`,
+`minRearrange` computes the size of the smallest subset of indices within the array
+that may be permuted such that the array becomes first increasing and then decreasing.
+For example, `minRearrange #[1, 6, 4, 3, 2, 5] = 2` since we can swap the first and
+the last element to achieve the desired property.
+
+The given efficient implementation computes the answer in `O(n log n)`.
+
+Examples:
+* `minRearrange #[] = 0`
+* `minRearrange #[1, 6, 4, 3, 2, 5] = 2`
+* `minRearrange #[4, 3, 2, 1, 5] = 4`
+* `minRearrange #[1, 2, 4, 3] = 0`
+* `minRearrange #[1, 2, 7, 4, 5, 6, 3, 8, 9, 10] = 2`
+-/
+
+def minRearrange (arr : Array Nat) : Nat :=
+  let n := arr.size
+  let v :=
+    (arr.zipIdx.filter (fun (a, i) => i + 1 ≤ a)).map (fun (a, i) => (2 * i + 1, 2 * (a - i - 1))) ++
+    (arr.zipIdx.filter (fun (a, i) => n ≤ a + i)).map (fun (a, i) => (2 * (a + i - n), 2 * (n - i) - 1))
+  let vv := (v.toList.mergeSort (le := fun a b => a = b ∨ Prod.Lex (· < ·) (· < ·) a b)).toArray
+  n - lis (vv.map (·.2))
+where
+  lis (arr : Array Nat) : Nat :=
+    if h : arr = #[] then
+      0
+    else
+      let dp := Array.replicate arr.size (arr.max h + 1)
+      loop arr 0 0 dp (by grind)
+  loop (arr : Array Nat) (ans i : Nat) (dp : Array Nat) (hi : i ≤ arr.size) : Nat :=
+    if hi' : i = arr.size then
+      ans
+    else
+      let pos := upperBound arr[i] dp
+      loop arr (max ans (pos + 1)) (i + 1) (dp.set! pos (arr[i])) (by grind)
+  upperBound (needle : Nat) (arr : Array Nat) : Nat :=
+    go needle arr 0 arr.size
+  go (needle : Nat) (arr : Array Nat) (lo hi : Nat) (hhi : hi ≤ arr.size := by omega) : Nat :=
+    if h : lo < hi then
+      let mid := lo + (hi - lo) / 2
+      if arr[mid] ≤ needle then
+        go needle arr (mid + 1) hi
+      else
+        go needle arr lo mid
+    else lo
+
+/--
+Property stating that the array can be decomposed into a strictly increasing and a strictly
+decreasing part.
+-/
+def Unimodal (arr : Array Nat) : Prop :=
+  ∃ b b', arr = b ++ b' ∧ b.toList.Pairwise (· < ·) ∧ b'.toList.Pairwise (· > ·)
+
+/--
+The number of indices at which the two given vectors differ
+-/
+def differences {n : Nat} (a b : Vector Nat n) : Nat :=
+  (List.finRange n).filter (fun i => a[i] ≠ b[i]) |>.length
+
+@[eval_problem]
+theorem 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) := sorry
+
+end ProgramVerification
+end LeanEval
diff --git a/manifests/problems.toml b/manifests/problems.toml
index d0d66c4..f8a39bf 100644
--- a/manifests/problems.toml
+++ b/manifests/problems.toml
@@ -645,3 +645,13 @@ module = "LeanEval.NumberTheory.NeukirchUchida"
 holes = ["neukirch_uchida"]
 submitter = "Junyan Xu"
 source = "Jürgen Neukirch, Alexander Schmidt, Kay Wingberg. *Cohomology of Number Fields*, Theorem 12.2.1."
+
+[[problem]]
+id = "permute_to_unimodal"
+title = "A competition programming problem about permuting a permutation to be unimodal"
+test = false
+module = "LeanEval.ProgramVerification.PermuteToUnimodal"
+holes = ["minRearrange_correct"]
+submitter = "Julia M. Himmel"
+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."
\ No newline at end of file

From ae2c1d971c76aeed5219d69a7f57da37b36aee58 Mon Sep 17 00:00:00 2001
From: Julia Markus Himmel <2065352+TwoFX@users.noreply.github.com>
Date: Wed, 6 May 2026 08:46:40 +0200
Subject: [PATCH 2/3] Add a docstring to `minRearrange_correct`

---
 LeanEval/ProgramVerification/PermuteToUnimodal.lean | 4 ++++
 1 file changed, 4 insertions(+)

diff --git a/LeanEval/ProgramVerification/PermuteToUnimodal.lean b/LeanEval/ProgramVerification/PermuteToUnimodal.lean
index 91a2d15..a0378a7 100644
--- a/LeanEval/ProgramVerification/PermuteToUnimodal.lean
+++ b/LeanEval/ProgramVerification/PermuteToUnimodal.lean
@@ -64,6 +64,10 @@ The number of indices at which the two given vectors differ
 def differences {n : Nat} (a b : Vector Nat n) : Nat :=
   (List.finRange n).filter (fun i => a[i] ≠ b[i]) |>.length
 
+/--
+`minRearrange` correctly computes the smallest number of indices that need to be permuted in order to
+turn `arr` into a unimodal permutation.
+-/
 @[eval_problem]
 theorem minRearrange_correct {arr : Array Nat} :
     arr.Perm (1...=arr.size).toArray →

From 44edb0c3ebd6e02fd4a8424b7658d4dc25617cfb Mon Sep 17 00:00:00 2001
From: Julia Markus Himmel <2065352+TwoFX@users.noreply.github.com>
Date: Wed, 6 May 2026 09:24:05 +0200
Subject: [PATCH 3/3] Use by sorry

---
 LeanEval/ProgramVerification/PermuteToUnimodal.lean | 3 ++-
 1 file changed, 2 insertions(+), 1 deletion(-)

diff --git a/LeanEval/ProgramVerification/PermuteToUnimodal.lean b/LeanEval/ProgramVerification/PermuteToUnimodal.lean
index a0378a7..49d06b3 100644
--- a/LeanEval/ProgramVerification/PermuteToUnimodal.lean
+++ b/LeanEval/ProgramVerification/PermuteToUnimodal.lean
@@ -72,7 +72,8 @@ turn `arr` into a unimodal permutation.
 theorem 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) := sorry
+      (∀ (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) := by
+  sorry
 
 end ProgramVerification
 end LeanEval