Merge pull request #9 from lean-ja/Q14,Q15

Q14,Q15

Src.lean

@@ -1,5 +1,7 @@
 import Src.Problem1
 import Src.Problem10
+import Src.Problem14
+import Src.Problem15
 import Src.Problem2
 import Src.Problem3
 import Src.Problem31

Src/Problem14.lean

@@ -0,0 +1,22 @@
+/-
+  # Problem 14
+  Duplicate the elements of a list.
+-/
+
+variable {α : Type}
+
+def dupli (l : List α) : List α :=
+  -- sorry
+  match l with
+  | [] => []
+  | a :: b => a :: a :: dupli b
+  -- sorry
+
+-- The following code is a test case and you should not change it.
+
+example : dupli [1, 2, 3] = [1, 1, 2, 2, 3, 3] := by rfl
+
+example : dupli ([] : List α) = [] := by rfl
+
+example : dupli ['a', 'b', 'c', 'c', 'd']
+  = ['a', 'a', 'b', 'b', 'c', 'c', 'c', 'c', 'd', 'd'] := by rfl

Src/Problem15.lean

@@ -0,0 +1,29 @@
+/-
+  # Problem 15
+  Replicate the elements of a list a given number of times.
+-/
+
+variable {α : Type}
+
+def repli (l : List α) (n : Nat) : List α :=
+  -- sorry
+  match l with
+  | [] => []
+  | a :: b => (solorepl a n) ++ repli b n
+  where solorepl (x : α) (n : Nat) : List α :=
+    match n with
+    | 0 => []
+    | m + 1 => x :: solorepl x m
+  -- sorry
+
+-- The following code is a test case and you should not change it.
+
+example : repli [1, 2, 3] 3 = [1, 1, 1, 2, 2, 2, 3, 3, 3] := by rfl
+
+example : repli [1, 2, 3] 2 = [1, 1, 2, 2, 3, 3] := by rfl
+
+example : repli [1, 2, 3] 1 = [1, 2, 3] := by rfl
+
+example : repli [1, 2, 3] 0 = [] := by rfl
+
+example : repli ([] : List α) 255 = [] := by rfl

md/SUMMARY.md

@@ -15,6 +15,11 @@
 * [9: Pack consecutive duplicates](./build/Problem9.md)
 * [10: Run-length encoding](./build/Problem10.md)
 
+# 11-20: Lists, continued
+
+* [14: Duplicate elements](./build/Problem14.md)
+* [15: Replicate elements K times](./build/Problem15.md)
+
 # 31-40: Arithmetic
 
 * [31: Prime number detection](./build/Problem31.md)