Day 3

1 files changed, 25 insertions, 1 deletions

diff --git a/Common/List.lean b/Common/List.lean
index 4076c87..1a76c3e 100644
--- a/Common/List.lean
+++ b/Common/List.lean
@@ -1,3 +1,5 @@
+namespace List
+
 theorem listFilterSmallerOrEqualList (l : List α) (p : α → Bool) : l.length ≥ (l.filter p).length := by
   induction l with
   | nil => simp[List.filter]
@@ -10,7 +12,6 @@ theorem listFilterSmallerOrEqualList (l : List α) (p : α → Bool) : l.length
       assumption
     | true => simp_arith[hi]
 
-
 def quicksort {α : Type} [Ord α] : List α → List α
 | [] => []
 | a :: as =>
@@ -22,3 +23,26 @@ def quicksort {α : Type} [Ord α] : List α → List α
   let biggers := as.filter largerEqualPred
   (quicksort smallers) ++ [a] ++ (quicksort biggers)
   termination_by quicksort l => l.length
+
+/-- Maps a List to another list, but keeps state.
+    The output list is a list of the state, and **has** the initial state
+    prepended!
+ -/
+def scan {α σ : Type} (step : σ → α → σ) (init : σ): List α → List σ
+| [] => [init]
+| a :: as =>
+  let next := step init a
+  init :: scan step next as
+
+/-- Removes repeated entries. [1,2,2,1] becomes [1,2,1]-/
+def dedup {α : Type} [BEq α] (input : List α) : List α :=
+  let rec helper : List α → α → List α := λ
+  | [], _ => []
+  | a :: as, b =>
+    if a == b then
+      helper as a
+    else
+      a :: helper as a
+  match input with
+  | [] => []
+  | a :: as => a :: helper as a