From 8835ab46adaec34f8144af3cc64d7f2e149dd3d3 Mon Sep 17 00:00:00 2001
From: Kim Morrison <scott.morrison@gmail.com>
Date: Sun, 29 Sep 2024 15:44:14 +1000
Subject: [PATCH] feat: Array.eraseReps (#5514)

Just an `Array` version of `List.eraseReps`. These functions are for now
outside of scope for verification, so there's just a simple `example` in
the tests.
---
 src/Init/Data/Array/Basic.lean | 20 +++++++++++++++++++-
 tests/lean/run/eraseReps.lean  |  2 ++
 2 files changed, 21 insertions(+), 1 deletion(-)
 create mode 100644 tests/lean/run/eraseReps.lean

diff --git a/src/Init/Data/Array/Basic.lean b/src/Init/Data/Array/Basic.lean
index fdcf69f9c6..23101ce8fe 100644
--- a/src/Init/Data/Array/Basic.lean
+++ b/src/Init/Data/Array/Basic.lean
@@ -810,11 +810,27 @@ def split (as : Array α) (p : α → Bool) : Array α × Array α :=
   as.foldl (init := (#[], #[])) fun (as, bs) a =>
     if p a then (as.push a, bs) else (as, bs.push a)
 
-/-! ### Auxiliary functions used in metaprogramming.
+/-! ## Auxiliary functions used in metaprogramming.
 
 We do not intend to provide verification theorems for these functions.
 -/
 
+/-! ### eraseReps -/
+
+/--
+`O(|l|)`. Erase repeated adjacent elements. Keeps the first occurrence of each run.
+* `eraseReps #[1, 3, 2, 2, 2, 3, 5] = #[1, 3, 2, 3, 5]`
+-/
+def eraseReps {α} [BEq α] (as : Array α) : Array α :=
+  if h : 0 < as.size then
+    let ⟨last, r⟩ := as.foldl (init := (as[0], #[])) fun ⟨last, r⟩ a =>
+      if a == last then ⟨last, r⟩ else ⟨a, r.push last⟩
+    r.push last
+  else
+    #[]
+
+/-! ### allDiff -/
+
 private def allDiffAuxAux [BEq α] (as : Array α) (a : α) : forall (i : Nat), i < as.size → Bool
   | 0,   _ => true
   | i+1, h =>
@@ -832,6 +848,8 @@ decreasing_by simp_wf; decreasing_trivial_pre_omega
 def allDiff [BEq α] (as : Array α) : Bool :=
   allDiffAux as 0
 
+/-! ### getEvenElems -/
+
 @[inline] def getEvenElems (as : Array α) : Array α :=
   (·.2) <| as.foldl (init := (true, Array.empty)) fun (even, r) a =>
     if even then
diff --git a/tests/lean/run/eraseReps.lean b/tests/lean/run/eraseReps.lean
new file mode 100644
index 0000000000..7db028d31b
--- /dev/null
+++ b/tests/lean/run/eraseReps.lean
@@ -0,0 +1,2 @@
+example : Array.eraseReps #[1, 3, 2, 2, 2, 3, 5] = #[1, 3, 2, 3, 5] := rfl
+example : List.eraseReps   [1, 3, 2, 2, 2, 3, 5] =  [1, 3, 2, 3, 5] := rfl