add Problem 13

Src.lean

@@ -2,6 +2,7 @@ import Src.Problem1
 import Src.Problem10
 import Src.Problem11
 import Src.Problem12
+import Src.Problem13
 import Src.Problem14
 import Src.Problem15
 import Src.Problem2

Src/Problem13.lean

@@ -0,0 +1,45 @@
+/-
+# Problem 13
+Implement the so-called run-length encoding data compression method directly. I.e. don't explicitly create the sublists containing the duplicates, as in problem 9, but only count them. As in problem P11, simplify the result list by replacing the singleton lists `(1 X)` by `X`.
+-/
+namespace P13 --#
+
+variable {α : Type} [BEq α] [Inhabited α]
+
+inductive Data (α : Type) where
+| multiple : Nat → α → Data α
+| single : α → Data α
+deriving Repr
+
+open Data
+
+def encodeDirect (l : List α) : List (Data α) :=
+  -- sorry
+  counting l |>.map fun (n, a) =>
+    if n == 1 then
+      single a
+    else
+      multiple n a
+where
+  counting : List α → List (Nat × α)
+  | [] => []
+  | [a] => [(1, a)]
+  | a :: b :: t =>
+    if a != b then
+      (1, a) :: counting (b :: t)
+    else
+      let (n, a) := counting (b :: t) |>.head!
+      (n + 1, a) :: (counting (b :: t) |>.tail!)
+  -- sorry
+
+-- The following code is a test case and you should not change it.
+
+example : encodeDirect ['a', 'a', 'b', 'c'] =
+  [multiple 2 'a', single 'b', single 'c'] := by rfl
+
+example : encodeDirect ([] : List α) = [] := by rfl
+
+example : encodeDirect ['a', 'b', 'b', 'b', 'c', 'b', 'b'] =
+  [single 'a', multiple 3 'b', single 'c', multiple 2 'b'] := by rfl
+
+end P13 --#

md/SUMMARY.md

@@ -19,6 +19,7 @@
 
 * [11: Modified run-length encoding](./build/Problem11.md)
 * [12: Decode a run-length encoded list](./build/Problem12.md)
+* [13: Direct run-length encoding](./build/Problem13.md)
 * [14: Duplicate elements](./build/Problem14.md)
 * [15: Replicate elements K times](./build/Problem15.md)
 * [20: Remove the K'th element](./build/Problem20.md)